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