2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/div_and_mod.ma".
13 include "basics/core_notation/exp_2.ma".
15 let rec exp n m on m ≝
18 | S p ⇒ (exp n p) * n].
20 interpretation "natural exponent" 'exp a b = (exp a b).
22 theorem exp_plus_times : ∀n,p,q:nat.
23 n^(p + q) = n^p * n^q.
24 #n #p #q elim p normalize //
27 theorem exp_n_O : ∀n:nat. 1 = n^O.
31 theorem exp_n_1 : ∀n:nat. n = n^1.
35 theorem exp_1_n : ∀n:nat. 1 = 1^n.
36 #n (elim n) normalize //
39 theorem exp_2: ∀n. n^2 = n*n.
43 theorem exp_exp_times : ∀n,p,q:nat.
45 #n #p #q (elim q) normalize
46 (* [applyS exp_n_O funziona ma non lo trova *)
50 theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m.
51 #n #m (elim m) normalize // #a #Hind #posn
52 @(le_times 1 ? 1) /2/ qed.
54 (* [applyS monotonic_le_minus_r /2/
57 [cut (∃x.∃y.∃z.(x - y ≤ x - z) = (1 ≤ n ^a))
62 @(rewrite_r \Nopf (S n \sup a - n \sup a )
64 .(S n \sup a - n \sup a \le S n \sup a -(S ?-?))=(x\le n \sup a ))
67 .(S n \sup a - n \sup a \le x)=(S n \sup a - n \sup a \le n \sup a ))
68 ( refl … Type[0] (S n \sup a - n \sup a \le n \sup a ) ) (S ?-(S ?-?))
69 (rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
70 (rewrite_l \Nopf 1 (\lambda x:\Nopf .S ?-x=n ^a -O) (minus_S_S ? O) (S ?-?)
73 (minus_Sn_n n \sup a ))
75 @(rewrite_r \Nopf (S ?-?)
77 .(S n \sup a - n \sup a \le S n \sup a -(S ?-?))=(x\le n \sup a ))
80 .(S n \sup a - n \sup a \le x)=(S n \sup a - n \sup a \le n \sup a ))
81 ( refl ??) (S ?-(S ?-?))
85 @(rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
88 @(rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
89 (rewrite_l \Nopf 1 (\lambda x:\Nopf .S ?-x=?-O)
93 @(rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
94 (rewrite_l \Nopf 1 (\lambda x:\Nopf .S ?-x=?-O) (minus_S_S ? O) (S ?-?)
98 applyS monotonic_le_minus_r /2/
101 theorem lt_m_exp_nm: ∀n,m:nat. 1 < n → m < n^m.
102 #n #m #lt1n (elim m) normalize //
103 #n #Hind @(transitive_le ? ((S n)*2)) // @le_times //
106 theorem exp_to_eq_O: ∀n,m:nat. 1 < n →
108 #n #m #ltin #eq1 @le_to_le_to_eq //
109 @le_S_S_to_le <eq1 @lt_m_exp_nm //
112 theorem injective_exp_r: ∀b:nat. 1 < b →
113 injective nat nat (λi:nat. b^i).
114 #b #lt1b @nat_elim2 normalize
115 [#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
116 |#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
117 <H in ⊢ (??%); @(lt_to_le_to_lt ? (1*b)) //
118 @le_times // @lt_O_exp /2/
119 |#n #m #Hind #H @eq_f @Hind @(injective_times_l … H) /2/
123 theorem le_exp: ∀n,m,p:nat. O < p →
126 [#ltm #len @lt_O_exp //
127 |#_ #len @False_ind /2/
128 |#Hind #p #posp #lenm normalize @le_times // @Hind /2/
132 theorem le_exp1: ∀n,m,a:nat. O < a →
134 #n #m #a #posa #lenm (elim posa) //
135 #a #posa #Hind @le_times //
138 theorem lt_exp: ∀n,m,p:nat. 1 < p →
141 cut (p \sup n ≤ p \sup m) [@le_exp /2/] #H
142 cases(le_to_or_lt_eq … H) // #eqexp
143 @False_ind @(absurd (n=m)) /2/
146 theorem lt_exp1: ∀n,m,p:nat. 0 < p →
148 #n #m #p #posp #ltnm (elim posp) //
149 #p #posp #Hind @lt_times //
152 theorem le_exp_to_le:
153 ∀b,n,m. 1 < b → b^n ≤ b^m → n ≤ m.
154 #b #n #m #lt1b #leexp cases(decidable_le n m) //
155 #notle @False_ind @(absurd … leexp) @lt_to_not_le
159 theorem le_exp_to_le1 : ∀n,m,p.O < p →
161 #n #m #p #posp #leexp @not_lt_to_le
162 @(not_to_not … (lt_exp1 ??? posp)) @le_to_not_lt //
165 theorem lt_exp_to_lt:
166 ∀a,n,m. 0 < a → a^n < a^m → n < m.
167 #a #n #m #lt1a #ltexp cases(decidable_le (S n) m) //
168 #H @False_ind @(absurd … ltexp) @le_to_not_lt
169 @le_exp // @not_lt_to_le @H
172 theorem lt_exp_to_lt1:
173 ∀a,n,m. O < a → n^a < m^a → n < m.
174 #a #n #m #posa #ltexp cases(decidable_le (S n) m) //
175 #H @False_ind @(absurd … ltexp) @le_to_not_lt
176 @le_exp1 // @not_lt_to_le @H
179 theorem times_exp: ∀n,m,p.
181 #n #m #p (elim p) // #p #Hind normalize //