This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dirith2

Description: Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to N . Theorem 9.4.1 of Shapiro, p. 375. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.u 
|- U = ( Unit ` Z )
rpvmasum.b 
|- ( ph -> A e. U )
rpvmasum.t 
|- T = ( `' L " { A } )
Assertion dirith2 
|- ( ph -> ( Prime i^i T ) ~~ NN )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum.u 
 |-  U = ( Unit ` Z )
5 rpvmasum.b 
 |-  ( ph -> A e. U )
6 rpvmasum.t 
 |-  T = ( `' L " { A } )
7 nnex 
 |-  NN e. _V
8 inss1 
 |-  ( Prime i^i T ) C_ Prime
9 prmssnn 
 |-  Prime C_ NN
10 8 9 sstri 
 |-  ( Prime i^i T ) C_ NN
11 ssdomg 
 |-  ( NN e. _V -> ( ( Prime i^i T ) C_ NN -> ( Prime i^i T ) ~<_ NN ) )
12 7 10 11 mp2 
 |-  ( Prime i^i T ) ~<_ NN
13 12 a1i 
 |-  ( ph -> ( Prime i^i T ) ~<_ NN )
14 logno1 
 |-  -. ( x e. RR+ |-> ( log ` x ) ) e. O(1)
15 3 adantr 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> N e. NN )
16 15 phicld 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( phi ` N ) e. NN )
17 16 nnred 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( phi ` N ) e. RR )
18 17 adantr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ x e. RR+ ) -> ( phi ` N ) e. RR )
19 simpr 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( Prime i^i T ) e. Fin )
20 inss2 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( Prime i^i T )
21 ssfi 
 |-  ( ( ( Prime i^i T ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( Prime i^i T ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) e. Fin )
22 19 20 21 sylancl 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) e. Fin )
23 elinel2 
 |-  ( n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) -> n e. ( Prime i^i T ) )
24 simpr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> n e. ( Prime i^i T ) )
25 10 24 sselid 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> n e. NN )
26 25 nnrpd 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> n e. RR+ )
27 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
28 26 27 syl 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> ( log ` n ) e. RR )
29 28 25 nndivred 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> ( ( log ` n ) / n ) e. RR )
30 23 29 sylan2 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> ( ( log ` n ) / n ) e. RR )
31 22 30 fsumrecl 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) e. RR )
32 31 adantr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ x e. RR+ ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) e. RR )
33 rpssre 
 |-  RR+ C_ RR
34 17 recnd 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( phi ` N ) e. CC )
35 o1const 
 |-  ( ( RR+ C_ RR /\ ( phi ` N ) e. CC ) -> ( x e. RR+ |-> ( phi ` N ) ) e. O(1) )
36 33 34 35 sylancr 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( x e. RR+ |-> ( phi ` N ) ) e. O(1) )
37 33 a1i 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> RR+ C_ RR )
38 1red 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> 1 e. RR )
39 19 29 fsumrecl 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> sum_ n e. ( Prime i^i T ) ( ( log ` n ) / n ) e. RR )
40 log1 
 |-  ( log ` 1 ) = 0
41 25 nnge1d 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> 1 <_ n )
42 1rp 
 |-  1 e. RR+
43 logleb 
 |-  ( ( 1 e. RR+ /\ n e. RR+ ) -> ( 1 <_ n <-> ( log ` 1 ) <_ ( log ` n ) ) )
44 42 26 43 sylancr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> ( 1 <_ n <-> ( log ` 1 ) <_ ( log ` n ) ) )
45 41 44 mpbid 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> ( log ` 1 ) <_ ( log ` n ) )
46 40 45 eqbrtrrid 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> 0 <_ ( log ` n ) )
47 28 26 46 divge0d 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( Prime i^i T ) ) -> 0 <_ ( ( log ` n ) / n ) )
48 20 a1i 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( Prime i^i T ) )
49 19 29 47 48 fsumless 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) <_ sum_ n e. ( Prime i^i T ) ( ( log ` n ) / n ) )
50 49 adantr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) <_ sum_ n e. ( Prime i^i T ) ( ( log ` n ) / n ) )
51 37 32 38 39 50 ello1d 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( x e. RR+ |-> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. <_O(1) )
52 0red 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> 0 e. RR )
53 23 47 sylan2 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> 0 <_ ( ( log ` n ) / n ) )
54 22 30 53 fsumge0 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> 0 <_ sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) )
55 54 adantr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ x e. RR+ ) -> 0 <_ sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) )
56 32 52 55 o1lo12 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( ( x e. RR+ |-> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. O(1) <-> ( x e. RR+ |-> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. <_O(1) ) )
57 51 56 mpbird 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( x e. RR+ |-> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. O(1) )
58 18 32 36 57 o1mul2 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( x e. RR+ |-> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) ) e. O(1) )
59 17 31 remulcld 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. RR )
60 59 recnd 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. CC )
61 60 adantr 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) e. CC )
62 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
63 62 adantl 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ x e. RR+ ) -> ( log ` x ) e. RR )
64 63 recnd 
 |-  ( ( ( ph /\ ( Prime i^i T ) e. Fin ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
65 1 2 3 4 5 6 rplogsum 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
66 65 adantr 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
67 61 64 66 o1dif 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( ( x e. RR+ |-> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` n ) / n ) ) ) e. O(1) <-> ( x e. RR+ |-> ( log ` x ) ) e. O(1) ) )
68 58 67 mpbid 
 |-  ( ( ph /\ ( Prime i^i T ) e. Fin ) -> ( x e. RR+ |-> ( log ` x ) ) e. O(1) )
69 68 ex 
 |-  ( ph -> ( ( Prime i^i T ) e. Fin -> ( x e. RR+ |-> ( log ` x ) ) e. O(1) ) )
70 14 69 mtoi 
 |-  ( ph -> -. ( Prime i^i T ) e. Fin )
71 nnenom 
 |-  NN ~~ _om
72 sdomentr 
 |-  ( ( ( Prime i^i T ) ~< NN /\ NN ~~ _om ) -> ( Prime i^i T ) ~< _om )
73 71 72 mpan2 
 |-  ( ( Prime i^i T ) ~< NN -> ( Prime i^i T ) ~< _om )
74 isfinite2 
 |-  ( ( Prime i^i T ) ~< _om -> ( Prime i^i T ) e. Fin )
75 73 74 syl 
 |-  ( ( Prime i^i T ) ~< NN -> ( Prime i^i T ) e. Fin )
76 70 75 nsyl 
 |-  ( ph -> -. ( Prime i^i T ) ~< NN )
77 bren2 
 |-  ( ( Prime i^i T ) ~~ NN <-> ( ( Prime i^i T ) ~<_ NN /\ -. ( Prime i^i T ) ~< NN ) )
78 13 76 77 sylanbrc 
 |-  ( ph -> ( Prime i^i T ) ~~ NN )