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

Theorem bposlem9 25437
Description: Lemma for bpos 25438. 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 11648 . . . . . 6 6 ∈ ℕ0
5 4nn 11442 . . . . . 6 4 ∈ ℕ
64, 5decnncl 11849 . . . . 5 64 ∈ ℕ
76a1i 11 . . . 4 (𝜑64 ∈ ℕ)
8 bposlem9.3 . . . 4 (𝜑𝑁 ∈ ℕ)
9 ere 15198 . . . . . . . 8 e ∈ ℝ
10 8re 11459 . . . . . . . 8 8 ∈ ℝ
11 egt2lt3 15315 . . . . . . . . . 10 (2 < e ∧ e < 3)
1211simpri 481 . . . . . . . . 9 e < 3
13 3lt8 11561 . . . . . . . . 9 3 < 8
14 3re 11438 . . . . . . . . . 10 3 ∈ ℝ
159, 14, 10lttri 10489 . . . . . . . . 9 ((e < 3 ∧ 3 < 8) → e < 8)
1612, 13, 15mp2an 683 . . . . . . . 8 e < 8
179, 10, 16ltleii 10486 . . . . . . 7 e ≤ 8
18 0re 10365 . . . . . . . . 9 0 ∈ ℝ
19 epos 15316 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 10486 . . . . . . . 8 0 ≤ e
21 8pos 11477 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 10486 . . . . . . . 8 0 ≤ 8
23 le2sq 13239 . . . . . . . 8 (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
249, 20, 10, 22, 23mp4an 684 . . . . . . 7 (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
2517, 24mpbi 222 . . . . . 6 (e↑2) ≤ (8↑2)
2610recni 10378 . . . . . . . 8 8 ∈ ℂ
2726sqvali 13244 . . . . . . 7 (8↑2) = (8 · 8)
28 8t8e64 11951 . . . . . . 7 (8 · 8) = 64
2927, 28eqtri 2849 . . . . . 6 (8↑2) = 64
3025, 29breqtri 4900 . . . . 5 (e↑2) ≤ 64
3130a1i 11 . . . 4 (𝜑 → (e↑2) ≤ 64)
329resqcli 13250 . . . . . 6 (e↑2) ∈ ℝ
3332a1i 11 . . . . 5 (𝜑 → (e↑2) ∈ ℝ)
346nnrei 11367 . . . . . 6 64 ∈ ℝ
3534a1i 11 . . . . 5 (𝜑64 ∈ ℝ)
368nnred 11374 . . . . 5 (𝜑𝑁 ∈ ℝ)
37 ltle 10452 . . . . . . 7 ((64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (64 < 𝑁64 ≤ 𝑁))
3834, 36, 37sylancr 581 . . . . . 6 (𝜑 → (64 < 𝑁64 ≤ 𝑁))
391, 38mpd 15 . . . . 5 (𝜑64 ≤ 𝑁)
4033, 35, 36, 31, 39letrd 10520 . . . 4 (𝜑 → (e↑2) ≤ 𝑁)
412, 3, 7, 8, 31, 40bposlem7 25435 . . 3 (𝜑 → (64 < 𝑁 → (𝐹𝑁) < (𝐹64)))
421, 41mpd 15 . 2 (𝜑 → (𝐹𝑁) < (𝐹64))
432, 3bposlem8 25436 . . . . 5 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
4443a1i 11 . . . 4 (𝜑 → ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2)))
4544simpld 490 . . 3 (𝜑 → (𝐹64) ∈ ℝ)
46 2fveq3 6442 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
4746oveq2d 6926 . . . . . . . 8 (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
48 fvoveq1 6933 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
4948oveq2d 6926 . . . . . . . 8 (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
5047, 49oveq12d 6928 . . . . . . 7 (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
51 oveq2 6918 . . . . . . . . 9 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
5251fveq2d 6441 . . . . . . . 8 (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
5352oveq2d 6926 . . . . . . 7 (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
5450, 53oveq12d 6928 . . . . . 6 (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
55 ovex 6942 . . . . . 6 ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
5654, 2, 55fvmpt 6533 . . . . 5 (𝑁 ∈ ℕ → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
578, 56syl 17 . . . 4 (𝜑 → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
58 sqrt2re 15360 . . . . . . 7 (√‘2) ∈ ℝ
598nnrpd 12161 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ+)
6059rpsqrtcld 14534 . . . . . . . . 9 (𝜑 → (√‘𝑁) ∈ ℝ+)
61 fveq2 6437 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
62 id 22 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
6361, 62oveq12d 6928 . . . . . . . . . 10 (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
64 ovex 6942 . . . . . . . . . 10 ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
6563, 3, 64fvmpt 6533 . . . . . . . . 9 ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6660, 65syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6760relogcld 24775 . . . . . . . . 9 (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
6867, 60rerpdivcld 12194 . . . . . . . 8 (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
6966, 68eqeltrd 2906 . . . . . . 7 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
70 remulcl 10344 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
7158, 69, 70sylancr 581 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
72 9re 11463 . . . . . . . 8 9 ∈ ℝ
73 4re 11443 . . . . . . . 8 4 ∈ ℝ
74 4ne0 11473 . . . . . . . 8 4 ≠ 0
7572, 73, 74redivcli 11125 . . . . . . 7 (9 / 4) ∈ ℝ
7659rphalfcld 12175 . . . . . . . . 9 (𝜑 → (𝑁 / 2) ∈ ℝ+)
77 fveq2 6437 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
78 id 22 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
7977, 78oveq12d 6928 . . . . . . . . . 10 (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
80 ovex 6942 . . . . . . . . . 10 ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
8179, 3, 80fvmpt 6533 . . . . . . . . 9 ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8276, 81syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8376relogcld 24775 . . . . . . . . 9 (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
8483, 76rerpdivcld 12194 . . . . . . . 8 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
8582, 84eqeltrd 2906 . . . . . . 7 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
86 remulcl 10344 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8775, 85, 86sylancr 581 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8871, 87readdcld 10393 . . . . 5 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
89 2rp 12124 . . . . . . 7 2 ∈ ℝ+
90 relogcl 24728 . . . . . . 7 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
9189, 90ax-mp 5 . . . . . 6 (log‘2) ∈ ℝ
92 rpmulcl 12144 . . . . . . . 8 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
9389, 59, 92sylancr 581 . . . . . . 7 (𝜑 → (2 · 𝑁) ∈ ℝ+)
9493rpsqrtcld 14534 . . . . . 6 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
95 rerpdivcl 12151 . . . . . 6 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9691, 94, 95sylancr 581 . . . . 5 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9788, 96readdcld 10393 . . . 4 (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
9857, 97eqeltrd 2906 . . 3 (𝜑 → (𝐹𝑁) ∈ ℝ)
9991a1i 11 . . . 4 (𝜑 → (log‘2) ∈ ℝ)
10044simprd 491 . . . 4 (𝜑 → (𝐹64) < (log‘2))
101 nnrp 12132 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
1025, 101ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
103 relogcl 24728 . . . . . . . . . 10 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
104102, 103ax-mp 5 . . . . . . . . 9 (log‘4) ∈ ℝ
105 remulcl 10344 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
10636, 104, 105sylancl 580 . . . . . . . 8 (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
10759relogcld 24775 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
108106, 107resubcld 10789 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
109 rpre 12127 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
110 rpge0 12134 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
111109, 110resqrtcld 14540 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
11293, 111syl 17 . . . . . . . . . . 11 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
113 3nn 11437 . . . . . . . . . . 11 3 ∈ ℕ
114 nndivre 11399 . . . . . . . . . . 11 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
115112, 113, 114sylancl 580 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
116 2re 11432 . . . . . . . . . 10 2 ∈ ℝ
117 readdcl 10342 . . . . . . . . . 10 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
118115, 116, 117sylancl 580 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
11993relogcld 24775 . . . . . . . . 9 (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
120118, 119remulcld 10394 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
121 remulcl 10344 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
12273, 36, 121sylancr 581 . . . . . . . . . . 11 (𝜑 → (4 · 𝑁) ∈ ℝ)
123 nndivre 11399 . . . . . . . . . . 11 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
124122, 113, 123sylancl 580 . . . . . . . . . 10 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
125 5re 11447 . . . . . . . . . 10 5 ∈ ℝ
126 resubcl 10673 . . . . . . . . . 10 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
127124, 125, 126sylancl 580 . . . . . . . . 9 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
128 remulcl 10344 . . . . . . . . 9 (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
129127, 91, 128sylancl 580 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
130120, 129readdcld 10393 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
131 remulcl 10344 . . . . . . . . 9 ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
132124, 91, 131sylancl 580 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
133132, 107resubcld 10789 . . . . . . 7 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
1348nnzd 11816 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
135 df-5 11424 . . . . . . . . . . . 12 5 = (4 + 1)
13673a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
137 6nn 11450 . . . . . . . . . . . . . . . 16 6 ∈ ℕ
138 4nn0 11646 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
139 4lt10 11966 . . . . . . . . . . . . . . . 16 4 < 10
140137, 138, 138, 139declti 11867 . . . . . . . . . . . . . . 15 4 < 64
141140a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 < 64)
142136, 35, 36, 141, 1lttrd 10524 . . . . . . . . . . . . 13 (𝜑 → 4 < 𝑁)
143 4z 11746 . . . . . . . . . . . . . 14 4 ∈ ℤ
144 zltp1le 11762 . . . . . . . . . . . . . 14 ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
145143, 134, 144sylancr 581 . . . . . . . . . . . . 13 (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
146142, 145mpbid 224 . . . . . . . . . . . 12 (𝜑 → (4 + 1) ≤ 𝑁)
147135, 146syl5eqbr 4910 . . . . . . . . . . 11 (𝜑 → 5 ≤ 𝑁)
148 5nn 11446 . . . . . . . . . . . . 13 5 ∈ ℕ
149148nnzi 11736 . . . . . . . . . . . 12 5 ∈ ℤ
150149eluz1i 11983 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
151134, 147, 150sylanbrc 578 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘5))
152 bposlem9.5 . . . . . . . . . . 11 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
153 breq2 4879 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑁 < 𝑝𝑁 < 𝑞))
154 breq1 4878 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
155153, 154anbi12d 624 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁))))
156155cbvrexv 3384 . . . . . . . . . . 11 (∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
157152, 156sylnib 320 . . . . . . . . . 10 (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
158 eqid 2825 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
159 eqid 2825 . . . . . . . . . 10 (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
160 eqid 2825 . . . . . . . . . 10 (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
161151, 157, 158, 159, 160bposlem6 25434 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
162 reexplog 24747 . . . . . . . . . . . 12 ((4 ∈ ℝ+𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
163102, 134, 162sylancr 581 . . . . . . . . . . 11 (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
16459reeflogd 24776 . . . . . . . . . . . 12 (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
165164eqcomd 2831 . . . . . . . . . . 11 (𝜑𝑁 = (exp‘(log‘𝑁)))
166163, 165oveq12d 6928 . . . . . . . . . 10 (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
167106recnd 10392 . . . . . . . . . . 11 (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
168107recnd 10392 . . . . . . . . . . 11 (𝜑 → (log‘𝑁) ∈ ℂ)
169 efsub 15209 . . . . . . . . . . 11 (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
170167, 168, 169syl2anc 579 . . . . . . . . . 10 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
171166, 170eqtr4d 2864 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
17293rpcnd 12165 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℂ)
17393rpne0d 12168 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ≠ 0)
174118recnd 10392 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
175172, 173, 174cxpefd 24864 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
176 2cn 11433 . . . . . . . . . . . 12 2 ∈ ℂ
177 2ne0 11469 . . . . . . . . . . . 12 2 ≠ 0
178127recnd 10392 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
179 cxpef 24817 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
180176, 177, 178, 179mp3an12i 1593 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
181175, 180oveq12d 6928 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
182120recnd 10392 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
183129recnd 10392 . . . . . . . . . . 11 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
184 efadd 15203 . . . . . . . . . . 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)))))
185182, 183, 184syl2anc 579 . . . . . . . . . 10 (𝜑 → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
186181, 185eqtr4d 2864 . . . . . . . . 9 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
187161, 171, 1863brtr3d 4906 . . . . . . . 8 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188 eflt 15226 . . . . . . . . 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))))))
189108, 130, 188syl2anc 579 . . . . . . . 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))))))
190187, 189mpbird 249 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
191108, 130, 133, 190ltsub1dd 10971 . . . . . 6 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
19236recnd 10392 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
193 mulcom 10345 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
194176, 192, 193sylancr 581 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 · 2))
195194oveq1d 6925 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
19691recni 10378 . . . . . . . . . . . 12 (log‘2) ∈ ℂ
197 mulass 10347 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
198176, 196, 197mp3an23 1581 . . . . . . . . . . 11 (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
199192, 198syl 17 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
2001962timesi 11503 . . . . . . . . . . . 12 (2 · (log‘2)) = ((log‘2) + (log‘2))
201 relogmul 24744 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
20289, 89, 201mp2an 683 . . . . . . . . . . . 12 (log‘(2 · 2)) = ((log‘2) + (log‘2))
203 2t2e4 11529 . . . . . . . . . . . . 13 (2 · 2) = 4
204203fveq2i 6440 . . . . . . . . . . . 12 (log‘(2 · 2)) = (log‘4)
205200, 202, 2043eqtr2i 2855 . . . . . . . . . . 11 (2 · (log‘2)) = (log‘4)
206205oveq2i 6921 . . . . . . . . . 10 (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
207199, 206syl6eq 2877 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
208195, 207eqtrd 2861 . . . . . . . 8 (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
209208oveq1d 6925 . . . . . . 7 (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
210124recnd 10392 . . . . . . . . . 10 (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
211 3rp 12125 . . . . . . . . . . . 12 3 ∈ ℝ+
212 rpdivcl 12146 . . . . . . . . . . . 12 (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
21393, 211, 212sylancl 580 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
214213rpcnd 12165 . . . . . . . . . 10 (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
215 4p2e6 11518 . . . . . . . . . . . . . 14 (4 + 2) = 6
216215oveq1i 6920 . . . . . . . . . . . . 13 ((4 + 2) · 𝑁) = (6 · 𝑁)
217 4cn 11444 . . . . . . . . . . . . . 14 4 ∈ ℂ
218 adddir 10354 . . . . . . . . . . . . . 14 ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
219217, 176, 192, 218mp3an12i 1593 . . . . . . . . . . . . 13 (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
220216, 219syl5eqr 2875 . . . . . . . . . . . 12 (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
221220oveq1d 6925 . . . . . . . . . . 11 (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
222 6cn 11452 . . . . . . . . . . . . . 14 6 ∈ ℂ
223 3cn 11439 . . . . . . . . . . . . . . 15 3 ∈ ℂ
224 3ne0 11471 . . . . . . . . . . . . . . 15 3 ≠ 0
225223, 224pm3.2i 464 . . . . . . . . . . . . . 14 (3 ∈ ℂ ∧ 3 ≠ 0)
226 div23 11036 . . . . . . . . . . . . . 14 ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
227222, 225, 226mp3an13 1580 . . . . . . . . . . . . 13 (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
228192, 227syl 17 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
229 3t2e6 11531 . . . . . . . . . . . . . . 15 (3 · 2) = 6
230229oveq1i 6920 . . . . . . . . . . . . . 14 ((3 · 2) / 3) = (6 / 3)
231176, 223, 224divcan3i 11104 . . . . . . . . . . . . . 14 ((3 · 2) / 3) = 2
232230, 231eqtr3i 2851 . . . . . . . . . . . . 13 (6 / 3) = 2
233232oveq1i 6920 . . . . . . . . . . . 12 ((6 / 3) · 𝑁) = (2 · 𝑁)
234228, 233syl6eq 2877 . . . . . . . . . . 11 (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
235122recnd 10392 . . . . . . . . . . . 12 (𝜑 → (4 · 𝑁) ∈ ℂ)
236 remulcl 10344 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
237116, 36, 236sylancr 581 . . . . . . . . . . . . 13 (𝜑 → (2 · 𝑁) ∈ ℝ)
238237recnd 10392 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℂ)
239 divdir 11042 . . . . . . . . . . . . 13 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240225, 239mp3an3 1578 . . . . . . . . . . . 12 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
241235, 238, 240syl2anc 579 . . . . . . . . . . 11 (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
242221, 234, 2413eqtr3d 2869 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
243210, 214, 242mvrladdd 10774 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
244243oveq1d 6925 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
24599recnd 10392 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℂ)
246238, 210, 245subdird 10818 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
247244, 246eqtr3d 2863 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
248132recnd 10392 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
249167, 248, 168nnncan2d 10755 . . . . . . 7 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
250209, 247, 2493eqtr4d 2871 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
251115recnd 10392 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
252176a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
253119recnd 10392 . . . . . . . . . 10 (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
254251, 252, 253adddird 10389 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
255 relogmul 24744 . . . . . . . . . . . . 13 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
25689, 59, 255sylancr 581 . . . . . . . . . . . 12 (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
257256oveq2d 6926 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
258252, 245, 168adddid 10388 . . . . . . . . . . 11 (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
259257, 258eqtrd 2861 . . . . . . . . . 10 (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
260259oveq2d 6926 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
261254, 260eqtrd 2861 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
262 5cn 11448 . . . . . . . . . . . 12 5 ∈ ℂ
263262a1i 11 . . . . . . . . . . 11 (𝜑 → 5 ∈ ℂ)
264210, 263, 245subdird 10818 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
265264oveq1d 6925 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
266262, 196mulcli 10371 . . . . . . . . . . 11 (5 · (log‘2)) ∈ ℂ
267266a1i 11 . . . . . . . . . 10 (𝜑 → (5 · (log‘2)) ∈ ℂ)
268248, 267, 168nnncan1d 10754 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
269265, 268eqtrd 2861 . . . . . . . 8 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
270261, 269oveq12d 6928 . . . . . . 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)))))
271133recnd 10392 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
272182, 183, 271addsubassd 10740 . . . . . . 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‘𝑁)))))
273262, 223, 196subdiri 10811 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
274 3p2e5 11516 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
275274oveq1i 6920 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = (5 − 3)
276 pncan2 10615 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
277223, 176, 276mp2an 683 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = 2
278275, 277eqtr3i 2851 . . . . . . . . . . . . . 14 (5 − 3) = 2
279278oveq1i 6920 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = (2 · (log‘2))
280273, 279eqtr3i 2851 . . . . . . . . . . . 12 ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
281280a1i 11 . . . . . . . . . . 11 (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
282 mulcl 10343 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
283176, 168, 282sylancr 581 . . . . . . . . . . . 12 (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
284 df-3 11422 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
285284oveq1i 6920 . . . . . . . . . . . . . . 15 (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
286 1cnd 10358 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
287252, 286, 168adddird 10389 . . . . . . . . . . . . . . 15 (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
288285, 287syl5eq 2873 . . . . . . . . . . . . . 14 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
289168mulid2d 10382 . . . . . . . . . . . . . . 15 (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
290289oveq2d 6926 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
291288, 290eqtrd 2861 . . . . . . . . . . . . 13 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
292291oveq1d 6925 . . . . . . . . . . . 12 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
293283, 168, 267, 292assraddsubd 10775 . . . . . . . . . . 11 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
294281, 293oveq12d 6928 . . . . . . . . . 10 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
295 relogdiv 24745 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
29659, 89, 295sylancl 580 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
297296oveq2d 6926 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
298 subdi 10794 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
299223, 196, 298mp3an13 1580 . . . . . . . . . . . . 13 ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
300168, 299syl 17 . . . . . . . . . . . 12 (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
301297, 300eqtrd 2861 . . . . . . . . . . 11 (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
302 div23 11036 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
303176, 225, 302mp3an13 1580 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
304192, 303syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
305223, 176, 223, 176, 177, 177divmuldivi 11118 . . . . . . . . . . . . . . . . 17 ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
306 3t3e9 11532 . . . . . . . . . . . . . . . . . 18 (3 · 3) = 9
307306, 203oveq12i 6922 . . . . . . . . . . . . . . . . 17 ((3 · 3) / (2 · 2)) = (9 / 4)
308305, 307eqtr2i 2850 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) · (3 / 2))
309308a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
310304, 309oveq12d 6928 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
311176, 223, 224divcli 11100 . . . . . . . . . . . . . . 15 (2 / 3) ∈ ℂ
312223, 176, 177divcli 11100 . . . . . . . . . . . . . . . 16 (3 / 2) ∈ ℂ
313 mul4 10531 . . . . . . . . . . . . . . . 16 ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
314312, 312, 313mpanr12 696 . . . . . . . . . . . . . . 15 (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
315311, 192, 314sylancr 581 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
316 divcan6 11065 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
317176, 177, 223, 224, 316mp4an 684 . . . . . . . . . . . . . . . . 17 ((2 / 3) · (3 / 2)) = 1
318317oveq1i 6920 . . . . . . . . . . . . . . . 16 (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
319 mulcl 10343 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
320192, 312, 319sylancl 580 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
321320mulid2d 10382 . . . . . . . . . . . . . . . 16 (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
322318, 321syl5eq 2873 . . . . . . . . . . . . . . 15 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
323 2cnne0 11575 . . . . . . . . . . . . . . . . 17 (2 ∈ ℂ ∧ 2 ≠ 0)
324 div12 11039 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
325223, 323, 324mp3an23 1581 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
326192, 325syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
327322, 326eqtrd 2861 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
328310, 315, 3273eqtrd 2865 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
329328, 82oveq12d 6928 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
33075recni 10378 . . . . . . . . . . . . . 14 (9 / 4) ∈ ℂ
331330a1i 11 . . . . . . . . . . . . 13 (𝜑 → (9 / 4) ∈ ℂ)
33285recnd 10392 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
333214, 331, 332mulassd 10387 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
334223a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 3 ∈ ℂ)
33576rpcnd 12165 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 / 2) ∈ ℂ)
33683recnd 10392 . . . . . . . . . . . . . . 15 (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
33776rpne0d 12168 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 / 2) ≠ 0)
338336, 335, 337divcld 11134 . . . . . . . . . . . . . 14 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
339334, 335, 338mulassd 10387 . . . . . . . . . . . . 13 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
340336, 335, 337divcan2d 11136 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
341340oveq2d 6926 . . . . . . . . . . . . 13 (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
342339, 341eqtrd 2861 . . . . . . . . . . . 12 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
343329, 333, 3423eqtr3d 2869 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
344223, 196mulcli 10371 . . . . . . . . . . . . 13 (3 · (log‘2)) ∈ ℂ
345344a1i 11 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘2)) ∈ ℂ)
346 mulcl 10343 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
347223, 168, 346sylancr 581 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
348267, 345, 347npncan3d 10756 . . . . . . . . . . 11 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
349301, 343, 3483eqtr4d 2871 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
350116, 91remulcli 10380 . . . . . . . . . . . . 13 (2 · (log‘2)) ∈ ℝ
351350recni 10378 . . . . . . . . . . . 12 (2 · (log‘2)) ∈ ℂ
352351a1i 11 . . . . . . . . . . 11 (𝜑 → (2 · (log‘2)) ∈ ℂ)
353 subcl 10607 . . . . . . . . . . . 12 (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
354168, 266, 353sylancl 580 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
355352, 283, 354addassd 10386 . . . . . . . . . 10 (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
356294, 349, 3553eqtr4d 2871 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
357356oveq2d 6926 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
358 mulcl 10343 . . . . . . . . . . 11 ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
359251, 196, 358sylancl 580 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
360251, 168mulcld 10384 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
36187recnd 10392 . . . . . . . . . . 11 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
362214, 361mulcld 10384 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
363359, 360, 362addassd 10386 . . . . . . . . 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)))))))
364256oveq2d 6926 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
365251, 245, 168adddid 10388 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
366364, 365eqtrd 2861 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
367366oveq1d 6925 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
36857oveq2d 6926 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
36988recnd 10392 . . . . . . . . . . . 12 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
37096recnd 10392 . . . . . . . . . . . 12 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
371214, 369, 370adddid 10388 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
372368, 371eqtrd 2861 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
37371recnd 10392 . . . . . . . . . . . . 13 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
374214, 373, 361adddid 10388 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
37593rpge0d 12167 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (2 · 𝑁))
376 remsqsqrt 14381 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
377237, 375, 376syl2anc 579 . . . . . . . . . . . . . . . . 17 (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
378377oveq1d 6925 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
379112recnd 10392 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
380224a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
381379, 379, 334, 380div23d 11171 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
382378, 381eqtr3d 2863 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
383382oveq1d 6925 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
384251, 379, 373mulassd 10387 . . . . . . . . . . . . . 14 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
385 0le2 11467 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
386116, 385pm3.2i 464 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ ∧ 0 ≤ 2)
38759rprege0d 12170 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
388 sqrtmul 14384 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
389386, 387, 388sylancr 581 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
390389oveq1d 6925 . . . . . . . . . . . . . . . 16 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
39158recni 10378 . . . . . . . . . . . . . . . . . 18 (√‘2) ∈ ℂ
392391a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘2) ∈ ℂ)
39360rpcnd 12165 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘𝑁) ∈ ℂ)
39469recnd 10392 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
395392, 393, 392, 394mul4d 10574 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
396 remsqsqrt 14381 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
397116, 385, 396mp2an 683 . . . . . . . . . . . . . . . . . . 19 ((√‘2) · (√‘2)) = 2
398397a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘2) · (√‘2)) = 2)
39966oveq2d 6926 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
40067recnd 10392 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
40160rpne0d 12168 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑁) ≠ 0)
402400, 393, 401divcan2d 11136 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
403399, 402eqtrd 2861 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
404398, 403oveq12d 6928 . . . . . . . . . . . . . . . . 17 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
4054002timesd 11608 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
40660, 60relogmuld 24777 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
407 remsqsqrt 14381 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
408387, 407syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
409408fveq2d 6441 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
410406, 409eqtr3d 2863 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
411404, 405, 4103eqtrd 2865 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
412390, 395, 4113eqtrd 2865 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
413412oveq2d 6926 . . . . . . . . . . . . . 14 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
414383, 384, 4133eqtrd 2865 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
415414oveq1d 6925 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
416374, 415eqtrd 2861 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
417382oveq1d 6925 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
418251, 379, 370mulassd 10387 . . . . . . . . . . . 12 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
41994rpne0d 12168 . . . . . . . . . . . . . 14 (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
420245, 379, 419divcan2d 11136 . . . . . . . . . . . . 13 (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
421420oveq2d 6926 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
422417, 418, 4213eqtrd 2865 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
423416, 422oveq12d 6928 . . . . . . . . . 10 (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
424360, 362addcld 10383 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
425424, 359addcomd 10564 . . . . . . . . . 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)))))))
426372, 423, 4253eqtrd 2865 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
427363, 367, 4263eqtr4rd 2872 . . . . . . . 8 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
428251, 253mulcld 10384 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
429 addcl 10341 . . . . . . . . . 10 (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
430351, 283, 429sylancr 581 . . . . . . . . 9 (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
431428, 430, 354addassd 10386 . . . . . . . 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))))))
432357, 427, 4313eqtr4d 2871 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
433270, 272, 4323eqtr4rd 2872 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
434191, 250, 4333brtr4d 4907 . . . . 5 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁)))
43599, 98, 213ltmul2d 12205 . . . . 5 (𝜑 → ((log‘2) < (𝐹𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁))))
436434, 435mpbird 249 . . . 4 (𝜑 → (log‘2) < (𝐹𝑁))
43745, 99, 98, 100, 436lttrd 10524 . . 3 (𝜑 → (𝐹64) < (𝐹𝑁))
43845, 98, 437ltnsymd 10512 . 2 (𝜑 → ¬ (𝐹𝑁) < (𝐹64))
43942, 438pm2.21dd 187 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1656  wcel 2164  wne 2999  wrex 3118  ifcif 4308   class class class wbr 4875  cmpt 4954  cfv 6127  (class class class)co 6910  cc 10257  cr 10258  0cc0 10259  1c1 10260   + caddc 10262   · cmul 10264   < clt 10398  cle 10399  cmin 10592   / cdiv 11016  cn 11357  2c2 11413  3c3 11414  4c4 11415  5c5 11416  6c6 11417  8c8 11419  9c9 11420  cz 11711  cdc 11828  cuz 11975  +crp 12119  cfl 12893  cexp 13161  Ccbc 13389  csqrt 14357  expce 15171  eceu 15172  cprime 15764   pCnt cpc 15919  logclog 24707  𝑐ccxp 24708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-inf2 8822  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336  ax-pre-sup 10337  ax-addf 10338  ax-mulf 10339
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-iin 4745  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-of 7162  df-om 7332  df-1st 7433  df-2nd 7434  df-supp 7565  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-2o 7832  df-oadd 7835  df-er 8014  df-map 8129  df-pm 8130  df-ixp 8182  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-fsupp 8551  df-fi 8592  df-sup 8623  df-inf 8624  df-oi 8691  df-card 9085  df-cda 9312  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-div 11017  df-nn 11358  df-2 11421  df-3 11422  df-4 11423  df-5 11424  df-6 11425  df-7 11426  df-8 11427  df-9 11428  df-n0 11626  df-xnn0 11698  df-z 11712  df-dec 11829  df-uz 11976  df-q 12079  df-rp 12120  df-xneg 12239  df-xadd 12240  df-xmul 12241  df-ioo 12474  df-ioc 12475  df-ico 12476  df-icc 12477  df-fz 12627  df-fzo 12768  df-fl 12895  df-mod 12971  df-seq 13103  df-exp 13162  df-fac 13361  df-bc 13390  df-hash 13418  df-shft 14191  df-cj 14223  df-re 14224  df-im 14225  df-sqrt 14359  df-abs 14360  df-limsup 14586  df-clim 14603  df-rlim 14604  df-sum 14801  df-ef 15177  df-e 15178  df-sin 15179  df-cos 15180  df-pi 15182  df-dvds 15365  df-gcd 15597  df-prm 15765  df-pc 15920  df-struct 16231  df-ndx 16232  df-slot 16233  df-base 16235  df-sets 16236  df-ress 16237  df-plusg 16325  df-mulr 16326  df-starv 16327  df-sca 16328  df-vsca 16329  df-ip 16330  df-tset 16331  df-ple 16332  df-ds 16334  df-unif 16335  df-hom 16336  df-cco 16337  df-rest 16443  df-topn 16444  df-0g 16462  df-gsum 16463  df-topgen 16464  df-pt 16465  df-prds 16468  df-xrs 16522  df-qtop 16527  df-imas 16528  df-xps 16530  df-mre 16606  df-mrc 16607  df-acs 16609  df-mgm 17602  df-sgrp 17644  df-mnd 17655  df-submnd 17696  df-mulg 17902  df-cntz 18107  df-cmn 18555  df-psmet 20105  df-xmet 20106  df-met 20107  df-bl 20108  df-mopn 20109  df-fbas 20110  df-fg 20111  df-cnfld 20114  df-top 21076  df-topon 21093  df-topsp 21115  df-bases 21128  df-cld 21201  df-ntr 21202  df-cls 21203  df-nei 21280  df-lp 21318  df-perf 21319  df-cn 21409  df-cnp 21410  df-haus 21497  df-tx 21743  df-hmeo 21936  df-fil 22027  df-fm 22119  df-flim 22120  df-flf 22121  df-xms 22502  df-ms 22503  df-tms 22504  df-cncf 23058  df-limc 24036  df-dv 24037  df-log 24709  df-cxp 24710  df-cht 25243  df-ppi 25246
This theorem is referenced by:  bpos  25438
  Copyright terms: Public domain W3C validator