79 lemma power_real_number_of: |
79 lemma power_real_number_of: |
80 "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" |
80 "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" |
81 by (simp only: real_number_of [symmetric] real_of_int_power) |
81 by (simp only: real_number_of [symmetric] real_of_int_power) |
82 |
82 |
83 declare power_real_number_of [of _ "number_of w", standard, simp] |
83 declare power_real_number_of [of _ "number_of w", standard, simp] |
84 |
|
85 |
|
86 subsection {* Properties of Squares *} |
|
87 |
|
88 lemma sum_squares_ge_zero: |
|
89 fixes x y :: "'a::ordered_ring_strict" |
|
90 shows "0 \<le> x * x + y * y" |
|
91 by (intro add_nonneg_nonneg zero_le_square) |
|
92 |
|
93 lemma not_sum_squares_lt_zero: |
|
94 fixes x y :: "'a::ordered_ring_strict" |
|
95 shows "\<not> x * x + y * y < 0" |
|
96 by (simp add: linorder_not_less sum_squares_ge_zero) |
|
97 |
|
98 lemma sum_nonneg_eq_zero_iff: |
|
99 fixes x y :: "'a::pordered_ab_group_add" |
|
100 assumes x: "0 \<le> x" and y: "0 \<le> y" |
|
101 shows "(x + y = 0) = (x = 0 \<and> y = 0)" |
|
102 proof (auto) |
|
103 from y have "x + 0 \<le> x + y" by (rule add_left_mono) |
|
104 also assume "x + y = 0" |
|
105 finally have "x \<le> 0" by simp |
|
106 thus "x = 0" using x by (rule order_antisym) |
|
107 next |
|
108 from x have "0 + y \<le> x + y" by (rule add_right_mono) |
|
109 also assume "x + y = 0" |
|
110 finally have "y \<le> 0" by simp |
|
111 thus "y = 0" using y by (rule order_antisym) |
|
112 qed |
|
113 |
|
114 lemma sum_squares_eq_zero_iff: |
|
115 fixes x y :: "'a::ordered_ring_strict" |
|
116 shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)" |
|
117 by (simp add: sum_nonneg_eq_zero_iff) |
|
118 |
|
119 lemma sum_squares_le_zero_iff: |
|
120 fixes x y :: "'a::ordered_ring_strict" |
|
121 shows "(x * x + y * y \<le> 0) = (x = 0 \<and> y = 0)" |
|
122 by (simp add: order_le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) |
|
123 |
|
124 lemma sum_squares_gt_zero_iff: |
|
125 fixes x y :: "'a::ordered_ring_strict" |
|
126 shows "(0 < x * x + y * y) = (x \<noteq> 0 \<or> y \<noteq> 0)" |
|
127 by (simp add: order_less_le sum_squares_ge_zero sum_squares_eq_zero_iff) |
|
128 |
|
129 lemma sum_power2_ge_zero: |
|
130 fixes x y :: "'a::{ordered_idom,recpower}" |
|
131 shows "0 \<le> x\<twosuperior> + y\<twosuperior>" |
|
132 unfolding power2_eq_square by (rule sum_squares_ge_zero) |
|
133 |
|
134 lemma not_sum_power2_lt_zero: |
|
135 fixes x y :: "'a::{ordered_idom,recpower}" |
|
136 shows "\<not> x\<twosuperior> + y\<twosuperior> < 0" |
|
137 unfolding power2_eq_square by (rule not_sum_squares_lt_zero) |
|
138 |
|
139 lemma sum_power2_eq_zero_iff: |
|
140 fixes x y :: "'a::{ordered_idom,recpower}" |
|
141 shows "(x\<twosuperior> + y\<twosuperior> = 0) = (x = 0 \<and> y = 0)" |
|
142 unfolding power2_eq_square by (rule sum_squares_eq_zero_iff) |
|
143 |
|
144 lemma sum_power2_le_zero_iff: |
|
145 fixes x y :: "'a::{ordered_idom,recpower}" |
|
146 shows "(x\<twosuperior> + y\<twosuperior> \<le> 0) = (x = 0 \<and> y = 0)" |
|
147 unfolding power2_eq_square by (rule sum_squares_le_zero_iff) |
|
148 |
|
149 lemma sum_power2_gt_zero_iff: |
|
150 fixes x y :: "'a::{ordered_idom,recpower}" |
|
151 shows "(0 < x\<twosuperior> + y\<twosuperior>) = (x \<noteq> 0 \<or> y \<noteq> 0)" |
|
152 unfolding power2_eq_square by (rule sum_squares_gt_zero_iff) |
|
153 |
84 |
154 |
85 |
155 subsection{* Squares of Reals *} |
86 subsection{* Squares of Reals *} |
156 |
87 |
157 lemma real_two_squares_add_zero_iff [simp]: |
88 lemma real_two_squares_add_zero_iff [simp]: |