equal
deleted
inserted
replaced
21 |
21 |
22 Goal "0 < i ==> 0 < i^n"; |
22 Goal "0 < i ==> 0 < i^n"; |
23 by (induct_tac "n" 1); |
23 by (induct_tac "n" 1); |
24 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
24 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
25 qed "zero_less_power"; |
25 qed "zero_less_power"; |
|
26 Addsimps [zero_less_power]; |
|
27 |
|
28 Goal "!!i::nat. 1 <= i ==> 1 <= i^n"; |
|
29 by (induct_tac "n" 1); |
|
30 by Auto_tac; |
|
31 qed "one_le_power"; |
|
32 Addsimps [one_le_power]; |
26 |
33 |
27 Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n"; |
34 Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n"; |
28 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
35 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
29 by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
36 by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
30 by (Blast_tac 1); |
37 by (Blast_tac 1); |