Metamath Proof Explorer

Theorem chebbnd1lem1

Description: Lemma for chebbnd1 : show a lower bound on ppi ( x ) at even integers using similar techniques to those used to prove bpos . (Note that the expression K is actually equal to 2 x. N , but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 , which shows that each term in the expansion ( ( 2 x. N )C N ) = prod p e. Prime ( p ^ ( p pCnt ( ( 2 x. N )C N ) ) ) is at most 2 x. N , so that the sum really only has nonzero elements up to 2 x. N , and since each term is at most 2 x. N , after taking logs we get the inequality ppi ( 2 x. N ) x. log ( 2 x. N ) < log ( ( 2 x. N ) _C N ) , and bclbnd finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 15-Apr-2016)

Ref Expression
Hypothesis chebbnd1lem1.1 
|- K = if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) )
Assertion chebbnd1lem1 
|- ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 4 ^ N ) / N ) ) < ( ( ppi ` ( 2 x. N ) ) x. ( log ` ( 2 x. N ) ) ) )

Proof

Step Hyp Ref Expression
1 chebbnd1lem1.1 
 |-  K = if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) )
2 4nn 
 |-  4 e. NN
3 eluznn 
 |-  ( ( 4 e. NN /\ N e. ( ZZ>= ` 4 ) ) -> N e. NN )
4 2 3 mpan 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. NN )
5 4 nnnn0d 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. NN0 )
6 nnexpcl 
 |-  ( ( 4 e. NN /\ N e. NN0 ) -> ( 4 ^ N ) e. NN )
7 2 5 6 sylancr 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 4 ^ N ) e. NN )
8 7 nnrpd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 4 ^ N ) e. RR+ )
9 4 nnrpd 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. RR+ )
10 8 9 rpdivcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) e. RR+ )
11 10 relogcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 4 ^ N ) / N ) ) e. RR )
12 fzctr 
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
13 5 12 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. ( 0 ... ( 2 x. N ) ) )
14 bccl2 
 |-  ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
15 13 14 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 2 x. N ) _C N ) e. NN )
16 15 nnrpd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 2 x. N ) _C N ) e. RR+ )
17 16 relogcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 2 x. N ) _C N ) ) e. RR )
18 2z 
 |-  2 e. ZZ
19 eluzelz 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. ZZ )
20 zmulcl 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
21 18 19 20 sylancr 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 x. N ) e. ZZ )
22 21 zred 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 x. N ) e. RR )
23 ppicl 
 |-  ( ( 2 x. N ) e. RR -> ( ppi ` ( 2 x. N ) ) e. NN0 )
24 22 23 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ppi ` ( 2 x. N ) ) e. NN0 )
25 24 nn0red 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ppi ` ( 2 x. N ) ) e. RR )
26 2nn 
 |-  2 e. NN
27 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
28 26 4 27 sylancr 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 x. N ) e. NN )
29 28 nnrpd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 x. N ) e. RR+ )
30 29 relogcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( 2 x. N ) ) e. RR )
31 25 30 remulcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( ppi ` ( 2 x. N ) ) x. ( log ` ( 2 x. N ) ) ) e. RR )
32 bclbnd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
33 logltb 
 |-  ( ( ( ( 4 ^ N ) / N ) e. RR+ /\ ( ( 2 x. N ) _C N ) e. RR+ ) -> ( ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) <-> ( log ` ( ( 4 ^ N ) / N ) ) < ( log ` ( ( 2 x. N ) _C N ) ) ) )
34 10 16 33 syl2anc 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) <-> ( log ` ( ( 4 ^ N ) / N ) ) < ( log ` ( ( 2 x. N ) _C N ) ) ) )
35 32 34 mpbid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 4 ^ N ) / N ) ) < ( log ` ( ( 2 x. N ) _C N ) ) )
36 28 15 ifcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) e. NN )
37 1 36 eqeltrid 
 |-  ( N e. ( ZZ>= ` 4 ) -> K e. NN )
38 37 nnred 
 |-  ( N e. ( ZZ>= ` 4 ) -> K e. RR )
39 ppicl 
 |-  ( K e. RR -> ( ppi ` K ) e. NN0 )
40 38 39 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ppi ` K ) e. NN0 )
41 40 nn0red 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ppi ` K ) e. RR )
42 41 30 remulcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( ppi ` K ) x. ( log ` ( 2 x. N ) ) ) e. RR )
43 fzfid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 1 ... K ) e. Fin )
44 inss1 
 |-  ( ( 1 ... K ) i^i Prime ) C_ ( 1 ... K )
45 ssfi 
 |-  ( ( ( 1 ... K ) e. Fin /\ ( ( 1 ... K ) i^i Prime ) C_ ( 1 ... K ) ) -> ( ( 1 ... K ) i^i Prime ) e. Fin )
46 43 44 45 sylancl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 1 ... K ) i^i Prime ) e. Fin )
47 37 nnzd 
 |-  ( N e. ( ZZ>= ` 4 ) -> K e. ZZ )
48 15 nnzd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 2 x. N ) _C N ) e. ZZ )
49 15 nnred 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 2 x. N ) _C N ) e. RR )
50 min2 
 |-  ( ( ( 2 x. N ) e. RR /\ ( ( 2 x. N ) _C N ) e. RR ) -> if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) <_ ( ( 2 x. N ) _C N ) )
51 22 49 50 syl2anc 
 |-  ( N e. ( ZZ>= ` 4 ) -> if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) <_ ( ( 2 x. N ) _C N ) )
52 1 51 eqbrtrid 
 |-  ( N e. ( ZZ>= ` 4 ) -> K <_ ( ( 2 x. N ) _C N ) )
53 eluz2 
 |-  ( ( ( 2 x. N ) _C N ) e. ( ZZ>= ` K ) <-> ( K e. ZZ /\ ( ( 2 x. N ) _C N ) e. ZZ /\ K <_ ( ( 2 x. N ) _C N ) ) )
54 47 48 52 53 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 2 x. N ) _C N ) e. ( ZZ>= ` K ) )
55 fzss2 
 |-  ( ( ( 2 x. N ) _C N ) e. ( ZZ>= ` K ) -> ( 1 ... K ) C_ ( 1 ... ( ( 2 x. N ) _C N ) ) )
56 54 55 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 1 ... K ) C_ ( 1 ... ( ( 2 x. N ) _C N ) ) )
57 56 ssrind 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 1 ... K ) i^i Prime ) C_ ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) )
58 57 sselda 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) )
59 simpr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) )
60 59 elin1d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> k e. ( 1 ... ( ( 2 x. N ) _C N ) ) )
61 elfznn 
 |-  ( k e. ( 1 ... ( ( 2 x. N ) _C N ) ) -> k e. NN )
62 60 61 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> k e. NN )
63 59 elin2d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> k e. Prime )
64 15 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( ( 2 x. N ) _C N ) e. NN )
65 63 64 pccld 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
66 62 65 nnexpcld 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) e. NN )
67 66 nnrpd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) e. RR+ )
68 67 relogcld 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) e. RR )
69 58 68 syldan 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) e. RR )
70 30 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( log ` ( 2 x. N ) ) e. RR )
71 elinel2 
 |-  ( k e. ( ( 1 ... K ) i^i Prime ) -> k e. Prime )
72 bposlem1 
 |-  ( ( N e. NN /\ k e. Prime ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
73 4 71 72 syl2an 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
74 58 67 syldan 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) e. RR+ )
75 74 reeflogd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( exp ` ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) ) = ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) )
76 29 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( 2 x. N ) e. RR+ )
77 76 reeflogd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( exp ` ( log ` ( 2 x. N ) ) ) = ( 2 x. N ) )
78 73 75 77 3brtr4d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( exp ` ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) ) <_ ( exp ` ( log ` ( 2 x. N ) ) ) )
79 efle 
 |-  ( ( ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) e. RR /\ ( log ` ( 2 x. N ) ) e. RR ) -> ( ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) <_ ( log ` ( 2 x. N ) ) <-> ( exp ` ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) ) <_ ( exp ` ( log ` ( 2 x. N ) ) ) ) )
80 69 70 79 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) <_ ( log ` ( 2 x. N ) ) <-> ( exp ` ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) ) <_ ( exp ` ( log ` ( 2 x. N ) ) ) ) )
81 78 80 mpbird 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) <_ ( log ` ( 2 x. N ) ) )
82 46 69 70 81 fsumle 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) <_ sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( 2 x. N ) ) )
83 68 recnd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) e. CC )
84 58 83 syldan 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... K ) i^i Prime ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) e. CC )
85 eldifn 
 |-  ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) -> -. k e. ( ( 1 ... K ) i^i Prime ) )
86 85 adantl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> -. k e. ( ( 1 ... K ) i^i Prime ) )
87 simpr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) )
88 87 eldifad 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) )
89 88 elin1d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k e. ( 1 ... ( ( 2 x. N ) _C N ) ) )
90 89 61 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k e. NN )
91 90 adantrr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k e. NN )
92 91 nnred 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k e. RR )
93 88 66 syldan 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) e. NN )
94 93 nnred 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) e. RR )
95 94 adantrr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) e. RR )
96 22 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( 2 x. N ) e. RR )
97 91 nncnd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k e. CC )
98 97 exp1d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k ^ 1 ) = k )
99 91 nnge1d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> 1 <_ k )
100 simprr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN )
101 nnuz 
 |-  NN = ( ZZ>= ` 1 )
102 100 101 eleqtrdi 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k pCnt ( ( 2 x. N ) _C N ) ) e. ( ZZ>= ` 1 ) )
103 92 99 102 leexp2ad 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k ^ 1 ) <_ ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) )
104 98 103 eqbrtrrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k <_ ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) )
105 4 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> N e. NN )
106 88 elin2d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k e. Prime )
107 106 adantrr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k e. Prime )
108 105 107 72 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
109 92 95 96 104 108 letrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k <_ ( 2 x. N ) )
110 elfzle2 
 |-  ( k e. ( 1 ... ( ( 2 x. N ) _C N ) ) -> k <_ ( ( 2 x. N ) _C N ) )
111 89 110 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k <_ ( ( 2 x. N ) _C N ) )
112 111 adantrr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k <_ ( ( 2 x. N ) _C N ) )
113 49 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( ( 2 x. N ) _C N ) e. RR )
114 lemin 
 |-  ( ( k e. RR /\ ( 2 x. N ) e. RR /\ ( ( 2 x. N ) _C N ) e. RR ) -> ( k <_ if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) <-> ( k <_ ( 2 x. N ) /\ k <_ ( ( 2 x. N ) _C N ) ) ) )
115 92 96 113 114 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k <_ if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) <-> ( k <_ ( 2 x. N ) /\ k <_ ( ( 2 x. N ) _C N ) ) ) )
116 109 112 115 mpbir2and 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k <_ if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) )
117 116 1 breqtrrdi 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k <_ K )
118 37 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> K e. NN )
119 118 nnzd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> K e. ZZ )
120 fznn 
 |-  ( K e. ZZ -> ( k e. ( 1 ... K ) <-> ( k e. NN /\ k <_ K ) ) )
121 119 120 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> ( k e. ( 1 ... K ) <-> ( k e. NN /\ k <_ K ) ) )
122 91 117 121 mpbir2and 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k e. ( 1 ... K ) )
123 122 107 elind 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN ) ) -> k e. ( ( 1 ... K ) i^i Prime ) )
124 123 expr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN -> k e. ( ( 1 ... K ) i^i Prime ) ) )
125 86 124 mtod 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> -. ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN )
126 88 65 syldan 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
127 elnn0 
 |-  ( ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN0 <-> ( ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN \/ ( k pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
128 126 127 sylib 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN \/ ( k pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
129 128 ord 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( -. ( k pCnt ( ( 2 x. N ) _C N ) ) e. NN -> ( k pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
130 125 129 mpd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k pCnt ( ( 2 x. N ) _C N ) ) = 0 )
131 130 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) = ( k ^ 0 ) )
132 90 nncnd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> k e. CC )
133 132 exp0d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k ^ 0 ) = 1 )
134 131 133 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) = 1 )
135 134 fveq2d 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = ( log ` 1 ) )
136 log1 
 |-  ( log ` 1 ) = 0
137 135 136 eqtrdi 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) \ ( ( 1 ... K ) i^i Prime ) ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = 0 )
138 fzfid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 1 ... ( ( 2 x. N ) _C N ) ) e. Fin )
139 inss1 
 |-  ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) C_ ( 1 ... ( ( 2 x. N ) _C N ) )
140 ssfi 
 |-  ( ( ( 1 ... ( ( 2 x. N ) _C N ) ) e. Fin /\ ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) C_ ( 1 ... ( ( 2 x. N ) _C N ) ) ) -> ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) e. Fin )
141 138 139 140 sylancl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) e. Fin )
142 57 84 137 141 fsumss 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = sum_ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) )
143 62 nnrpd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> k e. RR+ )
144 65 nn0zd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( k pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
145 relogexp 
 |-  ( ( k e. RR+ /\ ( k pCnt ( ( 2 x. N ) _C N ) ) e. ZZ ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = ( ( k pCnt ( ( 2 x. N ) _C N ) ) x. ( log ` k ) ) )
146 143 144 145 syl2anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ) -> ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = ( ( k pCnt ( ( 2 x. N ) _C N ) ) x. ( log ` k ) ) )
147 146 sumeq2dv 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = sum_ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ( ( k pCnt ( ( 2 x. N ) _C N ) ) x. ( log ` k ) ) )
148 pclogsum 
 |-  ( ( ( 2 x. N ) _C N ) e. NN -> sum_ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ( ( k pCnt ( ( 2 x. N ) _C N ) ) x. ( log ` k ) ) = ( log ` ( ( 2 x. N ) _C N ) ) )
149 15 148 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... ( ( 2 x. N ) _C N ) ) i^i Prime ) ( ( k pCnt ( ( 2 x. N ) _C N ) ) x. ( log ` k ) ) = ( log ` ( ( 2 x. N ) _C N ) ) )
150 142 147 149 3eqtrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( k ^ ( k pCnt ( ( 2 x. N ) _C N ) ) ) ) = ( log ` ( ( 2 x. N ) _C N ) ) )
151 30 recnd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( 2 x. N ) ) e. CC )
152 fsumconst 
 |-  ( ( ( ( 1 ... K ) i^i Prime ) e. Fin /\ ( log ` ( 2 x. N ) ) e. CC ) -> sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( 2 x. N ) ) = ( ( # ` ( ( 1 ... K ) i^i Prime ) ) x. ( log ` ( 2 x. N ) ) ) )
153 46 151 152 syl2anc 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( 2 x. N ) ) = ( ( # ` ( ( 1 ... K ) i^i Prime ) ) x. ( log ` ( 2 x. N ) ) ) )
154 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
155 ppival2g 
 |-  ( ( K e. ZZ /\ 2 e. ( ZZ>= ` 1 ) ) -> ( ppi ` K ) = ( # ` ( ( 1 ... K ) i^i Prime ) ) )
156 47 154 155 sylancl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ppi ` K ) = ( # ` ( ( 1 ... K ) i^i Prime ) ) )
157 156 oveq1d 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( ppi ` K ) x. ( log ` ( 2 x. N ) ) ) = ( ( # ` ( ( 1 ... K ) i^i Prime ) ) x. ( log ` ( 2 x. N ) ) ) )
158 153 157 eqtr4d 
 |-  ( N e. ( ZZ>= ` 4 ) -> sum_ k e. ( ( 1 ... K ) i^i Prime ) ( log ` ( 2 x. N ) ) = ( ( ppi ` K ) x. ( log ` ( 2 x. N ) ) ) )
159 82 150 158 3brtr3d 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 2 x. N ) _C N ) ) <_ ( ( ppi ` K ) x. ( log ` ( 2 x. N ) ) ) )
160 min1 
 |-  ( ( ( 2 x. N ) e. RR /\ ( ( 2 x. N ) _C N ) e. RR ) -> if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) <_ ( 2 x. N ) )
161 22 49 160 syl2anc 
 |-  ( N e. ( ZZ>= ` 4 ) -> if ( ( 2 x. N ) <_ ( ( 2 x. N ) _C N ) , ( 2 x. N ) , ( ( 2 x. N ) _C N ) ) <_ ( 2 x. N ) )
162 1 161 eqbrtrid 
 |-  ( N e. ( ZZ>= ` 4 ) -> K <_ ( 2 x. N ) )
163 ppiwordi 
 |-  ( ( K e. RR /\ ( 2 x. N ) e. RR /\ K <_ ( 2 x. N ) ) -> ( ppi ` K ) <_ ( ppi ` ( 2 x. N ) ) )
164 38 22 162 163 syl3anc 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ppi ` K ) <_ ( ppi ` ( 2 x. N ) ) )
165 1red 
 |-  ( N e. ( ZZ>= ` 4 ) -> 1 e. RR )
166 2re 
 |-  2 e. RR
167 166 a1i 
 |-  ( N e. ( ZZ>= ` 4 ) -> 2 e. RR )
168 1lt2 
 |-  1 < 2
169 168 a1i 
 |-  ( N e. ( ZZ>= ` 4 ) -> 1 < 2 )
170 2t1e2 
 |-  ( 2 x. 1 ) = 2
171 4 nnge1d 
 |-  ( N e. ( ZZ>= ` 4 ) -> 1 <_ N )
172 eluzelre 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. RR )
173 2pos 
 |-  0 < 2
174 166 173 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
175 174 a1i 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 e. RR /\ 0 < 2 ) )
176 lemul2 
 |-  ( ( 1 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 1 <_ N <-> ( 2 x. 1 ) <_ ( 2 x. N ) ) )
177 165 172 175 176 syl3anc 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 1 <_ N <-> ( 2 x. 1 ) <_ ( 2 x. N ) ) )
178 171 177 mpbid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 x. 1 ) <_ ( 2 x. N ) )
179 170 178 eqbrtrrid 
 |-  ( N e. ( ZZ>= ` 4 ) -> 2 <_ ( 2 x. N ) )
180 165 167 22 169 179 ltletrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> 1 < ( 2 x. N ) )
181 22 180 rplogcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( 2 x. N ) ) e. RR+ )
182 41 25 181 lemul1d 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( ppi ` K ) <_ ( ppi ` ( 2 x. N ) ) <-> ( ( ppi ` K ) x. ( log ` ( 2 x. N ) ) ) <_ ( ( ppi ` ( 2 x. N ) ) x. ( log ` ( 2 x. N ) ) ) ) )
183 164 182 mpbid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( ppi ` K ) x. ( log ` ( 2 x. N ) ) ) <_ ( ( ppi ` ( 2 x. N ) ) x. ( log ` ( 2 x. N ) ) ) )
184 17 42 31 159 183 letrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 2 x. N ) _C N ) ) <_ ( ( ppi ` ( 2 x. N ) ) x. ( log ` ( 2 x. N ) ) ) )
185 11 17 31 35 184 ltletrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( log ` ( ( 4 ^ N ) / N ) ) < ( ( ppi ` ( 2 x. N ) ) x. ( log ` ( 2 x. N ) ) ) )