144 qed "realpow_ge_one2"; |
144 qed "realpow_ge_one2"; |
145 |
145 |
146 Goal "(#1::real) <= #2 ^ n"; |
146 Goal "(#1::real) <= #2 ^ n"; |
147 by (res_inst_tac [("y","#1 ^ n")] order_trans 1); |
147 by (res_inst_tac [("y","#1 ^ n")] order_trans 1); |
148 by (rtac realpow_le 2); |
148 by (rtac realpow_le 2); |
149 by (auto_tac (claset() addIs [order_less_imp_le],simpset())); |
149 by (auto_tac (claset() addIs [order_less_imp_le], simpset())); |
150 qed "two_realpow_ge_one"; |
150 qed "two_realpow_ge_one"; |
151 |
151 |
152 Goal "real_of_nat n < #2 ^ n"; |
152 Goal "real_of_nat n < #2 ^ n"; |
153 by (induct_tac "n" 1); |
153 by (induct_tac "n" 1); |
154 by Auto_tac; |
154 by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); |
155 by (stac real_mult_2 1); |
155 by (stac real_mult_2 1); |
156 by (rtac real_add_less_le_mono 1); |
156 by (rtac real_add_less_le_mono 1); |
157 by (auto_tac (claset(), |
157 by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one])); |
158 simpset() addsimps [two_realpow_ge_one])); |
|
159 qed "two_realpow_gt"; |
158 qed "two_realpow_gt"; |
160 Addsimps [two_realpow_gt,two_realpow_ge_one]; |
159 Addsimps [two_realpow_gt,two_realpow_ge_one]; |
161 |
160 |
162 Goal "(#-1) ^ (#2*n) = (#1::real)"; |
161 Goal "(#-1) ^ (#2*n) = (#1::real)"; |
163 by (induct_tac "n" 1); |
162 by (induct_tac "n" 1); |