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	$⊢ F = (n \in ℕ ⟼ \sqrt{2} G (\sqrt{n}) + (\frac{9}{4}) G (\frac{n}{2}) + (\frac{\log 2}{\sqrt{2 n}}))$
	bposlem7.2	$⊢ G = (x \in ℝ^{+} ⟼ \frac{\log x}{x})$
	bposlem9.3	$⊢ φ \to N \in ℕ$
	bposlem9.4	$⊢ φ \to 64 < N$
	bposlem9.5	$⊢ φ \to \neg \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
Assertion	bposlem9	$⊢ φ \to ψ$

Proof

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

Metamath Proof Explorer

Theorem bposlem9

Proof