Metamath Proof Explorer

Theorem chtublem

Description: Lemma for chtub . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion chtublem 
|- ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
3 1 2 mpan 
 |-  ( N e. NN -> ( 2 x. N ) e. NN )
4 3 nnred 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
5 peano2rem 
 |-  ( ( 2 x. N ) e. RR -> ( ( 2 x. N ) - 1 ) e. RR )
6 4 5 syl 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) e. RR )
7 chtcl 
 |-  ( ( ( 2 x. N ) - 1 ) e. RR -> ( theta ` ( ( 2 x. N ) - 1 ) ) e. RR )
8 6 7 syl 
 |-  ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) e. RR )
9 nnre 
 |-  ( N e. NN -> N e. RR )
10 chtcl 
 |-  ( N e. RR -> ( theta ` N ) e. RR )
11 9 10 syl 
 |-  ( N e. NN -> ( theta ` N ) e. RR )
12 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
13 2m1e1 
 |-  ( 2 - 1 ) = 1
14 13 oveq2i 
 |-  ( ( 2 x. N ) - ( 2 - 1 ) ) = ( ( 2 x. N ) - 1 )
15 3 nncnd 
 |-  ( N e. NN -> ( 2 x. N ) e. CC )
16 2cn 
 |-  2 e. CC
17 ax-1cn 
 |-  1 e. CC
18 subsub 
 |-  ( ( ( 2 x. N ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( 2 x. N ) - ( 2 - 1 ) ) = ( ( ( 2 x. N ) - 2 ) + 1 ) )
19 16 17 18 mp3an23 
 |-  ( ( 2 x. N ) e. CC -> ( ( 2 x. N ) - ( 2 - 1 ) ) = ( ( ( 2 x. N ) - 2 ) + 1 ) )
20 15 19 syl 
 |-  ( N e. NN -> ( ( 2 x. N ) - ( 2 - 1 ) ) = ( ( ( 2 x. N ) - 2 ) + 1 ) )
21 nncn 
 |-  ( N e. NN -> N e. CC )
22 subdi 
 |-  ( ( 2 e. CC /\ N e. CC /\ 1 e. CC ) -> ( 2 x. ( N - 1 ) ) = ( ( 2 x. N ) - ( 2 x. 1 ) ) )
23 16 17 22 mp3an13 
 |-  ( N e. CC -> ( 2 x. ( N - 1 ) ) = ( ( 2 x. N ) - ( 2 x. 1 ) ) )
24 21 23 syl 
 |-  ( N e. NN -> ( 2 x. ( N - 1 ) ) = ( ( 2 x. N ) - ( 2 x. 1 ) ) )
25 2t1e2 
 |-  ( 2 x. 1 ) = 2
26 25 oveq2i 
 |-  ( ( 2 x. N ) - ( 2 x. 1 ) ) = ( ( 2 x. N ) - 2 )
27 24 26 eqtrdi 
 |-  ( N e. NN -> ( 2 x. ( N - 1 ) ) = ( ( 2 x. N ) - 2 ) )
28 27 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. ( N - 1 ) ) + 1 ) = ( ( ( 2 x. N ) - 2 ) + 1 ) )
29 20 28 eqtr4d 
 |-  ( N e. NN -> ( ( 2 x. N ) - ( 2 - 1 ) ) = ( ( 2 x. ( N - 1 ) ) + 1 ) )
30 14 29 eqtr3id 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) = ( ( 2 x. ( N - 1 ) ) + 1 ) )
31 2nn0 
 |-  2 e. NN0
32 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
33 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ ( N - 1 ) e. NN0 ) -> ( 2 x. ( N - 1 ) ) e. NN0 )
34 31 32 33 sylancr 
 |-  ( N e. NN -> ( 2 x. ( N - 1 ) ) e. NN0 )
35 nn0p1nn 
 |-  ( ( 2 x. ( N - 1 ) ) e. NN0 -> ( ( 2 x. ( N - 1 ) ) + 1 ) e. NN )
36 34 35 syl 
 |-  ( N e. NN -> ( ( 2 x. ( N - 1 ) ) + 1 ) e. NN )
37 30 36 eqeltrd 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) e. NN )
38 nnnn0 
 |-  ( ( ( 2 x. N ) - 1 ) e. NN -> ( ( 2 x. N ) - 1 ) e. NN0 )
39 37 38 syl 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) e. NN0 )
40 1re 
 |-  1 e. RR
41 40 a1i 
 |-  ( N e. NN -> 1 e. RR )
42 nnge1 
 |-  ( N e. NN -> 1 <_ N )
43 41 9 9 42 leadd2dd 
 |-  ( N e. NN -> ( N + 1 ) <_ ( N + N ) )
44 21 2timesd 
 |-  ( N e. NN -> ( 2 x. N ) = ( N + N ) )
45 43 44 breqtrrd 
 |-  ( N e. NN -> ( N + 1 ) <_ ( 2 x. N ) )
46 leaddsub 
 |-  ( ( N e. RR /\ 1 e. RR /\ ( 2 x. N ) e. RR ) -> ( ( N + 1 ) <_ ( 2 x. N ) <-> N <_ ( ( 2 x. N ) - 1 ) ) )
47 9 41 4 46 syl3anc 
 |-  ( N e. NN -> ( ( N + 1 ) <_ ( 2 x. N ) <-> N <_ ( ( 2 x. N ) - 1 ) ) )
48 45 47 mpbid 
 |-  ( N e. NN -> N <_ ( ( 2 x. N ) - 1 ) )
49 elfz2nn0 
 |-  ( N e. ( 0 ... ( ( 2 x. N ) - 1 ) ) <-> ( N e. NN0 /\ ( ( 2 x. N ) - 1 ) e. NN0 /\ N <_ ( ( 2 x. N ) - 1 ) ) )
50 12 39 48 49 syl3anbrc 
 |-  ( N e. NN -> N e. ( 0 ... ( ( 2 x. N ) - 1 ) ) )
51 bccl2 
 |-  ( N e. ( 0 ... ( ( 2 x. N ) - 1 ) ) -> ( ( ( 2 x. N ) - 1 ) _C N ) e. NN )
52 50 51 syl 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) e. NN )
53 52 nnrpd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) e. RR+ )
54 53 relogcld 
 |-  ( N e. NN -> ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) e. RR )
55 11 54 readdcld 
 |-  ( N e. NN -> ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) e. RR )
56 4re 
 |-  4 e. RR
57 4pos 
 |-  0 < 4
58 56 57 elrpii 
 |-  4 e. RR+
59 relogcl 
 |-  ( 4 e. RR+ -> ( log ` 4 ) e. RR )
60 58 59 ax-mp 
 |-  ( log ` 4 ) e. RR
61 32 nn0red 
 |-  ( N e. NN -> ( N - 1 ) e. RR )
62 remulcl 
 |-  ( ( ( log ` 4 ) e. RR /\ ( N - 1 ) e. RR ) -> ( ( log ` 4 ) x. ( N - 1 ) ) e. RR )
63 60 61 62 sylancr 
 |-  ( N e. NN -> ( ( log ` 4 ) x. ( N - 1 ) ) e. RR )
64 11 63 readdcld 
 |-  ( N e. NN -> ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) e. RR )
65 iftrue 
 |-  ( p <_ ( ( 2 x. N ) - 1 ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) = 1 )
66 65 adantl 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ ( ( 2 x. N ) - 1 ) ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) = 1 )
67 simpr 
 |-  ( ( N e. NN /\ p e. Prime ) -> p e. Prime )
68 52 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ( 2 x. N ) - 1 ) _C N ) e. NN )
69 67 68 pccld 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) e. NN0 )
70 nn0addge1 
 |-  ( ( 1 e. RR /\ ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) e. NN0 ) -> 1 <_ ( 1 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
71 40 69 70 sylancr 
 |-  ( ( N e. NN /\ p e. Prime ) -> 1 <_ ( 1 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
72 iftrue 
 |-  ( p <_ N -> if ( p <_ N , 1 , 0 ) = 1 )
73 72 oveq1d 
 |-  ( p <_ N -> ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( 1 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
74 73 breq2d 
 |-  ( p <_ N -> ( 1 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <-> 1 <_ ( 1 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
75 71 74 syl5ibrcom 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p <_ N -> 1 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
76 75 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ ( ( 2 x. N ) - 1 ) ) -> ( p <_ N -> 1 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
77 prmnn 
 |-  ( p e. Prime -> p e. NN )
78 77 ad2antlr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> p e. NN )
79 simprl 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> p <_ ( ( 2 x. N ) - 1 ) )
80 prmz 
 |-  ( p e. Prime -> p e. ZZ )
81 37 nnzd 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) e. ZZ )
82 eluz 
 |-  ( ( p e. ZZ /\ ( ( 2 x. N ) - 1 ) e. ZZ ) -> ( ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` p ) <-> p <_ ( ( 2 x. N ) - 1 ) ) )
83 80 81 82 syl2anr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` p ) <-> p <_ ( ( 2 x. N ) - 1 ) ) )
84 83 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` p ) <-> p <_ ( ( 2 x. N ) - 1 ) ) )
85 79 84 mpbird 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` p ) )
86 dvdsfac 
 |-  ( ( p e. NN /\ ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` p ) ) -> p || ( ! ` ( ( 2 x. N ) - 1 ) ) )
87 78 85 86 syl2anc 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> p || ( ! ` ( ( 2 x. N ) - 1 ) ) )
88 id 
 |-  ( p e. Prime -> p e. Prime )
89 39 faccld 
 |-  ( N e. NN -> ( ! ` ( ( 2 x. N ) - 1 ) ) e. NN )
90 pcelnn 
 |-  ( ( p e. Prime /\ ( ! ` ( ( 2 x. N ) - 1 ) ) e. NN ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. NN <-> p || ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
91 88 89 90 syl2anr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. NN <-> p || ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
92 91 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. NN <-> p || ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
93 87 92 mpbird 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. NN )
94 93 nnge1d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> 1 <_ ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
95 iffalse 
 |-  ( -. p <_ N -> if ( p <_ N , 1 , 0 ) = 0 )
96 95 oveq1d 
 |-  ( -. p <_ N -> ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( 0 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
97 96 ad2antll 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( 0 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
98 69 nn0cnd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) e. CC )
99 98 addid2d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( 0 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) )
100 99 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( 0 + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) )
101 bcval2 
 |-  ( N e. ( 0 ... ( ( 2 x. N ) - 1 ) ) -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( ( ( 2 x. N ) - 1 ) - N ) ) x. ( ! ` N ) ) ) )
102 50 101 syl 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( ( ( 2 x. N ) - 1 ) - N ) ) x. ( ! ` N ) ) ) )
103 32 nn0cnd 
 |-  ( N e. NN -> ( N - 1 ) e. CC )
104 17 a1i 
 |-  ( N e. NN -> 1 e. CC )
105 44 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) = ( ( N + N ) - 1 ) )
106 21 21 104 105 assraddsubd 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) = ( N + ( N - 1 ) ) )
107 21 103 106 mvrladdd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) - N ) = ( N - 1 ) )
108 107 fveq2d 
 |-  ( N e. NN -> ( ! ` ( ( ( 2 x. N ) - 1 ) - N ) ) = ( ! ` ( N - 1 ) ) )
109 108 oveq1d 
 |-  ( N e. NN -> ( ( ! ` ( ( ( 2 x. N ) - 1 ) - N ) ) x. ( ! ` N ) ) = ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) )
110 109 oveq2d 
 |-  ( N e. NN -> ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( ( ( 2 x. N ) - 1 ) - N ) ) x. ( ! ` N ) ) ) = ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) )
111 102 110 eqtrd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) )
112 111 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) )
113 112 oveq2d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( p pCnt ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) ) )
114 nnz 
 |-  ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. NN -> ( ! ` ( ( 2 x. N ) - 1 ) ) e. ZZ )
115 nnne0 
 |-  ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. NN -> ( ! ` ( ( 2 x. N ) - 1 ) ) =/= 0 )
116 114 115 jca 
 |-  ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. NN -> ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. ZZ /\ ( ! ` ( ( 2 x. N ) - 1 ) ) =/= 0 ) )
117 89 116 syl 
 |-  ( N e. NN -> ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. ZZ /\ ( ! ` ( ( 2 x. N ) - 1 ) ) =/= 0 ) )
118 117 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. ZZ /\ ( ! ` ( ( 2 x. N ) - 1 ) ) =/= 0 ) )
119 32 faccld 
 |-  ( N e. NN -> ( ! ` ( N - 1 ) ) e. NN )
120 12 faccld 
 |-  ( N e. NN -> ( ! ` N ) e. NN )
121 119 120 nnmulcld 
 |-  ( N e. NN -> ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) e. NN )
122 121 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) e. NN )
123 pcdiv 
 |-  ( ( p e. Prime /\ ( ( ! ` ( ( 2 x. N ) - 1 ) ) e. ZZ /\ ( ! ` ( ( 2 x. N ) - 1 ) ) =/= 0 ) /\ ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) e. NN ) -> ( p pCnt ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) ) = ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( p pCnt ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) ) )
124 67 118 122 123 syl3anc 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( ! ` ( ( 2 x. N ) - 1 ) ) / ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) ) = ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( p pCnt ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) ) )
125 nnz 
 |-  ( ( ! ` ( N - 1 ) ) e. NN -> ( ! ` ( N - 1 ) ) e. ZZ )
126 nnne0 
 |-  ( ( ! ` ( N - 1 ) ) e. NN -> ( ! ` ( N - 1 ) ) =/= 0 )
127 125 126 jca 
 |-  ( ( ! ` ( N - 1 ) ) e. NN -> ( ( ! ` ( N - 1 ) ) e. ZZ /\ ( ! ` ( N - 1 ) ) =/= 0 ) )
128 119 127 syl 
 |-  ( N e. NN -> ( ( ! ` ( N - 1 ) ) e. ZZ /\ ( ! ` ( N - 1 ) ) =/= 0 ) )
129 128 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ! ` ( N - 1 ) ) e. ZZ /\ ( ! ` ( N - 1 ) ) =/= 0 ) )
130 nnz 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. ZZ )
131 nnne0 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) =/= 0 )
132 130 131 jca 
 |-  ( ( ! ` N ) e. NN -> ( ( ! ` N ) e. ZZ /\ ( ! ` N ) =/= 0 ) )
133 120 132 syl 
 |-  ( N e. NN -> ( ( ! ` N ) e. ZZ /\ ( ! ` N ) =/= 0 ) )
134 133 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ! ` N ) e. ZZ /\ ( ! ` N ) =/= 0 ) )
135 pcmul 
 |-  ( ( p e. Prime /\ ( ( ! ` ( N - 1 ) ) e. ZZ /\ ( ! ` ( N - 1 ) ) =/= 0 ) /\ ( ( ! ` N ) e. ZZ /\ ( ! ` N ) =/= 0 ) ) -> ( p pCnt ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) = ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) )
136 67 129 134 135 syl3anc 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) = ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) )
137 136 oveq2d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( p pCnt ( ( ! ` ( N - 1 ) ) x. ( ! ` N ) ) ) ) = ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) ) )
138 113 124 137 3eqtrd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) ) )
139 138 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) ) )
140 simprr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> -. p <_ N )
141 prmfac1 
 |-  ( ( N e. NN0 /\ p e. Prime /\ p || ( ! ` N ) ) -> p <_ N )
142 141 3expia 
 |-  ( ( N e. NN0 /\ p e. Prime ) -> ( p || ( ! ` N ) -> p <_ N ) )
143 12 142 sylan 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p || ( ! ` N ) -> p <_ N ) )
144 143 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p || ( ! ` N ) -> p <_ N ) )
145 140 144 mtod 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> -. p || ( ! ` N ) )
146 80 adantl 
 |-  ( ( N e. NN /\ p e. Prime ) -> p e. ZZ )
147 129 simpld 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ! ` ( N - 1 ) ) e. ZZ )
148 nnz 
 |-  ( N e. NN -> N e. ZZ )
149 148 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> N e. ZZ )
150 dvdsmultr1 
 |-  ( ( p e. ZZ /\ ( ! ` ( N - 1 ) ) e. ZZ /\ N e. ZZ ) -> ( p || ( ! ` ( N - 1 ) ) -> p || ( ( ! ` ( N - 1 ) ) x. N ) ) )
151 146 147 149 150 syl3anc 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p || ( ! ` ( N - 1 ) ) -> p || ( ( ! ` ( N - 1 ) ) x. N ) ) )
152 facnn2 
 |-  ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
153 152 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
154 153 breq2d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p || ( ! ` N ) <-> p || ( ( ! ` ( N - 1 ) ) x. N ) ) )
155 151 154 sylibrd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p || ( ! ` ( N - 1 ) ) -> p || ( ! ` N ) ) )
156 155 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p || ( ! ` ( N - 1 ) ) -> p || ( ! ` N ) ) )
157 145 156 mtod 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> -. p || ( ! ` ( N - 1 ) ) )
158 pceq0 
 |-  ( ( p e. Prime /\ ( ! ` ( N - 1 ) ) e. NN ) -> ( ( p pCnt ( ! ` ( N - 1 ) ) ) = 0 <-> -. p || ( ! ` ( N - 1 ) ) ) )
159 88 119 158 syl2anr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( p pCnt ( ! ` ( N - 1 ) ) ) = 0 <-> -. p || ( ! ` ( N - 1 ) ) ) )
160 159 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` ( N - 1 ) ) ) = 0 <-> -. p || ( ! ` ( N - 1 ) ) ) )
161 157 160 mpbird 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p pCnt ( ! ` ( N - 1 ) ) ) = 0 )
162 pceq0 
 |-  ( ( p e. Prime /\ ( ! ` N ) e. NN ) -> ( ( p pCnt ( ! ` N ) ) = 0 <-> -. p || ( ! ` N ) ) )
163 88 120 162 syl2anr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( p pCnt ( ! ` N ) ) = 0 <-> -. p || ( ! ` N ) ) )
164 163 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` N ) ) = 0 <-> -. p || ( ! ` N ) ) )
165 145 164 mpbird 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p pCnt ( ! ` N ) ) = 0 )
166 161 165 oveq12d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) = ( 0 + 0 ) )
167 00id 
 |-  ( 0 + 0 ) = 0
168 166 167 eqtrdi 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) = 0 )
169 168 oveq2d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - ( ( p pCnt ( ! ` ( N - 1 ) ) ) + ( p pCnt ( ! ` N ) ) ) ) = ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - 0 ) )
170 pccl 
 |-  ( ( p e. Prime /\ ( ! ` ( ( 2 x. N ) - 1 ) ) e. NN ) -> ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. NN0 )
171 88 89 170 syl2anr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. NN0 )
172 171 nn0cnd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) e. CC )
173 172 subid1d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - 0 ) = ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
174 173 adantr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) - 0 ) = ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
175 139 169 174 3eqtrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
176 97 100 175 3eqtrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( p pCnt ( ! ` ( ( 2 x. N ) - 1 ) ) ) )
177 94 176 breqtrrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ ( p <_ ( ( 2 x. N ) - 1 ) /\ -. p <_ N ) ) -> 1 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
178 177 expr 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ ( ( 2 x. N ) - 1 ) ) -> ( -. p <_ N -> 1 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
179 76 178 pm2.61d 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ ( ( 2 x. N ) - 1 ) ) -> 1 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
180 66 179 eqbrtrd 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ p <_ ( ( 2 x. N ) - 1 ) ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
181 180 ex 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p <_ ( ( 2 x. N ) - 1 ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
182 1nn0 
 |-  1 e. NN0
183 0nn0 
 |-  0 e. NN0
184 182 183 ifcli 
 |-  if ( p <_ N , 1 , 0 ) e. NN0
185 nn0addcl 
 |-  ( ( if ( p <_ N , 1 , 0 ) e. NN0 /\ ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) e. NN0 ) -> ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) e. NN0 )
186 184 69 185 sylancr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) e. NN0 )
187 186 nn0ge0d 
 |-  ( ( N e. NN /\ p e. Prime ) -> 0 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
188 iffalse 
 |-  ( -. p <_ ( ( 2 x. N ) - 1 ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) = 0 )
189 188 breq1d 
 |-  ( -. p <_ ( ( 2 x. N ) - 1 ) -> ( if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <-> 0 <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
190 187 189 syl5ibrcom 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( -. p <_ ( ( 2 x. N ) - 1 ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
191 181 190 pm2.61d 
 |-  ( ( N e. NN /\ p e. Prime ) -> if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) <_ ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
192 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , n , 1 ) ) = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
193 192 prmorcht 
 |-  ( ( ( 2 x. N ) - 1 ) e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` ( ( 2 x. N ) - 1 ) ) )
194 37 193 syl 
 |-  ( N e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` ( ( 2 x. N ) - 1 ) ) )
195 194 oveq2d 
 |-  ( N e. NN -> ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) = ( p pCnt ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` ( ( 2 x. N ) - 1 ) ) ) )
196 195 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) = ( p pCnt ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` ( ( 2 x. N ) - 1 ) ) ) )
197 nncn 
 |-  ( n e. NN -> n e. CC )
198 197 exp1d 
 |-  ( n e. NN -> ( n ^ 1 ) = n )
199 198 ifeq1d 
 |-  ( n e. NN -> if ( n e. Prime , ( n ^ 1 ) , 1 ) = if ( n e. Prime , n , 1 ) )
200 199 mpteq2ia 
 |-  ( n e. NN |-> if ( n e. Prime , ( n ^ 1 ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
201 200 eqcomi 
 |-  ( n e. NN |-> if ( n e. Prime , n , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( n ^ 1 ) , 1 ) )
202 182 a1i 
 |-  ( ( ( N e. NN /\ p e. Prime ) /\ n e. Prime ) -> 1 e. NN0 )
203 202 ralrimiva 
 |-  ( ( N e. NN /\ p e. Prime ) -> A. n e. Prime 1 e. NN0 )
204 37 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( 2 x. N ) - 1 ) e. NN )
205 eqidd 
 |-  ( n = p -> 1 = 1 )
206 201 203 204 67 205 pcmpt 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` ( ( 2 x. N ) - 1 ) ) ) = if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) )
207 196 206 eqtrd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) = if ( p <_ ( ( 2 x. N ) - 1 ) , 1 , 0 ) )
208 efchtcl 
 |-  ( N e. RR -> ( exp ` ( theta ` N ) ) e. NN )
209 9 208 syl 
 |-  ( N e. NN -> ( exp ` ( theta ` N ) ) e. NN )
210 209 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( exp ` ( theta ` N ) ) e. NN )
211 nnz 
 |-  ( ( exp ` ( theta ` N ) ) e. NN -> ( exp ` ( theta ` N ) ) e. ZZ )
212 nnne0 
 |-  ( ( exp ` ( theta ` N ) ) e. NN -> ( exp ` ( theta ` N ) ) =/= 0 )
213 211 212 jca 
 |-  ( ( exp ` ( theta ` N ) ) e. NN -> ( ( exp ` ( theta ` N ) ) e. ZZ /\ ( exp ` ( theta ` N ) ) =/= 0 ) )
214 210 213 syl 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( exp ` ( theta ` N ) ) e. ZZ /\ ( exp ` ( theta ` N ) ) =/= 0 ) )
215 nnz 
 |-  ( ( ( ( 2 x. N ) - 1 ) _C N ) e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) e. ZZ )
216 nnne0 
 |-  ( ( ( ( 2 x. N ) - 1 ) _C N ) e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) =/= 0 )
217 215 216 jca 
 |-  ( ( ( ( 2 x. N ) - 1 ) _C N ) e. NN -> ( ( ( ( 2 x. N ) - 1 ) _C N ) e. ZZ /\ ( ( ( 2 x. N ) - 1 ) _C N ) =/= 0 ) )
218 68 217 syl 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( ( ( 2 x. N ) - 1 ) _C N ) e. ZZ /\ ( ( ( 2 x. N ) - 1 ) _C N ) =/= 0 ) )
219 pcmul 
 |-  ( ( p e. Prime /\ ( ( exp ` ( theta ` N ) ) e. ZZ /\ ( exp ` ( theta ` N ) ) =/= 0 ) /\ ( ( ( ( 2 x. N ) - 1 ) _C N ) e. ZZ /\ ( ( ( 2 x. N ) - 1 ) _C N ) =/= 0 ) ) -> ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( ( p pCnt ( exp ` ( theta ` N ) ) ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
220 67 214 218 219 syl3anc 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( ( p pCnt ( exp ` ( theta ` N ) ) ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
221 192 prmorcht 
 |-  ( N e. NN -> ( exp ` ( theta ` N ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` N ) )
222 221 oveq2d 
 |-  ( N e. NN -> ( p pCnt ( exp ` ( theta ` N ) ) ) = ( p pCnt ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` N ) ) )
223 222 adantr 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( exp ` ( theta ` N ) ) ) = ( p pCnt ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` N ) ) )
224 simpl 
 |-  ( ( N e. NN /\ p e. Prime ) -> N e. NN )
225 201 203 224 67 205 pcmpt 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` N ) ) = if ( p <_ N , 1 , 0 ) )
226 223 225 eqtrd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( exp ` ( theta ` N ) ) ) = if ( p <_ N , 1 , 0 ) )
227 226 oveq1d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( ( p pCnt ( exp ` ( theta ` N ) ) ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
228 220 227 eqtrd 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( if ( p <_ N , 1 , 0 ) + ( p pCnt ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
229 191 207 228 3brtr4d 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
230 229 ralrimiva 
 |-  ( N e. NN -> A. p e. Prime ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
231 efchtcl 
 |-  ( ( ( 2 x. N ) - 1 ) e. RR -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) e. NN )
232 6 231 syl 
 |-  ( N e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) e. NN )
233 232 nnzd 
 |-  ( N e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) e. ZZ )
234 209 52 nnmulcld 
 |-  ( N e. NN -> ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) e. NN )
235 234 nnzd 
 |-  ( N e. NN -> ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) e. ZZ )
236 pc2dvds 
 |-  ( ( ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) e. ZZ /\ ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) e. ZZ ) -> ( ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) || ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) <-> A. p e. Prime ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
237 233 235 236 syl2anc 
 |-  ( N e. NN -> ( ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) || ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) <-> A. p e. Prime ( p pCnt ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
238 230 237 mpbird 
 |-  ( N e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) || ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) )
239 dvdsle 
 |-  ( ( ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) e. ZZ /\ ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) e. NN ) -> ( ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) || ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) <_ ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
240 233 234 239 syl2anc 
 |-  ( N e. NN -> ( ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) || ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) <_ ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
241 238 240 mpd 
 |-  ( N e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) <_ ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) )
242 11 recnd 
 |-  ( N e. NN -> ( theta ` N ) e. CC )
243 54 recnd 
 |-  ( N e. NN -> ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) e. CC )
244 efadd 
 |-  ( ( ( theta ` N ) e. CC /\ ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) e. CC ) -> ( exp ` ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) = ( ( exp ` ( theta ` N ) ) x. ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
245 242 243 244 syl2anc 
 |-  ( N e. NN -> ( exp ` ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) = ( ( exp ` ( theta ` N ) ) x. ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
246 53 reeflogd 
 |-  ( N e. NN -> ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) = ( ( ( 2 x. N ) - 1 ) _C N ) )
247 246 oveq2d 
 |-  ( N e. NN -> ( ( exp ` ( theta ` N ) ) x. ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) = ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) )
248 245 247 eqtrd 
 |-  ( N e. NN -> ( exp ` ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) = ( ( exp ` ( theta ` N ) ) x. ( ( ( 2 x. N ) - 1 ) _C N ) ) )
249 241 248 breqtrrd 
 |-  ( N e. NN -> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) <_ ( exp ` ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) )
250 efle 
 |-  ( ( ( theta ` ( ( 2 x. N ) - 1 ) ) e. RR /\ ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) e. RR ) -> ( ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <-> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) <_ ( exp ` ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) ) )
251 8 55 250 syl2anc 
 |-  ( N e. NN -> ( ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <-> ( exp ` ( theta ` ( ( 2 x. N ) - 1 ) ) ) <_ ( exp ` ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) ) ) )
252 249 251 mpbird 
 |-  ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) )
253 fzfid 
 |-  ( N e. NN -> ( 0 ... ( ( 2 x. N ) - 1 ) ) e. Fin )
254 elfzelz 
 |-  ( k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) -> k e. ZZ )
255 bccl 
 |-  ( ( ( ( 2 x. N ) - 1 ) e. NN0 /\ k e. ZZ ) -> ( ( ( 2 x. N ) - 1 ) _C k ) e. NN0 )
256 39 254 255 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ) -> ( ( ( 2 x. N ) - 1 ) _C k ) e. NN0 )
257 256 nn0red 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ) -> ( ( ( 2 x. N ) - 1 ) _C k ) e. RR )
258 256 nn0ge0d 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ) -> 0 <_ ( ( ( 2 x. N ) - 1 ) _C k ) )
259 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
260 32 259 eleqtrdi 
 |-  ( N e. NN -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
261 fzss1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` 0 ) -> ( ( N - 1 ) ... N ) C_ ( 0 ... N ) )
262 260 261 syl 
 |-  ( N e. NN -> ( ( N - 1 ) ... N ) C_ ( 0 ... N ) )
263 eluz 
 |-  ( ( N e. ZZ /\ ( ( 2 x. N ) - 1 ) e. ZZ ) -> ( ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` N ) <-> N <_ ( ( 2 x. N ) - 1 ) ) )
264 148 81 263 syl2anc 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` N ) <-> N <_ ( ( 2 x. N ) - 1 ) ) )
265 48 264 mpbird 
 |-  ( N e. NN -> ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` N ) )
266 fzss2 
 |-  ( ( ( 2 x. N ) - 1 ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... ( ( 2 x. N ) - 1 ) ) )
267 265 266 syl 
 |-  ( N e. NN -> ( 0 ... N ) C_ ( 0 ... ( ( 2 x. N ) - 1 ) ) )
268 262 267 sstrd 
 |-  ( N e. NN -> ( ( N - 1 ) ... N ) C_ ( 0 ... ( ( 2 x. N ) - 1 ) ) )
269 253 257 258 268 fsumless 
 |-  ( N e. NN -> sum_ k e. ( ( N - 1 ) ... N ) ( ( ( 2 x. N ) - 1 ) _C k ) <_ sum_ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) )
270 32 nn0zd 
 |-  ( N e. NN -> ( N - 1 ) e. ZZ )
271 bccmpl 
 |-  ( ( ( ( 2 x. N ) - 1 ) e. NN0 /\ N e. ZZ ) -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ( 2 x. N ) - 1 ) _C ( ( ( 2 x. N ) - 1 ) - N ) ) )
272 39 148 271 syl2anc 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ( 2 x. N ) - 1 ) _C ( ( ( 2 x. N ) - 1 ) - N ) ) )
273 107 oveq2d 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C ( ( ( 2 x. N ) - 1 ) - N ) ) = ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) )
274 272 273 eqtrd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) = ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) )
275 52 nncnd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) e. CC )
276 274 275 eqeltrrd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) e. CC )
277 oveq2 
 |-  ( k = ( N - 1 ) -> ( ( ( 2 x. N ) - 1 ) _C k ) = ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) )
278 277 fsum1 
 |-  ( ( ( N - 1 ) e. ZZ /\ ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) e. CC ) -> sum_ k e. ( ( N - 1 ) ... ( N - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) = ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) )
279 270 276 278 syl2anc 
 |-  ( N e. NN -> sum_ k e. ( ( N - 1 ) ... ( N - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) = ( ( ( 2 x. N ) - 1 ) _C ( N - 1 ) ) )
280 279 274 eqtr4d 
 |-  ( N e. NN -> sum_ k e. ( ( N - 1 ) ... ( N - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) = ( ( ( 2 x. N ) - 1 ) _C N ) )
281 280 oveq1d 
 |-  ( N e. NN -> ( sum_ k e. ( ( N - 1 ) ... ( N - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) + ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( ( ( ( 2 x. N ) - 1 ) _C N ) + ( ( ( 2 x. N ) - 1 ) _C N ) ) )
282 21 104 npcand 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
283 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
284 270 283 syl 
 |-  ( N e. NN -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
285 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
286 284 285 syl 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
287 282 286 eqeltrrd 
 |-  ( N e. NN -> N e. ( ZZ>= ` ( N - 1 ) ) )
288 268 sselda 
 |-  ( ( N e. NN /\ k e. ( ( N - 1 ) ... N ) ) -> k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) )
289 256 nn0cnd 
 |-  ( ( N e. NN /\ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ) -> ( ( ( 2 x. N ) - 1 ) _C k ) e. CC )
290 288 289 syldan 
 |-  ( ( N e. NN /\ k e. ( ( N - 1 ) ... N ) ) -> ( ( ( 2 x. N ) - 1 ) _C k ) e. CC )
291 oveq2 
 |-  ( k = N -> ( ( ( 2 x. N ) - 1 ) _C k ) = ( ( ( 2 x. N ) - 1 ) _C N ) )
292 287 290 291 fsumm1 
 |-  ( N e. NN -> sum_ k e. ( ( N - 1 ) ... N ) ( ( ( 2 x. N ) - 1 ) _C k ) = ( sum_ k e. ( ( N - 1 ) ... ( N - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) + ( ( ( 2 x. N ) - 1 ) _C N ) ) )
293 275 2timesd 
 |-  ( N e. NN -> ( 2 x. ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( ( ( ( 2 x. N ) - 1 ) _C N ) + ( ( ( 2 x. N ) - 1 ) _C N ) ) )
294 281 292 293 3eqtr4rd 
 |-  ( N e. NN -> ( 2 x. ( ( ( 2 x. N ) - 1 ) _C N ) ) = sum_ k e. ( ( N - 1 ) ... N ) ( ( ( 2 x. N ) - 1 ) _C k ) )
295 binom11 
 |-  ( ( ( 2 x. N ) - 1 ) e. NN0 -> ( 2 ^ ( ( 2 x. N ) - 1 ) ) = sum_ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) )
296 39 295 syl 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 x. N ) - 1 ) ) = sum_ k e. ( 0 ... ( ( 2 x. N ) - 1 ) ) ( ( ( 2 x. N ) - 1 ) _C k ) )
297 269 294 296 3brtr4d 
 |-  ( N e. NN -> ( 2 x. ( ( ( 2 x. N ) - 1 ) _C N ) ) <_ ( 2 ^ ( ( 2 x. N ) - 1 ) ) )
298 mulcom 
 |-  ( ( 2 e. CC /\ ( ( ( 2 x. N ) - 1 ) _C N ) e. CC ) -> ( 2 x. ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( ( ( ( 2 x. N ) - 1 ) _C N ) x. 2 ) )
299 16 275 298 sylancr 
 |-  ( N e. NN -> ( 2 x. ( ( ( 2 x. N ) - 1 ) _C N ) ) = ( ( ( ( 2 x. N ) - 1 ) _C N ) x. 2 ) )
300 30 oveq2d 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 x. N ) - 1 ) ) = ( 2 ^ ( ( 2 x. ( N - 1 ) ) + 1 ) ) )
301 expp1 
 |-  ( ( 2 e. CC /\ ( 2 x. ( N - 1 ) ) e. NN0 ) -> ( 2 ^ ( ( 2 x. ( N - 1 ) ) + 1 ) ) = ( ( 2 ^ ( 2 x. ( N - 1 ) ) ) x. 2 ) )
302 16 34 301 sylancr 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 x. ( N - 1 ) ) + 1 ) ) = ( ( 2 ^ ( 2 x. ( N - 1 ) ) ) x. 2 ) )
303 16 a1i 
 |-  ( N e. NN -> 2 e. CC )
304 31 a1i 
 |-  ( N e. NN -> 2 e. NN0 )
305 303 32 304 expmuld 
 |-  ( N e. NN -> ( 2 ^ ( 2 x. ( N - 1 ) ) ) = ( ( 2 ^ 2 ) ^ ( N - 1 ) ) )
306 sq2 
 |-  ( 2 ^ 2 ) = 4
307 306 oveq1i 
 |-  ( ( 2 ^ 2 ) ^ ( N - 1 ) ) = ( 4 ^ ( N - 1 ) )
308 305 307 eqtrdi 
 |-  ( N e. NN -> ( 2 ^ ( 2 x. ( N - 1 ) ) ) = ( 4 ^ ( N - 1 ) ) )
309 308 oveq1d 
 |-  ( N e. NN -> ( ( 2 ^ ( 2 x. ( N - 1 ) ) ) x. 2 ) = ( ( 4 ^ ( N - 1 ) ) x. 2 ) )
310 300 302 309 3eqtrd 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 x. N ) - 1 ) ) = ( ( 4 ^ ( N - 1 ) ) x. 2 ) )
311 297 299 310 3brtr3d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) - 1 ) _C N ) x. 2 ) <_ ( ( 4 ^ ( N - 1 ) ) x. 2 ) )
312 52 nnred 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) e. RR )
313 reexpcl 
 |-  ( ( 4 e. RR /\ ( N - 1 ) e. NN0 ) -> ( 4 ^ ( N - 1 ) ) e. RR )
314 56 32 313 sylancr 
 |-  ( N e. NN -> ( 4 ^ ( N - 1 ) ) e. RR )
315 2re 
 |-  2 e. RR
316 2pos 
 |-  0 < 2
317 315 316 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
318 317 a1i 
 |-  ( N e. NN -> ( 2 e. RR /\ 0 < 2 ) )
319 lemul1 
 |-  ( ( ( ( ( 2 x. N ) - 1 ) _C N ) e. RR /\ ( 4 ^ ( N - 1 ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( ( 2 x. N ) - 1 ) _C N ) <_ ( 4 ^ ( N - 1 ) ) <-> ( ( ( ( 2 x. N ) - 1 ) _C N ) x. 2 ) <_ ( ( 4 ^ ( N - 1 ) ) x. 2 ) ) )
320 312 314 318 319 syl3anc 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) - 1 ) _C N ) <_ ( 4 ^ ( N - 1 ) ) <-> ( ( ( ( 2 x. N ) - 1 ) _C N ) x. 2 ) <_ ( ( 4 ^ ( N - 1 ) ) x. 2 ) ) )
321 311 320 mpbird 
 |-  ( N e. NN -> ( ( ( 2 x. N ) - 1 ) _C N ) <_ ( 4 ^ ( N - 1 ) ) )
322 60 recni 
 |-  ( log ` 4 ) e. CC
323 mulcom 
 |-  ( ( ( log ` 4 ) e. CC /\ ( N - 1 ) e. CC ) -> ( ( log ` 4 ) x. ( N - 1 ) ) = ( ( N - 1 ) x. ( log ` 4 ) ) )
324 322 103 323 sylancr 
 |-  ( N e. NN -> ( ( log ` 4 ) x. ( N - 1 ) ) = ( ( N - 1 ) x. ( log ` 4 ) ) )
325 324 fveq2d 
 |-  ( N e. NN -> ( exp ` ( ( log ` 4 ) x. ( N - 1 ) ) ) = ( exp ` ( ( N - 1 ) x. ( log ` 4 ) ) ) )
326 reexplog 
 |-  ( ( 4 e. RR+ /\ ( N - 1 ) e. ZZ ) -> ( 4 ^ ( N - 1 ) ) = ( exp ` ( ( N - 1 ) x. ( log ` 4 ) ) ) )
327 58 270 326 sylancr 
 |-  ( N e. NN -> ( 4 ^ ( N - 1 ) ) = ( exp ` ( ( N - 1 ) x. ( log ` 4 ) ) ) )
328 325 327 eqtr4d 
 |-  ( N e. NN -> ( exp ` ( ( log ` 4 ) x. ( N - 1 ) ) ) = ( 4 ^ ( N - 1 ) ) )
329 321 246 328 3brtr4d 
 |-  ( N e. NN -> ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <_ ( exp ` ( ( log ` 4 ) x. ( N - 1 ) ) ) )
330 efle 
 |-  ( ( ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) e. RR /\ ( ( log ` 4 ) x. ( N - 1 ) ) e. RR ) -> ( ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) <_ ( ( log ` 4 ) x. ( N - 1 ) ) <-> ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <_ ( exp ` ( ( log ` 4 ) x. ( N - 1 ) ) ) ) )
331 54 63 330 syl2anc 
 |-  ( N e. NN -> ( ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) <_ ( ( log ` 4 ) x. ( N - 1 ) ) <-> ( exp ` ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <_ ( exp ` ( ( log ` 4 ) x. ( N - 1 ) ) ) ) )
332 329 331 mpbird 
 |-  ( N e. NN -> ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) <_ ( ( log ` 4 ) x. ( N - 1 ) ) )
333 54 63 11 332 leadd2dd 
 |-  ( N e. NN -> ( ( theta ` N ) + ( log ` ( ( ( 2 x. N ) - 1 ) _C N ) ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )
334 8 55 64 252 333 letrd 
 |-  ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )