]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/totient1.ma
Complete proof of Bertrand for n >= 256.
[helm.git] / helm / software / matita / library / nat / totient1.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/totient.ma".
16 include "nat/iteration2.ma".
17 include "nat/gcd_properties1.ma".
18
19 (* This file contains the proof of the following theorem about Euler's totient
20  * function:
21  
22    The sum of the applications of Phi function over the divisor of a natural
23    number n is equal to n
24  *)
25
26 (*simple auxiliary properties*)   
27 theorem lt_O_to_divides_to_lt_O_div:
28 \forall a,b:nat.
29 O \lt b \to a \divides b \to O \lt (b/a).
30 intros.
31 apply (O_lt_times_to_O_lt ? a).
32 rewrite > (divides_to_div a b); 
33   assumption.
34 qed.
35
36 (*tha main theorem*) 
37 theorem sigma_p_Sn_divides_b_totient_n: \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
38 intros. 
39 unfold totient.
40 apply (trans_eq ? ? 
41 (sigma_p (S n) (\lambda d:nat.divides_b d n)
42 (\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
43 [ apply eq_sigma_p1
44   [ intros.
45     reflexivity
46   | intros.
47     apply sym_eq.
48     apply (trans_eq ? ? 
49      (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
50     [ apply false_to_eq_sigma_p
51       [ apply lt_to_le.          
52         assumption
53       | intros.
54         rewrite > lt_to_leb_false
55         [ reflexivity
56         | apply le_S_S.
57           assumption
58         ]
59       ]
60     | apply eq_sigma_p
61       [ intros.
62         rewrite > le_to_leb_true
63         [ reflexivity
64         | assumption
65         ]
66       | intros.
67         reflexivity
68       ]
69     ]
70   ]
71 | apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
72   [ apply sym_eq.
73     apply (sigma_p_knm
74      (\lambda x. (S O))
75      (\lambda i,j.j*(n/i))
76      (\lambda p. n / (gcd p n))
77      (\lambda p. p / (gcd p n))
78     );intros
79     [ cut (O \lt (gcd x n))
80       [split
81       [ split
82         [ split
83           [ split
84             [ apply divides_to_divides_b_true
85               [ apply (O_lt_times_to_O_lt ? (gcd x n)).
86                 rewrite > (divides_to_div (gcd x n) n)
87                 [ assumption
88                 | apply (divides_gcd_m)
89                 ]
90               | rewrite > sym_gcd.
91                 apply (divides_times_to_divides_div_gcd).
92                 apply (witness n (x * n) x).
93                 apply (symmetric_times x n)
94               ]
95             | apply (true_to_true_to_andb_true)
96               [ apply (le_to_leb_true).
97                 change with (x/(gcd x n) \lt n/(gcd x n)).
98                 apply (lt_times_n_to_lt (gcd x n) ? ?)
99                 [ assumption
100                 | rewrite > (divides_to_div (gcd x n) x)
101                   [ rewrite > (divides_to_div (gcd x n) n)
102                     [ assumption
103                     | apply divides_gcd_m
104                     ]
105                   | apply divides_gcd_n
106                   ]
107                 ]
108               | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
109                 rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
110                 [ apply (div_n_n (gcd x n) Hcut)
111                 | assumption
112                 | apply divides_gcd_n
113                 | apply divides_gcd_m                  
114                 ]
115               ]
116             ] 
117           | apply (inj_times_l1 (n/(gcd x n)))
118             [ apply lt_O_to_divides_to_lt_O_div
119               [ assumption
120               | apply divides_gcd_m 
121               ]
122             | rewrite > associative_times.
123               rewrite > (divides_to_div (n/(gcd x n)) n)
124               [ rewrite > sym_times.
125                 rewrite > (divides_to_eq_times_div_div_times x)
126                 [ apply (inj_times_l1 (gcd x n) Hcut).
127                   rewrite > (divides_to_div (gcd x n) (x * n))
128                   [ rewrite > assoc_times.
129                     rewrite > (divides_to_div (gcd x n) x)
130                     [ apply sym_times
131                     | apply divides_gcd_n
132                     ]
133                   | apply (trans_divides ? x)
134                     [ apply divides_gcd_n
135                     | apply (witness ? ? n).
136                       reflexivity
137                     ]
138                   ]
139                 | assumption
140                 | apply divides_gcd_m
141                 ]              
142               | apply (witness ? ? (gcd x n)).
143                 rewrite > divides_to_div
144                 [ reflexivity
145                 | apply divides_gcd_m                
146                 ]                
147               ]
148             ]  
149           ]
150         | apply (le_to_lt_to_lt ? n)
151           [ apply le_div.
152             assumption
153           | change with ((S n) \le (S n)).
154             apply le_n 
155           ]
156         ]
157       | apply (le_to_lt_to_lt ? x)
158         [ apply le_div.
159           assumption   
160         | apply (trans_lt ? n ?)
161           [ assumption
162           | change with ((S n) \le (S n)).
163             apply le_n
164           ]
165         ]
166       ]
167     | apply (divides_to_lt_O ? n)
168       [ assumption
169       | apply divides_gcd_m
170       ]
171     ]  
172     | cut (i \divides n)
173       [ cut (j \lt i)
174         [ cut ((gcd j i) = (S O) )
175           [ cut ((gcd (j*(n/i)) n) = n/i)
176             [ split
177               [ split
178                 [ split
179                   [ reflexivity
180                   | rewrite > Hcut3.
181                     apply (div_div);
182                       assumption
183                   ]               
184                 | rewrite > Hcut3.
185                   rewrite < divides_to_eq_times_div_div_times
186                   [ rewrite > div_n_n  
187                     [ apply sym_eq.
188                       apply times_n_SO.
189                     | apply lt_O_to_divides_to_lt_O_div;
190                         assumption
191                     ]
192                   | apply lt_O_to_divides_to_lt_O_div; 
193                       assumption
194                   | apply divides_n_n
195                   ]
196                 ]
197               | rewrite < (divides_to_div i n) in \vdash (? ? %)
198                 [ rewrite > sym_times.
199                   apply (lt_times_r1)
200                   [ apply lt_O_to_divides_to_lt_O_div;
201                       assumption
202                   | assumption
203                   ]
204                 | assumption
205                 ]               
206               ]
207             | rewrite < (divides_to_div i n) in \vdash (? ? (? ? %) ?)
208               [ rewrite > (sym_times j).
209                 rewrite > times_n_SO in \vdash (? ? ? %).
210                 rewrite < Hcut2.
211                 apply eq_gcd_times_times_times_gcd                
212               | assumption
213               ]
214             ]
215           | apply eqb_true_to_eq.
216             apply (andb_true_true_r (leb (S j) i)).            
217             assumption            
218           ]
219         | change with ((S j) \le i).
220           cut((leb (S j) i) = true)
221           [ change with(
222             match (true) with
223             [ true  \Rightarrow ((S j) \leq i) 
224             | false \Rightarrow ((S j) \nleq i)]
225             ).
226             rewrite < Hcut1.
227             apply (leb_to_Prop)
228           | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).            
229             assumption
230           ]
231         ]
232         | apply (divides_b_true_to_divides).
233           assumption
234       ]
235     ]
236   | apply (sigma_p_true).
237   ]
238 ]
239 qed.  
240     
241