447 \ ==> ALL N n. n < N --> r pow N <= r pow n"; |
447 \ ==> ALL N n. n < N --> r pow N <= r pow n"; |
448 by (blast_tac (claset() addSIs [hyperpow_less_le]) 1); |
448 by (blast_tac (claset() addSIs [hyperpow_less_le]) 1); |
449 qed "hyperpow_less_le2"; |
449 qed "hyperpow_less_le2"; |
450 |
450 |
451 Goal "[| #0 <= r; r < (#1::hypreal); N : HNatInfinite |] \ |
451 Goal "[| #0 <= r; r < (#1::hypreal); N : HNatInfinite |] \ |
452 \ ==> ALL n: SNat. r pow N <= r pow n"; |
452 \ ==> ALL n: Nats. r pow N <= r pow n"; |
453 by (auto_tac (claset() addSIs [hyperpow_less_le], |
453 by (auto_tac (claset() addSIs [hyperpow_less_le], |
454 simpset() addsimps [HNatInfinite_iff])); |
454 simpset() addsimps [HNatInfinite_iff])); |
455 qed "hyperpow_SHNat_le"; |
455 qed "hyperpow_SHNat_le"; |
456 |
456 |
457 Goalw [hypreal_of_real_def,hypnat_of_nat_def] |
457 Goalw [hypreal_of_real_def,hypnat_of_nat_def] |
458 "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"; |
458 "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"; |
459 by (auto_tac (claset(), simpset() addsimps [hyperpow])); |
459 by (auto_tac (claset(), simpset() addsimps [hyperpow])); |
460 qed "hyperpow_realpow"; |
460 qed "hyperpow_realpow"; |
461 |
461 |
462 Goalw [SReal_def] |
462 Goalw [SReal_def] |
463 "(hypreal_of_real r) pow (hypnat_of_nat n) : SReal"; |
463 "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals"; |
464 by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow])); |
464 by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow])); |
465 qed "hyperpow_SReal"; |
465 qed "hyperpow_SReal"; |
466 Addsimps [hyperpow_SReal]; |
466 Addsimps [hyperpow_SReal]; |
467 |
467 |
468 Goal "N : HNatInfinite ==> (#0::hypreal) pow N = 0"; |
468 Goal "N : HNatInfinite ==> (#0::hypreal) pow N = 0"; |