proposition: Theorem mBPadic_Fbounded : forall (p : float) (r : R), In p (mBFloat r) -> Fbounded b p.
proof: Proof. intros p r H'; red in |- *; repeat (split; auto). apply Zpred_Zle_Zabs_intro. apply mZlist_correct_rev1 with (q := Z.pred (Zpos (vNum b))); auto with real. apply mProd_correct_rev1 with (l2 := mZlist (- dExp b) (Fexp (boundR r))) (C := (Z * Z)%type) (b := Fexp p); auto. apply in_map_inv with (f := fun p : Z * Z => Float (fst p) (snd p)); auto. intros a1 b1; case a1; case b1; simpl in |- *. intros z z0 z1 z2 H'0; inversion H'0; auto. generalize H'; case p; auto. apply mZlist_correct_rev2 with (p := (- Z.pred (Zpos (vNum b)))%Z); auto. apply mProd_correct_rev1 with (l2 := mZlist (- dExp b) (Fexp (boundR r))) (C := (Z * Z)%type) (b := Fexp p); auto. apply in_map_inv with (f := fun p : Z * Z => Float (fst p) (snd p)); auto. intros a1 b1; case a1; case b1; simpl in |- *. intros z z0 z1 z2 H'0; inversion H'0; auto. generalize H'; case p; auto. apply mZlist_correct_rev1 with (q := Fexp (boundR r)); auto. apply mProd_correct_rev2 with (l1 := mZlist (- pPred (vNum b)) (pPred (vNum b))) (C := (Z * Z)%type) (a := Fnum p); auto. apply in_map_inv with (f := fun p : Z * Z => Float (fst p) (snd p)); auto. intros a1 b1; case a1; case b1; simpl in |- *. intros z z0 z1 z2 H'0; inversion H'0; auto. generalize H'; case p; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz