Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks4d1p1p2 Structured version   Visualization version   GIF version

Theorem aks4d1p1p2 39719
Description: Rewrite 𝐴 in more suitable form. (Contributed by metakunt, 19-Aug-2024.)
Hypotheses
Ref Expression
aks4d1p1p2.1 (𝜑𝑁 ∈ ℕ)
aks4d1p1p2.2 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
aks4d1p1p2.3 𝐵 = (⌈‘((2 logb 𝑁)↑5))
aks4d1p1p2.4 (𝜑 → 3 ≤ 𝑁)
Assertion
Ref Expression
aks4d1p1p2 (𝜑𝐴 < (𝑁𝑐(((2 logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2))))
Distinct variable groups:   𝑘,𝑁   𝜑,𝑘
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Proof of Theorem aks4d1p1p2
StepHypRef Expression
1 aks4d1p1p2.1 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
21nnred 11733 . . . . . . 7 (𝜑𝑁 ∈ ℝ)
3 2re 11792 . . . . . . . . . . . 12 2 ∈ ℝ
43a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
5 2pos 11821 . . . . . . . . . . . 12 0 < 2
65a1i 11 . . . . . . . . . . 11 (𝜑 → 0 < 2)
71nngt0d 11767 . . . . . . . . . . . . . . . 16 (𝜑 → 0 < 𝑁)
8 1red 10722 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
9 1lt2 11889 . . . . . . . . . . . . . . . . . . 19 1 < 2
109a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 < 2)
118, 10ltned 10856 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ≠ 2)
1211necomd 2989 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 1)
134, 6, 2, 7, 12relogbcld 39622 . . . . . . . . . . . . . . 15 (𝜑 → (2 logb 𝑁) ∈ ℝ)
14 5nn0 11998 . . . . . . . . . . . . . . . 16 5 ∈ ℕ0
1514a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 5 ∈ ℕ0)
1613, 15reexpcld 13621 . . . . . . . . . . . . . 14 (𝜑 → ((2 logb 𝑁)↑5) ∈ ℝ)
17 ceilcl 13305 . . . . . . . . . . . . . 14 (((2 logb 𝑁)↑5) ∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ)
1918zred 12170 . . . . . . . . . . . 12 (𝜑 → (⌈‘((2 logb 𝑁)↑5)) ∈ ℝ)
20 aks4d1p1p2.3 . . . . . . . . . . . . . 14 𝐵 = (⌈‘((2 logb 𝑁)↑5))
2120a1i 11 . . . . . . . . . . . . 13 (𝜑𝐵 = (⌈‘((2 logb 𝑁)↑5)))
2221eleq1d 2817 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∈ ℝ ↔ (⌈‘((2 logb 𝑁)↑5)) ∈ ℝ))
2319, 22mpbird 260 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
24 0red 10724 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
2515nn0zd 12168 . . . . . . . . . . . . . 14 (𝜑 → 5 ∈ ℤ)
26 3re 11798 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
2726a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ∈ ℝ)
28 1lt3 11891 . . . . . . . . . . . . . . . . 17 1 < 3
2928a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 1 < 3)
30 aks4d1p1p2.4 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ≤ 𝑁)
318, 27, 2, 29, 30ltletrd 10880 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 𝑁)
322, 7elrpd 12513 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ+)
33 2rp 12479 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ+
3433, 9pm3.2i 474 . . . . . . . . . . . . . . . . 17 (2 ∈ ℝ+ ∧ 1 < 2)
3534a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
36 logbgt0b 25533 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝑁) ↔ 1 < 𝑁))
3732, 35, 36syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (0 < (2 logb 𝑁) ↔ 1 < 𝑁))
3831, 37mpbird 260 . . . . . . . . . . . . . 14 (𝜑 → 0 < (2 logb 𝑁))
39 expgt0 13556 . . . . . . . . . . . . . 14 (((2 logb 𝑁) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑁)) → 0 < ((2 logb 𝑁)↑5))
4013, 25, 38, 39syl3anc 1372 . . . . . . . . . . . . 13 (𝜑 → 0 < ((2 logb 𝑁)↑5))
41 ceilge 13307 . . . . . . . . . . . . . 14 (((2 logb 𝑁)↑5) ∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2 logb 𝑁)↑5)))
4216, 41syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2 logb 𝑁)↑5) ≤ (⌈‘((2 logb 𝑁)↑5)))
4324, 16, 19, 40, 42ltletrd 10880 . . . . . . . . . . . 12 (𝜑 → 0 < (⌈‘((2 logb 𝑁)↑5)))
4421breq2d 5042 . . . . . . . . . . . 12 (𝜑 → (0 < 𝐵 ↔ 0 < (⌈‘((2 logb 𝑁)↑5))))
4543, 44mpbird 260 . . . . . . . . . . 11 (𝜑 → 0 < 𝐵)
464, 6, 23, 45, 12relogbcld 39622 . . . . . . . . . 10 (𝜑 → (2 logb 𝐵) ∈ ℝ)
4746flcld 13261 . . . . . . . . 9 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℤ)
48 7re 11811 . . . . . . . . . . . . . . . 16 7 ∈ ℝ
4948a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 7 ∈ ℝ)
50 1lt7 11909 . . . . . . . . . . . . . . . 16 1 < 7
5150a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 7)
522, 303lexlogpow5ineq3 39707 . . . . . . . . . . . . . . 15 (𝜑 → 7 < ((2 logb 𝑁)↑5))
538, 49, 16, 51, 52lttrd 10881 . . . . . . . . . . . . . 14 (𝜑 → 1 < ((2 logb 𝑁)↑5))
548, 16, 19, 53, 42ltletrd 10880 . . . . . . . . . . . . 13 (𝜑 → 1 < (⌈‘((2 logb 𝑁)↑5)))
5521breq2d 5042 . . . . . . . . . . . . 13 (𝜑 → (1 < 𝐵 ↔ 1 < (⌈‘((2 logb 𝑁)↑5))))
5654, 55mpbird 260 . . . . . . . . . . . 12 (𝜑 → 1 < 𝐵)
5723, 45elrpd 12513 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ+)
58 logbgt0b 25533 . . . . . . . . . . . . 13 ((𝐵 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐵) ↔ 1 < 𝐵))
5957, 35, 58syl2anc 587 . . . . . . . . . . . 12 (𝜑 → (0 < (2 logb 𝐵) ↔ 1 < 𝐵))
6056, 59mpbird 260 . . . . . . . . . . 11 (𝜑 → 0 < (2 logb 𝐵))
6124, 46, 60ltled 10868 . . . . . . . . . 10 (𝜑 → 0 ≤ (2 logb 𝐵))
62 0zd 12076 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℤ)
63 flge 13268 . . . . . . . . . . 11 (((2 logb 𝐵) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤ (⌊‘(2 logb 𝐵))))
6446, 62, 63syl2anc 587 . . . . . . . . . 10 (𝜑 → (0 ≤ (2 logb 𝐵) ↔ 0 ≤ (⌊‘(2 logb 𝐵))))
6561, 64mpbid 235 . . . . . . . . 9 (𝜑 → 0 ≤ (⌊‘(2 logb 𝐵)))
6647, 65jca 515 . . . . . . . 8 (𝜑 → ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵))))
67 elnn0z 12077 . . . . . . . 8 ((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔ ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵))))
6866, 67sylibr 237 . . . . . . 7 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℕ0)
692, 68reexpcld 13621 . . . . . 6 (𝜑 → (𝑁↑(⌊‘(2 logb 𝐵))) ∈ ℝ)
70 fzfid 13434 . . . . . . 7 (𝜑 → (1...(⌊‘((2 logb 𝑁)↑2))) ∈ Fin)
712adantr 484 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑁 ∈ ℝ)
72 elfznn 13029 . . . . . . . . . . 11 (𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2))) → 𝑘 ∈ ℕ)
7372adantl 485 . . . . . . . . . 10 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℕ)
74 nnnn0 11985 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
7573, 74syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0)
7671, 75reexpcld 13621 . . . . . . . 8 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑘) ∈ ℝ)
77 1red 10722 . . . . . . . 8 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ∈ ℝ)
7876, 77resubcld 11148 . . . . . . 7 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((𝑁𝑘) − 1) ∈ ℝ)
7970, 78fprodrecl 15401 . . . . . 6 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1) ∈ ℝ)
8069, 79remulcld 10751 . . . . 5 (𝜑 → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ∈ ℝ)
81 aks4d1p1p2.2 . . . . . . 7 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
8281a1i 11 . . . . . 6 (𝜑𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)))
8382eleq1d 2817 . . . . 5 (𝜑 → (𝐴 ∈ ℝ ↔ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ∈ ℝ))
8480, 83mpbird 260 . . . 4 (𝜑𝐴 ∈ ℝ)
851nnnn0d 12038 . . . . . 6 (𝜑𝑁 ∈ ℕ0)
8685nn0ge0d 12041 . . . . 5 (𝜑 → 0 ≤ 𝑁)
8716, 8readdcld 10750 . . . . . . 7 (𝜑 → (((2 logb 𝑁)↑5) + 1) ∈ ℝ)
8816ltp1d 11650 . . . . . . . 8 (𝜑 → ((2 logb 𝑁)↑5) < (((2 logb 𝑁)↑5) + 1))
8924, 16, 87, 40, 88lttrd 10881 . . . . . . 7 (𝜑 → 0 < (((2 logb 𝑁)↑5) + 1))
904, 6, 87, 89, 12relogbcld 39622 . . . . . 6 (𝜑 → (2 logb (((2 logb 𝑁)↑5) + 1)) ∈ ℝ)
9113resqcld 13705 . . . . . . . . . . . 12 (𝜑 → ((2 logb 𝑁)↑2) ∈ ℝ)
9291flcld 13261 . . . . . . . . . . 11 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ∈ ℤ)
9392zred 12170 . . . . . . . . . . . 12 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ∈ ℝ)
94 0lt1 11242 . . . . . . . . . . . . 13 0 < 1
9594a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < 1)
964, 6, 4, 6, 12relogbcld 39622 . . . . . . . . . . . . . 14 (𝜑 → (2 logb 2) ∈ ℝ)
9796resqcld 13705 . . . . . . . . . . . . 13 (𝜑 → ((2 logb 2)↑2) ∈ ℝ)
98 2nn0 11995 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
9998a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℕ0)
1008leidd 11286 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 1)
1014recnd 10749 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℂ)
10224, 6gtned 10855 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ≠ 0)
103 logbid1 25508 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) = 1)
104101, 102, 12, 103syl3anc 1372 . . . . . . . . . . . . . . . 16 (𝜑 → (2 logb 2) = 1)
105104eqcomd 2744 . . . . . . . . . . . . . . 15 (𝜑 → 1 = (2 logb 2))
106100, 105breqtrd 5056 . . . . . . . . . . . . . 14 (𝜑 → 1 ≤ (2 logb 2))
10796, 99, 106expge1d 13623 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ ((2 logb 2)↑2))
108105eqcomd 2744 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 logb 2) = 1)
109108oveq1d 7187 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 logb 2)↑2) = (1↑2))
11099nn0zd 12168 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℤ)
111 1exp 13552 . . . . . . . . . . . . . . . . 17 (2 ∈ ℤ → (1↑2) = 1)
112110, 111syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1↑2) = 1)
113109, 112eqtrd 2773 . . . . . . . . . . . . . . 15 (𝜑 → ((2 logb 2)↑2) = 1)
1144leidd 11286 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2 ≤ 2)
115 1nn0 11994 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℕ0
1163, 115nn0addge1i 12026 . . . . . . . . . . . . . . . . . . . . 21 2 ≤ (2 + 1)
117 2p1e3 11860 . . . . . . . . . . . . . . . . . . . . 21 (2 + 1) = 3
118116, 117breqtri 5055 . . . . . . . . . . . . . . . . . . . 20 2 ≤ 3
119118a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 2 ≤ 3)
1204, 27, 2, 119, 30letrd 10877 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2 ≤ 𝑁)
121110, 114, 4, 6, 2, 7, 120logblebd 39625 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 logb 2) ≤ (2 logb 𝑁))
1228, 96, 13, 106, 121letrd 10877 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ (2 logb 𝑁))
12313, 99, 122expge1d 13623 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ ((2 logb 𝑁)↑2))
124113, 123eqbrtrd 5052 . . . . . . . . . . . . . 14 (𝜑 → ((2 logb 2)↑2) ≤ ((2 logb 𝑁)↑2))
125 1z 12095 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℤ
126 zsqcl 13588 . . . . . . . . . . . . . . . . . . 19 (1 ∈ ℤ → (1↑2) ∈ ℤ)
127125, 126ax-mp 5 . . . . . . . . . . . . . . . . . 18 (1↑2) ∈ ℤ
128127a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (1↑2) ∈ ℤ)
129109eleq1d 2817 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 logb 2)↑2) ∈ ℤ ↔ (1↑2) ∈ ℤ))
130128, 129mpbird 260 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 logb 2)↑2) ∈ ℤ)
13191, 130jca 515 . . . . . . . . . . . . . . 15 (𝜑 → (((2 logb 𝑁)↑2) ∈ ℝ ∧ ((2 logb 2)↑2) ∈ ℤ))
132 flge 13268 . . . . . . . . . . . . . . 15 ((((2 logb 𝑁)↑2) ∈ ℝ ∧ ((2 logb 2)↑2) ∈ ℤ) → (((2 logb 2)↑2) ≤ ((2 logb 𝑁)↑2) ↔ ((2 logb 2)↑2) ≤ (⌊‘((2 logb 𝑁)↑2))))
133131, 132syl 17 . . . . . . . . . . . . . 14 (𝜑 → (((2 logb 2)↑2) ≤ ((2 logb 𝑁)↑2) ↔ ((2 logb 2)↑2) ≤ (⌊‘((2 logb 𝑁)↑2))))
134124, 133mpbid 235 . . . . . . . . . . . . 13 (𝜑 → ((2 logb 2)↑2) ≤ (⌊‘((2 logb 𝑁)↑2)))
1358, 97, 93, 107, 134letrd 10877 . . . . . . . . . . . 12 (𝜑 → 1 ≤ (⌊‘((2 logb 𝑁)↑2)))
13624, 8, 93, 95, 135ltletrd 10880 . . . . . . . . . . 11 (𝜑 → 0 < (⌊‘((2 logb 𝑁)↑2)))
13792, 136jca 515 . . . . . . . . . 10 (𝜑 → ((⌊‘((2 logb 𝑁)↑2)) ∈ ℤ ∧ 0 < (⌊‘((2 logb 𝑁)↑2))))
138 elnnz 12074 . . . . . . . . . . . 12 ((⌊‘((2 logb 𝑁)↑2)) ∈ ℕ ↔ ((⌊‘((2 logb 𝑁)↑2)) ∈ ℤ ∧ 0 < (⌊‘((2 logb 𝑁)↑2))))
139138bicomi 227 . . . . . . . . . . 11 (((⌊‘((2 logb 𝑁)↑2)) ∈ ℤ ∧ 0 < (⌊‘((2 logb 𝑁)↑2))) ↔ (⌊‘((2 logb 𝑁)↑2)) ∈ ℕ)
140139a1i 11 . . . . . . . . . 10 (𝜑 → (((⌊‘((2 logb 𝑁)↑2)) ∈ ℤ ∧ 0 < (⌊‘((2 logb 𝑁)↑2))) ↔ (⌊‘((2 logb 𝑁)↑2)) ∈ ℕ))
141137, 140mpbid 235 . . . . . . . . 9 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ∈ ℕ)
142141nnnn0d 12038 . . . . . . . 8 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ∈ ℕ0)
143 arisum 15310 . . . . . . . 8 ((⌊‘((2 logb 𝑁)↑2)) ∈ ℕ0 → Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘 = ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2))
144142, 143syl 17 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘 = ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2))
14573nnred 11733 . . . . . . . 8 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℝ)
14670, 145fsumrecl 15186 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘 ∈ ℝ)
147144, 146eqeltrrd 2834 . . . . . 6 (𝜑 → ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2) ∈ ℝ)
14890, 147readdcld 10750 . . . . 5 (𝜑 → ((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2)) ∈ ℝ)
1492, 86, 148recxpcld 25468 . . . 4 (𝜑 → (𝑁𝑐((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2))) ∈ ℝ)
150 4nn0 11997 . . . . . . . . . 10 4 ∈ ℕ0
151150a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℕ0)
15213, 151reexpcld 13621 . . . . . . . 8 (𝜑 → ((2 logb 𝑁)↑4) ∈ ℝ)
153152, 91readdcld 10750 . . . . . . 7 (𝜑 → (((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) ∈ ℝ)
154153rehalfcld 11965 . . . . . 6 (𝜑 → ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2) ∈ ℝ)
15590, 154readdcld 10750 . . . . 5 (𝜑 → ((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2)) ∈ ℝ)
1562, 86, 155recxpcld 25468 . . . 4 (𝜑 → (𝑁𝑐((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2))) ∈ ℝ)
157 reflcl 13259 . . . . . . . . . . 11 ((2 logb 𝐵) ∈ ℝ → (⌊‘(2 logb 𝐵)) ∈ ℝ)
15846, 157syl 17 . . . . . . . . . 10 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℝ)
1592, 86, 158recxpcld 25468 . . . . . . . . 9 (𝜑 → (𝑁𝑐(⌊‘(2 logb 𝐵))) ∈ ℝ)
16032, 146rpcxpcld 25477 . . . . . . . . . . . 12 (𝜑 → (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘) ∈ ℝ+)
16132, 141aks4d1p1p1 39712 . . . . . . . . . . . . 13 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘) = (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘))
162161eleq1d 2817 . . . . . . . . . . . 12 (𝜑 → (∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘) ∈ ℝ+ ↔ (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘) ∈ ℝ+))
163160, 162mpbird 260 . . . . . . . . . . 11 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘) ∈ ℝ+)
164163rpregt0d 12522 . . . . . . . . . 10 (𝜑 → (∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘) ∈ ℝ ∧ 0 < ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
165164simpld 498 . . . . . . . . 9 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘) ∈ ℝ)
166159, 165remulcld 10751 . . . . . . . 8 (𝜑 → ((𝑁𝑐(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)) ∈ ℝ)
1672, 86, 90recxpcld 25468 . . . . . . . . 9 (𝜑 → (𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) ∈ ℝ)
168167, 165remulcld 10751 . . . . . . . 8 (𝜑 → ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)) ∈ ℝ)
16970, 76fprodrecl 15401 . . . . . . . . . . . 12 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘) ∈ ℝ)
1702, 68, 86expge0d 13622 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁↑(⌊‘(2 logb 𝐵))))
171 nfv 1921 . . . . . . . . . . . . 13 𝑘𝜑
172 0red 10724 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 0 ∈ ℝ)
1731nnge1d 11766 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ≤ 𝑁)
174173adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ≤ 𝑁)
17571, 75, 174expge1d 13623 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ≤ (𝑁𝑘))
17676recnd 10749 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑘) ∈ ℂ)
177176subid1d 11066 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((𝑁𝑘) − 0) = (𝑁𝑘))
178177breq2d 5042 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (1 ≤ ((𝑁𝑘) − 0) ↔ 1 ≤ (𝑁𝑘)))
179175, 178mpbird 260 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ≤ ((𝑁𝑘) − 0))
18077, 76, 172, 179lesubd 11324 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 0 ≤ ((𝑁𝑘) − 1))
18176lem1d 11653 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((𝑁𝑘) − 1) ≤ (𝑁𝑘))
182171, 70, 78, 180, 76, 181fprodle 15444 . . . . . . . . . . . 12 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1) ≤ ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘))
18379, 169, 69, 170, 182lemul2ad 11660 . . . . . . . . . . 11 (𝜑 → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ≤ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘)))
18482breq1d 5040 . . . . . . . . . . 11 (𝜑 → (𝐴 ≤ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘)) ↔ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ≤ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘))))
185183, 184mpbird 260 . . . . . . . . . 10 (𝜑𝐴 ≤ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘)))
18671recnd 10749 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑁 ∈ ℂ)
187 cxpexp 25413 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑁𝑐𝑘) = (𝑁𝑘))
188186, 75, 187syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑐𝑘) = (𝑁𝑘))
189188eqcomd 2744 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑘) = (𝑁𝑐𝑘))
190189prodeq2dv 15371 . . . . . . . . . . 11 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘) = ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘))
191190oveq2d 7188 . . . . . . . . . 10 (𝜑 → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑘)) = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
192185, 191breqtrd 5056 . . . . . . . . 9 (𝜑𝐴 ≤ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
1932recnd 10749 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
194 cxpexp 25413 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ (⌊‘(2 logb 𝐵)) ∈ ℕ0) → (𝑁𝑐(⌊‘(2 logb 𝐵))) = (𝑁↑(⌊‘(2 logb 𝐵))))
195193, 68, 194syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝑁𝑐(⌊‘(2 logb 𝐵))) = (𝑁↑(⌊‘(2 logb 𝐵))))
196195oveq1d 7187 . . . . . . . . . 10 (𝜑 → ((𝑁𝑐(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)) = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
197196eqcomd 2744 . . . . . . . . 9 (𝜑 → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)) = ((𝑁𝑐(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
198192, 197breqtrd 5056 . . . . . . . 8 (𝜑𝐴 ≤ ((𝑁𝑐(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
199159, 167, 1643jca 1129 . . . . . . . . 9 (𝜑 → ((𝑁𝑐(⌊‘(2 logb 𝐵))) ∈ ℝ ∧ (𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) ∈ ℝ ∧ (∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘) ∈ ℝ ∧ 0 < ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘))))
2001, 20, 30aks4d1p1p3 39718 . . . . . . . . 9 (𝜑 → (𝑁𝑐(⌊‘(2 logb 𝐵))) < (𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))))
201 ltmul1a 11569 . . . . . . . . 9 ((((𝑁𝑐(⌊‘(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)))(𝑁𝑐𝑘)))
202199, 200, 201syl2anc 587 . . . . . . . 8 (𝜑 → ((𝑁𝑐(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)) < ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
20384, 166, 168, 198, 202lelttrd 10878 . . . . . . 7 (𝜑𝐴 < ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)))
204161oveq2d 7188 . . . . . . 7 (𝜑 → ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))(𝑁𝑐𝑘)) = ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘)))
205203, 204breqtrd 5056 . . . . . 6 (𝜑𝐴 < ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘)))
206144oveq2d 7188 . . . . . . 7 (𝜑 → (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘) = (𝑁𝑐((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2)))
207206oveq2d 7188 . . . . . 6 (𝜑 → ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · (𝑁𝑐Σ𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))𝑘)) = ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · (𝑁𝑐((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2))))
208205, 207breqtrd 5056 . . . . 5 (𝜑𝐴 < ((𝑁𝑐(2 logb (((2 logb 𝑁)↑5) + 1))) · (𝑁𝑐((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2))))
20924, 7gtned 10855 . . . . . . 7 (𝜑𝑁 ≠ 0)
21090recnd 10749 . . . . . . 7 (𝜑 → (2 logb (((2 logb 𝑁)↑5) + 1)) ∈ ℂ)
211141nncnd 11734 . . . . . . . . . 10 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ∈ ℂ)
212211sqcld 13602 . . . . . . . . 9 (𝜑 → ((⌊‘((2 logb 𝑁)↑2))↑2) ∈ ℂ)
213212, 211addcld 10740 . . . . . . . 8 (𝜑 → (((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) ∈ ℂ)
214213halfcld 11963 . . . . . . 7 (𝜑 → ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2) ∈ ℂ)
215193, 209, 210, 214cxpaddd 25462 . . . . . 6 (𝜑 → (𝑁𝑐((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))))
216215eqcomd 2744 . . . . 5 (𝜑 → ((𝑁𝑐(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))))
217208, 216breqtrd 5056 . . . 4 (𝜑𝐴 < (𝑁𝑐((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2))))
218 reflcl 13259 . . . . . . . . . 10 (((2 logb 𝑁)↑2) ∈ ℝ → (⌊‘((2 logb 𝑁)↑2)) ∈ ℝ)
21991, 218syl 17 . . . . . . . . 9 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ∈ ℝ)
220219resqcld 13705 . . . . . . . 8 (𝜑 → ((⌊‘((2 logb 𝑁)↑2))↑2) ∈ ℝ)
221220, 219readdcld 10750 . . . . . . 7 (𝜑 → (((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) ∈ ℝ)
22233a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℝ+)
22391, 99reexpcld 13621 . . . . . . . . 9 (𝜑 → (((2 logb 𝑁)↑2)↑2) ∈ ℝ)
224 id 22 . . . . . . . . . 10 (𝜑𝜑)
225142nn0ge0d 12041 . . . . . . . . . . 11 (𝜑 → 0 ≤ (⌊‘((2 logb 𝑁)↑2)))
226 flle 13262 . . . . . . . . . . . 12 (((2 logb 𝑁)↑2) ∈ ℝ → (⌊‘((2 logb 𝑁)↑2)) ≤ ((2 logb 𝑁)↑2))
22791, 226syl 17 . . . . . . . . . . 11 (𝜑 → (⌊‘((2 logb 𝑁)↑2)) ≤ ((2 logb 𝑁)↑2))
228219, 91, 99, 225, 227leexp1ad 39621 . . . . . . . . . 10 (𝜑 → ((⌊‘((2 logb 𝑁)↑2))↑2) ≤ (((2 logb 𝑁)↑2)↑2))
229224, 228syl 17 . . . . . . . . 9 (𝜑 → ((⌊‘((2 logb 𝑁)↑2))↑2) ≤ (((2 logb 𝑁)↑2)↑2))
23013recnd 10749 . . . . . . . . . . . . 13 (𝜑 → (2 logb 𝑁) ∈ ℂ)
231230, 99, 99expmuld 13607 . . . . . . . . . . . 12 (𝜑 → ((2 logb 𝑁)↑(2 · 2)) = (((2 logb 𝑁)↑2)↑2))
232231eqcomd 2744 . . . . . . . . . . 11 (𝜑 → (((2 logb 𝑁)↑2)↑2) = ((2 logb 𝑁)↑(2 · 2)))
233 2t2e4 11882 . . . . . . . . . . . . 13 (2 · 2) = 4
234233oveq2i 7183 . . . . . . . . . . . 12 ((2 logb 𝑁)↑(2 · 2)) = ((2 logb 𝑁)↑4)
235234a1i 11 . . . . . . . . . . 11 (𝜑 → ((2 logb 𝑁)↑(2 · 2)) = ((2 logb 𝑁)↑4))
236232, 235eqtrd 2773 . . . . . . . . . 10 (𝜑 → (((2 logb 𝑁)↑2)↑2) = ((2 logb 𝑁)↑4))
237223, 236eqled 10823 . . . . . . . . 9 (𝜑 → (((2 logb 𝑁)↑2)↑2) ≤ ((2 logb 𝑁)↑4))
238220, 223, 152, 229, 237letrd 10877 . . . . . . . 8 (𝜑 → ((⌊‘((2 logb 𝑁)↑2))↑2) ≤ ((2 logb 𝑁)↑4))
239220, 219, 152, 91, 238, 227le2addd 11339 . . . . . . 7 (𝜑 → (((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) ≤ (((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)))
240221, 153, 222, 239lediv1dd 12574 . . . . . 6 (𝜑 → ((((⌊‘((2 logb 𝑁)↑2))↑2) + (⌊‘((2 logb 𝑁)↑2))) / 2) ≤ ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2))
241147, 154, 90, 240leadd2dd 11335 . . . . 5 (𝜑 → ((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)))
2422, 31, 148, 155cxpled 25465 . . . . 5 (𝜑 → (((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)))))
243241, 242mpbid 235 . . . 4 (𝜑 → (𝑁𝑐((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))))
24484, 149, 156, 217, 243ltletrd 10880 . . 3 (𝜑𝐴 < (𝑁𝑐((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2))))
245152recnd 10749 . . . . . 6 (𝜑 → ((2 logb 𝑁)↑4) ∈ ℂ)
24691recnd 10749 . . . . . 6 (𝜑 → ((2 logb 𝑁)↑2) ∈ ℂ)
247245, 246, 101, 102divdird 11534 . . . . 5 (𝜑 → ((((2 logb 𝑁)↑4) + ((2 logb 𝑁)↑2)) / 2) = ((((2 logb 𝑁)↑4) / 2) + (((2 logb 𝑁)↑2) / 2)))
248247oveq2d 7188 . . . 4 (𝜑 → ((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))))
249248oveq2d 7188 . . 3 (𝜑 → (𝑁𝑐((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)))))
250244, 249breqtrd 5056 . 2 (𝜑𝐴 < (𝑁𝑐((2 logb (((2 logb 𝑁)↑5) + 1)) + ((((2 logb 𝑁)↑4) / 2) + (((2 logb 𝑁)↑2) / 2)))))
251245, 101, 102divcld 11496 . . . . . 6 (𝜑 → (((2 logb 𝑁)↑4) / 2) ∈ ℂ)
252246, 101, 102divcld 11496 . . . . . 6 (𝜑 → (((2 logb 𝑁)↑2) / 2) ∈ ℂ)
253251, 252addcomd 10922 . . . . 5 (𝜑 → ((((2 logb 𝑁)↑4) / 2) + (((2 logb 𝑁)↑2) / 2)) = ((((2 logb 𝑁)↑2) / 2) + (((2 logb 𝑁)↑4) / 2)))
254253oveq2d 7188 . . . 4 (𝜑 → ((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))))
255210, 252, 251addassd 10743 . . . . 5 (𝜑 → (((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))))
256255eqcomd 2744 . . . 4 (𝜑 → ((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)))
257254, 256eqtrd 2773 . . 3 (𝜑 → ((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)))
258257oveq2d 7188 . 2 (𝜑 → (𝑁𝑐((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))))
259250, 258breqtrd 5056 1 (𝜑𝐴 < (𝑁𝑐(((2 logb (((2 logb 𝑁)↑5) + 1)) + (((2 logb 𝑁)↑2) / 2)) + (((2 logb 𝑁)↑4) / 2))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2114  wne 2934   class class class wbr 5030  cfv 6339  (class class class)co 7172  cc 10615  cr 10616  0cc0 10617  1c1 10618   + caddc 10620   · cmul 10622   < clt 10755  cle 10756  cmin 10950   / cdiv 11377  cn 11718  2c2 11773  3c3 11774  4c4 11775  5c5 11776  7c7 11778  0cn0 11978  cz 12064  +crp 12474  ...cfz 12983  cfl 13253  cceil 13254  cexp 13523  Σcsu 15137  cprod 15353  𝑐ccxp 25301   logb clogb 25504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7481  ax-inf2 9179  ax-cnex 10673  ax-resscn 10674  ax-1cn 10675  ax-icn 10676  ax-addcl 10677  ax-addrcl 10678  ax-mulcl 10679  ax-mulrcl 10680  ax-mulcom 10681  ax-addass 10682  ax-mulass 10683  ax-distr 10684  ax-i2m1 10685  ax-1ne0 10686  ax-1rid 10687  ax-rnegex 10688  ax-rrecex 10689  ax-cnre 10690  ax-pre-lttri 10691  ax-pre-lttrn 10692  ax-pre-ltadd 10693  ax-pre-mulgt0 10694  ax-pre-sup 10695  ax-addf 10696  ax-mulf 10697
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7129  df-ov 7175  df-oprab 7176  df-mpo 7177  df-of 7427  df-om 7602  df-1st 7716  df-2nd 7717  df-supp 7859  df-wrecs 7978  df-recs 8039  df-rdg 8077  df-1o 8133  df-2o 8134  df-er 8322  df-map 8441  df-pm 8442  df-ixp 8510  df-en 8558  df-dom 8559  df-sdom 8560  df-fin 8561  df-fsupp 8909  df-fi 8950  df-sup 8981  df-inf 8982  df-oi 9049  df-card 9443  df-pnf 10757  df-mnf 10758  df-xr 10759  df-ltxr 10760  df-le 10761  df-sub 10952  df-neg 10953  df-div 11378  df-nn 11719  df-2 11781  df-3 11782  df-4 11783  df-5 11784  df-6 11785  df-7 11786  df-8 11787  df-9 11788  df-n0 11979  df-z 12065  df-dec 12182  df-uz 12327  df-q 12433  df-rp 12475  df-xneg 12592  df-xadd 12593  df-xmul 12594  df-ioo 12827  df-ioc 12828  df-ico 12829  df-icc 12830  df-fz 12984  df-fzo 13127  df-fl 13255  df-ceil 13256  df-mod 13331  df-seq 13463  df-exp 13524  df-fac 13728  df-bc 13757  df-hash 13785  df-shft 14518  df-cj 14550  df-re 14551  df-im 14552  df-sqrt 14686  df-abs 14687  df-limsup 14920  df-clim 14937  df-rlim 14938  df-sum 15138  df-prod 15354  df-ef 15515  df-sin 15517  df-cos 15518  df-pi 15520  df-struct 16590  df-ndx 16591  df-slot 16592  df-base 16594  df-sets 16595  df-ress 16596  df-plusg 16683  df-mulr 16684  df-starv 16685  df-sca 16686  df-vsca 16687  df-ip 16688  df-tset 16689  df-ple 16690  df-ds 16692  df-unif 16693  df-hom 16694  df-cco 16695  df-rest 16801  df-topn 16802  df-0g 16820  df-gsum 16821  df-topgen 16822  df-pt 16823  df-prds 16826  df-xrs 16880  df-qtop 16885  df-imas 16886  df-xps 16888  df-mre 16962  df-mrc 16963  df-acs 16965  df-mgm 17970  df-sgrp 18019  df-mnd 18030  df-submnd 18075  df-mulg 18345  df-cntz 18567  df-cmn 19028  df-psmet 20211  df-xmet 20212  df-met 20213  df-bl 20214  df-mopn 20215  df-fbas 20216  df-fg 20217  df-cnfld 20220  df-top 21647  df-topon 21664  df-topsp 21686  df-bases 21699  df-cld 21772  df-ntr 21773  df-cls 21774  df-nei 21851  df-lp 21889  df-perf 21890  df-cn 21980  df-cnp 21981  df-haus 22068  df-tx 22315  df-hmeo 22508  df-fil 22599  df-fm 22691  df-flim 22692  df-flf 22693  df-xms 23075  df-ms 23076  df-tms 23077  df-cncf 23632  df-limc 24620  df-dv 24621  df-log 25302  df-cxp 25303  df-logb 25505
This theorem is referenced by:  aks4d1p1p4  39720
  Copyright terms: Public domain W3C validator