Metamath Proof Explorer

Theorem aks4d1p1

Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 21-Aug-2024)

Ref Expression
Hypotheses aks4d1p1.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1p1.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p1.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
Assertion aks4d1p1 
|- ( ph -> A < ( 2 ^ B ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p1.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p1.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 3nn 
 |-  3 e. NN
5 4 a1i 
 |-  ( ( ph /\ 3 < N ) -> 3 e. NN )
6 1 adantr 
 |-  ( ( ph /\ 3 < N ) -> N e. ( ZZ>= ` 3 ) )
7 eluznn 
 |-  ( ( 3 e. NN /\ N e. ( ZZ>= ` 3 ) ) -> N e. NN )
8 5 6 7 syl2anc 
 |-  ( ( ph /\ 3 < N ) -> N e. NN )
9 3p1e4 
 |-  ( 3 + 1 ) = 4
10 simpr 
 |-  ( ( ph /\ 3 < N ) -> 3 < N )
11 3z 
 |-  3 e. ZZ
12 11 a1i 
 |-  ( ( ph /\ 3 < N ) -> 3 e. ZZ )
13 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
14 1 13 syl 
 |-  ( ph -> N e. ZZ )
15 14 adantr 
 |-  ( ( ph /\ 3 < N ) -> N e. ZZ )
16 12 15 zltp1led 
 |-  ( ( ph /\ 3 < N ) -> ( 3 < N <-> ( 3 + 1 ) <_ N ) )
17 10 16 mpbid 
 |-  ( ( ph /\ 3 < N ) -> ( 3 + 1 ) <_ N )
18 9 17 eqbrtrrid 
 |-  ( ( ph /\ 3 < N ) -> 4 <_ N )
19 eqid 
 |-  ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
20 eqid 
 |-  ( ( 2 logb N ) ^ 2 ) = ( ( 2 logb N ) ^ 2 )
21 eqid 
 |-  ( ( 2 logb N ) ^ 4 ) = ( ( 2 logb N ) ^ 4 )
22 8 2 3 18 19 20 21 aks4d1p1p5 
 |-  ( ( ph /\ 3 < N ) -> A < ( 2 ^ B ) )
23 22 ex 
 |-  ( ph -> ( 3 < N -> A < ( 2 ^ B ) ) )
24 simp2 
 |-  ( ( ph /\ 3 = N /\ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ) -> 3 = N )
25 24 eqcomd 
 |-  ( ( ph /\ 3 = N /\ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ) -> N = 3 )
26 25 oveq1d 
 |-  ( ( ph /\ 3 = N /\ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ) -> ( N ^ k ) = ( 3 ^ k ) )
27 26 oveq1d 
 |-  ( ( ph /\ 3 = N /\ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) = ( ( 3 ^ k ) - 1 ) )
28 27 3expa 
 |-  ( ( ( ph /\ 3 = N ) /\ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) = ( ( 3 ^ k ) - 1 ) )
29 28 prodeq2dv 
 |-  ( ( ph /\ 3 = N ) -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) = prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) )
30 29 oveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) = ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) ) )
31 2rp 
 |-  2 e. RR+
32 31 a1i 
 |-  ( ph -> 2 e. RR+ )
33 1red 
 |-  ( ph -> 1 e. RR )
34 1lt2 
 |-  1 < 2
35 34 a1i 
 |-  ( ph -> 1 < 2 )
36 33 35 ltned 
 |-  ( ph -> 1 =/= 2 )
37 36 necomd 
 |-  ( ph -> 2 =/= 1 )
38 11 a1i 
 |-  ( ph -> 3 e. ZZ )
39 32 37 38 relogbexpd 
 |-  ( ph -> ( 2 logb ( 2 ^ 3 ) ) = 3 )
40 39 eqcomd 
 |-  ( ph -> 3 = ( 2 logb ( 2 ^ 3 ) ) )
41 cu2 
 |-  ( 2 ^ 3 ) = 8
42 41 a1i 
 |-  ( ph -> ( 2 ^ 3 ) = 8 )
43 42 oveq2d 
 |-  ( ph -> ( 2 logb ( 2 ^ 3 ) ) = ( 2 logb 8 ) )
44 40 43 eqtrd 
 |-  ( ph -> 3 = ( 2 logb 8 ) )
45 2z 
 |-  2 e. ZZ
46 45 a1i 
 |-  ( ph -> 2 e. ZZ )
47 46 zred 
 |-  ( ph -> 2 e. RR )
48 47 leidd 
 |-  ( ph -> 2 <_ 2 )
49 8re 
 |-  8 e. RR
50 49 a1i 
 |-  ( ph -> 8 e. RR )
51 8pos 
 |-  0 < 8
52 51 a1i 
 |-  ( ph -> 0 < 8 )
53 32 rpgt0d 
 |-  ( ph -> 0 < 2 )
54 3re 
 |-  3 e. RR
55 54 a1i 
 |-  ( ph -> 3 e. RR )
56 4 nngt0i 
 |-  0 < 3
57 56 a1i 
 |-  ( ph -> 0 < 3 )
58 47 53 55 57 37 relogbcld 
 |-  ( ph -> ( 2 logb 3 ) e. RR )
59 5nn0 
 |-  5 e. NN0
60 59 a1i 
 |-  ( ph -> 5 e. NN0 )
61 58 60 reexpcld 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 5 ) e. RR )
62 ceilcl 
 |-  ( ( ( 2 logb 3 ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. ZZ )
63 61 62 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. ZZ )
64 63 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. RR )
65 0red 
 |-  ( ph -> 0 e. RR )
66 9re 
 |-  9 e. RR
67 66 a1i 
 |-  ( ph -> 9 e. RR )
68 50 lep1d 
 |-  ( ph -> 8 <_ ( 8 + 1 ) )
69 8p1e9 
 |-  ( 8 + 1 ) = 9
70 69 a1i 
 |-  ( ph -> ( 8 + 1 ) = 9 )
71 68 70 breqtrd 
 |-  ( ph -> 8 <_ 9 )
72 2re 
 |-  2 e. RR
73 72 a1i 
 |-  ( ph -> 2 e. RR )
74 2pos 
 |-  0 < 2
75 74 a1i 
 |-  ( ph -> 0 < 2 )
76 3pos 
 |-  0 < 3
77 76 a1i 
 |-  ( ph -> 0 < 3 )
78 73 75 55 77 37 relogbcld 
 |-  ( ph -> ( 2 logb 3 ) e. RR )
79 78 60 reexpcld 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 5 ) e. RR )
80 79 62 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. ZZ )
81 80 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. RR )
82 55 leidd 
 |-  ( ph -> 3 <_ 3 )
83 55 82 3lexlogpow5ineq4 
 |-  ( ph -> 9 < ( ( 2 logb 3 ) ^ 5 ) )
84 67 79 83 ltled 
 |-  ( ph -> 9 <_ ( ( 2 logb 3 ) ^ 5 ) )
85 ceilge 
 |-  ( ( ( 2 logb 3 ) ^ 5 ) e. RR -> ( ( 2 logb 3 ) ^ 5 ) <_ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) )
86 79 85 syl 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 5 ) <_ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) )
87 67 79 81 84 86 letrd 
 |-  ( ph -> 9 <_ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) )
88 50 67 64 71 87 letrd 
 |-  ( ph -> 8 <_ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) )
89 65 50 64 52 88 ltletrd 
 |-  ( ph -> 0 < ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) )
90 46 48 50 52 64 89 88 logblebd 
 |-  ( ph -> ( 2 logb 8 ) <_ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
91 44 90 eqbrtrd 
 |-  ( ph -> 3 <_ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
92 79 33 readdcld 
 |-  ( ph -> ( ( ( 2 logb 3 ) ^ 5 ) + 1 ) e. RR )
93 1nn0 
 |-  1 e. NN0
94 6nn 
 |-  6 e. NN
95 93 94 decnncl 
 |-  ; 1 6 e. NN
96 95 a1i 
 |-  ( ph -> ; 1 6 e. NN )
97 96 nnred 
 |-  ( ph -> ; 1 6 e. RR )
98 ceilm1lt 
 |-  ( ( ( 2 logb 3 ) ^ 5 ) e. RR -> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) - 1 ) < ( ( 2 logb 3 ) ^ 5 ) )
99 79 98 syl 
 |-  ( ph -> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) - 1 ) < ( ( 2 logb 3 ) ^ 5 ) )
100 81 33 79 ltsubaddd 
 |-  ( ph -> ( ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) - 1 ) < ( ( 2 logb 3 ) ^ 5 ) <-> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) < ( ( ( 2 logb 3 ) ^ 5 ) + 1 ) ) )
101 99 100 mpbid 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) < ( ( ( 2 logb 3 ) ^ 5 ) + 1 ) )
102 3lexlogpow5ineq5 
 |-  ( ( 2 logb 3 ) ^ 5 ) <_ ; 1 5
103 102 a1i 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 5 ) <_ ; 1 5 )
104 5p1e6 
 |-  ( 5 + 1 ) = 6
105 eqid 
 |-  ; 1 5 = ; 1 5
106 93 59 104 105 decsuc 
 |-  ( ; 1 5 + 1 ) = ; 1 6
107 106 a1i 
 |-  ( ph -> ( ; 1 5 + 1 ) = ; 1 6 )
108 97 recnd 
 |-  ( ph -> ; 1 6 e. CC )
109 1cnd 
 |-  ( ph -> 1 e. CC )
110 5nn 
 |-  5 e. NN
111 93 110 decnncl 
 |-  ; 1 5 e. NN
112 111 a1i 
 |-  ( ph -> ; 1 5 e. NN )
113 112 nncnd 
 |-  ( ph -> ; 1 5 e. CC )
114 108 109 113 subadd2d 
 |-  ( ph -> ( ( ; 1 6 - 1 ) = ; 1 5 <-> ( ; 1 5 + 1 ) = ; 1 6 ) )
115 107 114 mpbird 
 |-  ( ph -> ( ; 1 6 - 1 ) = ; 1 5 )
116 115 eqcomd 
 |-  ( ph -> ; 1 5 = ( ; 1 6 - 1 ) )
117 103 116 breqtrd 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 5 ) <_ ( ; 1 6 - 1 ) )
118 leaddsub 
 |-  ( ( ( ( 2 logb 3 ) ^ 5 ) e. RR /\ 1 e. RR /\ ; 1 6 e. RR ) -> ( ( ( ( 2 logb 3 ) ^ 5 ) + 1 ) <_ ; 1 6 <-> ( ( 2 logb 3 ) ^ 5 ) <_ ( ; 1 6 - 1 ) ) )
119 79 33 97 118 syl3anc 
 |-  ( ph -> ( ( ( ( 2 logb 3 ) ^ 5 ) + 1 ) <_ ; 1 6 <-> ( ( 2 logb 3 ) ^ 5 ) <_ ( ; 1 6 - 1 ) ) )
120 117 119 mpbird 
 |-  ( ph -> ( ( ( 2 logb 3 ) ^ 5 ) + 1 ) <_ ; 1 6 )
121 81 92 97 101 120 ltletrd 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) < ; 1 6 )
122 eqid 
 |-  ; 1 6 = ; 1 6
123 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
124 122 123 eqtr4i 
 |-  ; 1 6 = ( 2 ^ 4 )
125 124 a1i 
 |-  ( ph -> ; 1 6 = ( 2 ^ 4 ) )
126 121 125 breqtrd 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) < ( 2 ^ 4 ) )
127 46 uzidd 
 |-  ( ph -> 2 e. ( ZZ>= ` 2 ) )
128 64 89 elrpd 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. RR+ )
129 4z 
 |-  4 e. ZZ
130 129 a1i 
 |-  ( ph -> 4 e. ZZ )
131 32 130 rpexpcld 
 |-  ( ph -> ( 2 ^ 4 ) e. RR+ )
132 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. RR+ /\ ( 2 ^ 4 ) e. RR+ ) -> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) < ( 2 ^ 4 ) <-> ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 2 logb ( 2 ^ 4 ) ) ) )
133 127 128 131 132 syl3anc 
 |-  ( ph -> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) < ( 2 ^ 4 ) <-> ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 2 logb ( 2 ^ 4 ) ) ) )
134 126 133 mpbid 
 |-  ( ph -> ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 2 logb ( 2 ^ 4 ) ) )
135 32 37 130 relogbexpd 
 |-  ( ph -> ( 2 logb ( 2 ^ 4 ) ) = 4 )
136 9 eqcomi 
 |-  4 = ( 3 + 1 )
137 136 a1i 
 |-  ( ph -> 4 = ( 3 + 1 ) )
138 135 137 eqtrd 
 |-  ( ph -> ( 2 logb ( 2 ^ 4 ) ) = ( 3 + 1 ) )
139 134 138 breqtrd 
 |-  ( ph -> ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 3 + 1 ) )
140 91 139 jca 
 |-  ( ph -> ( 3 <_ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) /\ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 3 + 1 ) ) )
141 73 75 55 57 37 relogbcld 
 |-  ( ph -> ( 2 logb 3 ) e. RR )
142 141 60 reexpcld 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 5 ) e. RR )
143 142 62 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. ZZ )
144 143 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. RR )
145 9pos 
 |-  0 < 9
146 145 a1i 
 |-  ( ph -> 0 < 9 )
147 65 67 144 146 87 ltletrd 
 |-  ( ph -> 0 < ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) )
148 73 75 144 147 37 relogbcld 
 |-  ( ph -> ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) e. RR )
149 flbi 
 |-  ( ( ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) e. RR /\ 3 e. ZZ ) -> ( ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) = 3 <-> ( 3 <_ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) /\ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 3 + 1 ) ) ) )
150 148 38 149 syl2anc 
 |-  ( ph -> ( ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) = 3 <-> ( 3 <_ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) /\ ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) < ( 3 + 1 ) ) ) )
151 140 150 mpbird 
 |-  ( ph -> ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) = 3 )
152 151 oveq2d 
 |-  ( ph -> ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) = ( 3 ^ 3 ) )
153 78 resqcld 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 2 ) e. RR )
154 3lexlogpow2ineq2 
 |-  ( 2 < ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < 3 )
155 154 a1i 
 |-  ( ph -> ( 2 < ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < 3 ) )
156 155 simpld 
 |-  ( ph -> 2 < ( ( 2 logb 3 ) ^ 2 ) )
157 73 153 156 ltled 
 |-  ( ph -> 2 <_ ( ( 2 logb 3 ) ^ 2 ) )
158 155 simprd 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 2 ) < 3 )
159 df-3 
 |-  3 = ( 2 + 1 )
160 159 a1i 
 |-  ( ph -> 3 = ( 2 + 1 ) )
161 158 160 breqtrd 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 2 ) < ( 2 + 1 ) )
162 157 161 jca 
 |-  ( ph -> ( 2 <_ ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < ( 2 + 1 ) ) )
163 141 resqcld 
 |-  ( ph -> ( ( 2 logb 3 ) ^ 2 ) e. RR )
164 flbi 
 |-  ( ( ( ( 2 logb 3 ) ^ 2 ) e. RR /\ 2 e. ZZ ) -> ( ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) = 2 <-> ( 2 <_ ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < ( 2 + 1 ) ) ) )
165 163 46 164 syl2anc 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) = 2 <-> ( 2 <_ ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < ( 2 + 1 ) ) ) )
166 162 165 mpbird 
 |-  ( ph -> ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) = 2 )
167 166 oveq2d 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) = ( 1 ... 2 ) )
168 167 prodeq1d 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) = prod_ k e. ( 1 ... 2 ) ( ( 3 ^ k ) - 1 ) )
169 1zzd 
 |-  ( ph -> 1 e. ZZ )
170 169 46 jca 
 |-  ( ph -> ( 1 e. ZZ /\ 2 e. ZZ ) )
171 1le2 
 |-  1 <_ 2
172 171 a1i 
 |-  ( ( 1 e. ZZ /\ 2 e. ZZ ) -> 1 <_ 2 )
173 eluz 
 |-  ( ( 1 e. ZZ /\ 2 e. ZZ ) -> ( 2 e. ( ZZ>= ` 1 ) <-> 1 <_ 2 ) )
174 172 173 mpbird 
 |-  ( ( 1 e. ZZ /\ 2 e. ZZ ) -> 2 e. ( ZZ>= ` 1 ) )
175 170 174 syl 
 |-  ( ph -> 2 e. ( ZZ>= ` 1 ) )
176 3cn 
 |-  3 e. CC
177 176 a1i 
 |-  ( ( ph /\ k e. ( 1 ... 2 ) ) -> 3 e. CC )
178 elfznn 
 |-  ( k e. ( 1 ... 2 ) -> k e. NN )
179 178 adantl 
 |-  ( ( ph /\ k e. ( 1 ... 2 ) ) -> k e. NN )
180 179 nnnn0d 
 |-  ( ( ph /\ k e. ( 1 ... 2 ) ) -> k e. NN0 )
181 177 180 expcld 
 |-  ( ( ph /\ k e. ( 1 ... 2 ) ) -> ( 3 ^ k ) e. CC )
182 1cnd 
 |-  ( ( ph /\ k e. ( 1 ... 2 ) ) -> 1 e. CC )
183 181 182 subcld 
 |-  ( ( ph /\ k e. ( 1 ... 2 ) ) -> ( ( 3 ^ k ) - 1 ) e. CC )
184 oveq2 
 |-  ( k = 2 -> ( 3 ^ k ) = ( 3 ^ 2 ) )
185 184 oveq1d 
 |-  ( k = 2 -> ( ( 3 ^ k ) - 1 ) = ( ( 3 ^ 2 ) - 1 ) )
186 175 183 185 fprodm1 
 |-  ( ph -> prod_ k e. ( 1 ... 2 ) ( ( 3 ^ k ) - 1 ) = ( prod_ k e. ( 1 ... ( 2 - 1 ) ) ( ( 3 ^ k ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) )
187 2m1e1 
 |-  ( 2 - 1 ) = 1
188 187 a1i 
 |-  ( ph -> ( 2 - 1 ) = 1 )
189 188 oveq2d 
 |-  ( ph -> ( 1 ... ( 2 - 1 ) ) = ( 1 ... 1 ) )
190 189 prodeq1d 
 |-  ( ph -> prod_ k e. ( 1 ... ( 2 - 1 ) ) ( ( 3 ^ k ) - 1 ) = prod_ k e. ( 1 ... 1 ) ( ( 3 ^ k ) - 1 ) )
191 55 recnd 
 |-  ( ph -> 3 e. CC )
192 93 a1i 
 |-  ( ph -> 1 e. NN0 )
193 191 192 expcld 
 |-  ( ph -> ( 3 ^ 1 ) e. CC )
194 193 109 subcld 
 |-  ( ph -> ( ( 3 ^ 1 ) - 1 ) e. CC )
195 169 194 jca 
 |-  ( ph -> ( 1 e. ZZ /\ ( ( 3 ^ 1 ) - 1 ) e. CC ) )
196 oveq2 
 |-  ( k = 1 -> ( 3 ^ k ) = ( 3 ^ 1 ) )
197 196 oveq1d 
 |-  ( k = 1 -> ( ( 3 ^ k ) - 1 ) = ( ( 3 ^ 1 ) - 1 ) )
198 197 fprod1 
 |-  ( ( 1 e. ZZ /\ ( ( 3 ^ 1 ) - 1 ) e. CC ) -> prod_ k e. ( 1 ... 1 ) ( ( 3 ^ k ) - 1 ) = ( ( 3 ^ 1 ) - 1 ) )
199 195 198 syl 
 |-  ( ph -> prod_ k e. ( 1 ... 1 ) ( ( 3 ^ k ) - 1 ) = ( ( 3 ^ 1 ) - 1 ) )
200 190 199 eqtrd 
 |-  ( ph -> prod_ k e. ( 1 ... ( 2 - 1 ) ) ( ( 3 ^ k ) - 1 ) = ( ( 3 ^ 1 ) - 1 ) )
201 200 oveq1d 
 |-  ( ph -> ( prod_ k e. ( 1 ... ( 2 - 1 ) ) ( ( 3 ^ k ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) = ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) )
202 186 201 eqtrd 
 |-  ( ph -> prod_ k e. ( 1 ... 2 ) ( ( 3 ^ k ) - 1 ) = ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) )
203 168 202 eqtrd 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) = ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) )
204 152 203 oveq12d 
 |-  ( ph -> ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) ) = ( ( 3 ^ 3 ) x. ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) ) )
205 3nn0 
 |-  3 e. NN0
206 205 a1i 
 |-  ( ph -> 3 e. NN0 )
207 55 206 reexpcld 
 |-  ( ph -> ( 3 ^ 3 ) e. RR )
208 55 192 reexpcld 
 |-  ( ph -> ( 3 ^ 1 ) e. RR )
209 208 33 resubcld 
 |-  ( ph -> ( ( 3 ^ 1 ) - 1 ) e. RR )
210 55 resqcld 
 |-  ( ph -> ( 3 ^ 2 ) e. RR )
211 210 33 resubcld 
 |-  ( ph -> ( ( 3 ^ 2 ) - 1 ) e. RR )
212 209 211 remulcld 
 |-  ( ph -> ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) e. RR )
213 207 212 remulcld 
 |-  ( ph -> ( ( 3 ^ 3 ) x. ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) ) e. RR )
214 9nn0 
 |-  9 e. NN0
215 214 a1i 
 |-  ( ph -> 9 e. NN0 )
216 73 215 reexpcld 
 |-  ( ph -> ( 2 ^ 9 ) e. RR )
217 216 33 resubcld 
 |-  ( ph -> ( ( 2 ^ 9 ) - 1 ) e. RR )
218 elnnz 
 |-  ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN <-> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. ZZ /\ 0 < ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
219 143 147 218 sylanbrc 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN )
220 219 orcd 
 |-  ( ph -> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN \/ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) = 0 ) )
221 elnn0 
 |-  ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN0 <-> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN \/ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) = 0 ) )
222 221 a1i 
 |-  ( ph -> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN0 <-> ( ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN \/ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) = 0 ) ) )
223 220 222 mpbird 
 |-  ( ph -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) e. NN0 )
224 73 223 reexpcld 
 |-  ( ph -> ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) e. RR )
225 8cn 
 |-  8 e. CC
226 2cn 
 |-  2 e. CC
227 8t2e16 
 |-  ( 8 x. 2 ) = ; 1 6
228 225 226 227 mulcomli 
 |-  ( 2 x. 8 ) = ; 1 6
229 228 a1i 
 |-  ( ph -> ( 2 x. 8 ) = ; 1 6 )
230 229 oveq2d 
 |-  ( ph -> ( ; 2 7 x. ( 2 x. 8 ) ) = ( ; 2 7 x. ; 1 6 ) )
231 6nn0 
 |-  6 e. NN0
232 93 231 deccl 
 |-  ; 1 6 e. NN0
233 2nn0 
 |-  2 e. NN0
234 7nn0 
 |-  7 e. NN0
235 eqid 
 |-  ; 2 7 = ; 2 7
236 93 93 deccl 
 |-  ; 1 1 e. NN0
237 0nn0 
 |-  0 e. NN0
238 233 dec0h 
 |-  2 = ; 0 2
239 eqid 
 |-  ; 1 1 = ; 1 1
240 232 nn0cni 
 |-  ; 1 6 e. CC
241 240 mul02i 
 |-  ( 0 x. ; 1 6 ) = 0
242 ax-1cn 
 |-  1 e. CC
243 176 242 9 addcomli 
 |-  ( 1 + 3 ) = 4
244 241 243 oveq12i 
 |-  ( ( 0 x. ; 1 6 ) + ( 1 + 3 ) ) = ( 0 + 4 )
245 4cn 
 |-  4 e. CC
246 245 addid2i 
 |-  ( 0 + 4 ) = 4
247 244 246 eqtri 
 |-  ( ( 0 x. ; 1 6 ) + ( 1 + 3 ) ) = 4
248 93 dec0h 
 |-  1 = ; 0 1
249 2t1e2 
 |-  ( 2 x. 1 ) = 2
250 0p1e1 
 |-  ( 0 + 1 ) = 1
251 249 250 oveq12i 
 |-  ( ( 2 x. 1 ) + ( 0 + 1 ) ) = ( 2 + 1 )
252 2p1e3 
 |-  ( 2 + 1 ) = 3
253 251 252 eqtri 
 |-  ( ( 2 x. 1 ) + ( 0 + 1 ) ) = 3
254 6cn 
 |-  6 e. CC
255 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
256 254 226 255 mulcomli 
 |-  ( 2 x. 6 ) = ; 1 2
257 93 233 252 256 decsuc 
 |-  ( ( 2 x. 6 ) + 1 ) = ; 1 3
258 93 231 237 93 122 248 233 205 93 253 257 decma2c 
 |-  ( ( 2 x. ; 1 6 ) + 1 ) = ; 3 3
259 237 233 93 93 238 239 232 205 205 247 258 decmac 
 |-  ( ( 2 x. ; 1 6 ) + ; 1 1 ) = ; 4 3
260 4nn0 
 |-  4 e. NN0
261 7cn 
 |-  7 e. CC
262 261 mulid1i 
 |-  ( 7 x. 1 ) = 7
263 262 oveq1i 
 |-  ( ( 7 x. 1 ) + 4 ) = ( 7 + 4 )
264 7p4e11 
 |-  ( 7 + 4 ) = ; 1 1
265 263 264 eqtri 
 |-  ( ( 7 x. 1 ) + 4 ) = ; 1 1
266 7t6e42 
 |-  ( 7 x. 6 ) = ; 4 2
267 234 93 231 122 233 260 265 266 decmul2c 
 |-  ( 7 x. ; 1 6 ) = ; ; 1 1 2
268 232 233 234 235 233 236 259 267 decmul1c 
 |-  ( ; 2 7 x. ; 1 6 ) = ; ; 4 3 2
269 268 a1i 
 |-  ( ph -> ( ; 2 7 x. ; 1 6 ) = ; ; 4 3 2 )
270 230 269 eqtrd 
 |-  ( ph -> ( ; 2 7 x. ( 2 x. 8 ) ) = ; ; 4 3 2 )
271 260 205 deccl 
 |-  ; 4 3 e. NN0
272 59 93 deccl 
 |-  ; 5 1 e. NN0
273 2lt10 
 |-  2 < ; 1 0
274 3lt10 
 |-  3 < ; 1 0
275 4lt5 
 |-  4 < 5
276 260 59 205 93 274 275 decltc 
 |-  ; 4 3 < ; 5 1
277 271 272 233 93 273 276 decltc 
 |-  ; ; 4 3 2 < ; ; 5 1 1
278 277 a1i 
 |-  ( ph -> ; ; 4 3 2 < ; ; 5 1 1 )
279 270 278 eqbrtrd 
 |-  ( ph -> ( ; 2 7 x. ( 2 x. 8 ) ) < ; ; 5 1 1 )
280 3exp3 
 |-  ( 3 ^ 3 ) = ; 2 7
281 280 a1i 
 |-  ( ph -> ( 3 ^ 3 ) = ; 2 7 )
282 281 eqcomd 
 |-  ( ph -> ; 2 7 = ( 3 ^ 3 ) )
283 191 exp1d 
 |-  ( ph -> ( 3 ^ 1 ) = 3 )
284 283 oveq1d 
 |-  ( ph -> ( ( 3 ^ 1 ) - 1 ) = ( 3 - 1 ) )
285 3m1e2 
 |-  ( 3 - 1 ) = 2
286 285 a1i 
 |-  ( ph -> ( 3 - 1 ) = 2 )
287 284 286 eqtr2d 
 |-  ( ph -> 2 = ( ( 3 ^ 1 ) - 1 ) )
288 sq3 
 |-  ( 3 ^ 2 ) = 9
289 288 a1i 
 |-  ( ph -> ( 3 ^ 2 ) = 9 )
290 289 oveq1d 
 |-  ( ph -> ( ( 3 ^ 2 ) - 1 ) = ( 9 - 1 ) )
291 9m1e8 
 |-  ( 9 - 1 ) = 8
292 291 a1i 
 |-  ( ph -> ( 9 - 1 ) = 8 )
293 290 292 eqtr2d 
 |-  ( ph -> 8 = ( ( 3 ^ 2 ) - 1 ) )
294 287 293 oveq12d 
 |-  ( ph -> ( 2 x. 8 ) = ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) )
295 282 294 oveq12d 
 |-  ( ph -> ( ; 2 7 x. ( 2 x. 8 ) ) = ( ( 3 ^ 3 ) x. ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) ) )
296 df-9 
 |-  9 = ( 8 + 1 )
297 296 a1i 
 |-  ( ph -> 9 = ( 8 + 1 ) )
298 297 oveq2d 
 |-  ( ph -> ( 2 ^ 9 ) = ( 2 ^ ( 8 + 1 ) ) )
299 287 194 eqeltrd 
 |-  ( ph -> 2 e. CC )
300 8nn0 
 |-  8 e. NN0
301 300 a1i 
 |-  ( ph -> 8 e. NN0 )
302 299 192 301 expaddd 
 |-  ( ph -> ( 2 ^ ( 8 + 1 ) ) = ( ( 2 ^ 8 ) x. ( 2 ^ 1 ) ) )
303 298 302 eqtrd 
 |-  ( ph -> ( 2 ^ 9 ) = ( ( 2 ^ 8 ) x. ( 2 ^ 1 ) ) )
304 2exp8 
 |-  ( 2 ^ 8 ) = ; ; 2 5 6
305 304 a1i 
 |-  ( ph -> ( 2 ^ 8 ) = ; ; 2 5 6 )
306 305 oveq1d 
 |-  ( ph -> ( ( 2 ^ 8 ) x. ( 2 ^ 1 ) ) = ( ; ; 2 5 6 x. ( 2 ^ 1 ) ) )
307 299 exp1d 
 |-  ( ph -> ( 2 ^ 1 ) = 2 )
308 307 oveq2d 
 |-  ( ph -> ( ; ; 2 5 6 x. ( 2 ^ 1 ) ) = ( ; ; 2 5 6 x. 2 ) )
309 306 308 eqtrd 
 |-  ( ph -> ( ( 2 ^ 8 ) x. ( 2 ^ 1 ) ) = ( ; ; 2 5 6 x. 2 ) )
310 233 59 deccl 
 |-  ; 2 5 e. NN0
311 eqid 
 |-  ; ; 2 5 6 = ; ; 2 5 6
312 eqid 
 |-  ; 2 5 = ; 2 5
313 2t2e4 
 |-  ( 2 x. 2 ) = 4
314 313 250 oveq12i 
 |-  ( ( 2 x. 2 ) + ( 0 + 1 ) ) = ( 4 + 1 )
315 4p1e5 
 |-  ( 4 + 1 ) = 5
316 314 315 eqtri 
 |-  ( ( 2 x. 2 ) + ( 0 + 1 ) ) = 5
317 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
318 93 237 250 317 decsuc 
 |-  ( ( 5 x. 2 ) + 1 ) = ; 1 1
319 233 59 237 93 312 248 233 93 93 316 318 decmac 
 |-  ( ( ; 2 5 x. 2 ) + 1 ) = ; 5 1
320 233 310 231 311 233 93 319 255 decmul1c 
 |-  ( ; ; 2 5 6 x. 2 ) = ; ; 5 1 2
321 320 a1i 
 |-  ( ph -> ( ; ; 2 5 6 x. 2 ) = ; ; 5 1 2 )
322 309 321 eqtrd 
 |-  ( ph -> ( ( 2 ^ 8 ) x. ( 2 ^ 1 ) ) = ; ; 5 1 2 )
323 303 322 eqtrd 
 |-  ( ph -> ( 2 ^ 9 ) = ; ; 5 1 2 )
324 323 oveq1d 
 |-  ( ph -> ( ( 2 ^ 9 ) - 1 ) = ( ; ; 5 1 2 - 1 ) )
325 1p1e2 
 |-  ( 1 + 1 ) = 2
326 eqid 
 |-  ; ; 5 1 1 = ; ; 5 1 1
327 272 93 325 326 decsuc 
 |-  ( ; ; 5 1 1 + 1 ) = ; ; 5 1 2
328 272 233 deccl 
 |-  ; ; 5 1 2 e. NN0
329 328 nn0cni 
 |-  ; ; 5 1 2 e. CC
330 272 93 deccl 
 |-  ; ; 5 1 1 e. NN0
331 330 nn0cni 
 |-  ; ; 5 1 1 e. CC
332 329 242 331 subadd2i 
 |-  ( ( ; ; 5 1 2 - 1 ) = ; ; 5 1 1 <-> ( ; ; 5 1 1 + 1 ) = ; ; 5 1 2 )
333 327 332 mpbir 
 |-  ( ; ; 5 1 2 - 1 ) = ; ; 5 1 1
334 333 a1i 
 |-  ( ph -> ( ; ; 5 1 2 - 1 ) = ; ; 5 1 1 )
335 324 334 eqtr2d 
 |-  ( ph -> ; ; 5 1 1 = ( ( 2 ^ 9 ) - 1 ) )
336 279 295 335 3brtr3d 
 |-  ( ph -> ( ( 3 ^ 3 ) x. ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) ) < ( ( 2 ^ 9 ) - 1 ) )
337 216 ltm1d 
 |-  ( ph -> ( ( 2 ^ 9 ) - 1 ) < ( 2 ^ 9 ) )
338 215 nn0zd 
 |-  ( ph -> 9 e. ZZ )
339 73 338 143 35 leexp2d 
 |-  ( ph -> ( 9 <_ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) <-> ( 2 ^ 9 ) <_ ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) )
340 87 339 mpbid 
 |-  ( ph -> ( 2 ^ 9 ) <_ ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
341 217 216 224 337 340 ltletrd 
 |-  ( ph -> ( ( 2 ^ 9 ) - 1 ) < ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
342 213 217 224 336 341 lttrd 
 |-  ( ph -> ( ( 3 ^ 3 ) x. ( ( ( 3 ^ 1 ) - 1 ) x. ( ( 3 ^ 2 ) - 1 ) ) ) < ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
343 204 342 eqbrtrd 
 |-  ( ph -> ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) ) < ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
344 343 adantr 
 |-  ( ( ph /\ 3 = N ) -> ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( 3 ^ k ) - 1 ) ) < ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
345 30 344 eqbrtrd 
 |-  ( ( ph /\ 3 = N ) -> ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) < ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) )
346 simpr 
 |-  ( ( ph /\ 3 = N ) -> 3 = N )
347 oveq2 
 |-  ( 3 = N -> ( 2 logb 3 ) = ( 2 logb N ) )
348 347 adantl 
 |-  ( ( ph /\ 3 = N ) -> ( 2 logb 3 ) = ( 2 logb N ) )
349 348 oveq1d 
 |-  ( ( ph /\ 3 = N ) -> ( ( 2 logb 3 ) ^ 5 ) = ( ( 2 logb N ) ^ 5 ) )
350 349 fveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
351 3 a1i 
 |-  ( ( ph /\ 3 = N ) -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
352 351 eqcomd 
 |-  ( ( ph /\ 3 = N ) -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) = B )
353 350 352 eqtrd 
 |-  ( ( ph /\ 3 = N ) -> ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) = B )
354 353 oveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) = ( 2 logb B ) )
355 354 fveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) = ( |_ ` ( 2 logb B ) ) )
356 346 355 oveq12d 
 |-  ( ( ph /\ 3 = N ) -> ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) = ( N ^ ( |_ ` ( 2 logb B ) ) ) )
357 346 oveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( 2 logb 3 ) = ( 2 logb N ) )
358 357 oveq1d 
 |-  ( ( ph /\ 3 = N ) -> ( ( 2 logb 3 ) ^ 2 ) = ( ( 2 logb N ) ^ 2 ) )
359 358 fveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) = ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
360 359 oveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) = ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
361 360 prodeq1d 
 |-  ( ( ph /\ 3 = N ) -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) = prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
362 356 361 oveq12d 
 |-  ( ( ph /\ 3 = N ) -> ( ( 3 ^ ( |_ ` ( 2 logb ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb 3 ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
363 350 oveq2d 
 |-  ( ( ph /\ 3 = N ) -> ( 2 ^ ( |^ ` ( ( 2 logb 3 ) ^ 5 ) ) ) = ( 2 ^ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
364 345 362 363 3brtr3d 
 |-  ( ( ph /\ 3 = N ) -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) < ( 2 ^ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
365 2 a1i 
 |-  ( ( ph /\ 3 = N ) -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
366 365 eqcomd 
 |-  ( ( ph /\ 3 = N ) -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) = A )
367 3 oveq2i 
 |-  ( 2 ^ B ) = ( 2 ^ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
368 367 a1i 
 |-  ( ( ph /\ 3 = N ) -> ( 2 ^ B ) = ( 2 ^ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
369 368 eqcomd 
 |-  ( ( ph /\ 3 = N ) -> ( 2 ^ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) = ( 2 ^ B ) )
370 364 366 369 3brtr3d 
 |-  ( ( ph /\ 3 = N ) -> A < ( 2 ^ B ) )
371 370 ex 
 |-  ( ph -> ( 3 = N -> A < ( 2 ^ B ) ) )
372 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
373 1 372 syl 
 |-  ( ph -> 3 <_ N )
374 14 zred 
 |-  ( ph -> N e. RR )
375 55 374 leloed 
 |-  ( ph -> ( 3 <_ N <-> ( 3 < N \/ 3 = N ) ) )
376 373 375 mpbid 
 |-  ( ph -> ( 3 < N \/ 3 = N ) )
377 23 371 376 mpjaod 
 |-  ( ph -> A < ( 2 ^ B ) )