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 27031

Description: Lemma for bpos 27032. 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 12497	. . . . . 6 ⊢ 6 ∈ ℕ₀
5		4nn 12299	. . . . . 6 ⊢ 4 ∈ ℕ
6	4, 5	decnncl 12701	. . . . 5 ⊢ ;64 ∈ ℕ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → ;64 ∈ ℕ)
8		bposlem9.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		ere 16036	. . . . . . . 8 ⊢ e ∈ ℝ
10		8re 12312	. . . . . . . 8 ⊢ 8 ∈ ℝ
11		egt2lt3 16153	. . . . . . . . . 10 ⊢ (2 < e ∧ e < 3)
12	11	simpri 484	. . . . . . . . 9 ⊢ e < 3
13		3lt8 12412	. . . . . . . . 9 ⊢ 3 < 8
14		3re 12296	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
15	9, 14, 10	lttri 11344	. . . . . . . . 9 ⊢ ((e < 3 ∧ 3 < 8) → e < 8)
16	12, 13, 15	mp2an 688	. . . . . . . 8 ⊢ e < 8
17	9, 10, 16	ltleii 11341	. . . . . . 7 ⊢ e ≤ 8
18		0re 11220	. . . . . . . . 9 ⊢ 0 ∈ ℝ
19		epos 16154	. . . . . . . . 9 ⊢ 0 < e
20	18, 9, 19	ltleii 11341	. . . . . . . 8 ⊢ 0 ≤ e
21		8pos 12328	. . . . . . . . 9 ⊢ 0 < 8
22	18, 10, 21	ltleii 11341	. . . . . . . 8 ⊢ 0 ≤ 8
23		le2sq 14103	. . . . . . . 8 ⊢ (((e ∈ ℝ ∧ 0 ≤ e) ∧ (8 ∈ ℝ ∧ 0 ≤ 8)) → (e ≤ 8 ↔ (e↑2) ≤ (8↑2)))
24	9, 20, 10, 22, 23	mp4an 689	. . . . . . 7 ⊢ (e ≤ 8 ↔ (e↑2) ≤ (8↑2))
25	17, 24	mpbi 229	. . . . . 6 ⊢ (e↑2) ≤ (8↑2)
26	10	recni 11232	. . . . . . . 8 ⊢ 8 ∈ ℂ
27	26	sqvali 14148	. . . . . . 7 ⊢ (8↑2) = (8 · 8)
28		8t8e64 12802	. . . . . . 7 ⊢ (8 · 8) = ;64
29	27, 28	eqtri 2758	. . . . . 6 ⊢ (8↑2) = ;64
30	25, 29	breqtri 5172	. . . . 5 ⊢ (e↑2) ≤ ;64
31	30	a1i 11	. . . 4 ⊢ (𝜑 → (e↑2) ≤ ;64)
32	9	resqcli 14154	. . . . . 6 ⊢ (e↑2) ∈ ℝ
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → (e↑2) ∈ ℝ)
34	6	nnrei 12225	. . . . . 6 ⊢ ;64 ∈ ℝ
35	34	a1i 11	. . . . 5 ⊢ (𝜑 → ;64 ∈ ℝ)
36	8	nnred 12231	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
37		ltle 11306	. . . . . . 7 ⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁))
38	34, 36, 37	sylancr 585	. . . . . 6 ⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁))
39	1, 38	mpd 15	. . . . 5 ⊢ (𝜑 → ;64 ≤ 𝑁)
40	33, 35, 36, 31, 39	letrd 11375	. . . 4 ⊢ (𝜑 → (e↑2) ≤ 𝑁)
41	2, 3, 7, 8, 31, 40	bposlem7 27029	. . 3 ⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64)))
42	1, 41	mpd 15	. 2 ⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64))
43	2, 3	bposlem8 27030	. . . . 5 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
44	43	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)))
45	44	simpld 493	. . 3 ⊢ (𝜑 → (𝐹‘;64) ∈ ℝ)
46		2fveq3 6895	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
47	46	oveq2d 7427	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
48		fvoveq1 7434	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
49	48	oveq2d 7427	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
50	47, 49	oveq12d 7429	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
51		oveq2 7419	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
52	51	fveq2d 6894	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
53	52	oveq2d 7427	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
54	50, 53	oveq12d 7429	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
55		ovex 7444	. . . . . 6 ⊢ ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
56	54, 2, 55	fvmpt 6997	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57	8, 56	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
58		sqrt2re 16197	. . . . . . 7 ⊢ (√‘2) ∈ ℝ
59	8	nnrpd 13018	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
60	59	rpsqrtcld 15362	. . . . . . . . 9 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
61		fveq2 6890	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
62		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
63	61, 62	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
64		ovex 7444	. . . . . . . . . 10 ⊢ ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
65	63, 3, 64	fvmpt 6997	. . . . . . . . 9 ⊢ ((√‘𝑁) ∈ ℝ⁺ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66	60, 65	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
67	60	relogcld 26367	. . . . . . . . 9 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
68	67, 60	rerpdivcld 13051	. . . . . . . 8 ⊢ (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
69	66, 68	eqeltrd 2831	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
70		remulcl 11197	. . . . . . 7 ⊢ (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
71	58, 69, 70	sylancr 585	. . . . . 6 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
72		9re 12315	. . . . . . . 8 ⊢ 9 ∈ ℝ
73		4re 12300	. . . . . . . 8 ⊢ 4 ∈ ℝ
74		4ne0 12324	. . . . . . . 8 ⊢ 4 ≠ 0
75	72, 73, 74	redivcli 11985	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
76	59	rphalfcld 13032	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ⁺)
77		fveq2 6890	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
78		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
79	77, 78	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
80		ovex 7444	. . . . . . . . . 10 ⊢ ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
81	79, 3, 80	fvmpt 6997	. . . . . . . . 9 ⊢ ((𝑁 / 2) ∈ ℝ⁺ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82	76, 81	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
83	76	relogcld 26367	. . . . . . . . 9 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
84	83, 76	rerpdivcld 13051	. . . . . . . 8 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
85	82, 84	eqeltrd 2831	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
86		remulcl 11197	. . . . . . 7 ⊢ (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
87	75, 85, 86	sylancr 585	. . . . . 6 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
88	71, 87	readdcld 11247	. . . . 5 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
89		2rp 12983	. . . . . . 7 ⊢ 2 ∈ ℝ⁺
90		relogcl 26320	. . . . . . 7 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
91	89, 90	ax-mp 5	. . . . . 6 ⊢ (log‘2) ∈ ℝ
92		rpmulcl 13001	. . . . . . . 8 ⊢ ((2 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (2 · 𝑁) ∈ ℝ⁺)
93	89, 59, 92	sylancr 585	. . . . . . 7 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
94	93	rpsqrtcld 15362	. . . . . 6 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ⁺)
95		rerpdivcl 13008	. . . . . 6 ⊢ (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ⁺) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
96	91, 94, 95	sylancr 585	. . . . 5 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
97	88, 96	readdcld 11247	. . . 4 ⊢ (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
98	57, 97	eqeltrd 2831	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ)
99	91	a1i 11	. . . 4 ⊢ (𝜑 → (log‘2) ∈ ℝ)
100	44	simprd 494	. . . 4 ⊢ (𝜑 → (𝐹‘;64) < (log‘2))
101		nnrp 12989	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
102	5, 101	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
103		relogcl 26320	. . . . . . . . . 10 ⊢ (4 ∈ ℝ⁺ → (log‘4) ∈ ℝ)
104	102, 103	ax-mp 5	. . . . . . . . 9 ⊢ (log‘4) ∈ ℝ
105		remulcl 11197	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
106	36, 104, 105	sylancl 584	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
107	59	relogcld 26367	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
108	106, 107	resubcld 11646	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
109		rpre 12986	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → (2 · 𝑁) ∈ ℝ)
110		rpge0 12991	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → 0 ≤ (2 · 𝑁))
111	109, 110	resqrtcld 15368	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → (√‘(2 · 𝑁)) ∈ ℝ)
112	93, 111	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
113		3nn 12295	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
114		nndivre 12257	. . . . . . . . . . 11 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
115	112, 113, 114	sylancl 584	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
116		2re 12290	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
117		readdcl 11195	. . . . . . . . . 10 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
118	115, 116, 117	sylancl 584	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
119	93	relogcld 26367	. . . . . . . . 9 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
120	118, 119	remulcld 11248	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
121		remulcl 11197	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
122	73, 36, 121	sylancr 585	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
123		nndivre 12257	. . . . . . . . . . 11 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
124	122, 113, 123	sylancl 584	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
125		5re 12303	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
126		resubcl 11528	. . . . . . . . . 10 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
127	124, 125, 126	sylancl 584	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
128		remulcl 11197	. . . . . . . . 9 ⊢ (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
129	127, 91, 128	sylancl 584	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
130	120, 129	readdcld 11247	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
131		remulcl 11197	. . . . . . . . 9 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
132	124, 91, 131	sylancl 584	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
133	132, 107	resubcld 11646	. . . . . . 7 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
134	8	nnzd 12589	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
135		df-5 12282	. . . . . . . . . . . 12 ⊢ 5 = (4 + 1)
136	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
137		6nn 12305	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ
138		4nn0 12495	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
139		4lt10 12817	. . . . . . . . . . . . . . . 16 ⊢ 4 < ;10
140	137, 138, 138, 139	declti 12719	. . . . . . . . . . . . . . 15 ⊢ 4 < ;64
141	140	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 < ;64)
142	136, 35, 36, 141, 1	lttrd 11379	. . . . . . . . . . . . 13 ⊢ (𝜑 → 4 < 𝑁)
143		4z 12600	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
144		zltp1le 12616	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
145	143, 134, 144	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
146	142, 145	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 + 1) ≤ 𝑁)
147	135, 146	eqbrtrid 5182	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ≤ 𝑁)
148		5nn 12302	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ
149	148	nnzi 12590	. . . . . . . . . . . 12 ⊢ 5 ∈ ℤ
150	149	eluz1i 12834	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
151	134, 147, 150	sylanbrc 581	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
152		bposlem9.5	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
153		breq2 5151	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞))
154		breq1 5150	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
155	153, 154	anbi12d 629	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))))
156	155	cbvrexvw 3233	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
157	152, 156	sylnib 327	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
158		eqid 2730	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
159		eqid 2730	. . . . . . . . . 10 ⊢ (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
160		eqid 2730	. . . . . . . . . 10 ⊢ (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
161	151, 157, 158, 159, 160	bposlem6 27028	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
162		reexplog 26339	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
163	102, 134, 162	sylancr 585	. . . . . . . . . . 11 ⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
164	59	reeflogd 26368	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
165	164	eqcomd 2736	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁)))
166	163, 165	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
167	106	recnd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
168	107	recnd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
169		efsub 16047	. . . . . . . . . . 11 ⊢ (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
170	167, 168, 169	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
171	166, 170	eqtr4d 2773	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
172	93	rpcnd 13022	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
173	93	rpne0d 13025	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ≠ 0)
174	118	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
175	172, 173, 174	cxpefd 26456	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
176		2cn 12291	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
177		2ne0 12320	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
178	127	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
179		cxpef 26409	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
180	176, 177, 178, 179	mp3an12i 1463	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
181	175, 180	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
182	120	recnd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
183	129	recnd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
184		efadd 16041	. . . . . . . . . . 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 582	. . . . . . . . . 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 5178	. . . . . . . 8 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188		eflt 16064	. . . . . . . . 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 582	. . . . . . . 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 256	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
191	108, 130, 133, 190	ltsub1dd 11830	. . . . . 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 11246	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
193		mulcom 11198	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
194	176, 192, 193	sylancr 585	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2))
195	194	oveq1d 7426	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
196	91	recni 11232	. . . . . . . . . . . 12 ⊢ (log‘2) ∈ ℂ
197		mulass 11200	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
198	176, 196, 197	mp3an23 1451	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
199	192, 198	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200	196	2timesi 12354	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) = ((log‘2) + (log‘2))
201		relogmul 26336	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ 2 ∈ ℝ⁺) → (log‘(2 · 2)) = ((log‘2) + (log‘2)))
202	89, 89, 201	mp2an 688	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = ((log‘2) + (log‘2))
203		2t2e4 12380	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
204	203	fveq2i 6893	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = (log‘4)
205	200, 202, 204	3eqtr2i 2764	. . . . . . . . . . 11 ⊢ (2 · (log‘2)) = (log‘4)
206	205	oveq2i 7422	. . . . . . . . . 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 7426	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
210	124	recnd 11246	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
211		3rp 12984	. . . . . . . . . . . 12 ⊢ 3 ∈ ℝ⁺
212		rpdivcl 13003	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → ((2 · 𝑁) / 3) ∈ ℝ⁺)
213	93, 211, 212	sylancl 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ⁺)
214	213	rpcnd 13022	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
215		4p2e6 12369	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
216	215	oveq1i 7421	. . . . . . . . . . . . 13 ⊢ ((4 + 2) · 𝑁) = (6 · 𝑁)
217		4cn 12301	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
218		adddir 11209	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
219	217, 176, 192, 218	mp3an12i 1463	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
220	216, 219	eqtr3id 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
221	220	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
222		6cn 12307	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℂ
223		3cn 12297	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
224		3ne0 12322	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
225	223, 224	pm3.2i 469	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
226		div23 11895	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
227	222, 225, 226	mp3an13 1450	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
228	192, 227	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
229		3t2e6 12382	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
230	229	oveq1i 7421	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = (6 / 3)
231	176, 223, 224	divcan3i 11964	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = 2
232	230, 231	eqtr3i 2760	. . . . . . . . . . . . 13 ⊢ (6 / 3) = 2
233	232	oveq1i 7421	. . . . . . . . . . . 12 ⊢ ((6 / 3) · 𝑁) = (2 · 𝑁)
234	228, 233	eqtrdi 2786	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
235	122	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · 𝑁) ∈ ℂ)
236		remulcl 11197	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
237	116, 36, 236	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
238	237	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
239		divdir 11901	. . . . . . . . . . . . 13 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240	225, 239	mp3an3 1448	. . . . . . . . . . . 12 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
241	235, 238, 240	syl2anc 582	. . . . . . . . . . 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 11631	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
244	243	oveq1d 7426	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
245	99	recnd 11246	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℂ)
246	238, 210, 245	subdird 11675	. . . . . . . 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 11246	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
249	167, 248, 168	nnncan2d 11610	. . . . . . 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 11246	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
252	176	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
253	119	recnd 11246	. . . . . . . . . 10 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
254	251, 252, 253	adddird 11243	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
255		relogmul 26336	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
256	89, 59, 255	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
257	256	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
258	252, 245, 168	adddid 11242	. . . . . . . . . . 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 7427	. . . . . . . . 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 12304	. . . . . . . . . . . 12 ⊢ 5 ∈ ℂ
263	262	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ∈ ℂ)
264	210, 263, 245	subdird 11675	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
265	264	oveq1d 7426	. . . . . . . . 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 11225	. . . . . . . . . . 11 ⊢ (5 · (log‘2)) ∈ ℂ
267	266	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (5 · (log‘2)) ∈ ℂ)
268	248, 267, 168	nnncan1d 11609	. . . . . . . . 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 7429	. . . . . . 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 11246	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
272	182, 183, 271	addsubassd 11595	. . . . . . 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 11668	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
274		3p2e5 12367	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
275	274	oveq1i 7421	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = (5 − 3)
276		pncan2 11471	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
277	223, 176, 276	mp2an 688	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = 2
278	275, 277	eqtr3i 2760	. . . . . . . . . . . . . 14 ⊢ (5 − 3) = 2
279	278	oveq1i 7421	. . . . . . . . . . . . 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 11196	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
283	176, 168, 282	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
284		df-3 12280	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
285	284	oveq1i 7421	. . . . . . . . . . . . . . 15 ⊢ (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
286		1cnd 11213	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℂ)
287	252, 286, 168	adddird 11243	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
288	285, 287	eqtrid 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
289	168	mullidd 11236	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
290	289	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
291	288, 290	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
292	291	oveq1d 7426	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
293	283, 168, 267, 292	assraddsubd 11632	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
294	281, 293	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
295		relogdiv 26337	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ⁺ ∧ 2 ∈ ℝ⁺) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
296	59, 89, 295	sylancl 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
297	296	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
298		subdi 11651	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
299	223, 196, 298	mp3an13 1450	. . . . . . . . . . . . 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 11895	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
303	176, 225, 302	mp3an13 1450	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
304	192, 303	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
305	223, 176, 223, 176, 177, 177	divmuldivi 11978	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
306		3t3e9 12383	. . . . . . . . . . . . . . . . . 18 ⊢ (3 · 3) = 9
307	306, 203	oveq12i 7423	. . . . . . . . . . . . . . . . 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 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
311	176, 223, 224	divcli 11960	. . . . . . . . . . . . . . 15 ⊢ (2 / 3) ∈ ℂ
312	223, 176, 177	divcli 11960	. . . . . . . . . . . . . . . 16 ⊢ (3 / 2) ∈ ℂ
313		mul4 11386	. . . . . . . . . . . . . . . 16 ⊢ ((((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ ((3 / 2) ∈ ℂ ∧ (3 / 2) ∈ ℂ)) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
314	312, 312, 313	mpanr12 701	. . . . . . . . . . . . . . 15 ⊢ (((2 / 3) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
315	311, 192, 314	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
316		divcan6 11925	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 / 3) · (3 / 2)) = 1)
317	176, 177, 223, 224, 316	mp4an 689	. . . . . . . . . . . . . . . . 17 ⊢ ((2 / 3) · (3 / 2)) = 1
318	317	oveq1i 7421	. . . . . . . . . . . . . . . 16 ⊢ (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
319		mulcl 11196	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
320	192, 312, 319	sylancl 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
321	320	mullidd 11236	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
322	318, 321	eqtrid 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
323		2cnne0 12426	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
324		div12 11898	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
325	223, 323, 324	mp3an23 1451	. . . . . . . . . . . . . . . 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 7429	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
330	75	recni 11232	. . . . . . . . . . . . . 14 ⊢ (9 / 4) ∈ ℂ
331	330	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (9 / 4) ∈ ℂ)
332	85	recnd 11246	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
333	214, 331, 332	mulassd 11241	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
334	223	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 3 ∈ ℂ)
335	76	rpcnd 13022	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
336	83	recnd 11246	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
337	76	rpne0d 13025	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) ≠ 0)
338	336, 335, 337	divcld 11994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
339	334, 335, 338	mulassd 11241	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
340	336, 335, 337	divcan2d 11996	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
341	340	oveq2d 7427	. . . . . . . . . . . . 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 11225	. . . . . . . . . . . . 13 ⊢ (3 · (log‘2)) ∈ ℂ
345	344	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘2)) ∈ ℂ)
346		mulcl 11196	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
347	223, 168, 346	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
348	267, 345, 347	npncan3d 11611	. . . . . . . . . . 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 11234	. . . . . . . . . . . . 13 ⊢ (2 · (log‘2)) ∈ ℝ
351	350	recni 11232	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) ∈ ℂ
352	351	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘2)) ∈ ℂ)
353		subcl 11463	. . . . . . . . . . . 12 ⊢ (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
354	168, 266, 353	sylancl 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
355	352, 283, 354	addassd 11240	. . . . . . . . . 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 7427	. . . . . . . 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 11196	. . . . . . . . . . 11 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
359	251, 196, 358	sylancl 584	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
360	251, 168	mulcld 11238	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
361	87	recnd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
362	214, 361	mulcld 11238	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
363	359, 360, 362	addassd 11240	. . . . . . . . 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 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
365	251, 245, 168	adddid 11242	. . . . . . . . . . 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 7426	. . . . . . . . 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 7427	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
369	88	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
370	96	recnd 11246	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
371	214, 369, 370	adddid 11242	. . . . . . . . . . 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 11246	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
374	214, 373, 361	adddid 11242	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
375	93	rpge0d 13024	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
376		remsqsqrt 15207	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
377	237, 375, 376	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
378	377	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
379	112	recnd 11246	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
380	224	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≠ 0)
381	379, 379, 334, 380	div23d 12031	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
382	378, 381	eqtr3d 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
383	382	oveq1d 7426	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
384	251, 379, 373	mulassd 11241	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
385		0le2 12318	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 2
386	116, 385	pm3.2i 469	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ ∧ 0 ≤ 2)
387	59	rprege0d 13027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
388		sqrtmul 15210	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
389	386, 387, 388	sylancr 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
390	389	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
391	58	recni 11232	. . . . . . . . . . . . . . . . . 18 ⊢ (√‘2) ∈ ℂ
392	391	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘2) ∈ ℂ)
393	60	rpcnd 13022	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
394	69	recnd 11246	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
395	392, 393, 392, 394	mul4d 11430	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
396		remsqsqrt 15207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
397	116, 385, 396	mp2an 688	. . . . . . . . . . . . . . . . . . 19 ⊢ ((√‘2) · (√‘2)) = 2
398	397	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘2) · (√‘2)) = 2)
399	66	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
400	67	recnd 11246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
401	60	rpne0d 13025	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
402	400, 393, 401	divcan2d 11996	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
403	399, 402	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
404	398, 403	oveq12d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
405	400	2timesd 12459	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
406	60, 60	relogmuld 26369	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
407		remsqsqrt 15207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
408	387, 407	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
409	408	fveq2d 6894	. . . . . . . . . . . . . . . . . 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 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
414	383, 384, 413	3eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
415	414	oveq1d 7426	. . . . . . . . . . . 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 7426	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
418	251, 379, 370	mulassd 11241	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
419	94	rpne0d 13025	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
420	245, 379, 419	divcan2d 11996	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
421	420	oveq2d 7427	. . . . . . . . . . . 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 7429	. . . . . . . . . 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 11237	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
425	424, 359	addcomd 11420	. . . . . . . . . 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 11238	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
429		addcl 11194	. . . . . . . . . 10 ⊢ (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
430	351, 283, 429	sylancr 585	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
431	428, 430, 354	addassd 11240	. . . . . . . 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 5179	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁)))
435	99, 98, 213	ltmul2d 13062	. . . . 5 ⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁))))
436	434, 435	mpbird 256	. . . 4 ⊢ (𝜑 → (log‘2) < (𝐹‘𝑁))
437	45, 99, 98, 100, 436	lttrd 11379	. . 3 ⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁))
438	45, 98, 437	ltnsymd 11367	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64))
439	42, 438	pm2.21dd 194	1 ⊢ (𝜑 → 𝜓)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∃wrex 3068 ifcif 4527 class class class wbr 5147 ↦ cmpt 5230 ‘cfv 6542 (class class class)co 7411 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 · cmul 11117 < clt 11252 ≤ cle 11253 − cmin 11448 / cdiv 11875 ℕcn 12216 2c2 12271 3c3 12272 4c4 12273 5c5 12274 6c6 12275 8c8 12277 9c9 12278 ℤcz 12562 cdc 12681 ℤ_≥cuz 12826 ℝ⁺crp 12978 ⌊cfl 13759 ↑cexp 14031 Ccbc 14266 √csqrt 15184 expce 16009 eceu 16010 ℙcprime 16612 pCnt cpc 16773 logclog 26299 ↑_𝑐ccxp 26300

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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-oadd 8472 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-dju 9898 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-q 12937 df-rp 12979 df-xneg 13096 df-xadd 13097 df-xmul 13098 df-ioo 13332 df-ioc 13333 df-ico 13334 df-icc 13335 df-fz 13489 df-fzo 13632 df-fl 13761 df-mod 13839 df-seq 13971 df-exp 14032 df-fac 14238 df-bc 14267 df-hash 14295 df-shft 15018 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-limsup 15419 df-clim 15436 df-rlim 15437 df-sum 15637 df-ef 16015 df-e 16016 df-sin 16017 df-cos 16018 df-pi 16020 df-dvds 16202 df-gcd 16440 df-prm 16613 df-pc 16774 df-struct 17084 df-sets 17101 df-slot 17119 df-ndx 17131 df-base 17149 df-ress 17178 df-plusg 17214 df-mulr 17215 df-starv 17216 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ds 17223 df-unif 17224 df-hom 17225 df-cco 17226 df-rest 17372 df-topn 17373 df-0g 17391 df-gsum 17392 df-topgen 17393 df-pt 17394 df-prds 17397 df-xrs 17452 df-qtop 17457 df-imas 17458 df-xps 17460 df-mre 17534 df-mrc 17535 df-acs 17537 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18706 df-mulg 18987 df-cntz 19222 df-cmn 19691 df-psmet 21136 df-xmet 21137 df-met 21138 df-bl 21139 df-mopn 21140 df-fbas 21141 df-fg 21142 df-cnfld 21145 df-top 22616 df-topon 22633 df-topsp 22655 df-bases 22669 df-cld 22743 df-ntr 22744 df-cls 22745 df-nei 22822 df-lp 22860 df-perf 22861 df-cn 22951 df-cnp 22952 df-haus 23039 df-tx 23286 df-hmeo 23479 df-fil 23570 df-fm 23662 df-flim 23663 df-flf 23664 df-xms 24046 df-ms 24047 df-tms 24048 df-cncf 24618 df-limc 25615 df-dv 25616 df-log 26301 df-cxp 26302 df-cht 26837 df-ppi 26840

This theorem is referenced by: bpos 27032

W3C validator