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

Theorem bposlem9 25227
Description: Lemma for bpos 25228. 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 11576 . . . . . 6 6 ∈ ℕ0
5 4nn 11460 . . . . . 6 4 ∈ ℕ
64, 5decnncl 11775 . . . . 5 64 ∈ ℕ
76a1i 11 . . . 4 (𝜑64 ∈ ℕ)
8 bposlem9.3 . . . 4 (𝜑𝑁 ∈ ℕ)
9 ere 15035 . . . . . . . 8 e ∈ ℝ
10 8re 11385 . . . . . . . 8 8 ∈ ℝ
11 egt2lt3 15150 . . . . . . . . . 10 (2 < e ∧ e < 3)
1211simpri 475 . . . . . . . . 9 e < 3
13 3lt8 11491 . . . . . . . . 9 3 < 8
14 3re 11374 . . . . . . . . . 10 3 ∈ ℝ
159, 14, 10lttri 10444 . . . . . . . . 9 ((e < 3 ∧ 3 < 8) → e < 8)
1612, 13, 15mp2an 675 . . . . . . . 8 e < 8
179, 10, 16ltleii 10441 . . . . . . 7 e ≤ 8
18 0re 10323 . . . . . . . . 9 0 ∈ ℝ
19 epos 15151 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 10441 . . . . . . . 8 0 ≤ e
21 8pos 11400 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 10441 . . . . . . . 8 0 ≤ 8
23 le2sq 13157 . . . . . . . 8 (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
249, 20, 10, 22, 23mp4an 676 . . . . . . 7 (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
2517, 24mpbi 221 . . . . . 6 (e↑2) ≤ (8↑2)
2610recni 10335 . . . . . . . 8 8 ∈ ℂ
2726sqvali 13162 . . . . . . 7 (8↑2) = (8 · 8)
28 8t8e64 11876 . . . . . . 7 (8 · 8) = 64
2927, 28eqtri 2828 . . . . . 6 (8↑2) = 64
3025, 29breqtri 4869 . . . . 5 (e↑2) ≤ 64
3130a1i 11 . . . 4 (𝜑 → (e↑2) ≤ 64)
329resqcli 13168 . . . . . 6 (e↑2) ∈ ℝ
3332a1i 11 . . . . 5 (𝜑 → (e↑2) ∈ ℝ)
346nnrei 11310 . . . . . 6 64 ∈ ℝ
3534a1i 11 . . . . 5 (𝜑64 ∈ ℝ)
368nnred 11316 . . . . 5 (𝜑𝑁 ∈ ℝ)
37 ltle 10407 . . . . . . 7 ((64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (64 < 𝑁64 ≤ 𝑁))
3834, 36, 37sylancr 577 . . . . . 6 (𝜑 → (64 < 𝑁64 ≤ 𝑁))
391, 38mpd 15 . . . . 5 (𝜑64 ≤ 𝑁)
4033, 35, 36, 31, 39letrd 10475 . . . 4 (𝜑 → (e↑2) ≤ 𝑁)
412, 3, 7, 8, 31, 40bposlem7 25225 . . 3 (𝜑 → (64 < 𝑁 → (𝐹𝑁) < (𝐹64)))
421, 41mpd 15 . 2 (𝜑 → (𝐹𝑁) < (𝐹64))
432, 3bposlem8 25226 . . . . 5 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
4443a1i 11 . . . 4 (𝜑 → ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2)))
4544simpld 484 . . 3 (𝜑 → (𝐹64) ∈ ℝ)
46 2fveq3 6409 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
4746oveq2d 6886 . . . . . . . 8 (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
48 fvoveq1 6893 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
4948oveq2d 6886 . . . . . . . 8 (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
5047, 49oveq12d 6888 . . . . . . 7 (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
51 oveq2 6878 . . . . . . . . 9 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
5251fveq2d 6408 . . . . . . . 8 (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
5352oveq2d 6886 . . . . . . 7 (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
5450, 53oveq12d 6888 . . . . . 6 (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
55 ovex 6902 . . . . . 6 ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
5654, 2, 55fvmpt 6499 . . . . 5 (𝑁 ∈ ℕ → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
578, 56syl 17 . . . 4 (𝜑 → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
58 sqrt2re 15196 . . . . . . 7 (√‘2) ∈ ℝ
598nnrpd 12080 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ+)
6059rpsqrtcld 14369 . . . . . . . . 9 (𝜑 → (√‘𝑁) ∈ ℝ+)
61 fveq2 6404 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
62 id 22 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
6361, 62oveq12d 6888 . . . . . . . . . 10 (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
64 ovex 6902 . . . . . . . . . 10 ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
6563, 3, 64fvmpt 6499 . . . . . . . . 9 ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6660, 65syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6760relogcld 24579 . . . . . . . . 9 (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
6867, 60rerpdivcld 12113 . . . . . . . 8 (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
6966, 68eqeltrd 2885 . . . . . . 7 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
70 remulcl 10302 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
7158, 69, 70sylancr 577 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
72 9re 11387 . . . . . . . 8 9 ∈ ℝ
73 4re 11377 . . . . . . . 8 4 ∈ ℝ
74 4ne0 11396 . . . . . . . 8 4 ≠ 0
7572, 73, 74redivcli 11073 . . . . . . 7 (9 / 4) ∈ ℝ
7659rphalfcld 12094 . . . . . . . . 9 (𝜑 → (𝑁 / 2) ∈ ℝ+)
77 fveq2 6404 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
78 id 22 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
7977, 78oveq12d 6888 . . . . . . . . . 10 (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
80 ovex 6902 . . . . . . . . . 10 ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
8179, 3, 80fvmpt 6499 . . . . . . . . 9 ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8276, 81syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8376relogcld 24579 . . . . . . . . 9 (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
8483, 76rerpdivcld 12113 . . . . . . . 8 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
8582, 84eqeltrd 2885 . . . . . . 7 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
86 remulcl 10302 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8775, 85, 86sylancr 577 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8871, 87readdcld 10350 . . . . 5 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
89 2rp 12047 . . . . . . 7 2 ∈ ℝ+
90 relogcl 24532 . . . . . . 7 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
9189, 90ax-mp 5 . . . . . 6 (log‘2) ∈ ℝ
92 rpmulcl 12065 . . . . . . . 8 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
9389, 59, 92sylancr 577 . . . . . . 7 (𝜑 → (2 · 𝑁) ∈ ℝ+)
9493rpsqrtcld 14369 . . . . . 6 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
95 rerpdivcl 12071 . . . . . 6 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9691, 94, 95sylancr 577 . . . . 5 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9788, 96readdcld 10350 . . . 4 (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
9857, 97eqeltrd 2885 . . 3 (𝜑 → (𝐹𝑁) ∈ ℝ)
9991a1i 11 . . . 4 (𝜑 → (log‘2) ∈ ℝ)
10044simprd 485 . . . 4 (𝜑 → (𝐹64) < (log‘2))
101 nnrp 12052 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
1025, 101ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
103 relogcl 24532 . . . . . . . . . 10 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
104102, 103ax-mp 5 . . . . . . . . 9 (log‘4) ∈ ℝ
105 remulcl 10302 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
10636, 104, 105sylancl 576 . . . . . . . 8 (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
10759relogcld 24579 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
108106, 107resubcld 10739 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
109 rpre 12049 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
110 rpge0 12055 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
111109, 110resqrtcld 14375 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
11293, 111syl 17 . . . . . . . . . . 11 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
113 3nn 11459 . . . . . . . . . . 11 3 ∈ ℕ
114 nndivre 11338 . . . . . . . . . . 11 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
115112, 113, 114sylancl 576 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
116 2re 11370 . . . . . . . . . 10 2 ∈ ℝ
117 readdcl 10300 . . . . . . . . . 10 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
118115, 116, 117sylancl 576 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
11993relogcld 24579 . . . . . . . . 9 (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
120118, 119remulcld 10351 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
121 remulcl 10302 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
12273, 36, 121sylancr 577 . . . . . . . . . . 11 (𝜑 → (4 · 𝑁) ∈ ℝ)
123 nndivre 11338 . . . . . . . . . . 11 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
124122, 113, 123sylancl 576 . . . . . . . . . 10 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
125 5re 11379 . . . . . . . . . 10 5 ∈ ℝ
126 resubcl 10626 . . . . . . . . . 10 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
127124, 125, 126sylancl 576 . . . . . . . . 9 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
128 remulcl 10302 . . . . . . . . 9 (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
129127, 91, 128sylancl 576 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
130120, 129readdcld 10350 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
131 remulcl 10302 . . . . . . . . 9 ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
132124, 91, 131sylancl 576 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
133132, 107resubcld 10739 . . . . . . 7 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
1348nnzd 11743 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
135 df-5 11363 . . . . . . . . . . . 12 5 = (4 + 1)
13673a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
137 6nn 11462 . . . . . . . . . . . . . . . 16 6 ∈ ℕ
138 4nn0 11574 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
139 4lt10 11891 . . . . . . . . . . . . . . . 16 4 < 10
140137, 138, 138, 139declti 11793 . . . . . . . . . . . . . . 15 4 < 64
141140a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 < 64)
142136, 35, 36, 141, 1lttrd 10479 . . . . . . . . . . . . 13 (𝜑 → 4 < 𝑁)
143 4z 11673 . . . . . . . . . . . . . 14 4 ∈ ℤ
144 zltp1le 11689 . . . . . . . . . . . . . 14 ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
145143, 134, 144sylancr 577 . . . . . . . . . . . . 13 (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
146142, 145mpbid 223 . . . . . . . . . . . 12 (𝜑 → (4 + 1) ≤ 𝑁)
147135, 146syl5eqbr 4879 . . . . . . . . . . 11 (𝜑 → 5 ≤ 𝑁)
148 5nn 11461 . . . . . . . . . . . . 13 5 ∈ ℕ
149148nnzi 11663 . . . . . . . . . . . 12 5 ∈ ℤ
150149eluz1i 11908 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
151134, 147, 150sylanbrc 574 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘5))
152 bposlem9.5 . . . . . . . . . . 11 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
153 breq2 4848 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑁 < 𝑝𝑁 < 𝑞))
154 breq1 4847 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
155153, 154anbi12d 618 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁))))
156155cbvrexv 3361 . . . . . . . . . . 11 (∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
157152, 156sylnib 319 . . . . . . . . . 10 (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
158 eqid 2806 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
159 eqid 2806 . . . . . . . . . 10 (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
160 eqid 2806 . . . . . . . . . 10 (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
161151, 157, 158, 159, 160bposlem6 25224 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
162 reexplog 24551 . . . . . . . . . . . 12 ((4 ∈ ℝ+𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
163102, 134, 162sylancr 577 . . . . . . . . . . 11 (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
16459reeflogd 24580 . . . . . . . . . . . 12 (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
165164eqcomd 2812 . . . . . . . . . . 11 (𝜑𝑁 = (exp‘(log‘𝑁)))
166163, 165oveq12d 6888 . . . . . . . . . 10 (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
167106recnd 10349 . . . . . . . . . . 11 (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
168107recnd 10349 . . . . . . . . . . 11 (𝜑 → (log‘𝑁) ∈ ℂ)
169 efsub 15046 . . . . . . . . . . 11 (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
170167, 168, 169syl2anc 575 . . . . . . . . . 10 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
171166, 170eqtr4d 2843 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
17293rpcnd 12084 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℂ)
17393rpne0d 12087 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ≠ 0)
174118recnd 10349 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
175172, 173, 174cxpefd 24668 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
176 2cn 11371 . . . . . . . . . . . 12 2 ∈ ℂ
177 2ne0 11392 . . . . . . . . . . . 12 2 ≠ 0
178127recnd 10349 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
179 cxpef 24621 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
180176, 177, 178, 179mp3an12i 1582 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
181175, 180oveq12d 6888 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
182120recnd 10349 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
183129recnd 10349 . . . . . . . . . . 11 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
184 efadd 15040 . . . . . . . . . . 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 575 . . . . . . . . . 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 2843 . . . . . . . . 9 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
187161, 171, 1863brtr3d 4875 . . . . . . . 8 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188 eflt 15063 . . . . . . . . 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 575 . . . . . . . 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 248 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
191108, 130, 133, 190ltsub1dd 10920 . . . . . 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 10349 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
193 mulcom 10303 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
194176, 192, 193sylancr 577 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 · 2))
195194oveq1d 6885 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
19691recni 10335 . . . . . . . . . . . 12 (log‘2) ∈ ℂ
197 mulass 10305 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
198176, 196, 197mp3an23 1570 . . . . . . . . . . 11 (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
199192, 198syl 17 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
2001962timesi 11426 . . . . . . . . . . . 12 (2 · (log‘2)) = ((log‘2) + (log‘2))
201 relogmul 24548 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
20289, 89, 201mp2an 675 . . . . . . . . . . . 12 (log‘(2 · 2)) = ((log‘2) + (log‘2))
203 2t2e4 11451 . . . . . . . . . . . . 13 (2 · 2) = 4
204203fveq2i 6407 . . . . . . . . . . . 12 (log‘(2 · 2)) = (log‘4)
205200, 202, 2043eqtr2i 2834 . . . . . . . . . . 11 (2 · (log‘2)) = (log‘4)
206205oveq2i 6881 . . . . . . . . . 10 (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
207199, 206syl6eq 2856 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
208195, 207eqtrd 2840 . . . . . . . 8 (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
209208oveq1d 6885 . . . . . . 7 (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
210 4p2e6 11440 . . . . . . . . . . . . . . 15 (4 + 2) = 6
211210oveq1i 6880 . . . . . . . . . . . . . 14 ((4 + 2) · 𝑁) = (6 · 𝑁)
212 4cn 11378 . . . . . . . . . . . . . . 15 4 ∈ ℂ
213 adddir 10312 . . . . . . . . . . . . . . 15 ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
214212, 176, 192, 213mp3an12i 1582 . . . . . . . . . . . . . 14 (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
215211, 214syl5eqr 2854 . . . . . . . . . . . . 13 (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
216215oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
217 6cn 11382 . . . . . . . . . . . . . . 15 6 ∈ ℂ
218 3cn 11375 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
219 3ne0 11394 . . . . . . . . . . . . . . . 16 3 ≠ 0
220218, 219pm3.2i 458 . . . . . . . . . . . . . . 15 (3 ∈ ℂ ∧ 3 ≠ 0)
221 div23 10985 . . . . . . . . . . . . . . 15 ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
222217, 220, 221mp3an13 1569 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
223192, 222syl 17 . . . . . . . . . . . . 13 (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
224 3t2e6 11453 . . . . . . . . . . . . . . . 16 (3 · 2) = 6
225224oveq1i 6880 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = (6 / 3)
226176, 218, 219divcan3i 11052 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = 2
227225, 226eqtr3i 2830 . . . . . . . . . . . . . 14 (6 / 3) = 2
228227oveq1i 6880 . . . . . . . . . . . . 13 ((6 / 3) · 𝑁) = (2 · 𝑁)
229223, 228syl6eq 2856 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
230122recnd 10349 . . . . . . . . . . . . 13 (𝜑 → (4 · 𝑁) ∈ ℂ)
231 remulcl 10302 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
232116, 36, 231sylancr 577 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝑁) ∈ ℝ)
233232recnd 10349 . . . . . . . . . . . . 13 (𝜑 → (2 · 𝑁) ∈ ℂ)
234 divdir 10991 . . . . . . . . . . . . . 14 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
235220, 234mp3an3 1567 . . . . . . . . . . . . 13 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
236230, 233, 235syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
237216, 229, 2363eqtr3d 2848 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
238237oveq1d 6885 . . . . . . . . . 10 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)))
239124recnd 10349 . . . . . . . . . . 11 (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
240 3rp 12048 . . . . . . . . . . . . 13 3 ∈ ℝ+
241 rpdivcl 12066 . . . . . . . . . . . . 13 (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
24293, 240, 241sylancl 576 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
243242rpcnd 12084 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
244239, 243pncan2d 10675 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
245238, 244eqtrd 2840 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
246245oveq1d 6885 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
24799recnd 10349 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℂ)
248233, 239, 247subdird 10768 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
249246, 248eqtr3d 2842 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
250132recnd 10349 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
251167, 250, 168nnncan2d 10708 . . . . . . 7 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
252209, 249, 2513eqtr4d 2850 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
253115recnd 10349 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
254176a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
255119recnd 10349 . . . . . . . . . 10 (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
256253, 254, 255adddird 10346 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
257 relogmul 24548 . . . . . . . . . . . . 13 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
25889, 59, 257sylancr 577 . . . . . . . . . . . 12 (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
259258oveq2d 6886 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
260254, 247, 168adddid 10345 . . . . . . . . . . 11 (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
261259, 260eqtrd 2840 . . . . . . . . . 10 (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
262261oveq2d 6886 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
263256, 262eqtrd 2840 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
264 5cn 11380 . . . . . . . . . . . 12 5 ∈ ℂ
265264a1i 11 . . . . . . . . . . 11 (𝜑 → 5 ∈ ℂ)
266239, 265, 247subdird 10768 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
267266oveq1d 6885 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
268264, 196mulcli 10328 . . . . . . . . . . 11 (5 · (log‘2)) ∈ ℂ
269268a1i 11 . . . . . . . . . 10 (𝜑 → (5 · (log‘2)) ∈ ℂ)
270250, 269, 168nnncan1d 10707 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
271267, 270eqtrd 2840 . . . . . . . 8 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
272263, 271oveq12d 6888 . . . . . . 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)))))
273133recnd 10349 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
274182, 183, 273addsubassd 10693 . . . . . . 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‘𝑁)))))
275264, 218, 196subdiri 10761 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
276 3p2e5 11438 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
277276oveq1i 6880 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = (5 − 3)
278 pncan2 10569 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
279218, 176, 278mp2an 675 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = 2
280277, 279eqtr3i 2830 . . . . . . . . . . . . . 14 (5 − 3) = 2
281280oveq1i 6880 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = (2 · (log‘2))
282275, 281eqtr3i 2830 . . . . . . . . . . . 12 ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
283282a1i 11 . . . . . . . . . . 11 (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
284 df-3 11361 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
285284oveq1i 6880 . . . . . . . . . . . . . . 15 (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
286 1cnd 10316 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
287254, 286, 168adddird 10346 . . . . . . . . . . . . . . 15 (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
288285, 287syl5eq 2852 . . . . . . . . . . . . . 14 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
289168mulid2d 10339 . . . . . . . . . . . . . . 15 (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
290289oveq2d 6886 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
291288, 290eqtrd 2840 . . . . . . . . . . . . 13 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
292291oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
293 mulcl 10301 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
294176, 168, 293sylancr 577 . . . . . . . . . . . . 13 (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
295294, 168, 269addsubassd 10693 . . . . . . . . . . . 12 (𝜑 → (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
296292, 295eqtrd 2840 . . . . . . . . . . 11 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
297283, 296oveq12d 6888 . . . . . . . . . 10 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
298 relogdiv 24549 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
29959, 89, 298sylancl 576 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
300299oveq2d 6886 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
301 subdi 10744 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
302218, 196, 301mp3an13 1569 . . . . . . . . . . . . 13 ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
303168, 302syl 17 . . . . . . . . . . . 12 (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
304300, 303eqtrd 2840 . . . . . . . . . . 11 (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
305 div23 10985 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
306176, 220, 305mp3an13 1569 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
307192, 306syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
308218, 176, 218, 176, 177, 177divmuldivi 11066 . . . . . . . . . . . . . . . . 17 ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
309 3t3e9 11454 . . . . . . . . . . . . . . . . . 18 (3 · 3) = 9
310309, 203oveq12i 6882 . . . . . . . . . . . . . . . . 17 ((3 · 3) / (2 · 2)) = (9 / 4)
311308, 310eqtr2i 2829 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) · (3 / 2))
312311a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
313307, 312oveq12d 6888 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
314176, 218, 219divcli 11048 . . . . . . . . . . . . . . 15 (2 / 3) ∈ ℂ
315218, 176, 177divcli 11048 . . . . . . . . . . . . . . . 16 (3 / 2) ∈ ℂ
316 mul4 10486 . . . . . . . . . . . . . . . 16 ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
317315, 315, 316mpanr12 688 . . . . . . . . . . . . . . 15 (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
318314, 192, 317sylancr 577 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
319 divcan6 11013 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
320176, 177, 218, 219, 319mp4an 676 . . . . . . . . . . . . . . . . 17 ((2 / 3) · (3 / 2)) = 1
321320oveq1i 6880 . . . . . . . . . . . . . . . 16 (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
322 mulcl 10301 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
323192, 315, 322sylancl 576 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
324323mulid2d 10339 . . . . . . . . . . . . . . . 16 (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
325321, 324syl5eq 2852 . . . . . . . . . . . . . . 15 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
326 2cnne0 11505 . . . . . . . . . . . . . . . . 17 (2 ∈ ℂ ∧ 2 ≠ 0)
327 div12 10988 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
328218, 326, 327mp3an23 1570 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
329192, 328syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
330325, 329eqtrd 2840 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
331313, 318, 3303eqtrd 2844 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
332331, 82oveq12d 6888 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
33375recni 10335 . . . . . . . . . . . . . 14 (9 / 4) ∈ ℂ
334333a1i 11 . . . . . . . . . . . . 13 (𝜑 → (9 / 4) ∈ ℂ)
33585recnd 10349 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
336243, 334, 335mulassd 10344 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
337218a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 3 ∈ ℂ)
33876rpcnd 12084 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 / 2) ∈ ℂ)
33983recnd 10349 . . . . . . . . . . . . . . 15 (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
34076rpne0d 12087 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 / 2) ≠ 0)
341339, 338, 340divcld 11082 . . . . . . . . . . . . . 14 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
342337, 338, 341mulassd 10344 . . . . . . . . . . . . 13 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
343339, 338, 340divcan2d 11084 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
344343oveq2d 6886 . . . . . . . . . . . . 13 (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
345342, 344eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
346332, 336, 3453eqtr3d 2848 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
347218, 196mulcli 10328 . . . . . . . . . . . . 13 (3 · (log‘2)) ∈ ℂ
348347a1i 11 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘2)) ∈ ℂ)
349 mulcl 10301 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
350218, 168, 349sylancr 577 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
351269, 348, 350npncan3d 10709 . . . . . . . . . . 11 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
352304, 346, 3513eqtr4d 2850 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
353116, 91remulcli 10337 . . . . . . . . . . . . 13 (2 · (log‘2)) ∈ ℝ
354353recni 10335 . . . . . . . . . . . 12 (2 · (log‘2)) ∈ ℂ
355354a1i 11 . . . . . . . . . . 11 (𝜑 → (2 · (log‘2)) ∈ ℂ)
356 subcl 10561 . . . . . . . . . . . 12 (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
357168, 268, 356sylancl 576 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
358355, 294, 357addassd 10343 . . . . . . . . . 10 (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
359297, 352, 3583eqtr4d 2850 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
360359oveq2d 6886 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
361 mulcl 10301 . . . . . . . . . . 11 ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
362253, 196, 361sylancl 576 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
363253, 168mulcld 10341 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
36487recnd 10349 . . . . . . . . . . 11 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
365243, 364mulcld 10341 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
366362, 363, 365addassd 10343 . . . . . . . . 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)))))))
367258oveq2d 6886 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
368253, 247, 168adddid 10345 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
369367, 368eqtrd 2840 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
370369oveq1d 6885 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
37157oveq2d 6886 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
37288recnd 10349 . . . . . . . . . . . 12 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
37396recnd 10349 . . . . . . . . . . . 12 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
374243, 372, 373adddid 10345 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
375371, 374eqtrd 2840 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
37671recnd 10349 . . . . . . . . . . . . 13 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
377243, 376, 364adddid 10345 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
37893rpge0d 12086 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (2 · 𝑁))
379 remsqsqrt 14216 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
380232, 378, 379syl2anc 575 . . . . . . . . . . . . . . . . 17 (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
381380oveq1d 6885 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
382112recnd 10349 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
383219a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
384382, 382, 337, 383div23d 11119 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
385381, 384eqtr3d 2842 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
386385oveq1d 6885 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
387253, 382, 376mulassd 10344 . . . . . . . . . . . . . 14 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
388 0le2 11390 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
389116, 388pm3.2i 458 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ ∧ 0 ≤ 2)
39059rprege0d 12089 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
391 sqrtmul 14219 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
392389, 390, 391sylancr 577 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
393392oveq1d 6885 . . . . . . . . . . . . . . . 16 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
39458recni 10335 . . . . . . . . . . . . . . . . . 18 (√‘2) ∈ ℂ
395394a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘2) ∈ ℂ)
39660rpcnd 12084 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘𝑁) ∈ ℂ)
39769recnd 10349 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
398395, 396, 395, 397mul4d 10529 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
399 remsqsqrt 14216 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
400116, 388, 399mp2an 675 . . . . . . . . . . . . . . . . . . 19 ((√‘2) · (√‘2)) = 2
401400a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘2) · (√‘2)) = 2)
40266oveq2d 6886 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
40367recnd 10349 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
40460rpne0d 12087 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑁) ≠ 0)
405403, 396, 404divcan2d 11084 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
406402, 405eqtrd 2840 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
407401, 406oveq12d 6888 . . . . . . . . . . . . . . . . 17 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
4084032timesd 11538 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
40960, 60relogmuld 24581 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
410 remsqsqrt 14216 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
411390, 410syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
412411fveq2d 6408 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
413409, 412eqtr3d 2842 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
414407, 408, 4133eqtrd 2844 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
415393, 398, 4143eqtrd 2844 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
416415oveq2d 6886 . . . . . . . . . . . . . 14 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
417386, 387, 4163eqtrd 2844 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
418417oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
419377, 418eqtrd 2840 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
420385oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
421253, 382, 373mulassd 10344 . . . . . . . . . . . 12 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
42294rpne0d 12087 . . . . . . . . . . . . . 14 (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
423247, 382, 422divcan2d 11084 . . . . . . . . . . . . 13 (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
424423oveq2d 6886 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
425420, 421, 4243eqtrd 2844 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
426419, 425oveq12d 6888 . . . . . . . . . 10 (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
427363, 365addcld 10340 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
428427, 362addcomd 10519 . . . . . . . . . 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)))))))
429375, 426, 4283eqtrd 2844 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
430366, 370, 4293eqtr4rd 2851 . . . . . . . 8 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
431253, 255mulcld 10341 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
432 addcl 10299 . . . . . . . . . 10 (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
433354, 294, 432sylancr 577 . . . . . . . . 9 (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
434431, 433, 357addassd 10343 . . . . . . . 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))))))
435360, 430, 4343eqtr4d 2850 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
436272, 274, 4353eqtr4rd 2851 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
437191, 252, 4363brtr4d 4876 . . . . 5 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁)))
43899, 98, 242ltmul2d 12124 . . . . 5 (𝜑 → ((log‘2) < (𝐹𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁))))
439437, 438mpbird 248 . . . 4 (𝜑 → (log‘2) < (𝐹𝑁))
44045, 99, 98, 100, 439lttrd 10479 . . 3 (𝜑 → (𝐹64) < (𝐹𝑁))
44145, 98, 440ltnsymd 10467 . 2 (𝜑 → ¬ (𝐹𝑁) < (𝐹64))
44242, 441pm2.21dd 186 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wne 2978  wrex 3097  ifcif 4279   class class class wbr 4844  cmpt 4923  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222   < clt 10355  cle 10356  cmin 10547   / cdiv 10965  cn 11301  2c2 11352  3c3 11353  4c4 11354  5c5 11355  6c6 11356  8c8 11358  9c9 11359  cz 11639  cdc 11755  cuz 11900  +crp 12042  cfl 12811  cexp 13079  Ccbc 13305  csqrt 14192  expce 15008  eceu 15009  cprime 15599   pCnt cpc 15754  logclog 24511  𝑐ccxp 24512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295  ax-addf 10296  ax-mulf 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-oadd 7796  df-er 7975  df-map 8090  df-pm 8091  df-ixp 8142  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-fi 8552  df-sup 8583  df-inf 8584  df-oi 8650  df-card 9044  df-cda 9271  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-xnn0 11626  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-fac 13277  df-bc 13306  df-hash 13334  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-ef 15014  df-e 15015  df-sin 15016  df-cos 15017  df-pi 15019  df-dvds 15200  df-gcd 15432  df-prm 15600  df-pc 15755  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-fbas 19947  df-fg 19948  df-cnfld 19951  df-top 20908  df-topon 20925  df-topsp 20947  df-bases 20960  df-cld 21033  df-ntr 21034  df-cls 21035  df-nei 21112  df-lp 21150  df-perf 21151  df-cn 21241  df-cnp 21242  df-haus 21329  df-tx 21575  df-hmeo 21768  df-fil 21859  df-fm 21951  df-flim 21952  df-flf 21953  df-xms 22334  df-ms 22335  df-tms 22336  df-cncf 22890  df-limc 23840  df-dv 23841  df-log 24513  df-cxp 24514  df-cht 25033  df-ppi 25036
This theorem is referenced by:  bpos  25228
  Copyright terms: Public domain W3C validator