Metamath Proof Explorer

Theorem bposlem9

Description: Lemma for bpos . Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypotheses bposlem7.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) )
bposlem7.2 ⊢ 𝐺 = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) )
bposlem9.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
bposlem9.4 ⊢ ( 𝜑 → 6 4 < 𝑁 )
bposlem9.5 ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
Assertion bposlem9 ( 𝜑 → 𝜓 )

Proof

Step Hyp Ref Expression
1 bposlem7.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) )
2 bposlem7.2 ⊢ 𝐺 = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) )
3 bposlem9.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 bposlem9.4 ⊢ ( 𝜑 → 6 4 < 𝑁 )
5 bposlem9.5 ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
6 6nn0 ⊢ 6 ∈ ℕ0
7 4nn ⊢ 4 ∈ ℕ
8 6 7 decnncl ⊢ 6 4 ∈ ℕ
9 8 a1i ⊢ ( 𝜑 → 6 4 ∈ ℕ )
10 ere ⊢ e ∈ ℝ
11 8re ⊢ 8 ∈ ℝ
12 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
13 12 simpri ⊢ e < 3
14 3lt8 ⊢ 3 < 8
15 3re ⊢ 3 ∈ ℝ
16 10 15 11 lttri ⊢ ( ( e < 3 ∧ 3 < 8 ) → e < 8 )
17 13 14 16 mp2an ⊢ e < 8
18 10 11 17 ltleii ⊢ e ≤ 8
19 0re ⊢ 0 ∈ ℝ
20 epos ⊢ 0 < e
21 19 10 20 ltleii ⊢ 0 ≤ e
22 8pos ⊢ 0 < 8
23 19 11 22 ltleii ⊢ 0 ≤ 8
24 le2sq ⊢ ( ( ( e ∈ ℝ ∧ 0 ≤ e ) ∧ ( 8 ∈ ℝ ∧ 0 ≤ 8 ) ) → ( e ≤ 8 ↔ ( e ↑ 2 ) ≤ ( 8 ↑ 2 ) ) )
25 10 21 11 23 24 mp4an ⊢ ( e ≤ 8 ↔ ( e ↑ 2 ) ≤ ( 8 ↑ 2 ) )
26 18 25 mpbi ⊢ ( e ↑ 2 ) ≤ ( 8 ↑ 2 )
27 11 recni ⊢ 8 ∈ ℂ
28 27 sqvali ⊢ ( 8 ↑ 2 ) = ( 8 · 8 )
29 8t8e64 ⊢ ( 8 · 8 ) = 6 4
30 28 29 eqtri ⊢ ( 8 ↑ 2 ) = 6 4
31 26 30 breqtri ⊢ ( e ↑ 2 ) ≤ 6 4
32 31 a1i ⊢ ( 𝜑 → ( e ↑ 2 ) ≤ 6 4 )
33 10 resqcli ⊢ ( e ↑ 2 ) ∈ ℝ
34 33 a1i ⊢ ( 𝜑 → ( e ↑ 2 ) ∈ ℝ )
35 8 nnrei ⊢ 6 4 ∈ ℝ
36 35 a1i ⊢ ( 𝜑 → 6 4 ∈ ℝ )
37 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
38 ltle ⊢ ( ( 6 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 6 4 < 𝑁 → 6 4 ≤ 𝑁 ) )
39 35 37 38 sylancr ⊢ ( 𝜑 → ( 6 4 < 𝑁 → 6 4 ≤ 𝑁 ) )
40 4 39 mpd ⊢ ( 𝜑 → 6 4 ≤ 𝑁 )
41 34 36 37 32 40 letrd ⊢ ( 𝜑 → ( e ↑ 2 ) ≤ 𝑁 )
42 1 2 9 3 32 41 bposlem7 ⊢ ( 𝜑 → ( 6 4 < 𝑁 → ( 𝐹 ‘ 𝑁 ) < ( 𝐹 ‘ 6 4 ) ) )
43 4 42 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) < ( 𝐹 ‘ 6 4 ) )
44 1 2 bposlem8 ⊢ ( ( 𝐹 ‘ 6 4 ) ∈ ℝ ∧ ( 𝐹 ‘ 6 4 ) < ( log ‘ 2 ) )
45 44 a1i ⊢ ( 𝜑 → ( ( 𝐹 ‘ 6 4 ) ∈ ℝ ∧ ( 𝐹 ‘ 6 4 ) < ( log ‘ 2 ) ) )
46 45 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 6 4 ) ∈ ℝ )
47 2fveq3 ⊢ ( 𝑛 = 𝑁 → ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) = ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) )
48 47 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) = ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) )
49 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝐺 ‘ ( 𝑛 / 2 ) ) = ( 𝐺 ‘ ( 𝑁 / 2 ) ) )
50 49 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) = ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) )
51 48 50 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) ) = ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) )
52 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 2 · 𝑛 ) = ( 2 · 𝑁 ) )
53 52 fveq2d ⊢ ( 𝑛 = 𝑁 → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · 𝑁 ) ) )
54 53 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) = ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) )
55 51 54 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) = ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
56 ovex ⊢ ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ∈ V
57 55 1 56 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
58 3 57 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) = ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
59 sqrt2re ⊢ ( √ ‘ 2 ) ∈ ℝ
60 3 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
61 60 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ+ )
62 fveq2 ⊢ ( 𝑥 = ( √ ‘ 𝑁 ) → ( log ‘ 𝑥 ) = ( log ‘ ( √ ‘ 𝑁 ) ) )
63 id ⊢ ( 𝑥 = ( √ ‘ 𝑁 ) → 𝑥 = ( √ ‘ 𝑁 ) )
64 62 63 oveq12d ⊢ ( 𝑥 = ( √ ‘ 𝑁 ) → ( ( log ‘ 𝑥 ) / 𝑥 ) = ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) )
65 ovex ⊢ ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) ∈ V
66 64 2 65 fvmpt ⊢ ( ( √ ‘ 𝑁 ) ∈ ℝ+ → ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) = ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) )
67 61 66 syl ⊢ ( 𝜑 → ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) = ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) )
68 61 relogcld ⊢ ( 𝜑 → ( log ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ )
69 68 61 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) ∈ ℝ )
70 67 69 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ )
71 remulcl ⊢ ( ( ( √ ‘ 2 ) ∈ ℝ ∧ ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ ) → ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
72 59 70 71 sylancr ⊢ ( 𝜑 → ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
73 9re ⊢ 9 ∈ ℝ
74 4re ⊢ 4 ∈ ℝ
75 4ne0 ⊢ 4 ≠ 0
76 73 74 75 redivcli ⊢ ( 9 / 4 ) ∈ ℝ
77 60 rphalfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℝ+ )
78 fveq2 ⊢ ( 𝑥 = ( 𝑁 / 2 ) → ( log ‘ 𝑥 ) = ( log ‘ ( 𝑁 / 2 ) ) )
79 id ⊢ ( 𝑥 = ( 𝑁 / 2 ) → 𝑥 = ( 𝑁 / 2 ) )
80 78 79 oveq12d ⊢ ( 𝑥 = ( 𝑁 / 2 ) → ( ( log ‘ 𝑥 ) / 𝑥 ) = ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) )
81 ovex ⊢ ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ∈ V
82 80 2 81 fvmpt ⊢ ( ( 𝑁 / 2 ) ∈ ℝ+ → ( 𝐺 ‘ ( 𝑁 / 2 ) ) = ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) )
83 77 82 syl ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑁 / 2 ) ) = ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) )
84 77 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
85 84 77 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ∈ ℝ )
86 83 85 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
87 remulcl ⊢ ( ( ( 9 / 4 ) ∈ ℝ ∧ ( 𝐺 ‘ ( 𝑁 / 2 ) ) ∈ ℝ ) → ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ∈ ℝ )
88 76 86 87 sylancr ⊢ ( 𝜑 → ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ∈ ℝ )
89 72 88 readdcld ⊢ ( 𝜑 → ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ∈ ℝ )
90 2rp ⊢ 2 ∈ ℝ+
91 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
92 90 91 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
93 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( 2 · 𝑁 ) ∈ ℝ+ )
94 90 60 93 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
95 94 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ+ )
96 rerpdivcl ⊢ ( ( ( log ‘ 2 ) ∈ ℝ ∧ ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ+ ) → ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℝ )
97 92 95 96 sylancr ⊢ ( 𝜑 → ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℝ )
98 89 97 readdcld ⊢ ( 𝜑 → ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ∈ ℝ )
99 58 98 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
100 92 a1i ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
101 45 simprd ⊢ ( 𝜑 → ( 𝐹 ‘ 6 4 ) < ( log ‘ 2 ) )
102 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
103 7 102 ax-mp ⊢ 4 ∈ ℝ+
104 relogcl ⊢ ( 4 ∈ ℝ+ → ( log ‘ 4 ) ∈ ℝ )
105 103 104 ax-mp ⊢ ( log ‘ 4 ) ∈ ℝ
106 remulcl ⊢ ( ( 𝑁 ∈ ℝ ∧ ( log ‘ 4 ) ∈ ℝ ) → ( 𝑁 · ( log ‘ 4 ) ) ∈ ℝ )
107 37 105 106 sylancl ⊢ ( 𝜑 → ( 𝑁 · ( log ‘ 4 ) ) ∈ ℝ )
108 60 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
109 107 108 resubcld ⊢ ( 𝜑 → ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) ∈ ℝ )
110 rpre ⊢ ( ( 2 · 𝑁 ) ∈ ℝ+ → ( 2 · 𝑁 ) ∈ ℝ )
111 rpge0 ⊢ ( ( 2 · 𝑁 ) ∈ ℝ+ → 0 ≤ ( 2 · 𝑁 ) )
112 110 111 resqrtcld ⊢ ( ( 2 · 𝑁 ) ∈ ℝ+ → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
113 94 112 syl ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
114 3nn ⊢ 3 ∈ ℕ
115 nndivre ⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
116 113 114 115 sylancl ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
117 2re ⊢ 2 ∈ ℝ
118 readdcl ⊢ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
119 116 117 118 sylancl ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
120 94 relogcld ⊢ ( 𝜑 → ( log ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
121 119 120 remulcld ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ∈ ℝ )
122 remulcl ⊢ ( ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 4 · 𝑁 ) ∈ ℝ )
123 74 37 122 sylancr ⊢ ( 𝜑 → ( 4 · 𝑁 ) ∈ ℝ )
124 nndivre ⊢ ( ( ( 4 · 𝑁 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ )
125 123 114 124 sylancl ⊢ ( 𝜑 → ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ )
126 5re ⊢ 5 ∈ ℝ
127 resubcl ⊢ ( ( ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ ∧ 5 ∈ ℝ ) → ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℝ )
128 125 126 127 sylancl ⊢ ( 𝜑 → ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℝ )
129 remulcl ⊢ ( ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℝ ∧ ( log ‘ 2 ) ∈ ℝ ) → ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ∈ ℝ )
130 128 92 129 sylancl ⊢ ( 𝜑 → ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ∈ ℝ )
131 121 130 readdcld ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) ∈ ℝ )
132 remulcl ⊢ ( ( ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ ∧ ( log ‘ 2 ) ∈ ℝ ) → ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ∈ ℝ )
133 125 92 132 sylancl ⊢ ( 𝜑 → ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ∈ ℝ )
134 133 108 resubcld ⊢ ( 𝜑 → ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ∈ ℝ )
135 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
136 df-5 ⊢ 5 = ( 4 + 1 )
137 74 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
138 6nn ⊢ 6 ∈ ℕ
139 4nn0 ⊢ 4 ∈ ℕ0
140 4lt10 ⊢ 4 < 1 0
141 138 139 139 140 declti ⊢ 4 < 6 4
142 141 a1i ⊢ ( 𝜑 → 4 < 6 4 )
143 137 36 37 142 4 lttrd ⊢ ( 𝜑 → 4 < 𝑁 )
144 4z ⊢ 4 ∈ ℤ
145 zltp1le ⊢ ( ( 4 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 4 < 𝑁 ↔ ( 4 + 1 ) ≤ 𝑁 ) )
146 144 135 145 sylancr ⊢ ( 𝜑 → ( 4 < 𝑁 ↔ ( 4 + 1 ) ≤ 𝑁 ) )
147 143 146 mpbid ⊢ ( 𝜑 → ( 4 + 1 ) ≤ 𝑁 )
148 136 147 eqbrtrid ⊢ ( 𝜑 → 5 ≤ 𝑁 )
149 5nn ⊢ 5 ∈ ℕ
150 149 nnzi ⊢ 5 ∈ ℤ
151 150 eluz1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ↔ ( 𝑁 ∈ ℤ ∧ 5 ≤ 𝑁 ) )
152 135 148 151 sylanbrc ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
153 breq2 ⊢ ( 𝑝 = 𝑞 → ( 𝑁 < 𝑝 ↔ 𝑁 < 𝑞 ) )
154 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ≤ ( 2 · 𝑁 ) ↔ 𝑞 ≤ ( 2 · 𝑁 ) ) )
155 153 154 anbi12d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ↔ ( 𝑁 < 𝑞 ∧ 𝑞 ≤ ( 2 · 𝑁 ) ) ) )
156 155 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ↔ ∃ 𝑞 ∈ ℙ ( 𝑁 < 𝑞 ∧ 𝑞 ≤ ( 2 · 𝑁 ) ) )
157 5 156 sylnib ⊢ ( 𝜑 → ¬ ∃ 𝑞 ∈ ℙ ( 𝑁 < 𝑞 ∧ 𝑞 ≤ ( 2 · 𝑁 ) ) )
158 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
159 eqid ⊢ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
160 eqid ⊢ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
161 152 157 158 159 160 bposlem6 ⊢ ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )
162 reexplog ⊢ ( ( 4 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 4 ↑ 𝑁 ) = ( exp ‘ ( 𝑁 · ( log ‘ 4 ) ) ) )
163 103 135 162 sylancr ⊢ ( 𝜑 → ( 4 ↑ 𝑁 ) = ( exp ‘ ( 𝑁 · ( log ‘ 4 ) ) ) )
164 60 reeflogd ⊢ ( 𝜑 → ( exp ‘ ( log ‘ 𝑁 ) ) = 𝑁 )
165 164 eqcomd ⊢ ( 𝜑 → 𝑁 = ( exp ‘ ( log ‘ 𝑁 ) ) )
166 163 165 oveq12d ⊢ ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) = ( ( exp ‘ ( 𝑁 · ( log ‘ 4 ) ) ) / ( exp ‘ ( log ‘ 𝑁 ) ) ) )
167 107 recnd ⊢ ( 𝜑 → ( 𝑁 · ( log ‘ 4 ) ) ∈ ℂ )
168 108 recnd ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
169 efsub ⊢ ( ( ( 𝑁 · ( log ‘ 4 ) ) ∈ ℂ ∧ ( log ‘ 𝑁 ) ∈ ℂ ) → ( exp ‘ ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) ) = ( ( exp ‘ ( 𝑁 · ( log ‘ 4 ) ) ) / ( exp ‘ ( log ‘ 𝑁 ) ) ) )
170 167 168 169 syl2anc ⊢ ( 𝜑 → ( exp ‘ ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) ) = ( ( exp ‘ ( 𝑁 · ( log ‘ 4 ) ) ) / ( exp ‘ ( log ‘ 𝑁 ) ) ) )
171 166 170 eqtr4d ⊢ ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) = ( exp ‘ ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) ) )
172 94 rpcnd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
173 94 rpne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
174 119 recnd ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℂ )
175 172 173 174 cxpefd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) = ( exp ‘ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ) )
176 2cn ⊢ 2 ∈ ℂ
177 2ne0 ⊢ 2 ≠ 0
178 128 recnd ⊢ ( 𝜑 → ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℂ )
179 cxpef ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℂ ) → ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) = ( exp ‘ ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) )
180 176 177 178 179 mp3an12i ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) = ( exp ‘ ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) )
181 175 180 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) = ( ( exp ‘ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ) · ( exp ‘ ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) ) )
182 121 recnd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ∈ ℂ )
183 130 recnd ⊢ ( 𝜑 → ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ∈ ℂ )
184 efadd ⊢ ( ( ( ( ( ( √ ‘ ( 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 ) ) ) ) )
185 182 183 184 syl2anc ⊢ ( 𝜑 → ( exp ‘ ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) ) = ( ( exp ‘ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ) · ( exp ‘ ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) ) )
186 181 185 eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) = ( exp ‘ ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) ) )
187 161 171 186 3brtr3d ⊢ ( 𝜑 → ( exp ‘ ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) ) < ( exp ‘ ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) ) )
188 eflt ⊢ ( ( ( ( 𝑁 · ( 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 ) ) ) ) ) )
189 109 131 188 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑁 · ( 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 ) ) ) ) ) )
190 187 189 mpbird ⊢ ( 𝜑 → ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) < ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) )
191 109 131 134 190 ltsub1dd ⊢ ( 𝜑 → ( ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) < ( ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) )
192 37 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
193 mulcom ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 2 · 𝑁 ) = ( 𝑁 · 2 ) )
194 176 192 193 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( 𝑁 · 2 ) )
195 194 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( log ‘ 2 ) ) = ( ( 𝑁 · 2 ) · ( log ‘ 2 ) ) )
196 92 recni ⊢ ( log ‘ 2 ) ∈ ℂ
197 mulass ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ ( log ‘ 2 ) ∈ ℂ ) → ( ( 𝑁 · 2 ) · ( log ‘ 2 ) ) = ( 𝑁 · ( 2 · ( log ‘ 2 ) ) ) )
198 176 196 197 mp3an23 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 · 2 ) · ( log ‘ 2 ) ) = ( 𝑁 · ( 2 · ( log ‘ 2 ) ) ) )
199 192 198 syl ⊢ ( 𝜑 → ( ( 𝑁 · 2 ) · ( log ‘ 2 ) ) = ( 𝑁 · ( 2 · ( log ‘ 2 ) ) ) )
200 196 2timesi ⊢ ( 2 · ( log ‘ 2 ) ) = ( ( log ‘ 2 ) + ( log ‘ 2 ) )
201 relogmul ⊢ ( ( 2 ∈ ℝ+ ∧ 2 ∈ ℝ+ ) → ( log ‘ ( 2 · 2 ) ) = ( ( log ‘ 2 ) + ( log ‘ 2 ) ) )
202 90 90 201 mp2an ⊢ ( log ‘ ( 2 · 2 ) ) = ( ( log ‘ 2 ) + ( log ‘ 2 ) )
203 2t2e4 ⊢ ( 2 · 2 ) = 4
204 203 fveq2i ⊢ ( log ‘ ( 2 · 2 ) ) = ( log ‘ 4 )
205 200 202 204 3eqtr2i ⊢ ( 2 · ( log ‘ 2 ) ) = ( log ‘ 4 )
206 205 oveq2i ⊢ ( 𝑁 · ( 2 · ( log ‘ 2 ) ) ) = ( 𝑁 · ( log ‘ 4 ) )
207 199 206 eqtrdi ⊢ ( 𝜑 → ( ( 𝑁 · 2 ) · ( log ‘ 2 ) ) = ( 𝑁 · ( log ‘ 4 ) ) )
208 195 207 eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( log ‘ 2 ) ) = ( 𝑁 · ( log ‘ 4 ) ) )
209 208 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( log ‘ 2 ) ) − ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ) = ( ( 𝑁 · ( log ‘ 4 ) ) − ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ) )
210 125 recnd ⊢ ( 𝜑 → ( ( 4 · 𝑁 ) / 3 ) ∈ ℂ )
211 3rp ⊢ 3 ∈ ℝ+
212 rpdivcl ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ+ )
213 94 211 212 sylancl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ+ )
214 213 rpcnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) ∈ ℂ )
215 4p2e6 ⊢ ( 4 + 2 ) = 6
216 215 oveq1i ⊢ ( ( 4 + 2 ) · 𝑁 ) = ( 6 · 𝑁 )
217 4cn ⊢ 4 ∈ ℂ
218 adddir ⊢ ( ( 4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 4 + 2 ) · 𝑁 ) = ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) )
219 217 176 192 218 mp3an12i ⊢ ( 𝜑 → ( ( 4 + 2 ) · 𝑁 ) = ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) )
220 216 219 eqtr3id ⊢ ( 𝜑 → ( 6 · 𝑁 ) = ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) )
221 220 oveq1d ⊢ ( 𝜑 → ( ( 6 · 𝑁 ) / 3 ) = ( ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) / 3 ) )
222 6cn ⊢ 6 ∈ ℂ
223 3cn ⊢ 3 ∈ ℂ
224 3ne0 ⊢ 3 ≠ 0
225 223 224 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
226 div23 ⊢ ( ( 6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 6 · 𝑁 ) / 3 ) = ( ( 6 / 3 ) · 𝑁 ) )
227 222 225 226 mp3an13 ⊢ ( 𝑁 ∈ ℂ → ( ( 6 · 𝑁 ) / 3 ) = ( ( 6 / 3 ) · 𝑁 ) )
228 192 227 syl ⊢ ( 𝜑 → ( ( 6 · 𝑁 ) / 3 ) = ( ( 6 / 3 ) · 𝑁 ) )
229 3t2e6 ⊢ ( 3 · 2 ) = 6
230 229 oveq1i ⊢ ( ( 3 · 2 ) / 3 ) = ( 6 / 3 )
231 176 223 224 divcan3i ⊢ ( ( 3 · 2 ) / 3 ) = 2
232 230 231 eqtr3i ⊢ ( 6 / 3 ) = 2
233 232 oveq1i ⊢ ( ( 6 / 3 ) · 𝑁 ) = ( 2 · 𝑁 )
234 228 233 eqtrdi ⊢ ( 𝜑 → ( ( 6 · 𝑁 ) / 3 ) = ( 2 · 𝑁 ) )
235 123 recnd ⊢ ( 𝜑 → ( 4 · 𝑁 ) ∈ ℂ )
236 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 2 · 𝑁 ) ∈ ℝ )
237 117 37 236 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
238 237 recnd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
239 divdir ⊢ ( ( ( 4 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) / 3 ) = ( ( ( 4 · 𝑁 ) / 3 ) + ( ( 2 · 𝑁 ) / 3 ) ) )
240 225 239 mp3an3 ⊢ ( ( ( 4 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ∈ ℂ ) → ( ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) / 3 ) = ( ( ( 4 · 𝑁 ) / 3 ) + ( ( 2 · 𝑁 ) / 3 ) ) )
241 235 238 240 syl2anc ⊢ ( 𝜑 → ( ( ( 4 · 𝑁 ) + ( 2 · 𝑁 ) ) / 3 ) = ( ( ( 4 · 𝑁 ) / 3 ) + ( ( 2 · 𝑁 ) / 3 ) ) )
242 221 234 241 3eqtr3d ⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( ( ( 4 · 𝑁 ) / 3 ) + ( ( 2 · 𝑁 ) / 3 ) ) )
243 210 214 242 mvrladdd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) − ( ( 4 · 𝑁 ) / 3 ) ) = ( ( 2 · 𝑁 ) / 3 ) )
244 243 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) − ( ( 4 · 𝑁 ) / 3 ) ) · ( log ‘ 2 ) ) = ( ( ( 2 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) )
245 100 recnd ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
246 238 210 245 subdird ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) − ( ( 4 · 𝑁 ) / 3 ) ) · ( log ‘ 2 ) ) = ( ( ( 2 · 𝑁 ) · ( log ‘ 2 ) ) − ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ) )
247 244 246 eqtr3d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) = ( ( ( 2 · 𝑁 ) · ( log ‘ 2 ) ) − ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ) )
248 133 recnd ⊢ ( 𝜑 → ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ∈ ℂ )
249 167 248 168 nnncan2d ⊢ ( 𝜑 → ( ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) = ( ( 𝑁 · ( log ‘ 4 ) ) − ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) ) )
250 209 247 249 3eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) = ( ( ( 𝑁 · ( log ‘ 4 ) ) − ( log ‘ 𝑁 ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) )
251 116 recnd ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℂ )
252 176 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
253 120 recnd ⊢ ( 𝜑 → ( log ‘ ( 2 · 𝑁 ) ) ∈ ℂ )
254 251 252 253 adddird ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( 2 · ( log ‘ ( 2 · 𝑁 ) ) ) ) )
255 relogmul ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( log ‘ ( 2 · 𝑁 ) ) = ( ( log ‘ 2 ) + ( log ‘ 𝑁 ) ) )
256 90 60 255 sylancr ⊢ ( 𝜑 → ( log ‘ ( 2 · 𝑁 ) ) = ( ( log ‘ 2 ) + ( log ‘ 𝑁 ) ) )
257 256 oveq2d ⊢ ( 𝜑 → ( 2 · ( log ‘ ( 2 · 𝑁 ) ) ) = ( 2 · ( ( log ‘ 2 ) + ( log ‘ 𝑁 ) ) ) )
258 252 245 168 adddid ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 2 ) + ( log ‘ 𝑁 ) ) ) = ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) )
259 257 258 eqtrd ⊢ ( 𝜑 → ( 2 · ( log ‘ ( 2 · 𝑁 ) ) ) = ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) )
260 259 oveq2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( 2 · ( log ‘ ( 2 · 𝑁 ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) ) )
261 254 260 eqtrd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) ) )
262 5cn ⊢ 5 ∈ ℂ
263 262 a1i ⊢ ( 𝜑 → 5 ∈ ℂ )
264 210 263 245 subdird ⊢ ( 𝜑 → ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) = ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( 5 · ( log ‘ 2 ) ) ) )
265 264 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) = ( ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( 5 · ( log ‘ 2 ) ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) )
266 262 196 mulcli ⊢ ( 5 · ( log ‘ 2 ) ) ∈ ℂ
267 266 a1i ⊢ ( 𝜑 → ( 5 · ( log ‘ 2 ) ) ∈ ℂ )
268 248 267 168 nnncan1d ⊢ ( 𝜑 → ( ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( 5 · ( log ‘ 2 ) ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) = ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) )
269 265 268 eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) = ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) )
270 261 269 oveq12d ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 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 ) ) ) ) )
271 134 recnd ⊢ ( 𝜑 → ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ∈ ℂ )
272 182 183 271 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( ( √ ‘ ( 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 ‘ 𝑁 ) ) ) ) )
273 262 223 196 subdiri ⊢ ( ( 5 − 3 ) · ( log ‘ 2 ) ) = ( ( 5 · ( log ‘ 2 ) ) − ( 3 · ( log ‘ 2 ) ) )
274 3p2e5 ⊢ ( 3 + 2 ) = 5
275 274 oveq1i ⊢ ( ( 3 + 2 ) − 3 ) = ( 5 − 3 )
276 pncan2 ⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 3 + 2 ) − 3 ) = 2 )
277 223 176 276 mp2an ⊢ ( ( 3 + 2 ) − 3 ) = 2
278 275 277 eqtr3i ⊢ ( 5 − 3 ) = 2
279 278 oveq1i ⊢ ( ( 5 − 3 ) · ( log ‘ 2 ) ) = ( 2 · ( log ‘ 2 ) )
280 273 279 eqtr3i ⊢ ( ( 5 · ( log ‘ 2 ) ) − ( 3 · ( log ‘ 2 ) ) ) = ( 2 · ( log ‘ 2 ) )
281 280 a1i ⊢ ( 𝜑 → ( ( 5 · ( log ‘ 2 ) ) − ( 3 · ( log ‘ 2 ) ) ) = ( 2 · ( log ‘ 2 ) ) )
282 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( log ‘ 𝑁 ) ∈ ℂ ) → ( 2 · ( log ‘ 𝑁 ) ) ∈ ℂ )
283 176 168 282 sylancr ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑁 ) ) ∈ ℂ )
284 df-3 ⊢ 3 = ( 2 + 1 )
285 284 oveq1i ⊢ ( 3 · ( log ‘ 𝑁 ) ) = ( ( 2 + 1 ) · ( log ‘ 𝑁 ) )
286 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
287 252 286 168 adddird ⊢ ( 𝜑 → ( ( 2 + 1 ) · ( log ‘ 𝑁 ) ) = ( ( 2 · ( log ‘ 𝑁 ) ) + ( 1 · ( log ‘ 𝑁 ) ) ) )
288 285 287 eqtrid ⊢ ( 𝜑 → ( 3 · ( log ‘ 𝑁 ) ) = ( ( 2 · ( log ‘ 𝑁 ) ) + ( 1 · ( log ‘ 𝑁 ) ) ) )
289 168 mulid2d ⊢ ( 𝜑 → ( 1 · ( log ‘ 𝑁 ) ) = ( log ‘ 𝑁 ) )
290 289 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑁 ) ) + ( 1 · ( log ‘ 𝑁 ) ) ) = ( ( 2 · ( log ‘ 𝑁 ) ) + ( log ‘ 𝑁 ) ) )
291 288 290 eqtrd ⊢ ( 𝜑 → ( 3 · ( log ‘ 𝑁 ) ) = ( ( 2 · ( log ‘ 𝑁 ) ) + ( log ‘ 𝑁 ) ) )
292 291 oveq1d ⊢ ( 𝜑 → ( ( 3 · ( log ‘ 𝑁 ) ) − ( 5 · ( log ‘ 2 ) ) ) = ( ( ( 2 · ( log ‘ 𝑁 ) ) + ( log ‘ 𝑁 ) ) − ( 5 · ( log ‘ 2 ) ) ) )
293 283 168 267 292 assraddsubd ⊢ ( 𝜑 → ( ( 3 · ( log ‘ 𝑁 ) ) − ( 5 · ( log ‘ 2 ) ) ) = ( ( 2 · ( log ‘ 𝑁 ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) )
294 281 293 oveq12d ⊢ ( 𝜑 → ( ( ( 5 · ( log ‘ 2 ) ) − ( 3 · ( log ‘ 2 ) ) ) + ( ( 3 · ( log ‘ 𝑁 ) ) − ( 5 · ( log ‘ 2 ) ) ) ) = ( ( 2 · ( log ‘ 2 ) ) + ( ( 2 · ( log ‘ 𝑁 ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) ) )
295 relogdiv ⊢ ( ( 𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+ ) → ( log ‘ ( 𝑁 / 2 ) ) = ( ( log ‘ 𝑁 ) − ( log ‘ 2 ) ) )
296 60 90 295 sylancl ⊢ ( 𝜑 → ( log ‘ ( 𝑁 / 2 ) ) = ( ( log ‘ 𝑁 ) − ( log ‘ 2 ) ) )
297 296 oveq2d ⊢ ( 𝜑 → ( 3 · ( log ‘ ( 𝑁 / 2 ) ) ) = ( 3 · ( ( log ‘ 𝑁 ) − ( log ‘ 2 ) ) ) )
298 subdi ⊢ ( ( 3 ∈ ℂ ∧ ( log ‘ 𝑁 ) ∈ ℂ ∧ ( log ‘ 2 ) ∈ ℂ ) → ( 3 · ( ( log ‘ 𝑁 ) − ( log ‘ 2 ) ) ) = ( ( 3 · ( log ‘ 𝑁 ) ) − ( 3 · ( log ‘ 2 ) ) ) )
299 223 196 298 mp3an13 ⊢ ( ( log ‘ 𝑁 ) ∈ ℂ → ( 3 · ( ( log ‘ 𝑁 ) − ( log ‘ 2 ) ) ) = ( ( 3 · ( log ‘ 𝑁 ) ) − ( 3 · ( log ‘ 2 ) ) ) )
300 168 299 syl ⊢ ( 𝜑 → ( 3 · ( ( log ‘ 𝑁 ) − ( log ‘ 2 ) ) ) = ( ( 3 · ( log ‘ 𝑁 ) ) − ( 3 · ( log ‘ 2 ) ) ) )
301 297 300 eqtrd ⊢ ( 𝜑 → ( 3 · ( log ‘ ( 𝑁 / 2 ) ) ) = ( ( 3 · ( log ‘ 𝑁 ) ) − ( 3 · ( log ‘ 2 ) ) ) )
302 div23 ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 2 · 𝑁 ) / 3 ) = ( ( 2 / 3 ) · 𝑁 ) )
303 176 225 302 mp3an13 ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · 𝑁 ) / 3 ) = ( ( 2 / 3 ) · 𝑁 ) )
304 192 303 syl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) = ( ( 2 / 3 ) · 𝑁 ) )
305 223 176 223 176 177 177 divmuldivi ⊢ ( ( 3 / 2 ) · ( 3 / 2 ) ) = ( ( 3 · 3 ) / ( 2 · 2 ) )
306 3t3e9 ⊢ ( 3 · 3 ) = 9
307 306 203 oveq12i ⊢ ( ( 3 · 3 ) / ( 2 · 2 ) ) = ( 9 / 4 )
308 305 307 eqtr2i ⊢ ( 9 / 4 ) = ( ( 3 / 2 ) · ( 3 / 2 ) )
309 308 a1i ⊢ ( 𝜑 → ( 9 / 4 ) = ( ( 3 / 2 ) · ( 3 / 2 ) ) )
310 304 309 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 9 / 4 ) ) = ( ( ( 2 / 3 ) · 𝑁 ) · ( ( 3 / 2 ) · ( 3 / 2 ) ) ) )
311 176 223 224 divcli ⊢ ( 2 / 3 ) ∈ ℂ
312 223 176 177 divcli ⊢ ( 3 / 2 ) ∈ ℂ
313 mul4 ⊢ ( ( ( ( 2 / 3 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( ( 3 / 2 ) ∈ ℂ ∧ ( 3 / 2 ) ∈ ℂ ) ) → ( ( ( 2 / 3 ) · 𝑁 ) · ( ( 3 / 2 ) · ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) · ( 3 / 2 ) ) · ( 𝑁 · ( 3 / 2 ) ) ) )
314 312 312 313 mpanr12 ⊢ ( ( ( 2 / 3 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 2 / 3 ) · 𝑁 ) · ( ( 3 / 2 ) · ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) · ( 3 / 2 ) ) · ( 𝑁 · ( 3 / 2 ) ) ) )
315 311 192 314 sylancr ⊢ ( 𝜑 → ( ( ( 2 / 3 ) · 𝑁 ) · ( ( 3 / 2 ) · ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) · ( 3 / 2 ) ) · ( 𝑁 · ( 3 / 2 ) ) ) )
316 divcan6 ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 2 / 3 ) · ( 3 / 2 ) ) = 1 )
317 176 177 223 224 316 mp4an ⊢ ( ( 2 / 3 ) · ( 3 / 2 ) ) = 1
318 317 oveq1i ⊢ ( ( ( 2 / 3 ) · ( 3 / 2 ) ) · ( 𝑁 · ( 3 / 2 ) ) ) = ( 1 · ( 𝑁 · ( 3 / 2 ) ) )
319 mulcl ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 3 / 2 ) ∈ ℂ ) → ( 𝑁 · ( 3 / 2 ) ) ∈ ℂ )
320 192 312 319 sylancl ⊢ ( 𝜑 → ( 𝑁 · ( 3 / 2 ) ) ∈ ℂ )
321 320 mulid2d ⊢ ( 𝜑 → ( 1 · ( 𝑁 · ( 3 / 2 ) ) ) = ( 𝑁 · ( 3 / 2 ) ) )
322 318 321 eqtrid ⊢ ( 𝜑 → ( ( ( 2 / 3 ) · ( 3 / 2 ) ) · ( 𝑁 · ( 3 / 2 ) ) ) = ( 𝑁 · ( 3 / 2 ) ) )
323 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
324 div12 ⊢ ( ( 𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( 𝑁 · ( 3 / 2 ) ) = ( 3 · ( 𝑁 / 2 ) ) )
325 223 323 324 mp3an23 ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 · ( 3 / 2 ) ) = ( 3 · ( 𝑁 / 2 ) ) )
326 192 325 syl ⊢ ( 𝜑 → ( 𝑁 · ( 3 / 2 ) ) = ( 3 · ( 𝑁 / 2 ) ) )
327 322 326 eqtrd ⊢ ( 𝜑 → ( ( ( 2 / 3 ) · ( 3 / 2 ) ) · ( 𝑁 · ( 3 / 2 ) ) ) = ( 3 · ( 𝑁 / 2 ) ) )
328 310 315 327 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 9 / 4 ) ) = ( 3 · ( 𝑁 / 2 ) ) )
329 328 83 oveq12d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) / 3 ) · ( 9 / 4 ) ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) = ( ( 3 · ( 𝑁 / 2 ) ) · ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) )
330 76 recni ⊢ ( 9 / 4 ) ∈ ℂ
331 330 a1i ⊢ ( 𝜑 → ( 9 / 4 ) ∈ ℂ )
332 86 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑁 / 2 ) ) ∈ ℂ )
333 214 331 332 mulassd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) / 3 ) · ( 9 / 4 ) ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) = ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) )
334 223 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
335 77 rpcnd ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℂ )
336 84 recnd ⊢ ( 𝜑 → ( log ‘ ( 𝑁 / 2 ) ) ∈ ℂ )
337 77 rpne0d ⊢ ( 𝜑 → ( 𝑁 / 2 ) ≠ 0 )
338 336 335 337 divcld ⊢ ( 𝜑 → ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ∈ ℂ )
339 334 335 338 mulassd ⊢ ( 𝜑 → ( ( 3 · ( 𝑁 / 2 ) ) · ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) = ( 3 · ( ( 𝑁 / 2 ) · ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) ) )
340 336 335 337 divcan2d ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) · ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) = ( log ‘ ( 𝑁 / 2 ) ) )
341 340 oveq2d ⊢ ( 𝜑 → ( 3 · ( ( 𝑁 / 2 ) · ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) ) = ( 3 · ( log ‘ ( 𝑁 / 2 ) ) ) )
342 339 341 eqtrd ⊢ ( 𝜑 → ( ( 3 · ( 𝑁 / 2 ) ) · ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) = ( 3 · ( log ‘ ( 𝑁 / 2 ) ) ) )
343 329 333 342 3eqtr3d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) = ( 3 · ( log ‘ ( 𝑁 / 2 ) ) ) )
344 223 196 mulcli ⊢ ( 3 · ( log ‘ 2 ) ) ∈ ℂ
345 344 a1i ⊢ ( 𝜑 → ( 3 · ( log ‘ 2 ) ) ∈ ℂ )
346 mulcl ⊢ ( ( 3 ∈ ℂ ∧ ( log ‘ 𝑁 ) ∈ ℂ ) → ( 3 · ( log ‘ 𝑁 ) ) ∈ ℂ )
347 223 168 346 sylancr ⊢ ( 𝜑 → ( 3 · ( log ‘ 𝑁 ) ) ∈ ℂ )
348 267 345 347 npncan3d ⊢ ( 𝜑 → ( ( ( 5 · ( log ‘ 2 ) ) − ( 3 · ( log ‘ 2 ) ) ) + ( ( 3 · ( log ‘ 𝑁 ) ) − ( 5 · ( log ‘ 2 ) ) ) ) = ( ( 3 · ( log ‘ 𝑁 ) ) − ( 3 · ( log ‘ 2 ) ) ) )
349 301 343 348 3eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) = ( ( ( 5 · ( log ‘ 2 ) ) − ( 3 · ( log ‘ 2 ) ) ) + ( ( 3 · ( log ‘ 𝑁 ) ) − ( 5 · ( log ‘ 2 ) ) ) ) )
350 117 92 remulcli ⊢ ( 2 · ( log ‘ 2 ) ) ∈ ℝ
351 350 recni ⊢ ( 2 · ( log ‘ 2 ) ) ∈ ℂ
352 351 a1i ⊢ ( 𝜑 → ( 2 · ( log ‘ 2 ) ) ∈ ℂ )
353 subcl ⊢ ( ( ( log ‘ 𝑁 ) ∈ ℂ ∧ ( 5 · ( log ‘ 2 ) ) ∈ ℂ ) → ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ∈ ℂ )
354 168 266 353 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ∈ ℂ )
355 352 283 354 addassd ⊢ ( 𝜑 → ( ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) = ( ( 2 · ( log ‘ 2 ) ) + ( ( 2 · ( log ‘ 𝑁 ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) ) )
356 294 349 355 3eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) = ( ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) )
357 356 oveq2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) ) )
358 mulcl ⊢ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℂ ∧ ( log ‘ 2 ) ∈ ℂ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) ∈ ℂ )
359 251 196 358 sylancl ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) ∈ ℂ )
360 251 168 mulcld ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) ∈ ℂ )
361 88 recnd ⊢ ( 𝜑 → ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ∈ ℂ )
362 214 361 mulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ∈ ℂ )
363 359 360 362 addassd ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) ) )
364 256 oveq2d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( ( log ‘ 2 ) + ( log ‘ 𝑁 ) ) ) )
365 251 245 168 adddid ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( ( log ‘ 2 ) + ( log ‘ 𝑁 ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) ) )
366 364 365 eqtrd ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) ) )
367 366 oveq1d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) = ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) )
368 58 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) = ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) )
369 89 recnd ⊢ ( 𝜑 → ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ∈ ℂ )
370 97 recnd ⊢ ( 𝜑 → ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℂ )
371 214 369 370 adddid ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) = ( ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) )
372 368 371 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) = ( ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) )
373 72 recnd ⊢ ( 𝜑 → ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℂ )
374 214 373 361 adddid ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) = ( ( ( ( 2 · 𝑁 ) / 3 ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) )
375 94 rpge0d ⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑁 ) )
376 remsqsqrt ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) = ( 2 · 𝑁 ) )
377 237 375 376 syl2anc ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) = ( 2 · 𝑁 ) )
378 377 oveq1d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) / 3 ) = ( ( 2 · 𝑁 ) / 3 ) )
379 113 recnd ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℂ )
380 224 a1i ⊢ ( 𝜑 → 3 ≠ 0 )
381 379 379 334 380 div23d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) · ( √ ‘ ( 2 · 𝑁 ) ) ) / 3 ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( √ ‘ ( 2 · 𝑁 ) ) ) )
382 378 381 eqtr3d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( √ ‘ ( 2 · 𝑁 ) ) ) )
383 382 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( √ ‘ ( 2 · 𝑁 ) ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) )
384 251 379 373 mulassd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( √ ‘ ( 2 · 𝑁 ) ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
385 0le2 ⊢ 0 ≤ 2
386 117 385 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 ≤ 2 )
387 60 rprege0d ⊢ ( 𝜑 → ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
388 sqrtmul ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ) → ( √ ‘ ( 2 · 𝑁 ) ) = ( ( √ ‘ 2 ) · ( √ ‘ 𝑁 ) ) )
389 386 387 388 sylancr ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) = ( ( √ ‘ 2 ) · ( √ ‘ 𝑁 ) ) )
390 389 oveq1d ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ( ( √ ‘ 2 ) · ( √ ‘ 𝑁 ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) )
391 59 recni ⊢ ( √ ‘ 2 ) ∈ ℂ
392 391 a1i ⊢ ( 𝜑 → ( √ ‘ 2 ) ∈ ℂ )
393 61 rpcnd ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℂ )
394 70 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ∈ ℂ )
395 392 393 392 394 mul4d ⊢ ( 𝜑 → ( ( ( √ ‘ 2 ) · ( √ ‘ 𝑁 ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) · ( ( √ ‘ 𝑁 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) )
396 remsqsqrt ⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) = 2 )
397 117 385 396 mp2an ⊢ ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) = 2
398 397 a1i ⊢ ( 𝜑 → ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) = 2 )
399 67 oveq2d ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) = ( ( √ ‘ 𝑁 ) · ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) ) )
400 68 recnd ⊢ ( 𝜑 → ( log ‘ ( √ ‘ 𝑁 ) ) ∈ ℂ )
401 61 rpne0d ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ≠ 0 )
402 400 393 401 divcan2d ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · ( ( log ‘ ( √ ‘ 𝑁 ) ) / ( √ ‘ 𝑁 ) ) ) = ( log ‘ ( √ ‘ 𝑁 ) ) )
403 399 402 eqtrd ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) = ( log ‘ ( √ ‘ 𝑁 ) ) )
404 398 403 oveq12d ⊢ ( 𝜑 → ( ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) · ( ( √ ‘ 𝑁 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( 2 · ( log ‘ ( √ ‘ 𝑁 ) ) ) )
405 400 2timesd ⊢ ( 𝜑 → ( 2 · ( log ‘ ( √ ‘ 𝑁 ) ) ) = ( ( log ‘ ( √ ‘ 𝑁 ) ) + ( log ‘ ( √ ‘ 𝑁 ) ) ) )
406 61 61 relogmuld ⊢ ( 𝜑 → ( log ‘ ( ( √ ‘ 𝑁 ) · ( √ ‘ 𝑁 ) ) ) = ( ( log ‘ ( √ ‘ 𝑁 ) ) + ( log ‘ ( √ ‘ 𝑁 ) ) ) )
407 remsqsqrt ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → ( ( √ ‘ 𝑁 ) · ( √ ‘ 𝑁 ) ) = 𝑁 )
408 387 407 syl ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · ( √ ‘ 𝑁 ) ) = 𝑁 )
409 408 fveq2d ⊢ ( 𝜑 → ( log ‘ ( ( √ ‘ 𝑁 ) · ( √ ‘ 𝑁 ) ) ) = ( log ‘ 𝑁 ) )
410 406 409 eqtr3d ⊢ ( 𝜑 → ( ( log ‘ ( √ ‘ 𝑁 ) ) + ( log ‘ ( √ ‘ 𝑁 ) ) ) = ( log ‘ 𝑁 ) )
411 404 405 410 3eqtrd ⊢ ( 𝜑 → ( ( ( √ ‘ 2 ) · ( √ ‘ 2 ) ) · ( ( √ ‘ 𝑁 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( log ‘ 𝑁 ) )
412 390 395 411 3eqtrd ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( log ‘ 𝑁 ) )
413 412 oveq2d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) )
414 383 384 413 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) )
415 414 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) / 3 ) · ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) )
416 374 415 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) )
417 382 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( √ ‘ ( 2 · 𝑁 ) ) ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
418 251 379 370 mulassd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( √ ‘ ( 2 · 𝑁 ) ) ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) )
419 95 rpne0d ⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ≠ 0 )
420 245 379 419 divcan2d ⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) = ( log ‘ 2 ) )
421 420 oveq2d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) )
422 417 418 421 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) = ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) )
423 416 422 oveq12d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) / 3 ) · ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑁 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) = ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) + ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) ) )
424 360 362 addcld ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) ∈ ℂ )
425 424 359 addcomd ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) + ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) ) )
426 372 423 425 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 2 ) ) + ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ 𝑁 ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) ) )
427 363 367 426 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) = ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( 2 · 𝑁 ) / 3 ) · ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑁 / 2 ) ) ) ) ) )
428 251 253 mulcld ⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ∈ ℂ )
429 addcl ⊢ ( ( ( 2 · ( log ‘ 2 ) ) ∈ ℂ ∧ ( 2 · ( log ‘ 𝑁 ) ) ∈ ℂ ) → ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) ∈ ℂ )
430 351 283 429 sylancr ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) ∈ ℂ )
431 428 430 354 addassd ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 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 ) ) ) ) ) )
432 357 427 431 3eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) = ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( 2 · ( log ‘ 2 ) ) + ( 2 · ( log ‘ 𝑁 ) ) ) ) + ( ( log ‘ 𝑁 ) − ( 5 · ( log ‘ 2 ) ) ) ) )
433 270 272 432 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) = ( ( ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) · ( log ‘ ( 2 · 𝑁 ) ) ) + ( ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) · ( log ‘ 2 ) ) ) − ( ( ( ( 4 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) − ( log ‘ 𝑁 ) ) ) )
434 191 250 433 3brtr4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) < ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) )
435 100 99 213 ltmul2d ⊢ ( 𝜑 → ( ( log ‘ 2 ) < ( 𝐹 ‘ 𝑁 ) ↔ ( ( ( 2 · 𝑁 ) / 3 ) · ( log ‘ 2 ) ) < ( ( ( 2 · 𝑁 ) / 3 ) · ( 𝐹 ‘ 𝑁 ) ) ) )
436 434 435 mpbird ⊢ ( 𝜑 → ( log ‘ 2 ) < ( 𝐹 ‘ 𝑁 ) )
437 46 100 99 101 436 lttrd ⊢ ( 𝜑 → ( 𝐹 ‘ 6 4 ) < ( 𝐹 ‘ 𝑁 ) )
438 46 99 437 ltnsymd ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑁 ) < ( 𝐹 ‘ 6 4 ) )
439 43 438 pm2.21dd ⊢ ( 𝜑 → 𝜓 )