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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p1.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p1.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
Assertion aks4d1p1 ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )

Proof

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