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

Theorem bposlem9 24817
 Description: Lemma for bpos 24818. 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 11190 . . . . . 6 6 ∈ ℕ0
5 4nn 11064 . . . . . 6 4 ∈ ℕ
64, 5decnncl 11394 . . . . 5 64 ∈ ℕ
76a1i 11 . . . 4 (𝜑64 ∈ ℕ)
8 bposlem9.3 . . . 4 (𝜑𝑁 ∈ ℕ)
9 ere 14658 . . . . . . . 8 e ∈ ℝ
10 8re 10982 . . . . . . . 8 8 ∈ ℝ
11 egt2lt3 14773 . . . . . . . . . 10 (2 < e ∧ e < 3)
1211simpri 477 . . . . . . . . 9 e < 3
13 3lt8 11096 . . . . . . . . 9 3 < 8
14 3re 10971 . . . . . . . . . 10 3 ∈ ℝ
159, 14, 10lttri 10042 . . . . . . . . 9 ((e < 3 ∧ 3 < 8) → e < 8)
1612, 13, 15mp2an 704 . . . . . . . 8 e < 8
179, 10, 16ltleii 10039 . . . . . . 7 e ≤ 8
18 0re 9919 . . . . . . . . 9 0 ∈ ℝ
19 epos 14774 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 10039 . . . . . . . 8 0 ≤ e
21 8pos 10998 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 10039 . . . . . . . 8 0 ≤ 8
23 le2sq 12800 . . . . . . . 8 (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
249, 20, 10, 22, 23mp4an 705 . . . . . . 7 (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
2517, 24mpbi 219 . . . . . 6 (e↑2) ≤ (8↑2)
2610recni 9931 . . . . . . . 8 8 ∈ ℂ
2726sqvali 12805 . . . . . . 7 (8↑2) = (8 · 8)
28 8t8e64 11538 . . . . . . 7 (8 · 8) = 64
2927, 28eqtri 2632 . . . . . 6 (8↑2) = 64
3025, 29breqtri 4608 . . . . 5 (e↑2) ≤ 64
3130a1i 11 . . . 4 (𝜑 → (e↑2) ≤ 64)
329resqcli 12811 . . . . . 6 (e↑2) ∈ ℝ
3332a1i 11 . . . . 5 (𝜑 → (e↑2) ∈ ℝ)
346nnrei 10906 . . . . . 6 64 ∈ ℝ
3534a1i 11 . . . . 5 (𝜑64 ∈ ℝ)
368nnred 10912 . . . . 5 (𝜑𝑁 ∈ ℝ)
37 ltle 10005 . . . . . . 7 ((64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (64 < 𝑁64 ≤ 𝑁))
3834, 36, 37sylancr 694 . . . . . 6 (𝜑 → (64 < 𝑁64 ≤ 𝑁))
391, 38mpd 15 . . . . 5 (𝜑64 ≤ 𝑁)
4033, 35, 36, 31, 39letrd 10073 . . . 4 (𝜑 → (e↑2) ≤ 𝑁)
412, 3, 7, 8, 31, 40bposlem7 24815 . . 3 (𝜑 → (64 < 𝑁 → (𝐹𝑁) < (𝐹64)))
421, 41mpd 15 . 2 (𝜑 → (𝐹𝑁) < (𝐹64))
432, 3bposlem8 24816 . . . . 5 ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2))
4443a1i 11 . . . 4 (𝜑 → ((𝐹64) ∈ ℝ ∧ (𝐹64) < (log‘2)))
4544simpld 474 . . 3 (𝜑 → (𝐹64) ∈ ℝ)
46 fveq2 6103 . . . . . . . . . 10 (𝑛 = 𝑁 → (√‘𝑛) = (√‘𝑁))
4746fveq2d 6107 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
4847oveq2d 6565 . . . . . . . 8 (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
49 oveq1 6556 . . . . . . . . . 10 (𝑛 = 𝑁 → (𝑛 / 2) = (𝑁 / 2))
5049fveq2d 6107 . . . . . . . . 9 (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
5150oveq2d 6565 . . . . . . . 8 (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
5248, 51oveq12d 6567 . . . . . . 7 (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
53 oveq2 6557 . . . . . . . . 9 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
5453fveq2d 6107 . . . . . . . 8 (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
5554oveq2d 6565 . . . . . . 7 (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
5652, 55oveq12d 6567 . . . . . 6 (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57 ovex 6577 . . . . . 6 ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
5856, 2, 57fvmpt 6191 . . . . 5 (𝑁 ∈ ℕ → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
598, 58syl 17 . . . 4 (𝜑 → (𝐹𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
60 sqrt2re 14818 . . . . . . 7 (√‘2) ∈ ℝ
618nnrpd 11746 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ+)
6261rpsqrtcld 13998 . . . . . . . . 9 (𝜑 → (√‘𝑁) ∈ ℝ+)
63 fveq2 6103 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
64 id 22 . . . . . . . . . . 11 (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
6563, 64oveq12d 6567 . . . . . . . . . 10 (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66 ovex 6577 . . . . . . . . . 10 ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
6765, 3, 66fvmpt 6191 . . . . . . . . 9 ((√‘𝑁) ∈ ℝ+ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6862, 67syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
6962relogcld 24173 . . . . . . . . 9 (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
7069, 62rerpdivcld 11779 . . . . . . . 8 (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
7168, 70eqeltrd 2688 . . . . . . 7 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
72 remulcl 9900 . . . . . . 7 (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
7360, 71, 72sylancr 694 . . . . . 6 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
74 9re 10984 . . . . . . . 8 9 ∈ ℝ
75 4re 10974 . . . . . . . 8 4 ∈ ℝ
76 4ne0 10994 . . . . . . . 8 4 ≠ 0
7774, 75, 76redivcli 10671 . . . . . . 7 (9 / 4) ∈ ℝ
7861rphalfcld 11760 . . . . . . . . 9 (𝜑 → (𝑁 / 2) ∈ ℝ+)
79 fveq2 6103 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
80 id 22 . . . . . . . . . . 11 (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
8179, 80oveq12d 6567 . . . . . . . . . 10 (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82 ovex 6577 . . . . . . . . . 10 ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
8381, 3, 82fvmpt 6191 . . . . . . . . 9 ((𝑁 / 2) ∈ ℝ+ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8478, 83syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
8578relogcld 24173 . . . . . . . . 9 (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
8685, 78rerpdivcld 11779 . . . . . . . 8 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
8784, 86eqeltrd 2688 . . . . . . 7 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
88 remulcl 9900 . . . . . . 7 (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
8977, 87, 88sylancr 694 . . . . . 6 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
9073, 89readdcld 9948 . . . . 5 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
91 2rp 11713 . . . . . . 7 2 ∈ ℝ+
92 relogcl 24126 . . . . . . 7 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
9391, 92ax-mp 5 . . . . . 6 (log‘2) ∈ ℝ
94 rpmulcl 11731 . . . . . . . 8 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (2 · 𝑁) ∈ ℝ+)
9591, 61, 94sylancr 694 . . . . . . 7 (𝜑 → (2 · 𝑁) ∈ ℝ+)
9695rpsqrtcld 13998 . . . . . 6 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ+)
97 rerpdivcl 11737 . . . . . 6 (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ+) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9893, 96, 97sylancr 694 . . . . 5 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
9990, 98readdcld 9948 . . . 4 (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
10059, 99eqeltrd 2688 . . 3 (𝜑 → (𝐹𝑁) ∈ ℝ)
10193a1i 11 . . . 4 (𝜑 → (log‘2) ∈ ℝ)
10244simprd 478 . . . 4 (𝜑 → (𝐹64) < (log‘2))
103 nnrp 11718 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
1045, 103ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
105 relogcl 24126 . . . . . . . . . 10 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
106104, 105ax-mp 5 . . . . . . . . 9 (log‘4) ∈ ℝ
107 remulcl 9900 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
10836, 106, 107sylancl 693 . . . . . . . 8 (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
10961relogcld 24173 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
110108, 109resubcld 10337 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
111 rpre 11715 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → (2 · 𝑁) ∈ ℝ)
112 rpge0 11721 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ ℝ+ → 0 ≤ (2 · 𝑁))
113111, 112resqrtcld 14004 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℝ+ → (√‘(2 · 𝑁)) ∈ ℝ)
11495, 113syl 17 . . . . . . . . . . 11 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
115 3nn 11063 . . . . . . . . . . 11 3 ∈ ℕ
116 nndivre 10933 . . . . . . . . . . 11 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
117114, 115, 116sylancl 693 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
118 2re 10967 . . . . . . . . . 10 2 ∈ ℝ
119 readdcl 9898 . . . . . . . . . 10 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
120117, 118, 119sylancl 693 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
12195relogcld 24173 . . . . . . . . 9 (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
122120, 121remulcld 9949 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
123 remulcl 9900 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
12475, 36, 123sylancr 694 . . . . . . . . . . 11 (𝜑 → (4 · 𝑁) ∈ ℝ)
125 nndivre 10933 . . . . . . . . . . 11 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
126124, 115, 125sylancl 693 . . . . . . . . . 10 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
127 5re 10976 . . . . . . . . . 10 5 ∈ ℝ
128 resubcl 10224 . . . . . . . . . 10 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
129126, 127, 128sylancl 693 . . . . . . . . 9 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
130 remulcl 9900 . . . . . . . . 9 (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
131129, 93, 130sylancl 693 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
132122, 131readdcld 9948 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
133 remulcl 9900 . . . . . . . . 9 ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
134126, 93, 133sylancl 693 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
135134, 109resubcld 10337 . . . . . . 7 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
1368nnzd 11357 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
137 df-5 10959 . . . . . . . . . . . 12 5 = (4 + 1)
13875a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
139 6nn 11066 . . . . . . . . . . . . . . . 16 6 ∈ ℕ
140 4nn0 11188 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
141 4lt10 11554 . . . . . . . . . . . . . . . 16 4 < 10
142139, 140, 140, 141declti 11422 . . . . . . . . . . . . . . 15 4 < 64
143142a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 < 64)
144138, 35, 36, 143, 1lttrd 10077 . . . . . . . . . . . . 13 (𝜑 → 4 < 𝑁)
145 4z 11288 . . . . . . . . . . . . . 14 4 ∈ ℤ
146 zltp1le 11304 . . . . . . . . . . . . . 14 ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
147145, 136, 146sylancr 694 . . . . . . . . . . . . 13 (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
148144, 147mpbid 221 . . . . . . . . . . . 12 (𝜑 → (4 + 1) ≤ 𝑁)
149137, 148syl5eqbr 4618 . . . . . . . . . . 11 (𝜑 → 5 ≤ 𝑁)
150 5nn 11065 . . . . . . . . . . . . 13 5 ∈ ℕ
151150nnzi 11278 . . . . . . . . . . . 12 5 ∈ ℤ
152151eluz1i 11571 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
153136, 149, 152sylanbrc 695 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘5))
154 bposlem9.5 . . . . . . . . . . 11 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
155 breq2 4587 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑁 < 𝑝𝑁 < 𝑞))
156 breq1 4586 . . . . . . . . . . . . 13 (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
157155, 156anbi12d 743 . . . . . . . . . . . 12 (𝑝 = 𝑞 → ((𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁))))
158157cbvrexv 3148 . . . . . . . . . . 11 (∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
159154, 158sylnib 317 . . . . . . . . . 10 (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞𝑞 ≤ (2 · 𝑁)))
160 eqid 2610 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
161 eqid 2610 . . . . . . . . . 10 (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
162 eqid 2610 . . . . . . . . . 10 (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
163153, 159, 160, 161, 162bposlem6 24814 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
164 reexplog 24145 . . . . . . . . . . . 12 ((4 ∈ ℝ+𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
165104, 136, 164sylancr 694 . . . . . . . . . . 11 (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
16661reeflogd 24174 . . . . . . . . . . . 12 (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
167166eqcomd 2616 . . . . . . . . . . 11 (𝜑𝑁 = (exp‘(log‘𝑁)))
168165, 167oveq12d 6567 . . . . . . . . . 10 (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
169108recnd 9947 . . . . . . . . . . 11 (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
170109recnd 9947 . . . . . . . . . . 11 (𝜑 → (log‘𝑁) ∈ ℂ)
171 efsub 14669 . . . . . . . . . . 11 (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
172169, 170, 171syl2anc 691 . . . . . . . . . 10 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
173168, 172eqtr4d 2647 . . . . . . . . 9 (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
17495rpcnd 11750 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℂ)
17595rpne0d 11753 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ≠ 0)
176120recnd 9947 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
177174, 175, 176cxpefd 24258 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
178 2cn 10968 . . . . . . . . . . . 12 2 ∈ ℂ
179 2ne0 10990 . . . . . . . . . . . 12 2 ≠ 0
180129recnd 9947 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
181 cxpef 24211 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
182178, 179, 180, 181mp3an12i 1420 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
183177, 182oveq12d 6567 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
184122recnd 9947 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
185131recnd 9947 . . . . . . . . . . 11 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
186 efadd 14663 . . . . . . . . . . 11 ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ ∧ ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ) → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
187184, 185, 186syl2anc 691 . . . . . . . . . 10 (𝜑 → (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188183, 187eqtr4d 2647 . . . . . . . . 9 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
189163, 173, 1883brtr3d 4614 . . . . . . . 8 (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
190 eflt 14686 . . . . . . . . 9 ((((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ ∧ (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ) → (((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ↔ (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))))
191110, 132, 190syl2anc 691 . . . . . . . 8 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ↔ (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))))
192189, 191mpbird 246 . . . . . . 7 (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
193110, 132, 135, 192ltsub1dd 10518 . . . . . 6 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
19436recnd 9947 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
195 mulcom 9901 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
196178, 194, 195sylancr 694 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) = (𝑁 · 2))
197196oveq1d 6564 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
19893recni 9931 . . . . . . . . . . . 12 (log‘2) ∈ ℂ
199 mulass 9903 . . . . . . . . . . . 12 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200178, 198, 199mp3an23 1408 . . . . . . . . . . 11 (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
201194, 200syl 17 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
2021982timesi 11024 . . . . . . . . . . . 12 (2 · (log‘2)) = ((log‘2) + (log‘2))
203 relogmul 24142 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
20491, 91, 203mp2an 704 . . . . . . . . . . . 12 (log‘(2 · 2)) = ((log‘2) + (log‘2))
205 2t2e4 11054 . . . . . . . . . . . . 13 (2 · 2) = 4
206205fveq2i 6106 . . . . . . . . . . . 12 (log‘(2 · 2)) = (log‘4)
207202, 204, 2063eqtr2i 2638 . . . . . . . . . . 11 (2 · (log‘2)) = (log‘4)
208207oveq2i 6560 . . . . . . . . . 10 (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
209201, 208syl6eq 2660 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
210197, 209eqtrd 2644 . . . . . . . 8 (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
211210oveq1d 6564 . . . . . . 7 (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
212 4p2e6 11039 . . . . . . . . . . . . . . 15 (4 + 2) = 6
213212oveq1i 6559 . . . . . . . . . . . . . 14 ((4 + 2) · 𝑁) = (6 · 𝑁)
214 4cn 10975 . . . . . . . . . . . . . . 15 4 ∈ ℂ
215 adddir 9910 . . . . . . . . . . . . . . 15 ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
216214, 178, 194, 215mp3an12i 1420 . . . . . . . . . . . . . 14 (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
217213, 216syl5eqr 2658 . . . . . . . . . . . . 13 (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
218217oveq1d 6564 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
219 6cn 10979 . . . . . . . . . . . . . . 15 6 ∈ ℂ
220 3cn 10972 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
221 3ne0 10992 . . . . . . . . . . . . . . . 16 3 ≠ 0
222220, 221pm3.2i 470 . . . . . . . . . . . . . . 15 (3 ∈ ℂ ∧ 3 ≠ 0)
223 div23 10583 . . . . . . . . . . . . . . 15 ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
224219, 222, 223mp3an13 1407 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
225194, 224syl 17 . . . . . . . . . . . . 13 (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
226 3t2e6 11056 . . . . . . . . . . . . . . . 16 (3 · 2) = 6
227226oveq1i 6559 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = (6 / 3)
228178, 220, 221divcan3i 10650 . . . . . . . . . . . . . . 15 ((3 · 2) / 3) = 2
229227, 228eqtr3i 2634 . . . . . . . . . . . . . 14 (6 / 3) = 2
230229oveq1i 6559 . . . . . . . . . . . . 13 ((6 / 3) · 𝑁) = (2 · 𝑁)
231225, 230syl6eq 2660 . . . . . . . . . . . 12 (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
232124recnd 9947 . . . . . . . . . . . . 13 (𝜑 → (4 · 𝑁) ∈ ℂ)
233 remulcl 9900 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
234118, 36, 233sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝑁) ∈ ℝ)
235234recnd 9947 . . . . . . . . . . . . 13 (𝜑 → (2 · 𝑁) ∈ ℂ)
236 divdir 10589 . . . . . . . . . . . . . 14 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
237222, 236mp3an3 1405 . . . . . . . . . . . . 13 (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
238232, 235, 237syl2anc 691 . . . . . . . . . . . 12 (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
239218, 231, 2383eqtr3d 2652 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240239oveq1d 6564 . . . . . . . . . 10 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)))
241126recnd 9947 . . . . . . . . . . 11 (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
242 3rp 11714 . . . . . . . . . . . . 13 3 ∈ ℝ+
243 rpdivcl 11732 . . . . . . . . . . . . 13 (((2 · 𝑁) ∈ ℝ+ ∧ 3 ∈ ℝ+) → ((2 · 𝑁) / 3) ∈ ℝ+)
24495, 242, 243sylancl 693 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ+)
245244rpcnd 11750 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
246241, 245pncan2d 10273 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
247240, 246eqtrd 2644 . . . . . . . . 9 (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
248247oveq1d 6564 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
249101recnd 9947 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℂ)
250235, 241, 249subdird 10366 . . . . . . . 8 (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
251248, 250eqtr3d 2646 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
252134recnd 9947 . . . . . . . 8 (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
253169, 252, 170nnncan2d 10306 . . . . . . 7 (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
254211, 251, 2533eqtr4d 2654 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
255117recnd 9947 . . . . . . . . . 10 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
256178a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
257121recnd 9947 . . . . . . . . . 10 (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
258255, 256, 257adddird 9944 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
259 relogmul 24142 . . . . . . . . . . . . 13 ((2 ∈ ℝ+𝑁 ∈ ℝ+) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
26091, 61, 259sylancr 694 . . . . . . . . . . . 12 (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
261260oveq2d 6565 . . . . . . . . . . 11 (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
262256, 249, 170adddid 9943 . . . . . . . . . . 11 (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
263261, 262eqtrd 2644 . . . . . . . . . 10 (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
264263oveq2d 6565 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
265258, 264eqtrd 2644 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
266 5cn 10977 . . . . . . . . . . . 12 5 ∈ ℂ
267266a1i 11 . . . . . . . . . . 11 (𝜑 → 5 ∈ ℂ)
268241, 267, 249subdird 10366 . . . . . . . . . 10 (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
269268oveq1d 6564 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
270266, 198mulcli 9924 . . . . . . . . . . 11 (5 · (log‘2)) ∈ ℂ
271270a1i 11 . . . . . . . . . 10 (𝜑 → (5 · (log‘2)) ∈ ℂ)
272252, 271, 170nnncan1d 10305 . . . . . . . . 9 (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
273269, 272eqtrd 2644 . . . . . . . 8 (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
274265, 273oveq12d 6567 . . . . . . 7 (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)))) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
275135recnd 9947 . . . . . . . 8 (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
276184, 185, 275addsubassd 10291 . . . . . . 7 (𝜑 → ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)))))
277266, 220, 198subdiri 10359 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
278 3p2e5 11037 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
279278oveq1i 6559 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = (5 − 3)
280 pncan2 10167 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
281220, 178, 280mp2an 704 . . . . . . . . . . . . . . 15 ((3 + 2) − 3) = 2
282279, 281eqtr3i 2634 . . . . . . . . . . . . . 14 (5 − 3) = 2
283282oveq1i 6559 . . . . . . . . . . . . 13 ((5 − 3) · (log‘2)) = (2 · (log‘2))
284277, 283eqtr3i 2634 . . . . . . . . . . . 12 ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
285284a1i 11 . . . . . . . . . . 11 (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
286 df-3 10957 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
287286oveq1i 6559 . . . . . . . . . . . . . . 15 (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
288 1cnd 9935 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
289256, 288, 170adddird 9944 . . . . . . . . . . . . . . 15 (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
290287, 289syl5eq 2656 . . . . . . . . . . . . . 14 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
291170mulid2d 9937 . . . . . . . . . . . . . . 15 (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
292291oveq2d 6565 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
293290, 292eqtrd 2644 . . . . . . . . . . . . 13 (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
294293oveq1d 6564 . . . . . . . . . . . 12 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
295 mulcl 9899 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
296178, 170, 295sylancr 694 . . . . . . . . . . . . 13 (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
297296, 170, 271addsubassd 10291 . . . . . . . . . . . 12 (𝜑 → (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
298294, 297eqtrd 2644 . . . . . . . . . . 11 (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
299285, 298oveq12d 6567 . . . . . . . . . 10 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
300 relogdiv 24143 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
30161, 91, 300sylancl 693 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
302301oveq2d 6565 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
303 subdi 10342 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
304220, 198, 303mp3an13 1407 . . . . . . . . . . . . 13 ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
305170, 304syl 17 . . . . . . . . . . . 12 (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
306302, 305eqtrd 2644 . . . . . . . . . . 11 (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
307 div23 10583 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
308178, 222, 307mp3an13 1407 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
309194, 308syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
310220, 178, 220, 178, 179, 179divmuldivi 10664 . . . . . . . . . . . . . . . . 17 ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
311 3t3e9 11057 . . . . . . . . . . . . . . . . . 18 (3 · 3) = 9
312311, 205oveq12i 6561 . . . . . . . . . . . . . . . . 17 ((3 · 3) / (2 · 2)) = (9 / 4)
313310, 312eqtr2i 2633 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) · (3 / 2))
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
315309, 314oveq12d 6567 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
316178, 220, 221divcli 10646 . . . . . . . . . . . . . . 15 (2 / 3) ∈ ℂ
317220, 178, 179divcli 10646 . . . . . . . . . . . . . . . 16 (3 / 2) ∈ ℂ
318 mul4 10084 . . . . . . . . . . . . . . . 16 ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
319317, 317, 318mpanr12 717 . . . . . . . . . . . . . . 15 (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
320316, 194, 319sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
321 divcan6 10611 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
322178, 179, 220, 221, 321mp4an 705 . . . . . . . . . . . . . . . . 17 ((2 / 3) · (3 / 2)) = 1
323322oveq1i 6559 . . . . . . . . . . . . . . . 16 (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
324 mulcl 9899 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
325194, 317, 324sylancl 693 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
326325mulid2d 9937 . . . . . . . . . . . . . . . 16 (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
327323, 326syl5eq 2656 . . . . . . . . . . . . . . 15 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
328 2cnne0 11119 . . . . . . . . . . . . . . . . 17 (2 ∈ ℂ ∧ 2 ≠ 0)
329 div12 10586 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
330220, 328, 329mp3an23 1408 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
331194, 330syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
332327, 331eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
333315, 320, 3323eqtrd 2648 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
334333, 84oveq12d 6567 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
33577recni 9931 . . . . . . . . . . . . . 14 (9 / 4) ∈ ℂ
336335a1i 11 . . . . . . . . . . . . 13 (𝜑 → (9 / 4) ∈ ℂ)
33787recnd 9947 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
338245, 336, 337mulassd 9942 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
339220a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 3 ∈ ℂ)
34078rpcnd 11750 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 / 2) ∈ ℂ)
34185recnd 9947 . . . . . . . . . . . . . . 15 (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
34278rpne0d 11753 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 / 2) ≠ 0)
343341, 340, 342divcld 10680 . . . . . . . . . . . . . 14 (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
344339, 340, 343mulassd 9942 . . . . . . . . . . . . 13 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
345341, 340, 342divcan2d 10682 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
346345oveq2d 6565 . . . . . . . . . . . . 13 (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
347344, 346eqtrd 2644 . . . . . . . . . . . 12 (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
348334, 338, 3473eqtr3d 2652 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
349220, 198mulcli 9924 . . . . . . . . . . . . 13 (3 · (log‘2)) ∈ ℂ
350349a1i 11 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘2)) ∈ ℂ)
351 mulcl 9899 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
352220, 170, 351sylancr 694 . . . . . . . . . . . 12 (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
353271, 350, 352npncan3d 10307 . . . . . . . . . . 11 (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
354306, 348, 3533eqtr4d 2654 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
355118, 93remulcli 9933 . . . . . . . . . . . . 13 (2 · (log‘2)) ∈ ℝ
356355recni 9931 . . . . . . . . . . . 12 (2 · (log‘2)) ∈ ℂ
357356a1i 11 . . . . . . . . . . 11 (𝜑 → (2 · (log‘2)) ∈ ℂ)
358 subcl 10159 . . . . . . . . . . . 12 (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
359170, 270, 358sylancl 693 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
360357, 296, 359addassd 9941 . . . . . . . . . 10 (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
361299, 354, 3603eqtr4d 2654 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
362361oveq2d 6565 . . . . . . . 8 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
363 mulcl 9899 . . . . . . . . . . 11 ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
364255, 198, 363sylancl 693 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
365255, 170mulcld 9939 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
36689recnd 9947 . . . . . . . . . . 11 (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
367245, 366mulcld 9939 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
368364, 365, 367addassd 9941 . . . . . . . . 9 (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
369260oveq2d 6565 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
370255, 249, 170adddid 9943 . . . . . . . . . . 11 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
371369, 370eqtrd 2644 . . . . . . . . . 10 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
372371oveq1d 6564 . . . . . . . . 9 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
37359oveq2d 6565 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
37490recnd 9947 . . . . . . . . . . . 12 (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
37598recnd 9947 . . . . . . . . . . . 12 (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
376245, 374, 375adddid 9943 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
377373, 376eqtrd 2644 . . . . . . . . . 10 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
37873recnd 9947 . . . . . . . . . . . . 13 (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
379245, 378, 366adddid 9943 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
38095rpge0d 11752 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (2 · 𝑁))
381 remsqsqrt 13845 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
382234, 380, 381syl2anc 691 . . . . . . . . . . . . . . . . 17 (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
383382oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
384114recnd 9947 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
385221a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
386384, 384, 339, 385div23d 10717 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
387383, 386eqtr3d 2646 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
388387oveq1d 6564 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
389255, 384, 378mulassd 9942 . . . . . . . . . . . . . 14 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
390 0le2 10988 . . . . . . . . . . . . . . . . . . 19 0 ≤ 2
391118, 390pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ ∧ 0 ≤ 2)
39261rprege0d 11755 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
393 sqrtmul 13848 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
394391, 392, 393sylancr 694 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
395394oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
39660recni 9931 . . . . . . . . . . . . . . . . . 18 (√‘2) ∈ ℂ
397396a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘2) ∈ ℂ)
39862rpcnd 11750 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘𝑁) ∈ ℂ)
39971recnd 9947 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
400397, 398, 397, 399mul4d 10127 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
401 remsqsqrt 13845 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
402118, 390, 401mp2an 704 . . . . . . . . . . . . . . . . . . 19 ((√‘2) · (√‘2)) = 2
403402a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘2) · (√‘2)) = 2)
40468oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
40569recnd 9947 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
40662rpne0d 11753 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑁) ≠ 0)
407405, 398, 406divcan2d 10682 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
408404, 407eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
409403, 408oveq12d 6567 . . . . . . . . . . . . . . . . 17 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
4104052timesd 11152 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
41162, 62relogmuld 24175 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
412 remsqsqrt 13845 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
413392, 412syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
414413fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
415411, 414eqtr3d 2646 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
416409, 410, 4153eqtrd 2648 . . . . . . . . . . . . . . . 16 (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
417395, 400, 4163eqtrd 2648 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
418417oveq2d 6565 . . . . . . . . . . . . . 14 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
419388, 389, 4183eqtrd 2648 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
420419oveq1d 6564 . . . . . . . . . . . 12 (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
421379, 420eqtrd 2644 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
422387oveq1d 6564 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
423255, 384, 375mulassd 9942 . . . . . . . . . . . 12 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
42496rpne0d 11753 . . . . . . . . . . . . . 14 (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
425249, 384, 424divcan2d 10682 . . . . . . . . . . . . 13 (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
426425oveq2d 6565 . . . . . . . . . . . 12 (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
427422, 423, 4263eqtrd 2648 . . . . . . . . . . 11 (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
428421, 427oveq12d 6567 . . . . . . . . . 10 (𝜑 → ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))))
429365, 367addcld 9938 . . . . . . . . . . 11 (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
430429, 364addcomd 10117 . . . . . . . . . 10 (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((√‘(2 · 𝑁)) / 3) · (log‘2))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
431377, 428, 4303eqtrd 2648 . . . . . . . . 9 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
432368, 372, 4313eqtr4rd 2655 . . . . . . . 8 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
433255, 257mulcld 9939 . . . . . . . . 9 (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
434 addcl 9897 . . . . . . . . . 10 (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
435356, 296, 434sylancr 694 . . . . . . . . 9 (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
436433, 435, 359addassd 9941 . . . . . . . 8 (𝜑 → (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
437362, 432, 4363eqtr4d 2654 . . . . . . 7 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
438274, 276, 4373eqtr4rd 2655 . . . . . 6 (𝜑 → (((2 · 𝑁) / 3) · (𝐹𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
439193, 254, 4383brtr4d 4615 . . . . 5 (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁)))
440101, 100, 244ltmul2d 11790 . . . . 5 (𝜑 → ((log‘2) < (𝐹𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹𝑁))))
441439, 440mpbird 246 . . . 4 (𝜑 → (log‘2) < (𝐹𝑁))
44245, 101, 100, 102, 441lttrd 10077 . . 3 (𝜑 → (𝐹64) < (𝐹𝑁))
44345, 100, 442ltnsymd 10065 . 2 (𝜑 → ¬ (𝐹𝑁) < (𝐹64))
44442, 443pm2.21dd 185 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  3c3 10948  4c4 10949  5c5 10950  6c6 10951  8c8 10953  9c9 10954  ℤcz 11254  ;cdc 11369  ℤ≥cuz 11563  ℝ+crp 11708  ⌊cfl 12453  ↑cexp 12722  Ccbc 12951  √csqrt 13821  expce 14631  eceu 14632  ℙcprime 15223   pCnt cpc 15379  logclog 24105  ↑𝑐ccxp 24106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-xnn0 11241  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-e 14638  df-sin 14639  df-cos 14640  df-pi 14642  df-dvds 14822  df-gcd 15055  df-prm 15224  df-pc 15380  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108  df-cht 24623  df-ppi 24626 This theorem is referenced by:  bpos  24818
 Copyright terms: Public domain W3C validator