equal
deleted
inserted
replaced
28 Goal "!!i::nat. 1 <= i ==> 1 <= i^n"; |
28 Goal "!!i::nat. 1 <= i ==> 1 <= i^n"; |
29 by (induct_tac "n" 1); |
29 by (induct_tac "n" 1); |
30 by Auto_tac; |
30 by Auto_tac; |
31 qed "one_le_power"; |
31 qed "one_le_power"; |
32 Addsimps [one_le_power]; |
32 Addsimps [one_le_power]; |
|
33 |
|
34 Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)"; |
|
35 by (induct_tac "n" 1); |
|
36 by Auto_tac; |
|
37 by (ALLGOALS (case_tac "m")); |
|
38 by Auto_tac; |
|
39 qed_spec_mp "power_inject"; |
|
40 Addsimps [power_inject]; |
33 |
41 |
34 Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; |
42 Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; |
35 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
43 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
36 by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
44 by (asm_simp_tac (simpset() addsimps [power_add]) 1); |
37 qed "le_imp_power_dvd"; |
45 qed "le_imp_power_dvd"; |