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