MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem9 Structured version   Visualization version   GIF version

Theorem bposlem9 25208
Description: Lemma for bpos 25209. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
Hypotheses
Ref Expression
bposlem7.1 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
bposlem7.2 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
bposlem9.3 (𝜑𝑁 ∈ ℕ)
bposlem9.4 (𝜑64 < 𝑁)
bposlem9.5 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
Assertion
Ref Expression
bposlem9 (𝜑𝜓)
Distinct variable groups:   𝑛,𝑁   𝑛,𝐺   𝜑,𝑛   𝑁,𝑝   𝑥,𝑁
Allowed substitution hints:   𝜑(𝑥,𝑝)   𝜓(𝑥,𝑛,𝑝)   𝐹(𝑥,𝑛,𝑝)   𝐺(𝑥,𝑝)

Proof of Theorem bposlem9
Dummy variable 𝑞 is distinct from all other variables.
StepHypRef Expression
1 bposlem9.4 . . 3 (𝜑64 < 𝑁)
2 bposlem7.1 . . . 4 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
3 bposlem7.2 . . . 4 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))
4 6nn0 11497 . . . . . 6 6 ∈ ℕ0
5 4nn 11371 . . . . . 6 4 ∈ ℕ
64, 5decnncl 11702 . . . . 5 64 ∈ ℕ
76a1i 11 . . . 4 (𝜑64 ∈ ℕ)
8 bposlem9.3 . . . 4 (𝜑𝑁 ∈ ℕ)
9 ere 15010 . . . . . . . 8 e ∈ ℝ
10 8re 11289 . . . . . . . 8 8 ∈ ℝ
11 egt2lt3 15125 . . . . . . . . . 10 (2 < e ∧ e < 3)
1211simpri 481 . . . . . . . . 9 e < 3
13 3lt8 11403 . . . . . . . . 9 3 < 8
14 3re 11278 . . . . . . . . . 10 3 ∈ ℝ
159, 14, 10lttri 10347 . . . . . . . . 9 ((e < 3 ∧ 3 < 8) → e < 8)
1612, 13, 15mp2an 710 . . . . . . . 8 e < 8
179, 10, 16ltleii 10344 . . . . . . 7 e ≤ 8
18 0re 10224 . . . . . . . . 9 0 ∈ ℝ
19 epos 15126 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 10344 . . . . . . . 8 0 ≤ e
21 8pos 11305 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 10344 . . . . . . . 8 0 ≤ 8
23 le2sq 13124 . . . . . . . 8 (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
249, 20, 10, 22, 23mp4an 711 . . . . . . 7 (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
2517, 24mpbi 220 . . . . . 6 (e↑2) ≤ (8↑2)
2610recni 10236 . . . . . . . 8 8 ∈ ℂ
2726sqvali 13129 . . . . . . 7 (8↑2) = (8 · 8)
28 8t8e64 11846 . . . . . . 7 (8 · 8) = 64
2927, 28eqtri 2774 . . . . . 6 (8↑2) = 64
3025, 29breqtri 4821 . . . . 5 (e↑2) ≤ 64
3130a1i 11 . . . 4 (𝜑 → (e↑2) ≤ 64)
329resqcli 13135 . . . . . 6 (e↑2) ∈ ℝ
3332a1i 11 . . . . 5 (𝜑 → (e↑2) ∈ ℝ)
346nnrei 11213 . . . . . 6 64 ∈ ℝ
3534a1i 11 . . . . 5 (𝜑64 ∈ ℝ)
368nnred 11219 . . . . 5 (𝜑𝑁 ∈ ℝ)
37 ltle 10310 . . . . . . 7 ((64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (64 < 𝑁64 ≤ 𝑁))
3834, 36, 37sylancr 698 . . . . . 6 (𝜑 → (64 < 𝑁64 ≤ 𝑁))
391, 38mpd 15 . . . . 5 (𝜑64 ≤ 𝑁)
4033, 35, 36, 31, 39letrd 10378 . . . 4 (𝜑 → (e↑2) ≤ 𝑁)
412, 3, 7, 8, 31, 40bposlem7 25206 . . 3 (𝜑 → (64 < 𝑁 → (𝐹𝑁) < (𝐹64)))
421, 41mpd 15 . 2 (𝜑 → (𝐹𝑁) < (𝐹64))
432, 3bposlem8 25207 . . . . 5 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
4443a1i 11 . . . 4 (𝜑 → ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2)))
4544simpld 477 . . 3 (𝜑 → (𝐹64) ∈ ℝ)
46 fveq2 6344 . . . . . . . . . 10 (𝑛 = 𝑁 → (√‘𝑛) = (√‘𝑁))
4746fveq2d 6348 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
4847oveq2d 6821 . . . . . . . 8 (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
49 oveq1 6812 . . . . . . . . . 10 (𝑛 = 𝑁 → (𝑛 / 2) = (𝑁 / 2))
5049fveq2d 6348 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
5150oveq2d 6821 . . . . . . . 8 (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
5248, 51oveq12d 6823 . . . . . . 7 (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
53 oveq2 6813 . . . . . . . . 9 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
5453fveq2d 6348 . . . . . . . 8 (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
5554oveq2d 6821 . . . . . . 7 (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
5652, 55oveq12d 6823 . . . . . 6 (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57 ovex 6833 . . . . . 6 ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
5856, 2, 57fvmpt 6436 . . . . 5 (𝑁 ∈ ℕ → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
598, 58syl 17 . . . 4 (𝜑 → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
60 sqrt2re 15171 . . . . . . 7 (√‘2) ∈ ℝ
618nnrpd 12055 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ+)
6261rpsqrtcld 14341 . . . . . . . . 9 (𝜑 → (√‘𝑁) ∈ ℝ+)
63 fveq2 6344 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
64 id 22 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
6563, 64oveq12d 6823 . . . . . . . . . 10 (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66 ovex 6833 . . . . . . . . . 10 ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
6765, 3, 66fvmpt 6436 . . . . . . . . 9 ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6862, 67syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6962relogcld 24560 . . . . . . . . 9 (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
7069, 62rerpdivcld 12088 . . . . . . . 8 (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
7168, 70eqeltrd 2831 . . . . . . 7 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
72 remulcl 10205 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
7360, 71, 72sylancr 698 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
74 9re 11291 . . . . . . . 8 9 ∈ ℝ
75 4re 11281 . . . . . . . 8 4 ∈ ℝ
76 4ne0 11301 . . . . . . . 8 4 ≠ 0
7774, 75, 76redivcli 10976 . . . . . . 7 (9 / 4) ∈ ℝ
7861rphalfcld 12069 . . . . . . . . 9 (𝜑 → (𝑁 / 2) ∈ ℝ+)
79 fveq2 6344 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
80 id 22 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
8179, 80oveq12d 6823 . . . . . . . . . 10 (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82 ovex 6833 . . . . . . . . . 10 ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
8381, 3, 82fvmpt 6436 . . . . . . . . 9 ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8478, 83syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8578relogcld 24560 . . . . . . . . 9 (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
8685, 78rerpdivcld 12088 . . . . . . . 8 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
8784, 86eqeltrd 2831 . . . . . . 7 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
88 remulcl 10205 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8977, 87, 88sylancr 698 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
9073, 89readdcld 10253 . . . . 5 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
91 2rp 12022 . . . . . . 7 2 ∈ ℝ+
92 relogcl 24513 . . . . . . 7 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
9391, 92ax-mp 5 . . . . . 6 (log‘2) ∈ ℝ
94 rpmulcl 12040 . . . . . . . 8 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
9591, 61, 94sylancr 698 . . . . . . 7 (𝜑 → (2 · 𝑁) ∈ ℝ+)
9695rpsqrtcld 14341 . . . . . 6 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
97 rerpdivcl 12046 . . . . . 6 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9893, 96, 97sylancr 698 . . . . 5 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9990, 98readdcld 10253 . . . 4 (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
10059, 99eqeltrd 2831 . . 3 (𝜑 → (𝐹𝑁) ∈ ℝ)
10193a1i 11 . . . 4 (𝜑 → (log‘2) ∈ ℝ)
10244simprd 482 . . . 4 (𝜑 → (𝐹64) < (log‘2))
103 nnrp 12027 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
1045, 103ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
105 relogcl 24513 . . . . . . . . . 10 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
106104, 105ax-mp 5 . . . . . . . . 9 (log‘4) ∈ ℝ
107 remulcl 10205 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
10836, 106, 107sylancl 697 . . . . . . . 8 (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
10961relogcld 24560 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
110108, 109resubcld 10642 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
111 rpre 12024 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
112 rpge0 12030 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
113111, 112resqrtcld 14347 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
11495, 113syl 17 . . . . . . . . . . 11 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
115 3nn 11370 . . . . . . . . . . 11 3 ∈ ℕ
116 nndivre 11240 . . . . . . . . . . 11 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
117114, 115, 116sylancl 697 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
118 2re 11274 . . . . . . . . . 10 2 ∈ ℝ
119 readdcl 10203 . . . . . . . . . 10 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
120117, 118, 119sylancl 697 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
12195relogcld 24560 . . . . . . . . 9 (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
122120, 121remulcld 10254 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
123 remulcl 10205 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
12475, 36, 123sylancr 698 . . . . . . . . . . 11 (𝜑 → (4 · 𝑁) ∈ ℝ)
125 nndivre 11240 . . . . . . . . . . 11 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
126124, 115, 125sylancl 697 . . . . . . . . . 10 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
127 5re 11283 . . . . . . . . . 10 5 ∈ ℝ
128 resubcl 10529 . . . . . . . . . 10 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
129126, 127, 128sylancl 697 . . . . . . . . 9 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
130 remulcl 10205 . . . . . . . . 9 (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
131129, 93, 130sylancl 697 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
132122, 131readdcld 10253 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
133 remulcl 10205 . . . . . . . . 9 ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
134126, 93, 133sylancl 697 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
135134, 109resubcld 10642 . . . . . . 7 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
1368nnzd 11665 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
137 df-5 11266 . . . . . . . . . . . 12 5 = (4 + 1)
13875a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
139 6nn 11373 . . . . . . . . . . . . . . . 16 6 ∈ ℕ
140 4nn0 11495 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
141 4lt10 11862 . . . . . . . . . . . . . . . 16 4 < 10
142139, 140, 140, 141declti 11730 . . . . . . . . . . . . . . 15 4 < 64
143142a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 < 64)
144138, 35, 36, 143, 1lttrd 10382 . . . . . . . . . . . . 13 (𝜑 → 4 < 𝑁)
145 4z 11595 . . . . . . . . . . . . . 14 4 ∈ ℤ
146 zltp1le 11611 . . . . . . . . . . . . . 14 ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
147145, 136, 146sylancr 698 . . . . . . . . . . . . 13 (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
148144, 147mpbid 222 . . . . . . . . . . . 12 (𝜑 → (4 + 1) ≤ 𝑁)
149137, 148syl5eqbr 4831 . . . . . . . . . . 11 (𝜑 → 5 ≤ 𝑁)
150 5nn 11372 . . . . . . . . . . . . 13 5 ∈ ℕ
151150nnzi 11585 . . . . . . . . . . . 12 5 ∈ ℤ
152151eluz1i 11879 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
153136, 149, 152sylanbrc 701 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘5))
154 bposlem9.5 . . . . . . . . . . 11 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
155 breq2 4800 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑁 < 𝑝𝑁 < 𝑞))
156 breq1 4799 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
157155, 156anbi12d 749 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁))))
158157cbvrexv 3303 . . . . . . . . . . 11 (∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
159154, 158sylnib 317 . . . . . . . . . 10 (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
160 eqid 2752 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
161 eqid 2752 . . . . . . . . . 10 (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
162 eqid 2752 . . . . . . . . . 10 (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
163153, 159, 160, 161, 162bposlem6 25205 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
164 reexplog 24532 . . . . . . . . . . . 12 ((4 ∈ ℝ+𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
165104, 136, 164sylancr 698 . . . . . . . . . . 11 (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
16661reeflogd 24561 . . . . . . . . . . . 12 (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
167166eqcomd 2758 . . . . . . . . . . 11 (𝜑𝑁 = (exp‘(log‘𝑁)))
168165, 167oveq12d 6823 . . . . . . . . . 10 (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
169108recnd 10252 . . . . . . . . . . 11 (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
170109recnd 10252 . . . . . . . . . . 11 (𝜑 → (log‘𝑁) ∈ ℂ)
171 efsub 15021 . . . . . . . . . . 11 (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
172169, 170, 171syl2anc 696 . . . . . . . . . 10 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
173168, 172eqtr4d 2789 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
17495rpcnd 12059 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℂ)
17595rpne0d 12062 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ≠ 0)
176120recnd 10252 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
177174, 175, 176cxpefd 24649 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
178 2cn 11275 . . . . . . . . . . . 12 2 ∈ ℂ
179 2ne0 11297 . . . . . . . . . . . 12 2 ≠ 0
180129recnd 10252 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
181 cxpef 24602 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
182178, 179, 180, 181mp3an12i 1569 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
183177, 182oveq12d 6823 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
184122recnd 10252 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
185131recnd 10252 . . . . . . . . . . 11 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
186 efadd 15015 . . . . . . . . . . 11 ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ ∧ ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ) → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
187184, 185, 186syl2anc 696 . . . . . . . . . 10 (𝜑 → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188183, 187eqtr4d 2789 . . . . . . . . 9 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
189163, 173, 1883brtr3d 4827 . . . . . . . 8 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
190 eflt 15038 . . . . . . . . 9 ((((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ ∧ (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ) → (((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ↔ (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))))
191110, 132, 190syl2anc 696 . . . . . . . 8 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ↔ (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))))
192189, 191mpbird 247 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
193110, 132, 135, 192ltsub1dd 10823 . . . . . 6 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
19436recnd 10252 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
195 mulcom 10206 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
196178, 194, 195sylancr 698 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 · 2))
197196oveq1d 6820 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
19893recni 10236 . . . . . . . . . . . 12 (log‘2) ∈ ℂ
199 mulass 10208 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200178, 198, 199mp3an23 1557 . . . . . . . . . . 11 (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
201194, 200syl 17 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
2021982timesi 11331 . . . . . . . . . . . 12 (2 · (log‘2)) = ((log‘2) + (log‘2))
203 relogmul 24529 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
20491, 91, 203mp2an 710 . . . . . . . . . . . 12 (log‘(2 · 2)) = ((log‘2) + (log‘2))
205 2t2e4 11361 . . . . . . . . . . . . 13 (2 · 2) = 4
206205fveq2i 6347 . . . . . . . . . . . 12 (log‘(2 · 2)) = (log‘4)
207202, 204, 2063eqtr2i 2780 . . . . . . . . . . 11 (2 · (log‘2)) = (log‘4)
208207oveq2i 6816 . . . . . . . . . 10 (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
209201, 208syl6eq 2802 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
210197, 209eqtrd 2786 . . . . . . . 8 (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
211210oveq1d 6820 . . . . . . 7 (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
212 4p2e6 11346 . . . . . . . . . . . . . . 15 (4 + 2) = 6
213212oveq1i 6815 . . . . . . . . . . . . . 14 ((4 + 2) · 𝑁) = (6 · 𝑁)
214 4cn 11282 . . . . . . . . . . . . . . 15 4 ∈ ℂ
215 adddir 10215 . . . . . . . . . . . . . . 15 ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
216214, 178, 194, 215mp3an12i 1569 . . . . . . . . . . . . . 14 (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
217213, 216syl5eqr 2800 . . . . . . . . . . . . 13 (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
218217oveq1d 6820 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
219 6cn 11286 . . . . . . . . . . . . . . 15 6 ∈ ℂ
220 3cn 11279 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
221 3ne0 11299 . . . . . . . . . . . . . . . 16 3 ≠ 0
222220, 221pm3.2i 470 . . . . . . . . . . . . . . 15 (3 ∈ ℂ ∧ 3 ≠ 0)
223 div23 10888 . . . . . . . . . . . . . . 15 ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
224219, 222, 223mp3an13 1556 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
225194, 224syl 17 . . . . . . . . . . . . 13 (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
226 3t2e6 11363 . . . . . . . . . . . . . . . 16 (3 · 2) = 6
227226oveq1i 6815 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = (6 / 3)
228178, 220, 221divcan3i 10955 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = 2
229227, 228eqtr3i 2776 . . . . . . . . . . . . . 14 (6 / 3) = 2
230229oveq1i 6815 . . . . . . . . . . . . 13 ((6 / 3) · 𝑁) = (2 · 𝑁)
231225, 230syl6eq 2802 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
232124recnd 10252 . . . . . . . . . . . . 13 (𝜑 → (4 · 𝑁) ∈ ℂ)
233 remulcl 10205 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
234118, 36, 233sylancr 698 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝑁) ∈ ℝ)
235234recnd 10252 . . . . . . . . . . . . 13 (𝜑 → (2 · 𝑁) ∈ ℂ)
236 divdir 10894 . . . . . . . . . . . . . 14 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
237222, 236mp3an3 1554 . . . . . . . . . . . . 13 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
238232, 235, 237syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
239218, 231, 2383eqtr3d 2794 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240239oveq1d 6820 . . . . . . . . . 10 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)))
241126recnd 10252 . . . . . . . . . . 11 (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
242 3rp 12023 . . . . . . . . . . . . 13 3 ∈ ℝ+
243 rpdivcl 12041 . . . . . . . . . . . . 13 (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
24495, 242, 243sylancl 697 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
245244rpcnd 12059 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
246241, 245pncan2d 10578 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
247240, 246eqtrd 2786 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
248247oveq1d 6820 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
249101recnd 10252 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℂ)
250235, 241, 249subdird 10671 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
251248, 250eqtr3d 2788 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
252134recnd 10252 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
253169, 252, 170nnncan2d 10611 . . . . . . 7 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
254211, 251, 2533eqtr4d 2796 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
255117recnd 10252 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
256178a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
257121recnd 10252 . . . . . . . . . 10 (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
258255, 256, 257adddird 10249 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
259 relogmul 24529 . . . . . . . . . . . . 13 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
26091, 61, 259sylancr 698 . . . . . . . . . . . 12 (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
261260oveq2d 6821 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
262256, 249, 170adddid 10248 . . . . . . . . . . 11 (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
263261, 262eqtrd 2786 . . . . . . . . . 10 (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
264263oveq2d 6821 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
265258, 264eqtrd 2786 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
266 5cn 11284 . . . . . . . . . . . 12 5 ∈ ℂ
267266a1i 11 . . . . . . . . . . 11 (𝜑 → 5 ∈ ℂ)
268241, 267, 249subdird 10671 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
269268oveq1d 6820 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
270266, 198mulcli 10229 . . . . . . . . . . 11 (5 · (log‘2)) ∈ ℂ
271270a1i 11 . . . . . . . . . 10 (𝜑 → (5 · (log‘2)) ∈ ℂ)
272252, 271, 170nnncan1d 10610 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
273269, 272eqtrd 2786 . . . . . . . 8 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
274265, 273oveq12d 6823 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)))) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
275135recnd 10252 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
276184, 185, 275addsubassd 10596 . . . . . . 7 (𝜑 → ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)))))
277266, 220, 198subdiri 10664 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
278 3p2e5 11344 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
279278oveq1i 6815 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = (5 − 3)
280 pncan2 10472 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
281220, 178, 280mp2an 710 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = 2
282279, 281eqtr3i 2776 . . . . . . . . . . . . . 14 (5 − 3) = 2
283282oveq1i 6815 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = (2 · (log‘2))
284277, 283eqtr3i 2776 . . . . . . . . . . . 12 ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
285284a1i 11 . . . . . . . . . . 11 (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
286 df-3 11264 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
287286oveq1i 6815 . . . . . . . . . . . . . . 15 (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
288 1cnd 10240 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
289256, 288, 170adddird 10249 . . . . . . . . . . . . . . 15 (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
290287, 289syl5eq 2798 . . . . . . . . . . . . . 14 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
291170mulid2d 10242 . . . . . . . . . . . . . . 15 (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
292291oveq2d 6821 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
293290, 292eqtrd 2786 . . . . . . . . . . . . 13 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
294293oveq1d 6820 . . . . . . . . . . . 12 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
295 mulcl 10204 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
296178, 170, 295sylancr 698 . . . . . . . . . . . . 13 (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
297296, 170, 271addsubassd 10596 . . . . . . . . . . . 12 (𝜑 → (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
298294, 297eqtrd 2786 . . . . . . . . . . 11 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
299285, 298oveq12d 6823 . . . . . . . . . 10 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
300 relogdiv 24530 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
30161, 91, 300sylancl 697 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
302301oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
303 subdi 10647 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
304220, 198, 303mp3an13 1556 . . . . . . . . . . . . 13 ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
305170, 304syl 17 . . . . . . . . . . . 12 (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
306302, 305eqtrd 2786 . . . . . . . . . . 11 (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
307 div23 10888 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
308178, 222, 307mp3an13 1556 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
309194, 308syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
310220, 178, 220, 178, 179, 179divmuldivi 10969 . . . . . . . . . . . . . . . . 17 ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
311 3t3e9 11364 . . . . . . . . . . . . . . . . . 18 (3 · 3) = 9
312311, 205oveq12i 6817 . . . . . . . . . . . . . . . . 17 ((3 · 3) / (2 · 2)) = (9 / 4)
313310, 312eqtr2i 2775 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) · (3 / 2))
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
315309, 314oveq12d 6823 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
316178, 220, 221divcli 10951 . . . . . . . . . . . . . . 15 (2 / 3) ∈ ℂ
317220, 178, 179divcli 10951 . . . . . . . . . . . . . . . 16 (3 / 2) ∈ ℂ
318 mul4 10389 . . . . . . . . . . . . . . . 16 ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
319317, 317, 318mpanr12 723 . . . . . . . . . . . . . . 15 (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
320316, 194, 319sylancr 698 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
321 divcan6 10916 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
322178, 179, 220, 221, 321mp4an 711 . . . . . . . . . . . . . . . . 17 ((2 / 3) · (3 / 2)) = 1
323322oveq1i 6815 . . . . . . . . . . . . . . . 16 (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
324 mulcl 10204 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
325194, 317, 324sylancl 697 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
326325mulid2d 10242 . . . . . . . . . . . . . . . 16 (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
327323, 326syl5eq 2798 . . . . . . . . . . . . . . 15 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
328 2cnne0 11426 . . . . . . . . . . . . . . . . 17 (2 ∈ ℂ ∧ 2 ≠ 0)
329 div12 10891 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
330220, 328, 329mp3an23 1557 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
331194, 330syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
332327, 331eqtrd 2786 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
333315, 320, 3323eqtrd 2790 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
334333, 84oveq12d 6823 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
33577recni 10236 . . . . . . . . . . . . . 14 (9 / 4) ∈ ℂ
336335a1i 11 . . . . . . . . . . . . 13 (𝜑 → (9 / 4) ∈ ℂ)
33787recnd 10252 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
338245, 336, 337mulassd 10247 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
339220a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 3 ∈ ℂ)
34078rpcnd 12059 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 / 2) ∈ ℂ)
34185recnd 10252 . . . . . . . . . . . . . . 15 (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
34278rpne0d 12062 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 / 2) ≠ 0)
343341, 340, 342divcld 10985 . . . . . . . . . . . . . 14 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
344339, 340, 343mulassd 10247 . . . . . . . . . . . . 13 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
345341, 340, 342divcan2d 10987 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
346345oveq2d 6821 . . . . . . . . . . . . 13 (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
347344, 346eqtrd 2786 . . . . . . . . . . . 12 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
348334, 338, 3473eqtr3d 2794 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
349220, 198mulcli 10229 . . . . . . . . . . . . 13 (3 · (log‘2)) ∈ ℂ
350349a1i 11 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘2)) ∈ ℂ)
351 mulcl 10204 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
352220, 170, 351sylancr 698 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
353271, 350, 352npncan3d 10612 . . . . . . . . . . 11 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
354306, 348, 3533eqtr4d 2796 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
355118, 93remulcli 10238 . . . . . . . . . . . . 13 (2 · (log‘2)) ∈ ℝ
356355recni 10236 . . . . . . . . . . . 12 (2 · (log‘2)) ∈ ℂ
357356a1i 11 . . . . . . . . . . 11 (𝜑 → (2 · (log‘2)) ∈ ℂ)
358 subcl 10464 . . . . . . . . . . . 12 (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
359170, 270, 358sylancl 697 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
360357, 296, 359addassd 10246 . . . . . . . . . 10 (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
361299, 354, 3603eqtr4d 2796 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
362361oveq2d 6821 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
363 mulcl 10204 . . . . . . . . . . 11 ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
364255, 198, 363sylancl 697 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
365255, 170mulcld 10244 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
36689recnd 10252 . . . . . . . . . . 11 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
367245, 366mulcld 10244 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
368364, 365, 367addassd 10246 . . . . . . . . 9 (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
369260oveq2d 6821 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
370255, 249, 170adddid 10248 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
371369, 370eqtrd 2786 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
372371oveq1d 6820 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
37359oveq2d 6821 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
37490recnd 10252 . . . . . . . . . . . 12 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
37598recnd 10252 . . . . . . . . . . . 12 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
376245, 374, 375adddid 10248 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
377373, 376eqtrd 2786 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
37873recnd 10252 . . . . . . . . . . . . 13 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
379245, 378, 366adddid 10248 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
38095rpge0d 12061 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (2 · 𝑁))
381 remsqsqrt 14188 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
382234, 380, 381syl2anc 696 . . . . . . . . . . . . . . . . 17 (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
383382oveq1d 6820 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
384114recnd 10252 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
385221a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
386384, 384, 339, 385div23d 11022 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
387383, 386eqtr3d 2788 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
388387oveq1d 6820 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
389255, 384, 378mulassd 10247 . . . . . . . . . . . . . 14 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
390 0le2 11295 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
391118, 390pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ ∧ 0 ≤ 2)
39261rprege0d 12064 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
393 sqrtmul 14191 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
394391, 392, 393sylancr 698 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
395394oveq1d 6820 . . . . . . . . . . . . . . . 16 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
39660recni 10236 . . . . . . . . . . . . . . . . . 18 (√‘2) ∈ ℂ
397396a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘2) ∈ ℂ)
39862rpcnd 12059 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘𝑁) ∈ ℂ)
39971recnd 10252 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
400397, 398, 397, 399mul4d 10432 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
401 remsqsqrt 14188 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
402118, 390, 401mp2an 710 . . . . . . . . . . . . . . . . . . 19 ((√‘2) · (√‘2)) = 2
403402a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘2) · (√‘2)) = 2)
40468oveq2d 6821 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
40569recnd 10252 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
40662rpne0d 12062 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑁) ≠ 0)
407405, 398, 406divcan2d 10987 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
408404, 407eqtrd 2786 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
409403, 408oveq12d 6823 . . . . . . . . . . . . . . . . 17 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
4104052timesd 11459 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
41162, 62relogmuld 24562 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
412 remsqsqrt 14188 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
413392, 412syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
414413fveq2d 6348 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
415411, 414eqtr3d 2788 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
416409, 410, 4153eqtrd 2790 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
417395, 400, 4163eqtrd 2790 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
418417oveq2d 6821 . . . . . . . . . . . . . 14 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
419388, 389, 4183eqtrd 2790 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
420419oveq1d 6820 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
421379, 420eqtrd 2786 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
422387oveq1d 6820 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
423255, 384, 375mulassd 10247 . . . . . . . . . . . 12 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
42496rpne0d 12062 . . . . . . . . . . . . . 14 (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
425249, 384, 424divcan2d 10987 . . . . . . . . . . . . 13 (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
426425oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
427422, 423, 4263eqtrd 2790 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
428421, 427oveq12d 6823 . . . . . . . . . 10 (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
429365, 367addcld 10243 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
430429, 364addcomd 10422 . . . . . . . . . 10 (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
431377, 428, 4303eqtrd 2790 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
432368, 372, 4313eqtr4rd 2797 . . . . . . . 8 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
433255, 257mulcld 10244 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
434 addcl 10202 . . . . . . . . . 10 (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
435356, 296, 434sylancr 698 . . . . . . . . 9 (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
436433, 435, 359addassd 10246 . . . . . . . 8 (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
437362, 432, 4363eqtr4d 2796 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
438274, 276, 4373eqtr4rd 2797 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
439193, 254, 4383brtr4d 4828 . . . . 5 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁)))
440101, 100, 244ltmul2d 12099 . . . . 5 (𝜑 → ((log‘2) < (𝐹𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁))))
441439, 440mpbird 247 . . . 4 (𝜑 → (log‘2) < (𝐹𝑁))
44245, 101, 100, 102, 441lttrd 10382 . . 3 (𝜑 → (𝐹64) < (𝐹𝑁))
44345, 100, 442ltnsymd 10370 . 2 (𝜑 → ¬ (𝐹𝑁) < (𝐹64))
44442, 443pm2.21dd 186 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wne 2924  wrex 3043  ifcif 4222   class class class wbr 4796  cmpt 4873  cfv 6041  (class class class)co 6805  cc 10118  cr 10119  0cc0 10120  1c1 10121   + caddc 10123   · cmul 10125   < clt 10258  cle 10259  cmin 10450   / cdiv 10868  cn 11204  2c2 11254  3c3 11255  4c4 11256  5c5 11257  6c6 11258  8c8 11260  9c9 11261  cz 11561  cdc 11677  cuz 11871  +crp 12017  cfl 12777  cexp 13046  Ccbc 13275  csqrt 14164  expce 14983  eceu 14984  cprime 15579   pCnt cpc 15735  logclog 24492  𝑐ccxp 24493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-1st 7325  df-2nd 7326  df-supp 7456  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-xnn0 11548  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ioc 12365  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-mod 12855  df-seq 12988  df-exp 13047  df-fac 13247  df-bc 13276  df-hash 13304  df-shft 13998  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-limsup 14393  df-clim 14410  df-rlim 14411  df-sum 14608  df-ef 14989  df-e 14990  df-sin 14991  df-cos 14992  df-pi 14994  df-dvds 15175  df-gcd 15411  df-prm 15580  df-pc 15736  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-sets 16058  df-ress 16059  df-plusg 16148  df-mulr 16149  df-starv 16150  df-sca 16151  df-vsca 16152  df-ip 16153  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-hom 16160  df-cco 16161  df-rest 16277  df-topn 16278  df-0g 16296  df-gsum 16297  df-topgen 16298  df-pt 16299  df-prds 16302  df-xrs 16356  df-qtop 16361  df-imas 16362  df-xps 16364  df-mre 16440  df-mrc 16441  df-acs 16443  df-mgm 17435  df-sgrp 17477  df-mnd 17488  df-submnd 17529  df-mulg 17734  df-cntz 17942  df-cmn 18387  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-fbas 19937  df-fg 19938  df-cnfld 19941  df-top 20893  df-topon 20910  df-topsp 20931  df-bases 20944  df-cld 21017  df-ntr 21018  df-cls 21019  df-nei 21096  df-lp 21134  df-perf 21135  df-cn 21225  df-cnp 21226  df-haus 21313  df-tx 21559  df-hmeo 21752  df-fil 21843  df-fm 21935  df-flim 21936  df-flf 21937  df-xms 22318  df-ms 22319  df-tms 22320  df-cncf 22874  df-limc 23821  df-dv 23822  df-log 24494  df-cxp 24495  df-cht 25014  df-ppi 25017
This theorem is referenced by:  bpos  25209
  Copyright terms: Public domain W3C validator