bposlem9 - Metamath Proof Explorer

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

Theorem bposlem9 27255

Description: Lemma for bpos 27256. 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.

Step	Hyp	Ref	Expression
1		bposlem9.4	. . 3 ⊢ (𝜑 → ;64 < 𝑁)
2		bposlem7.1	. . . 4 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))
3		bposlem7.2	. . . 4 ⊢ 𝐺 = (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) / 𝑥))
4		6nn0 12522	. . . . . 6 ⊢ 6 ∈ ℕ₀
5		4nn 12323	. . . . . 6 ⊢ 4 ∈ ℕ
6	4, 5	decnncl 12728	. . . . 5 ⊢ ;64 ∈ ℕ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → ;64 ∈ ℕ)
8		bposlem9.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		ere 16105	. . . . . . . 8 ⊢ e ∈ ℝ
10		8re 12336	. . . . . . . 8 ⊢ 8 ∈ ℝ
11		egt2lt3 16224	. . . . . . . . . 10 ⊢ (2 < e ∧ e < 3)
12	11	simpri 485	. . . . . . . . 9 ⊢ e < 3
13		3lt8 12436	. . . . . . . . 9 ⊢ 3 < 8
14		3re 12320	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
15	9, 14, 10	lttri 11361	. . . . . . . . 9 ⊢ ((e < 3 ∧ 3 < 8) → e < 8)
16	12, 13, 15	mp2an 692	. . . . . . . 8 ⊢ e < 8
17	9, 10, 16	ltleii 11358	. . . . . . 7 ⊢ e ≤ 8
18		0re 11237	. . . . . . . . 9 ⊢ 0 ∈ ℝ
19		epos 16225	. . . . . . . . 9 ⊢ 0 < e
20	18, 9, 19	ltleii 11358	. . . . . . . 8 ⊢ 0 ≤ e
21		8pos 12352	. . . . . . . . 9 ⊢ 0 < 8
22	18, 10, 21	ltleii 11358	. . . . . . . 8 ⊢ 0 ≤ 8
23		le2sq 14152	. . . . . . . 8 ⊢ (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
24	9, 20, 10, 22, 23	mp4an 693	. . . . . . 7 ⊢ (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
25	17, 24	mpbi 230	. . . . . 6 ⊢ (e↑2) ≤ (8↑2)
26	10	recni 11249	. . . . . . . 8 ⊢ 8 ∈ ℂ
27	26	sqvali 14198	. . . . . . 7 ⊢ (8↑2) = (8 · 8)
28		8t8e64 12829	. . . . . . 7 ⊢ (8 · 8) = ;64
29	27, 28	eqtri 2758	. . . . . 6 ⊢ (8↑2) = ;64
30	25, 29	breqtri 5144	. . . . 5 ⊢ (e↑2) ≤ ;64
31	30	a1i 11	. . . 4 ⊢ (𝜑 → (e↑2) ≤ ;64)
32	9	resqcli 14204	. . . . . 6 ⊢ (e↑2) ∈ ℝ
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → (e↑2) ∈ ℝ)
34	6	nnrei 12249	. . . . . 6 ⊢ ;64 ∈ ℝ
35	34	a1i 11	. . . . 5 ⊢ (𝜑 → ;64 ∈ ℝ)
36	8	nnred 12255	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
37		ltle 11323	. . . . . . 7 ⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁))
38	34, 36, 37	sylancr 587	. . . . . 6 ⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁))
39	1, 38	mpd 15	. . . . 5 ⊢ (𝜑 → ;64 ≤ 𝑁)
40	33, 35, 36, 31, 39	letrd 11392	. . . 4 ⊢ (𝜑 → (e↑2) ≤ 𝑁)
41	2, 3, 7, 8, 31, 40	bposlem7 27253	. . 3 ⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64)))
42	1, 41	mpd 15	. 2 ⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64))
43	2, 3	bposlem8 27254	. . . . 5 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
44	43	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)))
45	44	simpld 494	. . 3 ⊢ (𝜑 → (𝐹‘;64) ∈ ℝ)
46		2fveq3 6881	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
47	46	oveq2d 7421	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
48		fvoveq1 7428	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
49	48	oveq2d 7421	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
50	47, 49	oveq12d 7423	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
51		oveq2 7413	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
52	51	fveq2d 6880	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
53	52	oveq2d 7421	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
54	50, 53	oveq12d 7423	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
55		ovex 7438	. . . . . 6 ⊢ ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
56	54, 2, 55	fvmpt 6986	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57	8, 56	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
58		sqrt2re 16268	. . . . . . 7 ⊢ (√‘2) ∈ ℝ
59	8	nnrpd 13049	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
60	59	rpsqrtcld 15430	. . . . . . . . 9 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
61		fveq2 6876	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
62		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
63	61, 62	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
64		ovex 7438	. . . . . . . . . 10 ⊢ ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
65	63, 3, 64	fvmpt 6986	. . . . . . . . 9 ⊢ ((√‘𝑁) ∈ ℝ⁺ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66	60, 65	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
67	60	relogcld 26584	. . . . . . . . 9 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
68	67, 60	rerpdivcld 13082	. . . . . . . 8 ⊢ (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
69	66, 68	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
70		remulcl 11214	. . . . . . 7 ⊢ (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
71	58, 69, 70	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
72		9re 12339	. . . . . . . 8 ⊢ 9 ∈ ℝ
73		4re 12324	. . . . . . . 8 ⊢ 4 ∈ ℝ
74		4ne0 12348	. . . . . . . 8 ⊢ 4 ≠ 0
75	72, 73, 74	redivcli 12008	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
76	59	rphalfcld 13063	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ⁺)
77		fveq2 6876	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
78		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
79	77, 78	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
80		ovex 7438	. . . . . . . . . 10 ⊢ ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
81	79, 3, 80	fvmpt 6986	. . . . . . . . 9 ⊢ ((𝑁 / 2) ∈ ℝ⁺ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82	76, 81	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
83	76	relogcld 26584	. . . . . . . . 9 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
84	83, 76	rerpdivcld 13082	. . . . . . . 8 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
85	82, 84	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
86		remulcl 11214	. . . . . . 7 ⊢ (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
87	75, 85, 86	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
88	71, 87	readdcld 11264	. . . . 5 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
89		2rp 13013	. . . . . . 7 ⊢ 2 ∈ ℝ⁺
90		relogcl 26536	. . . . . . 7 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
91	89, 90	ax-mp 5	. . . . . 6 ⊢ (log‘2) ∈ ℝ
92		rpmulcl 13032	. . . . . . . 8 ⊢ ((2 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (2 · 𝑁) ∈ ℝ⁺)
93	89, 59, 92	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
94	93	rpsqrtcld 15430	. . . . . 6 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ⁺)
95		rerpdivcl 13039	. . . . . 6 ⊢ (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ⁺) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
96	91, 94, 95	sylancr 587	. . . . 5 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
97	88, 96	readdcld 11264	. . . 4 ⊢ (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
98	57, 97	eqeltrd 2834	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ)
99	91	a1i 11	. . . 4 ⊢ (𝜑 → (log‘2) ∈ ℝ)
100	44	simprd 495	. . . 4 ⊢ (𝜑 → (𝐹‘;64) < (log‘2))
101		nnrp 13020	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
102	5, 101	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
103		relogcl 26536	. . . . . . . . . 10 ⊢ (4 ∈ ℝ⁺ → (log‘4) ∈ ℝ)
104	102, 103	ax-mp 5	. . . . . . . . 9 ⊢ (log‘4) ∈ ℝ
105		remulcl 11214	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
106	36, 104, 105	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
107	59	relogcld 26584	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
108	106, 107	resubcld 11665	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
109		rpre 13017	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → (2 · 𝑁) ∈ ℝ)
110		rpge0 13022	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → 0 ≤ (2 · 𝑁))
111	109, 110	resqrtcld 15436	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → (√‘(2 · 𝑁)) ∈ ℝ)
112	93, 111	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
113		3nn 12319	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
114		nndivre 12281	. . . . . . . . . . 11 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
115	112, 113, 114	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
116		2re 12314	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
117		readdcl 11212	. . . . . . . . . 10 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
118	115, 116, 117	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
119	93	relogcld 26584	. . . . . . . . 9 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
120	118, 119	remulcld 11265	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
121		remulcl 11214	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
122	73, 36, 121	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
123		nndivre 12281	. . . . . . . . . . 11 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
124	122, 113, 123	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
125		5re 12327	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
126		resubcl 11547	. . . . . . . . . 10 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
127	124, 125, 126	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
128		remulcl 11214	. . . . . . . . 9 ⊢ (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
129	127, 91, 128	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
130	120, 129	readdcld 11264	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
131		remulcl 11214	. . . . . . . . 9 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
132	124, 91, 131	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
133	132, 107	resubcld 11665	. . . . . . 7 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
134	8	nnzd 12615	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
135		df-5 12306	. . . . . . . . . . . 12 ⊢ 5 = (4 + 1)
136	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
137		6nn 12329	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ
138		4nn0 12520	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
139		4lt10 12844	. . . . . . . . . . . . . . . 16 ⊢ 4 < ;10
140	137, 138, 138, 139	declti 12746	. . . . . . . . . . . . . . 15 ⊢ 4 < ;64
141	140	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 < ;64)
142	136, 35, 36, 141, 1	lttrd 11396	. . . . . . . . . . . . 13 ⊢ (𝜑 → 4 < 𝑁)
143		4z 12626	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
144		zltp1le 12642	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
145	143, 134, 144	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
146	142, 145	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 + 1) ≤ 𝑁)
147	135, 146	eqbrtrid 5154	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ≤ 𝑁)
148		5nn 12326	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ
149	148	nnzi 12616	. . . . . . . . . . . 12 ⊢ 5 ∈ ℤ
150	149	eluz1i 12860	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
151	134, 147, 150	sylanbrc 583	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
152		bposlem9.5	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
153		breq2 5123	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞))
154		breq1 5122	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
155	153, 154	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))))
156	155	cbvrexvw 3221	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
157	152, 156	sylnib 328	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
158		eqid 2735	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
159		eqid 2735	. . . . . . . . . 10 ⊢ (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
160		eqid 2735	. . . . . . . . . 10 ⊢ (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
161	151, 157, 158, 159, 160	bposlem6 27252	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
162		reexplog 26556	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
163	102, 134, 162	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
164	59	reeflogd 26585	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
165	164	eqcomd 2741	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁)))
166	163, 165	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
167	106	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
168	107	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
169		efsub 16118	. . . . . . . . . . 11 ⊢ (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
170	167, 168, 169	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
171	166, 170	eqtr4d 2773	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
172	93	rpcnd 13053	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
173	93	rpne0d 13056	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ≠ 0)
174	118	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
175	172, 173, 174	cxpefd 26673	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
176		2cn 12315	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
177		2ne0 12344	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
178	127	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
179		cxpef 26626	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
180	176, 177, 178, 179	mp3an12i 1467	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
181	175, 180	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
182	120	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
183	129	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
184		efadd 16110	. . . . . . . . . . 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)))))
185	182, 183, 184	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (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 2773	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))) = (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
187	161, 171, 186	3brtr3d 5150	. . . . . . . 8 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188		eflt 16135	. . . . . . . . 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))))))
189	108, 130, 188	syl2anc 584	. . . . . . . 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))))))
190	187, 189	mpbird 257	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
191	108, 130, 133, 190	ltsub1dd 11849	. . . . . 6 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) < ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
192	36	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
193		mulcom 11215	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
194	176, 192, 193	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2))
195	194	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
196	91	recni 11249	. . . . . . . . . . . 12 ⊢ (log‘2) ∈ ℂ
197		mulass 11217	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
198	176, 196, 197	mp3an23 1455	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
199	192, 198	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200	196	2timesi 12378	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) = ((log‘2) + (log‘2))
201		relogmul 26553	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ 2 ∈ ℝ⁺) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
202	89, 89, 201	mp2an 692	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = ((log‘2) + (log‘2))
203		2t2e4 12404	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
204	203	fveq2i 6879	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = (log‘4)
205	200, 202, 204	3eqtr2i 2764	. . . . . . . . . . 11 ⊢ (2 · (log‘2)) = (log‘4)
206	205	oveq2i 7416	. . . . . . . . . 10 ⊢ (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
207	199, 206	eqtrdi 2786	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
208	195, 207	eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
209	208	oveq1d 7420	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
210	124	recnd 11263	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
211		3rp 13014	. . . . . . . . . . . 12 ⊢ 3 ∈ ℝ⁺
212		rpdivcl 13034	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → ((2 · 𝑁) / 3) ∈ ℝ⁺)
213	93, 211, 212	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ⁺)
214	213	rpcnd 13053	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
215		4p2e6 12393	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
216	215	oveq1i 7415	. . . . . . . . . . . . 13 ⊢ ((4 + 2) · 𝑁) = (6 · 𝑁)
217		4cn 12325	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
218		adddir 11226	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
219	217, 176, 192, 218	mp3an12i 1467	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
220	216, 219	eqtr3id 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
221	220	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
222		6cn 12331	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℂ
223		3cn 12321	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
224		3ne0 12346	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
225	223, 224	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
226		div23 11915	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
227	222, 225, 226	mp3an13 1454	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
228	192, 227	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
229		3t2e6 12406	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
230	229	oveq1i 7415	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = (6 / 3)
231	176, 223, 224	divcan3i 11987	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = 2
232	230, 231	eqtr3i 2760	. . . . . . . . . . . . 13 ⊢ (6 / 3) = 2
233	232	oveq1i 7415	. . . . . . . . . . . 12 ⊢ ((6 / 3) · 𝑁) = (2 · 𝑁)
234	228, 233	eqtrdi 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
235	122	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · 𝑁) ∈ ℂ)
236		remulcl 11214	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
237	116, 36, 236	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
238	237	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
239		divdir 11921	. . . . . . . . . . . . 13 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240	225, 239	mp3an3 1452	. . . . . . . . . . . 12 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
241	235, 238, 240	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
242	221, 234, 241	3eqtr3d 2778	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
243	210, 214, 242	mvrladdd 11650	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
244	243	oveq1d 7420	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
245	99	recnd 11263	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℂ)
246	238, 210, 245	subdird 11694	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
247	244, 246	eqtr3d 2772	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
248	132	recnd 11263	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
249	167, 248, 168	nnncan2d 11629	. . . . . . 7 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
250	209, 247, 249	3eqtr4d 2780	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
251	115	recnd 11263	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
252	176	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
253	119	recnd 11263	. . . . . . . . . 10 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
254	251, 252, 253	adddird 11260	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
255		relogmul 26553	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
256	89, 59, 255	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
257	256	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
258	252, 245, 168	adddid 11259	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
259	257, 258	eqtrd 2770	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
260	259	oveq2d 7421	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
261	254, 260	eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
262		5cn 12328	. . . . . . . . . . . 12 ⊢ 5 ∈ ℂ
263	262	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ∈ ℂ)
264	210, 263, 245	subdird 11694	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
265	264	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → (((((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 11242	. . . . . . . . . . 11 ⊢ (5 · (log‘2)) ∈ ℂ
267	266	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (5 · (log‘2)) ∈ ℂ)
268	248, 267, 168	nnncan1d 11628	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
269	265, 268	eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
270	261, 269	oveq12d 7423	. . . . . . 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)))))
271	133	recnd 11263	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
272	182, 183, 271	addsubassd 11614	. . . . . . 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‘𝑁)))))
273	262, 223, 196	subdiri 11687	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
274		3p2e5 12391	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
275	274	oveq1i 7415	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = (5 − 3)
276		pncan2 11489	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
277	223, 176, 276	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = 2
278	275, 277	eqtr3i 2760	. . . . . . . . . . . . . 14 ⊢ (5 − 3) = 2
279	278	oveq1i 7415	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = (2 · (log‘2))
280	273, 279	eqtr3i 2760	. . . . . . . . . . . 12 ⊢ ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2))
281	280	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ((5 · (log‘2)) − (3 · (log‘2))) = (2 · (log‘2)))
282		mulcl 11213	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
283	176, 168, 282	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
284		df-3 12304	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
285	284	oveq1i 7415	. . . . . . . . . . . . . . 15 ⊢ (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
286		1cnd 11230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℂ)
287	252, 286, 168	adddird 11260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
288	285, 287	eqtrid 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
289	168	mullidd 11253	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
290	289	oveq2d 7421	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
291	288, 290	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
292	291	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
293	283, 168, 267, 292	assraddsubd 11651	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
294	281, 293	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
295		relogdiv 26554	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ⁺ ∧ 2 ∈ ℝ⁺) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
296	59, 89, 295	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
297	296	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
298		subdi 11670	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
299	223, 196, 298	mp3an13 1454	. . . . . . . . . . . . 13 ⊢ ((log‘𝑁) ∈ ℂ → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
300	168, 299	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
301	297, 300	eqtrd 2770	. . . . . . . . . . 11 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
302		div23 11915	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
303	176, 225, 302	mp3an13 1454	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
304	192, 303	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
305	223, 176, 223, 176, 177, 177	divmuldivi 12001	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
306		3t3e9 12407	. . . . . . . . . . . . . . . . . 18 ⊢ (3 · 3) = 9
307	306, 203	oveq12i 7417	. . . . . . . . . . . . . . . . 17 ⊢ ((3 · 3) / (2 · 2)) = (9 / 4)
308	305, 307	eqtr2i 2759	. . . . . . . . . . . . . . . 16 ⊢ (9 / 4) = ((3 / 2) · (3 / 2))
309	308	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
310	304, 309	oveq12d 7423	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
311	176, 223, 224	divcli 11983	. . . . . . . . . . . . . . 15 ⊢ (2 / 3) ∈ ℂ
312	223, 176, 177	divcli 11983	. . . . . . . . . . . . . . . 16 ⊢ (3 / 2) ∈ ℂ
313		mul4 11403	. . . . . . . . . . . . . . . 16 ⊢ ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
314	312, 312, 313	mpanr12 705	. . . . . . . . . . . . . . 15 ⊢ (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
315	311, 192, 314	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
316		divcan6 11948	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
317	176, 177, 223, 224, 316	mp4an 693	. . . . . . . . . . . . . . . . 17 ⊢ ((2 / 3) · (3 / 2)) = 1
318	317	oveq1i 7415	. . . . . . . . . . . . . . . 16 ⊢ (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
319		mulcl 11213	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
320	192, 312, 319	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
321	320	mullidd 11253	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
322	318, 321	eqtrid 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
323		2cnne0 12450	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
324		div12 11918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
325	223, 323, 324	mp3an23 1455	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
326	192, 325	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
327	322, 326	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
328	310, 315, 327	3eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
329	328, 82	oveq12d 7423	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
330	75	recni 11249	. . . . . . . . . . . . . 14 ⊢ (9 / 4) ∈ ℂ
331	330	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (9 / 4) ∈ ℂ)
332	85	recnd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
333	214, 331, 332	mulassd 11258	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
334	223	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 3 ∈ ℂ)
335	76	rpcnd 13053	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
336	83	recnd 11263	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
337	76	rpne0d 13056	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) ≠ 0)
338	336, 335, 337	divcld 12017	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
339	334, 335, 338	mulassd 11258	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
340	336, 335, 337	divcan2d 12019	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
341	340	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
342	339, 341	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
343	329, 333, 342	3eqtr3d 2778	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
344	223, 196	mulcli 11242	. . . . . . . . . . . . 13 ⊢ (3 · (log‘2)) ∈ ℂ
345	344	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘2)) ∈ ℂ)
346		mulcl 11213	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
347	223, 168, 346	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
348	267, 345, 347	npncan3d 11630	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
349	301, 343, 348	3eqtr4d 2780	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
350	116, 91	remulcli 11251	. . . . . . . . . . . . 13 ⊢ (2 · (log‘2)) ∈ ℝ
351	350	recni 11249	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) ∈ ℂ
352	351	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘2)) ∈ ℂ)
353		subcl 11481	. . . . . . . . . . . 12 ⊢ (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
354	168, 266, 353	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
355	352, 283, 354	addassd 11257	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
356	294, 349, 355	3eqtr4d 2780	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
357	356	oveq2d 7421	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2))))))
358		mulcl 11213	. . . . . . . . . . 11 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
359	251, 196, 358	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
360	251, 168	mulcld 11255	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
361	87	recnd 11263	. . . . . . . . . . 11 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
362	214, 361	mulcld 11255	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
363	359, 360, 362	addassd 11257	. . . . . . . . 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)))))))
364	256	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
365	251, 245, 168	adddid 11259	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
366	364, 365	eqtrd 2770	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
367	366	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = (((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
368	57	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
369	88	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
370	96	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
371	214, 369, 370	adddid 11259	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
372	368, 371	eqtrd 2770	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
373	71	recnd 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
374	214, 373, 361	adddid 11259	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
375	93	rpge0d 13055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
376		remsqsqrt 15275	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
377	237, 375, 376	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
378	377	oveq1d 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
379	112	recnd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
380	224	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≠ 0)
381	379, 379, 334, 380	div23d 12054	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
382	378, 381	eqtr3d 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
383	382	oveq1d 7420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
384	251, 379, 373	mulassd 11258	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
385		0le2 12342	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 2
386	116, 385	pm3.2i 470	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ ∧ 0 ≤ 2)
387	59	rprege0d 13058	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
388		sqrtmul 15278	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
389	386, 387, 388	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
390	389	oveq1d 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
391	58	recni 11249	. . . . . . . . . . . . . . . . . 18 ⊢ (√‘2) ∈ ℂ
392	391	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘2) ∈ ℂ)
393	60	rpcnd 13053	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
394	69	recnd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
395	392, 393, 392, 394	mul4d 11447	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
396		remsqsqrt 15275	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
397	116, 385, 396	mp2an 692	. . . . . . . . . . . . . . . . . . 19 ⊢ ((√‘2) · (√‘2)) = 2
398	397	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘2) · (√‘2)) = 2)
399	66	oveq2d 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
400	67	recnd 11263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
401	60	rpne0d 13056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
402	400, 393, 401	divcan2d 12019	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
403	399, 402	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
404	398, 403	oveq12d 7423	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
405	400	2timesd 12484	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
406	60, 60	relogmuld 26586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
407		remsqsqrt 15275	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
408	387, 407	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
409	408	fveq2d 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
410	406, 409	eqtr3d 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
411	404, 405, 410	3eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
412	390, 395, 411	3eqtrd 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
413	412	oveq2d 7421	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
414	383, 384, 413	3eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
415	414	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
416	374, 415	eqtrd 2770	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
417	382	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
418	251, 379, 370	mulassd 11258	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
419	94	rpne0d 13056	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
420	245, 379, 419	divcan2d 12019	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
421	420	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
422	417, 418, 421	3eqtrd 2774	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
423	416, 422	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝜑 → ((((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 11254	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
425	424, 359	addcomd 11437	. . . . . . . . . 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)))))))
426	372, 423, 425	3eqtrd 2774	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
427	363, 367, 426	3eqtr4rd 2781	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
428	251, 253	mulcld 11255	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
429		addcl 11211	. . . . . . . . . 10 ⊢ (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
430	351, 283, 429	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
431	428, 430, 354	addassd 11257	. . . . . . . 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))))))
432	357, 427, 431	3eqtr4d 2780	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
433	270, 272, 432	3eqtr4rd 2781	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
434	191, 250, 433	3brtr4d 5151	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁)))
435	99, 98, 213	ltmul2d 13093	. . . . 5 ⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁))))
436	434, 435	mpbird 257	. . . 4 ⊢ (𝜑 → (log‘2) < (𝐹‘𝑁))
437	45, 99, 98, 100, 436	lttrd 11396	. . 3 ⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁))
438	45, 98, 437	ltnsymd 11384	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64))
439	42, 438	pm2.21dd 195	1 ⊢ (𝜑 → 𝜓)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∃wrex 3060 ifcif 4500 class class class wbr 5119 ↦ cmpt 5201 ‘cfv 6531 (class class class)co 7405 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 < clt 11269 ≤ cle 11270 − cmin 11466 / cdiv 11894 ℕcn 12240 2c2 12295 3c3 12296 4c4 12297 5c5 12298 6c6 12299 8c8 12301 9c9 12302 ℤcz 12588 cdc 12708 ℤ_≥cuz 12852 ℝ⁺crp 13008 ⌊cfl 13807 ↑cexp 14079 Ccbc 14320 √csqrt 15252 expce 16077 eceu 16078 ℙcprime 16690 pCnt cpc 16856 logclog 26515 ↑_𝑐ccxp 26516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-inf2 9655 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207 ax-addf 11208

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7671 df-om 7862 df-1st 7988 df-2nd 7989 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8719 df-map 8842 df-pm 8843 df-ixp 8912 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fsupp 9374 df-fi 9423 df-sup 9454 df-inf 9455 df-oi 9524 df-dju 9915 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-xnn0 12575 df-z 12589 df-dec 12709 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13366 df-ioc 13367 df-ico 13368 df-icc 13369 df-fz 13525 df-fzo 13672 df-fl 13809 df-mod 13887 df-seq 14020 df-exp 14080 df-fac 14292 df-bc 14321 df-hash 14349 df-shft 15086 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-limsup 15487 df-clim 15504 df-rlim 15505 df-sum 15703 df-ef 16083 df-e 16084 df-sin 16085 df-cos 16086 df-pi 16088 df-dvds 16273 df-gcd 16514 df-prm 16691 df-pc 16857 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-starv 17286 df-sca 17287 df-vsca 17288 df-ip 17289 df-tset 17290 df-ple 17291 df-ds 17293 df-unif 17294 df-hom 17295 df-cco 17296 df-rest 17436 df-topn 17437 df-0g 17455 df-gsum 17456 df-topgen 17457 df-pt 17458 df-prds 17461 df-xrs 17516 df-qtop 17521 df-imas 17522 df-xps 17524 df-mre 17598 df-mrc 17599 df-acs 17601 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-submnd 18762 df-mulg 19051 df-cntz 19300 df-cmn 19763 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-fbas 21312 df-fg 21313 df-cnfld 21316 df-top 22832 df-topon 22849 df-topsp 22871 df-bases 22884 df-cld 22957 df-ntr 22958 df-cls 22959 df-nei 23036 df-lp 23074 df-perf 23075 df-cn 23165 df-cnp 23166 df-haus 23253 df-tx 23500 df-hmeo 23693 df-fil 23784 df-fm 23876 df-flim 23877 df-flf 23878 df-xms 24259 df-ms 24260 df-tms 24261 df-cncf 24822 df-limc 25819 df-dv 25820 df-log 26517 df-cxp 26518 df-cht 27059 df-ppi 27062

This theorem is referenced by: bpos 27256

W3C validator