35 "(R::hypreal) pow (N::hypnat) == |
35 "(R::hypreal) pow (N::hypnat) == |
36 Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N). |
36 Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N). |
37 hyprel``{%n::nat. (X n) ^ (Y n)})" |
37 hyprel``{%n::nat. (X n) ^ (Y n)})" |
38 |
38 |
39 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
39 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
40 apply (simp (no_asm)) |
40 by simp |
41 done |
|
42 |
41 |
43 lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)" |
42 lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)" |
44 by (auto simp add: zero_le_mult_iff) |
43 by (auto simp add: zero_le_mult_iff) |
45 declare hrealpow_two_le [simp] |
44 declare hrealpow_two_le [simp] |
46 |
45 |
47 lemma hrealpow_two_le_add_order: |
46 lemma hrealpow_two_le_add_order: |
48 "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" |
47 "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" |
49 apply (simp only: hrealpow_two_le hypreal_le_add_order) |
48 by (simp only: hrealpow_two_le hypreal_le_add_order) |
50 done |
|
51 declare hrealpow_two_le_add_order [simp] |
49 declare hrealpow_two_le_add_order [simp] |
52 |
50 |
53 lemma hrealpow_two_le_add_order2: |
51 lemma hrealpow_two_le_add_order2: |
54 "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" |
52 "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" |
55 apply (simp only: hrealpow_two_le hypreal_le_add_order) |
53 apply (simp only: hrealpow_two_le hypreal_le_add_order) |