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 ) ) ) )