Step |
Hyp |
Ref |
Expression |
1 |
|
aks4d1p1p2.1 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
2 |
|
aks4d1p1p2.2 |
⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) |
3 |
|
aks4d1p1p2.3 |
⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) |
4 |
|
aks4d1p1p2.4 |
⊢ ( 𝜑 → 3 ≤ 𝑁 ) |
5 |
1
|
nnred |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
6 |
|
2re |
⊢ 2 ∈ ℝ |
7 |
6
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ ) |
8 |
|
2pos |
⊢ 0 < 2 |
9 |
8
|
a1i |
⊢ ( 𝜑 → 0 < 2 ) |
10 |
1
|
nngt0d |
⊢ ( 𝜑 → 0 < 𝑁 ) |
11 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
12 |
|
1lt2 |
⊢ 1 < 2 |
13 |
12
|
a1i |
⊢ ( 𝜑 → 1 < 2 ) |
14 |
11 13
|
ltned |
⊢ ( 𝜑 → 1 ≠ 2 ) |
15 |
14
|
necomd |
⊢ ( 𝜑 → 2 ≠ 1 ) |
16 |
7 9 5 10 15
|
relogbcld |
⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ ) |
17 |
|
5nn0 |
⊢ 5 ∈ ℕ0 |
18 |
17
|
a1i |
⊢ ( 𝜑 → 5 ∈ ℕ0 ) |
19 |
16 18
|
reexpcld |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ ) |
20 |
|
ceilcl |
⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ ) |
21 |
19 20
|
syl |
⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ ) |
22 |
21
|
zred |
⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ ) |
23 |
3
|
a1i |
⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) |
24 |
23
|
eleq1d |
⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ ) ) |
25 |
22 24
|
mpbird |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
26 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
27 |
18
|
nn0zd |
⊢ ( 𝜑 → 5 ∈ ℤ ) |
28 |
|
3re |
⊢ 3 ∈ ℝ |
29 |
28
|
a1i |
⊢ ( 𝜑 → 3 ∈ ℝ ) |
30 |
|
1lt3 |
⊢ 1 < 3 |
31 |
30
|
a1i |
⊢ ( 𝜑 → 1 < 3 ) |
32 |
11 29 5 31 4
|
ltletrd |
⊢ ( 𝜑 → 1 < 𝑁 ) |
33 |
5 10
|
elrpd |
⊢ ( 𝜑 → 𝑁 ∈ ℝ+ ) |
34 |
|
2rp |
⊢ 2 ∈ ℝ+ |
35 |
34 12
|
pm3.2i |
⊢ ( 2 ∈ ℝ+ ∧ 1 < 2 ) |
36 |
35
|
a1i |
⊢ ( 𝜑 → ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) |
37 |
|
logbgt0b |
⊢ ( ( 𝑁 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) → ( 0 < ( 2 logb 𝑁 ) ↔ 1 < 𝑁 ) ) |
38 |
33 36 37
|
syl2anc |
⊢ ( 𝜑 → ( 0 < ( 2 logb 𝑁 ) ↔ 1 < 𝑁 ) ) |
39 |
32 38
|
mpbird |
⊢ ( 𝜑 → 0 < ( 2 logb 𝑁 ) ) |
40 |
|
expgt0 |
⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 𝑁 ) ) → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) ) |
41 |
16 27 39 40
|
syl3anc |
⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) ) |
42 |
|
ceilge |
⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) |
43 |
19 42
|
syl |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) |
44 |
26 19 22 41 43
|
ltletrd |
⊢ ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) |
45 |
23
|
breq2d |
⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) ) |
46 |
44 45
|
mpbird |
⊢ ( 𝜑 → 0 < 𝐵 ) |
47 |
7 9 25 46 15
|
relogbcld |
⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ ) |
48 |
47
|
flcld |
⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ) |
49 |
|
7re |
⊢ 7 ∈ ℝ |
50 |
49
|
a1i |
⊢ ( 𝜑 → 7 ∈ ℝ ) |
51 |
|
1lt7 |
⊢ 1 < 7 |
52 |
51
|
a1i |
⊢ ( 𝜑 → 1 < 7 ) |
53 |
5 4
|
3lexlogpow5ineq3 |
⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) ) |
54 |
11 50 19 52 53
|
lttrd |
⊢ ( 𝜑 → 1 < ( ( 2 logb 𝑁 ) ↑ 5 ) ) |
55 |
11 19 22 54 43
|
ltletrd |
⊢ ( 𝜑 → 1 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) |
56 |
23
|
breq2d |
⊢ ( 𝜑 → ( 1 < 𝐵 ↔ 1 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) ) |
57 |
55 56
|
mpbird |
⊢ ( 𝜑 → 1 < 𝐵 ) |
58 |
25 46
|
elrpd |
⊢ ( 𝜑 → 𝐵 ∈ ℝ+ ) |
59 |
|
logbgt0b |
⊢ ( ( 𝐵 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) → ( 0 < ( 2 logb 𝐵 ) ↔ 1 < 𝐵 ) ) |
60 |
58 36 59
|
syl2anc |
⊢ ( 𝜑 → ( 0 < ( 2 logb 𝐵 ) ↔ 1 < 𝐵 ) ) |
61 |
57 60
|
mpbird |
⊢ ( 𝜑 → 0 < ( 2 logb 𝐵 ) ) |
62 |
26 47 61
|
ltled |
⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) ) |
63 |
|
0zd |
⊢ ( 𝜑 → 0 ∈ ℤ ) |
64 |
|
flge |
⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
65 |
47 63 64
|
syl2anc |
⊢ ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
66 |
62 65
|
mpbid |
⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) |
67 |
48 66
|
jca |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
68 |
|
elnn0z |
⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
69 |
67 68
|
sylibr |
⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ) |
70 |
5 69
|
reexpcld |
⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ ) |
71 |
|
fzfid |
⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin ) |
72 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℝ ) |
73 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ ) |
74 |
73
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ ) |
75 |
|
nnnn0 |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 ) |
76 |
74 75
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 ) |
77 |
72 76
|
reexpcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℝ ) |
78 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℝ ) |
79 |
77 78
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℝ ) |
80 |
71 79
|
fprodrecl |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℝ ) |
81 |
70 80
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℝ ) |
82 |
2
|
a1i |
⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ) |
83 |
82
|
eleq1d |
⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℝ ) ) |
84 |
81 83
|
mpbird |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
85 |
1
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
86 |
85
|
nn0ge0d |
⊢ ( 𝜑 → 0 ≤ 𝑁 ) |
87 |
19 11
|
readdcld |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ∈ ℝ ) |
88 |
19
|
ltp1d |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) |
89 |
26 19 87 41 88
|
lttrd |
⊢ ( 𝜑 → 0 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) |
90 |
7 9 87 89 15
|
relogbcld |
⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℝ ) |
91 |
16
|
resqcld |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ) |
92 |
91
|
flcld |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ) |
93 |
92
|
zred |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ ) |
94 |
|
0lt1 |
⊢ 0 < 1 |
95 |
94
|
a1i |
⊢ ( 𝜑 → 0 < 1 ) |
96 |
7 9 7 9 15
|
relogbcld |
⊢ ( 𝜑 → ( 2 logb 2 ) ∈ ℝ ) |
97 |
96
|
resqcld |
⊢ ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ∈ ℝ ) |
98 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
99 |
98
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℕ0 ) |
100 |
11
|
leidd |
⊢ ( 𝜑 → 1 ≤ 1 ) |
101 |
7
|
recnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
102 |
26 9
|
gtned |
⊢ ( 𝜑 → 2 ≠ 0 ) |
103 |
|
logbid1 |
⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 ) |
104 |
101 102 15 103
|
syl3anc |
⊢ ( 𝜑 → ( 2 logb 2 ) = 1 ) |
105 |
104
|
eqcomd |
⊢ ( 𝜑 → 1 = ( 2 logb 2 ) ) |
106 |
100 105
|
breqtrd |
⊢ ( 𝜑 → 1 ≤ ( 2 logb 2 ) ) |
107 |
96 99 106
|
expge1d |
⊢ ( 𝜑 → 1 ≤ ( ( 2 logb 2 ) ↑ 2 ) ) |
108 |
105
|
eqcomd |
⊢ ( 𝜑 → ( 2 logb 2 ) = 1 ) |
109 |
108
|
oveq1d |
⊢ ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) = ( 1 ↑ 2 ) ) |
110 |
99
|
nn0zd |
⊢ ( 𝜑 → 2 ∈ ℤ ) |
111 |
|
1exp |
⊢ ( 2 ∈ ℤ → ( 1 ↑ 2 ) = 1 ) |
112 |
110 111
|
syl |
⊢ ( 𝜑 → ( 1 ↑ 2 ) = 1 ) |
113 |
109 112
|
eqtrd |
⊢ ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) = 1 ) |
114 |
7
|
leidd |
⊢ ( 𝜑 → 2 ≤ 2 ) |
115 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
116 |
6 115
|
nn0addge1i |
⊢ 2 ≤ ( 2 + 1 ) |
117 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
118 |
116 117
|
breqtri |
⊢ 2 ≤ 3 |
119 |
118
|
a1i |
⊢ ( 𝜑 → 2 ≤ 3 ) |
120 |
7 29 5 119 4
|
letrd |
⊢ ( 𝜑 → 2 ≤ 𝑁 ) |
121 |
110 114 7 9 5 10 120
|
logblebd |
⊢ ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝑁 ) ) |
122 |
11 96 16 106 121
|
letrd |
⊢ ( 𝜑 → 1 ≤ ( 2 logb 𝑁 ) ) |
123 |
16 99 122
|
expge1d |
⊢ ( 𝜑 → 1 ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) |
124 |
113 123
|
eqbrtrd |
⊢ ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) |
125 |
|
1z |
⊢ 1 ∈ ℤ |
126 |
|
zsqcl |
⊢ ( 1 ∈ ℤ → ( 1 ↑ 2 ) ∈ ℤ ) |
127 |
125 126
|
ax-mp |
⊢ ( 1 ↑ 2 ) ∈ ℤ |
128 |
127
|
a1i |
⊢ ( 𝜑 → ( 1 ↑ 2 ) ∈ ℤ ) |
129 |
109
|
eleq1d |
⊢ ( 𝜑 → ( ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ↔ ( 1 ↑ 2 ) ∈ ℤ ) ) |
130 |
128 129
|
mpbird |
⊢ ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ) |
131 |
91 130
|
jca |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ∧ ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ) ) |
132 |
|
flge |
⊢ ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ∧ ( ( 2 logb 2 ) ↑ 2 ) ∈ ℤ ) → ( ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ↔ ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) |
133 |
131 132
|
syl |
⊢ ( 𝜑 → ( ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ↔ ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) |
134 |
124 133
|
mpbid |
⊢ ( 𝜑 → ( ( 2 logb 2 ) ↑ 2 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) |
135 |
11 97 93 107 134
|
letrd |
⊢ ( 𝜑 → 1 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) |
136 |
26 11 93 95 135
|
ltletrd |
⊢ ( 𝜑 → 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) |
137 |
92 136
|
jca |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) |
138 |
|
elnnz |
⊢ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) |
139 |
138
|
bicomi |
⊢ ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↔ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ ) |
140 |
139
|
a1i |
⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↔ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ ) ) |
141 |
137 140
|
mpbid |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ ) |
142 |
141
|
nnnn0d |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ0 ) |
143 |
|
arisum |
⊢ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℕ0 → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) |
144 |
142 143
|
syl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) |
145 |
74
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℝ ) |
146 |
71 145
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ∈ ℝ ) |
147 |
144 146
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ∈ ℝ ) |
148 |
90 147
|
readdcld |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ∈ ℝ ) |
149 |
5 86 148
|
recxpcld |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ∈ ℝ ) |
150 |
|
4nn0 |
⊢ 4 ∈ ℕ0 |
151 |
150
|
a1i |
⊢ ( 𝜑 → 4 ∈ ℕ0 ) |
152 |
16 151
|
reexpcld |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℝ ) |
153 |
152 91
|
readdcld |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ ) |
154 |
153
|
rehalfcld |
⊢ ( 𝜑 → ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ∈ ℝ ) |
155 |
90 154
|
readdcld |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ∈ ℝ ) |
156 |
5 86 155
|
recxpcld |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) ∈ ℝ ) |
157 |
|
reflcl |
⊢ ( ( 2 logb 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ ) |
158 |
47 157
|
syl |
⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ ) |
159 |
5 86 158
|
recxpcld |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ ) |
160 |
33 146
|
rpcxpcld |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ∈ ℝ+ ) |
161 |
33 141
|
aks4d1p1p1 |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) = ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) |
162 |
161
|
eleq1d |
⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ∈ ℝ+ ↔ ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ∈ ℝ+ ) ) |
163 |
160 162
|
mpbird |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ∈ ℝ+ ) |
164 |
163
|
rpregt0d |
⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ∈ ℝ ∧ 0 < ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
165 |
164
|
simpld |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ∈ ℝ ) |
166 |
159 165
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ∈ ℝ ) |
167 |
5 86 90
|
recxpcld |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ ) |
168 |
167 165
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ∈ ℝ ) |
169 |
71 77
|
fprodrecl |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ∈ ℝ ) |
170 |
5 69 86
|
expge0d |
⊢ ( 𝜑 → 0 ≤ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
171 |
|
nfv |
⊢ Ⅎ 𝑘 𝜑 |
172 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 ∈ ℝ ) |
173 |
1
|
nnge1d |
⊢ ( 𝜑 → 1 ≤ 𝑁 ) |
174 |
173
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ 𝑁 ) |
175 |
72 76 174
|
expge1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ ( 𝑁 ↑ 𝑘 ) ) |
176 |
77
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℂ ) |
177 |
176
|
subid1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 0 ) = ( 𝑁 ↑ 𝑘 ) ) |
178 |
177
|
breq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 1 ≤ ( ( 𝑁 ↑ 𝑘 ) − 0 ) ↔ 1 ≤ ( 𝑁 ↑ 𝑘 ) ) ) |
179 |
175 178
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ ( ( 𝑁 ↑ 𝑘 ) − 0 ) ) |
180 |
78 77 172 179
|
lesubd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 ≤ ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) |
181 |
77
|
lem1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ≤ ( 𝑁 ↑ 𝑘 ) ) |
182 |
171 71 79 180 77 181
|
fprodle |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ≤ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ) |
183 |
80 169 70 170 182
|
lemul2ad |
⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ) ) |
184 |
82
|
breq1d |
⊢ ( 𝜑 → ( 𝐴 ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ) ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ) ) ) |
185 |
183 184
|
mpbird |
⊢ ( 𝜑 → 𝐴 ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ) ) |
186 |
72
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℂ ) |
187 |
|
cxpexp |
⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ↑𝑐 𝑘 ) = ( 𝑁 ↑ 𝑘 ) ) |
188 |
186 76 187
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑𝑐 𝑘 ) = ( 𝑁 ↑ 𝑘 ) ) |
189 |
188
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) = ( 𝑁 ↑𝑐 𝑘 ) ) |
190 |
189
|
prodeq2dv |
⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) |
191 |
190
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑ 𝑘 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
192 |
185 191
|
breqtrd |
⊢ ( 𝜑 → 𝐴 ≤ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
193 |
5
|
recnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
194 |
|
cxpexp |
⊢ ( ( 𝑁 ∈ ℂ ∧ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ) → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) = ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
195 |
193 69 194
|
syl2anc |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) = ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) |
196 |
195
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
197 |
196
|
eqcomd |
⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) = ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
198 |
192 197
|
breqtrd |
⊢ ( 𝜑 → 𝐴 ≤ ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
199 |
159 167 164
|
3jca |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ ∧ ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ ∧ ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ∈ ℝ ∧ 0 < ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) ) |
200 |
1 3 4
|
aks4d1p1p3 |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ) |
201 |
|
ltmul1a |
⊢ ( ( ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℝ ∧ ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ ∧ ( ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ∈ ℝ ∧ 0 < ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) ∧ ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ) → ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) < ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
202 |
199 200 201
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) < ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
203 |
84 166 168 198 202
|
lelttrd |
⊢ ( 𝜑 → 𝐴 < ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) ) |
204 |
161
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( 𝑁 ↑𝑐 𝑘 ) ) = ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) ) |
205 |
203 204
|
breqtrd |
⊢ ( 𝜑 → 𝐴 < ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) ) |
206 |
144
|
oveq2d |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) = ( 𝑁 ↑𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) |
207 |
206
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) 𝑘 ) ) = ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ) |
208 |
205 207
|
breqtrd |
⊢ ( 𝜑 → 𝐴 < ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ) |
209 |
26 10
|
gtned |
⊢ ( 𝜑 → 𝑁 ≠ 0 ) |
210 |
90
|
recnd |
⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℂ ) |
211 |
141
|
nncnd |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℂ ) |
212 |
211
|
sqcld |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ∈ ℂ ) |
213 |
212 211
|
addcld |
⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ ℂ ) |
214 |
213
|
halfcld |
⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ∈ ℂ ) |
215 |
193 209 210 214
|
cxpaddd |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) = ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ) |
216 |
215
|
eqcomd |
⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) · ( 𝑁 ↑𝑐 ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) = ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ) |
217 |
208 216
|
breqtrd |
⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ) |
218 |
|
reflcl |
⊢ ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ ) |
219 |
91 218
|
syl |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℝ ) |
220 |
219
|
resqcld |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ∈ ℝ ) |
221 |
220 219
|
readdcld |
⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ ℝ ) |
222 |
34
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ+ ) |
223 |
91 99
|
reexpcld |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ∈ ℝ ) |
224 |
|
id |
⊢ ( 𝜑 → 𝜑 ) |
225 |
142
|
nn0ge0d |
⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) |
226 |
|
flle |
⊢ ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) |
227 |
91 226
|
syl |
⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) |
228 |
219 91 99 225 227
|
leexp1ad |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ) |
229 |
224 228
|
syl |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ) |
230 |
16
|
recnd |
⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℂ ) |
231 |
230 99 99
|
expmuld |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) = ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ) |
232 |
231
|
eqcomd |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) = ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) ) |
233 |
|
2t2e4 |
⊢ ( 2 · 2 ) = 4 |
234 |
233
|
oveq2i |
⊢ ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) = ( ( 2 logb 𝑁 ) ↑ 4 ) |
235 |
234
|
a1i |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ ( 2 · 2 ) ) = ( ( 2 logb 𝑁 ) ↑ 4 ) ) |
236 |
232 235
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) = ( ( 2 logb 𝑁 ) ↑ 4 ) ) |
237 |
223 236
|
eqled |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 4 ) ) |
238 |
220 223 152 229 237
|
letrd |
⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 4 ) ) |
239 |
220 219 152 91 238 227
|
le2addd |
⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ≤ ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) |
240 |
221 153 222 239
|
lediv1dd |
⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ≤ ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) |
241 |
147 154 90 240
|
leadd2dd |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ≤ ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) |
242 |
5 32 148 155
|
cxpled |
⊢ ( 𝜑 → ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ≤ ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ↔ ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ≤ ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) ) ) |
243 |
241 242
|
mpbid |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ↑ 2 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) / 2 ) ) ) ≤ ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) ) |
244 |
84 149 156 217 243
|
ltletrd |
⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) ) |
245 |
152
|
recnd |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 4 ) ∈ ℂ ) |
246 |
91
|
recnd |
⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℂ ) |
247 |
245 246 101 102
|
divdird |
⊢ ( 𝜑 → ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) = ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) |
248 |
247
|
oveq2d |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) = ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) |
249 |
248
|
oveq2d |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) + ( ( 2 logb 𝑁 ) ↑ 2 ) ) / 2 ) ) ) = ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) ) |
250 |
244 249
|
breqtrd |
⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) ) |
251 |
245 101 102
|
divcld |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ∈ ℂ ) |
252 |
246 101 102
|
divcld |
⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ∈ ℂ ) |
253 |
251 252
|
addcomd |
⊢ ( 𝜑 → ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) = ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) |
254 |
253
|
oveq2d |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) = ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) ) |
255 |
210 252 251
|
addassd |
⊢ ( 𝜑 → ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) = ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) ) |
256 |
255
|
eqcomd |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) = ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) |
257 |
254 256
|
eqtrd |
⊢ ( 𝜑 → ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) = ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) |
258 |
257
|
oveq2d |
⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) ) ) = ( 𝑁 ↑𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) ) |
259 |
250 258
|
breqtrd |
⊢ ( 𝜑 → 𝐴 < ( 𝑁 ↑𝑐 ( ( ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 2 ) / 2 ) ) + ( ( ( 2 logb 𝑁 ) ↑ 4 ) / 2 ) ) ) ) |