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 26028

Description: Lemma for bpos 26029. 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 11998	. . . . . 6 ⊢ 6 ∈ ℕ₀
5		4nn 11800	. . . . . 6 ⊢ 4 ∈ ℕ
6	4, 5	decnncl 12200	. . . . 5 ⊢ ;64 ∈ ℕ
7	6	a1i 11	. . . 4 ⊢ (𝜑 → ;64 ∈ ℕ)
8		bposlem9.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		ere 15535	. . . . . . . 8 ⊢ e ∈ ℝ
10		8re 11813	. . . . . . . 8 ⊢ 8 ∈ ℝ
11		egt2lt3 15652	. . . . . . . . . 10 ⊢ (2 < e ∧ e < 3)
12	11	simpri 489	. . . . . . . . 9 ⊢ e < 3
13		3lt8 11913	. . . . . . . . 9 ⊢ 3 < 8
14		3re 11797	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
15	9, 14, 10	lttri 10845	. . . . . . . . 9 ⊢ ((e < 3 ∧ 3 < 8) → e < 8)
16	12, 13, 15	mp2an 692	. . . . . . . 8 ⊢ e < 8
17	9, 10, 16	ltleii 10842	. . . . . . 7 ⊢ e ≤ 8
18		0re 10722	. . . . . . . . 9 ⊢ 0 ∈ ℝ
19		epos 15653	. . . . . . . . 9 ⊢ 0 < e
20	18, 9, 19	ltleii 10842	. . . . . . . 8 ⊢ 0 ≤ e
21		8pos 11829	. . . . . . . . 9 ⊢ 0 < 8
22	18, 10, 21	ltleii 10842	. . . . . . . 8 ⊢ 0 ≤ 8
23		le2sq 13592	. . . . . . . 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 233	. . . . . 6 ⊢ (e↑2) ≤ (8↑2)
26	10	recni 10734	. . . . . . . 8 ⊢ 8 ∈ ℂ
27	26	sqvali 13636	. . . . . . 7 ⊢ (8↑2) = (8 · 8)
28		8t8e64 12301	. . . . . . 7 ⊢ (8 · 8) = ;64
29	27, 28	eqtri 2761	. . . . . 6 ⊢ (8↑2) = ;64
30	25, 29	breqtri 5056	. . . . 5 ⊢ (e↑2) ≤ ;64
31	30	a1i 11	. . . 4 ⊢ (𝜑 → (e↑2) ≤ ;64)
32	9	resqcli 13642	. . . . . 6 ⊢ (e↑2) ∈ ℝ
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → (e↑2) ∈ ℝ)
34	6	nnrei 11726	. . . . . 6 ⊢ ;64 ∈ ℝ
35	34	a1i 11	. . . . 5 ⊢ (𝜑 → ;64 ∈ ℝ)
36	8	nnred 11732	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ)
37		ltle 10808	. . . . . . 7 ⊢ ((;64 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (;64 < 𝑁 → ;64 ≤ 𝑁))
38	34, 36, 37	sylancr 590	. . . . . 6 ⊢ (𝜑 → (;64 < 𝑁 → ;64 ≤ 𝑁))
39	1, 38	mpd 15	. . . . 5 ⊢ (𝜑 → ;64 ≤ 𝑁)
40	33, 35, 36, 31, 39	letrd 10876	. . . 4 ⊢ (𝜑 → (e↑2) ≤ 𝑁)
41	2, 3, 7, 8, 31, 40	bposlem7 26026	. . 3 ⊢ (𝜑 → (;64 < 𝑁 → (𝐹‘𝑁) < (𝐹‘;64)))
42	1, 41	mpd 15	. 2 ⊢ (𝜑 → (𝐹‘𝑁) < (𝐹‘;64))
43	2, 3	bposlem8 26027	. . . . 5 ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
44	43	a1i 11	. . . 4 ⊢ (𝜑 → ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2)))
45	44	simpld 498	. . 3 ⊢ (𝜑 → (𝐹‘;64) ∈ ℝ)
46		2fveq3 6680	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(√‘𝑛)) = (𝐺‘(√‘𝑁)))
47	46	oveq2d 7187	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((√‘2) · (𝐺‘(√‘𝑛))) = ((√‘2) · (𝐺‘(√‘𝑁))))
48		fvoveq1 7194	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (𝐺‘(𝑛 / 2)) = (𝐺‘(𝑁 / 2)))
49	48	oveq2d 7187	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → ((9 / 4) · (𝐺‘(𝑛 / 2))) = ((9 / 4) · (𝐺‘(𝑁 / 2))))
50	47, 49	oveq12d 7189	. . . . . . 7 ⊢ (𝑛 = 𝑁 → (((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) = (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))))
51		oveq2 7179	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
52	51	fveq2d 6679	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (√‘(2 · 𝑛)) = (√‘(2 · 𝑁)))
53	52	oveq2d 7187	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((log‘2) / (√‘(2 · 𝑛))) = ((log‘2) / (√‘(2 · 𝑁))))
54	50, 53	oveq12d 7189	. . . . . 6 ⊢ (𝑛 = 𝑁 → ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
55		ovex 7204	. . . . . 6 ⊢ ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ V
56	54, 2, 55	fvmpt 6776	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
57	8, 56	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘𝑁) = ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))))
58		sqrt2re 15696	. . . . . . 7 ⊢ (√‘2) ∈ ℝ
59	8	nnrpd 12513	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
60	59	rpsqrtcld 14862	. . . . . . . . 9 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
61		fveq2 6675	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → (log‘𝑥) = (log‘(√‘𝑁)))
62		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (√‘𝑁) → 𝑥 = (√‘𝑁))
63	61, 62	oveq12d 7189	. . . . . . . . . 10 ⊢ (𝑥 = (√‘𝑁) → ((log‘𝑥) / 𝑥) = ((log‘(√‘𝑁)) / (√‘𝑁)))
64		ovex 7204	. . . . . . . . . 10 ⊢ ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ V
65	63, 3, 64	fvmpt 6776	. . . . . . . . 9 ⊢ ((√‘𝑁) ∈ ℝ⁺ → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
66	60, 65	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) = ((log‘(√‘𝑁)) / (√‘𝑁)))
67	60	relogcld 25366	. . . . . . . . 9 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℝ)
68	67, 60	rerpdivcld 12546	. . . . . . . 8 ⊢ (𝜑 → ((log‘(√‘𝑁)) / (√‘𝑁)) ∈ ℝ)
69	66, 68	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℝ)
70		remulcl 10701	. . . . . . 7 ⊢ (((√‘2) ∈ ℝ ∧ (𝐺‘(√‘𝑁)) ∈ ℝ) → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
71	58, 69, 70	sylancr 590	. . . . . 6 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℝ)
72		9re 11816	. . . . . . . 8 ⊢ 9 ∈ ℝ
73		4re 11801	. . . . . . . 8 ⊢ 4 ∈ ℝ
74		4ne0 11825	. . . . . . . 8 ⊢ 4 ≠ 0
75	72, 73, 74	redivcli 11486	. . . . . . 7 ⊢ (9 / 4) ∈ ℝ
76	59	rphalfcld 12527	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ⁺)
77		fveq2 6675	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → (log‘𝑥) = (log‘(𝑁 / 2)))
78		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑁 / 2) → 𝑥 = (𝑁 / 2))
79	77, 78	oveq12d 7189	. . . . . . . . . 10 ⊢ (𝑥 = (𝑁 / 2) → ((log‘𝑥) / 𝑥) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
80		ovex 7204	. . . . . . . . . 10 ⊢ ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ V
81	79, 3, 80	fvmpt 6776	. . . . . . . . 9 ⊢ ((𝑁 / 2) ∈ ℝ⁺ → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
82	76, 81	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) = ((log‘(𝑁 / 2)) / (𝑁 / 2)))
83	76	relogcld 25366	. . . . . . . . 9 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℝ)
84	83, 76	rerpdivcld 12546	. . . . . . . 8 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℝ)
85	82, 84	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℝ)
86		remulcl 10701	. . . . . . 7 ⊢ (((9 / 4) ∈ ℝ ∧ (𝐺‘(𝑁 / 2)) ∈ ℝ) → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
87	75, 85, 86	sylancr 590	. . . . . 6 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℝ)
88	71, 87	readdcld 10749	. . . . 5 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℝ)
89		2rp 12478	. . . . . . 7 ⊢ 2 ∈ ℝ⁺
90		relogcl 25319	. . . . . . 7 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
91	89, 90	ax-mp 5	. . . . . 6 ⊢ (log‘2) ∈ ℝ
92		rpmulcl 12496	. . . . . . . 8 ⊢ ((2 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (2 · 𝑁) ∈ ℝ⁺)
93	89, 59, 92	sylancr 590	. . . . . . 7 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
94	93	rpsqrtcld 14862	. . . . . 6 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ⁺)
95		rerpdivcl 12503	. . . . . 6 ⊢ (((log‘2) ∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ⁺) → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
96	91, 94, 95	sylancr 590	. . . . 5 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℝ)
97	88, 96	readdcld 10749	. . . 4 ⊢ (𝜑 → ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁)))) ∈ ℝ)
98	57, 97	eqeltrd 2833	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ)
99	91	a1i 11	. . . 4 ⊢ (𝜑 → (log‘2) ∈ ℝ)
100	44	simprd 499	. . . 4 ⊢ (𝜑 → (𝐹‘;64) < (log‘2))
101		nnrp 12484	. . . . . . . . . . 11 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
102	5, 101	ax-mp 5	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
103		relogcl 25319	. . . . . . . . . 10 ⊢ (4 ∈ ℝ⁺ → (log‘4) ∈ ℝ)
104	102, 103	ax-mp 5	. . . . . . . . 9 ⊢ (log‘4) ∈ ℝ
105		remulcl 10701	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ (log‘4) ∈ ℝ) → (𝑁 · (log‘4)) ∈ ℝ)
106	36, 104, 105	sylancl 589	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℝ)
107	59	relogcld 25366	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
108	106, 107	resubcld 11147	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) ∈ ℝ)
109		rpre 12481	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → (2 · 𝑁) ∈ ℝ)
110		rpge0 12486	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → 0 ≤ (2 · 𝑁))
111	109, 110	resqrtcld 14868	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ⁺ → (√‘(2 · 𝑁)) ∈ ℝ)
112	93, 111	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
113		3nn 11796	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
114		nndivre 11758	. . . . . . . . . . 11 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
115	112, 113, 114	sylancl 589	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
116		2re 11791	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
117		readdcl 10699	. . . . . . . . . 10 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
118	115, 116, 117	sylancl 589	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
119	93	relogcld 25366	. . . . . . . . 9 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℝ)
120	118, 119	remulcld 10750	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℝ)
121		remulcl 10701	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (4 · 𝑁) ∈ ℝ)
122	73, 36, 121	sylancr 590	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
123		nndivre 11758	. . . . . . . . . . 11 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
124	122, 113, 123	sylancl 589	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
125		5re 11804	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
126		resubcl 11029	. . . . . . . . . 10 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
127	124, 125, 126	sylancl 589	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
128		remulcl 10701	. . . . . . . . 9 ⊢ (((((4 · 𝑁) / 3) − 5) ∈ ℝ ∧ (log‘2) ∈ ℝ) → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
129	127, 91, 128	sylancl 589	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℝ)
130	120, 129	readdcld 10749	. . . . . . 7 ⊢ (𝜑 → (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) ∈ ℝ)
131		remulcl 10701	. . . . . . . . 9 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ (log‘2) ∈ ℝ) → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
132	124, 91, 131	sylancl 589	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℝ)
133	132, 107	resubcld 11147	. . . . . . 7 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℝ)
134	8	nnzd 12168	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
135		df-5 11783	. . . . . . . . . . . 12 ⊢ 5 = (4 + 1)
136	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
137		6nn 11806	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ
138		4nn0 11996	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
139		4lt10 12316	. . . . . . . . . . . . . . . 16 ⊢ 4 < ;10
140	137, 138, 138, 139	declti 12218	. . . . . . . . . . . . . . 15 ⊢ 4 < ;64
141	140	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 < ;64)
142	136, 35, 36, 141, 1	lttrd 10880	. . . . . . . . . . . . 13 ⊢ (𝜑 → 4 < 𝑁)
143		4z 12098	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℤ
144		zltp1le 12114	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
145	143, 134, 144	sylancr 590	. . . . . . . . . . . . 13 ⊢ (𝜑 → (4 < 𝑁 ↔ (4 + 1) ≤ 𝑁))
146	142, 145	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 + 1) ≤ 𝑁)
147	135, 146	eqbrtrid 5066	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ≤ 𝑁)
148		5nn 11803	. . . . . . . . . . . . 13 ⊢ 5 ∈ ℕ
149	148	nnzi 12088	. . . . . . . . . . . 12 ⊢ 5 ∈ ℤ
150	149	eluz1i 12333	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘5) ↔ (𝑁 ∈ ℤ ∧ 5 ≤ 𝑁))
151	134, 147, 150	sylanbrc 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
152		bposlem9.5	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
153		breq2 5035	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑁 < 𝑝 ↔ 𝑁 < 𝑞))
154		breq1 5034	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑞 → (𝑝 ≤ (2 · 𝑁) ↔ 𝑞 ≤ (2 · 𝑁)))
155	153, 154	anbi12d 634	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑞 → ((𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁))))
156	155	cbvrexvw 3350	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) ↔ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
157	152, 156	sylnib 331	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ∃𝑞 ∈ ℙ (𝑁 < 𝑞 ∧ 𝑞 ≤ (2 · 𝑁)))
158		eqid 2738	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
159		eqid 2738	. . . . . . . . . 10 ⊢ (⌊‘((2 · 𝑁) / 3)) = (⌊‘((2 · 𝑁) / 3))
160		eqid 2738	. . . . . . . . . 10 ⊢ (⌊‘(√‘(2 · 𝑁))) = (⌊‘(√‘(2 · 𝑁)))
161	151, 157, 158, 159, 160	bposlem6 26025	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
162		reexplog 25338	. . . . . . . . . . . 12 ⊢ ((4 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ) → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
163	102, 134, 162	sylancr 590	. . . . . . . . . . 11 ⊢ (𝜑 → (4↑𝑁) = (exp‘(𝑁 · (log‘4))))
164	59	reeflogd 25367	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
165	164	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (exp‘(log‘𝑁)))
166	163, 165	oveq12d 7189	. . . . . . . . . 10 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
167	106	recnd 10748	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · (log‘4)) ∈ ℂ)
168	107	recnd 10748	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
169		efsub 15546	. . . . . . . . . . 11 ⊢ (((𝑁 · (log‘4)) ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
170	167, 168, 169	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) = ((exp‘(𝑁 · (log‘4))) / (exp‘(log‘𝑁))))
171	166, 170	eqtr4d 2776	. . . . . . . . 9 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) = (exp‘((𝑁 · (log‘4)) − (log‘𝑁))))
172	93	rpcnd 12517	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
173	93	rpne0d 12520	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ≠ 0)
174	118	recnd 10748	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℂ)
175	172, 173, 174	cxpefd 25455	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) = (exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))))
176		2cn 11792	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
177		2ne0 11821	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
178	127	recnd 10748	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℂ)
179		cxpef 25408	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ (((4 · 𝑁) / 3) − 5) ∈ ℂ) → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
180	176, 177, 178, 179	mp3an12i 1466	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) = (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2))))
181	175, 180	oveq12d 7189	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))) = ((exp‘((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁)))) · (exp‘((((4 · 𝑁) / 3) − 5) · (log‘2)))))
182	120	recnd 10748	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) ∈ ℂ)
183	129	recnd 10748	. . . . . . . . . . 11 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) ∈ ℂ)
184		efadd 15540	. . . . . . . . . . 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 587	. . . . . . . . . 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 2776	. . . . . . . . 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 5062	. . . . . . . 8 ⊢ (𝜑 → (exp‘((𝑁 · (log‘4)) − (log‘𝑁))) < (exp‘(((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2)))))
188		eflt 15563	. . . . . . . . 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 587	. . . . . . . 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 260	. . . . . . 7 ⊢ (𝜑 → ((𝑁 · (log‘4)) − (log‘𝑁)) < (((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))))
191	108, 130, 133, 190	ltsub1dd 11331	. . . . . 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 10748	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
193		mulcom 10702	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) = (𝑁 · 2))
194	176, 192, 193	sylancr 590	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 · 2))
195	194	oveq1d 7186	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = ((𝑁 · 2) · (log‘2)))
196	91	recni 10734	. . . . . . . . . . . 12 ⊢ (log‘2) ∈ ℂ
197		mulass 10704	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ (log‘2) ∈ ℂ) → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
198	176, 196, 197	mp3an23 1454	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℂ → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
199	192, 198	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (2 · (log‘2))))
200	196	2timesi 11855	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) = ((log‘2) + (log‘2))
201		relogmul 25335	. . . . . . . . . . . . 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 11881	. . . . . . . . . . . . 13 ⊢ (2 · 2) = 4
204	203	fveq2i 6678	. . . . . . . . . . . 12 ⊢ (log‘(2 · 2)) = (log‘4)
205	200, 202, 204	3eqtr2i 2767	. . . . . . . . . . 11 ⊢ (2 · (log‘2)) = (log‘4)
206	205	oveq2i 7182	. . . . . . . . . 10 ⊢ (𝑁 · (2 · (log‘2))) = (𝑁 · (log‘4))
207	199, 206	eqtrdi 2789	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) · (log‘2)) = (𝑁 · (log‘4)))
208	195, 207	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝑁) · (log‘2)) = (𝑁 · (log‘4)))
209	208	oveq1d 7186	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
210	124	recnd 10748	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℂ)
211		3rp 12479	. . . . . . . . . . . 12 ⊢ 3 ∈ ℝ⁺
212		rpdivcl 12498	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺) → ((2 · 𝑁) / 3) ∈ ℝ⁺)
213	93, 211, 212	sylancl 589	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ⁺)
214	213	rpcnd 12517	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℂ)
215		4p2e6 11870	. . . . . . . . . . . . . 14 ⊢ (4 + 2) = 6
216	215	oveq1i 7181	. . . . . . . . . . . . 13 ⊢ ((4 + 2) · 𝑁) = (6 · 𝑁)
217		4cn 11802	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℂ
218		adddir 10711	. . . . . . . . . . . . . 14 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
219	217, 176, 192, 218	mp3an12i 1466	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 + 2) · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
220	216, 219	eqtr3id 2787	. . . . . . . . . . . 12 ⊢ (𝜑 → (6 · 𝑁) = ((4 · 𝑁) + (2 · 𝑁)))
221	220	oveq1d 7186	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (((4 · 𝑁) + (2 · 𝑁)) / 3))
222		6cn 11808	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℂ
223		3cn 11798	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
224		3ne0 11823	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
225	223, 224	pm3.2i 474	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
226		div23 11396	. . . . . . . . . . . . . 14 ⊢ ((6 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
227	222, 225, 226	mp3an13 1453	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
228	192, 227	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((6 · 𝑁) / 3) = ((6 / 3) · 𝑁))
229		3t2e6 11883	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
230	229	oveq1i 7181	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = (6 / 3)
231	176, 223, 224	divcan3i 11465	. . . . . . . . . . . . . 14 ⊢ ((3 · 2) / 3) = 2
232	230, 231	eqtr3i 2763	. . . . . . . . . . . . 13 ⊢ (6 / 3) = 2
233	232	oveq1i 7181	. . . . . . . . . . . 12 ⊢ ((6 / 3) · 𝑁) = (2 · 𝑁)
234	228, 233	eqtrdi 2789	. . . . . . . . . . 11 ⊢ (𝜑 → ((6 · 𝑁) / 3) = (2 · 𝑁))
235	122	recnd 10748	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · 𝑁) ∈ ℂ)
236		remulcl 10701	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
237	116, 36, 236	sylancr 590	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
238	237	recnd 10748	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
239		divdir 11402	. . . . . . . . . . . . 13 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
240	225, 239	mp3an3 1451	. . . . . . . . . . . 12 ⊢ (((4 · 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ) → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
241	235, 238, 240	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝑁) + (2 · 𝑁)) / 3) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
242	221, 234, 241	3eqtr3d 2781	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) = (((4 · 𝑁) / 3) + ((2 · 𝑁) / 3)))
243	210, 214, 242	mvrladdd 11132	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁) − ((4 · 𝑁) / 3)) = ((2 · 𝑁) / 3))
244	243	oveq1d 7186	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) / 3) · (log‘2)))
245	99	recnd 10748	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℂ)
246	238, 210, 245	subdird 11176	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) − ((4 · 𝑁) / 3)) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
247	244, 246	eqtr3d 2775	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((2 · 𝑁) · (log‘2)) − (((4 · 𝑁) / 3) · (log‘2))))
248	132	recnd 10748	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑁) / 3) · (log‘2)) ∈ ℂ)
249	167, 248, 168	nnncan2d 11111	. . . . . . 7 ⊢ (𝜑 → (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((𝑁 · (log‘4)) − (((4 · 𝑁) / 3) · (log‘2))))
250	209, 247, 249	3eqtr4d 2783	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) = (((𝑁 · (log‘4)) − (log‘𝑁)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
251	115	recnd 10748	. . . . . . . . . 10 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℂ)
252	176	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
253	119	recnd 10748	. . . . . . . . . 10 ⊢ (𝜑 → (log‘(2 · 𝑁)) ∈ ℂ)
254	251, 252, 253	adddird 10745	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))))
255		relogmul 25335	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
256	89, 59, 255	sylancr 590	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘(2 · 𝑁)) = ((log‘2) + (log‘𝑁)))
257	256	oveq2d 7187	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = (2 · ((log‘2) + (log‘𝑁))))
258	252, 245, 168	adddid 10744	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((log‘2) + (log‘𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
259	257, 258	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (log‘(2 · 𝑁))) = ((2 · (log‘2)) + (2 · (log‘𝑁))))
260	259	oveq2d 7187	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (2 · (log‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
261	254, 260	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))))
262		5cn 11805	. . . . . . . . . . . 12 ⊢ 5 ∈ ℂ
263	262	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 5 ∈ ℂ)
264	210, 263, 245	subdird 11176	. . . . . . . . . 10 ⊢ (𝜑 → ((((4 · 𝑁) / 3) − 5) · (log‘2)) = ((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))))
265	264	oveq1d 7186	. . . . . . . . 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 10727	. . . . . . . . . . 11 ⊢ (5 · (log‘2)) ∈ ℂ
267	266	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (5 · (log‘2)) ∈ ℂ)
268	248, 267, 168	nnncan1d 11110	. . . . . . . . 9 ⊢ (𝜑 → (((((4 · 𝑁) / 3) · (log‘2)) − (5 · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
269	265, 268	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → (((((4 · 𝑁) / 3) − 5) · (log‘2)) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))) = ((log‘𝑁) − (5 · (log‘2))))
270	261, 269	oveq12d 7189	. . . . . . 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 10748	. . . . . . . 8 ⊢ (𝜑 → ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁)) ∈ ℂ)
272	182, 183, 271	addsubassd 11096	. . . . . . 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 11169	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = ((5 · (log‘2)) − (3 · (log‘2)))
274		3p2e5 11868	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
275	274	oveq1i 7181	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = (5 − 3)
276		pncan2 10972	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
277	223, 176, 276	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 3) = 2
278	275, 277	eqtr3i 2763	. . . . . . . . . . . . . 14 ⊢ (5 − 3) = 2
279	278	oveq1i 7181	. . . . . . . . . . . . 13 ⊢ ((5 − 3) · (log‘2)) = (2 · (log‘2))
280	273, 279	eqtr3i 2763	. . . . . . . . . . . 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 10700	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (2 · (log‘𝑁)) ∈ ℂ)
283	176, 168, 282	sylancr 590	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · (log‘𝑁)) ∈ ℂ)
284		df-3 11781	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
285	284	oveq1i 7181	. . . . . . . . . . . . . . 15 ⊢ (3 · (log‘𝑁)) = ((2 + 1) · (log‘𝑁))
286		1cnd 10715	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℂ)
287	252, 286, 168	adddird 10745	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 + 1) · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
288	285, 287	syl5eq 2785	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (1 · (log‘𝑁))))
289	168	mulid2d 10738	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (log‘𝑁)) = (log‘𝑁))
290	289	oveq2d 7187	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (log‘𝑁)) + (1 · (log‘𝑁))) = ((2 · (log‘𝑁)) + (log‘𝑁)))
291	288, 290	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · (log‘𝑁)) = ((2 · (log‘𝑁)) + (log‘𝑁)))
292	291	oveq1d 7186	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = (((2 · (log‘𝑁)) + (log‘𝑁)) − (5 · (log‘2))))
293	283, 168, 267, 292	assraddsubd 11133	. . . . . . . . . . 11 ⊢ (𝜑 → ((3 · (log‘𝑁)) − (5 · (log‘2))) = ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2)))))
294	281, 293	oveq12d 7189	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
295		relogdiv 25336	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ⁺ ∧ 2 ∈ ℝ⁺) → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
296	59, 89, 295	sylancl 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (log‘(𝑁 / 2)) = ((log‘𝑁) − (log‘2)))
297	296	oveq2d 7187	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = (3 · ((log‘𝑁) − (log‘2))))
298		subdi 11152	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (3 · ((log‘𝑁) − (log‘2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
299	223, 196, 298	mp3an13 1453	. . . . . . . . . . . . 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 2773	. . . . . . . . . . 11 ⊢ (𝜑 → (3 · (log‘(𝑁 / 2))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
302		div23 11396	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
303	176, 225, 302	mp3an13 1453	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
304	192, 303	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = ((2 / 3) · 𝑁))
305	223, 176, 223, 176, 177, 177	divmuldivi 11479	. . . . . . . . . . . . . . . . 17 ⊢ ((3 / 2) · (3 / 2)) = ((3 · 3) / (2 · 2))
306		3t3e9 11884	. . . . . . . . . . . . . . . . . 18 ⊢ (3 · 3) = 9
307	306, 203	oveq12i 7183	. . . . . . . . . . . . . . . . 17 ⊢ ((3 · 3) / (2 · 2)) = (9 / 4)
308	305, 307	eqtr2i 2762	. . . . . . . . . . . . . . . 16 ⊢ (9 / 4) = ((3 / 2) · (3 / 2))
309	308	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (9 / 4) = ((3 / 2) · (3 / 2)))
310	304, 309	oveq12d 7189	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))))
311	176, 223, 224	divcli 11461	. . . . . . . . . . . . . . 15 ⊢ (2 / 3) ∈ ℂ
312	223, 176, 177	divcli 11461	. . . . . . . . . . . . . . . 16 ⊢ (3 / 2) ∈ ℂ
313		mul4 10887	. . . . . . . . . . . . . . . 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 590	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · 𝑁) · ((3 / 2) · (3 / 2))) = (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))))
316		divcan6 11426	. . . . . . . . . . . . . . . . . 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 7181	. . . . . . . . . . . . . . . 16 ⊢ (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (1 · (𝑁 · (3 / 2)))
319		mulcl 10700	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℂ ∧ (3 / 2) ∈ ℂ) → (𝑁 · (3 / 2)) ∈ ℂ)
320	192, 312, 319	sylancl 589	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 · (3 / 2)) ∈ ℂ)
321	320	mulid2d 10738	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
322	318, 321	syl5eq 2785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (𝑁 · (3 / 2)))
323		2cnne0 11927	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
324		div12 11399	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
325	223, 323, 324	mp3an23 1454	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℂ → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
326	192, 325	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · (3 / 2)) = (3 · (𝑁 / 2)))
327	322, 326	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 / 3) · (3 / 2)) · (𝑁 · (3 / 2))) = (3 · (𝑁 / 2)))
328	310, 315, 327	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (9 / 4)) = (3 · (𝑁 / 2)))
329	328, 82	oveq12d 7189	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))))
330	75	recni 10734	. . . . . . . . . . . . . 14 ⊢ (9 / 4) ∈ ℂ
331	330	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (9 / 4) ∈ ℂ)
332	85	recnd 10748	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(𝑁 / 2)) ∈ ℂ)
333	214, 331, 332	mulassd 10743	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · (9 / 4)) · (𝐺‘(𝑁 / 2))) = (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))
334	223	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 3 ∈ ℂ)
335	76	rpcnd 12517	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
336	83	recnd 10748	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (log‘(𝑁 / 2)) ∈ ℂ)
337	76	rpne0d 12520	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) ≠ 0)
338	336, 335, 337	divcld 11495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((log‘(𝑁 / 2)) / (𝑁 / 2)) ∈ ℂ)
339	334, 335, 338	mulassd 10743	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))))
340	336, 335, 337	divcan2d 11497	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (log‘(𝑁 / 2)))
341	340	oveq2d 7187	. . . . . . . . . . . . 13 ⊢ (𝜑 → (3 · ((𝑁 / 2) · ((log‘(𝑁 / 2)) / (𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
342	339, 341	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → ((3 · (𝑁 / 2)) · ((log‘(𝑁 / 2)) / (𝑁 / 2))) = (3 · (log‘(𝑁 / 2))))
343	329, 333, 342	3eqtr3d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (3 · (log‘(𝑁 / 2))))
344	223, 196	mulcli 10727	. . . . . . . . . . . . 13 ⊢ (3 · (log‘2)) ∈ ℂ
345	344	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘2)) ∈ ℂ)
346		mulcl 10700	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ (log‘𝑁) ∈ ℂ) → (3 · (log‘𝑁)) ∈ ℂ)
347	223, 168, 346	sylancr 590	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 · (log‘𝑁)) ∈ ℂ)
348	267, 345, 347	npncan3d 11112	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))) = ((3 · (log‘𝑁)) − (3 · (log‘2))))
349	301, 343, 348	3eqtr4d 2783	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((5 · (log‘2)) − (3 · (log‘2))) + ((3 · (log‘𝑁)) − (5 · (log‘2)))))
350	116, 91	remulcli 10736	. . . . . . . . . . . . 13 ⊢ (2 · (log‘2)) ∈ ℝ
351	350	recni 10734	. . . . . . . . . . . 12 ⊢ (2 · (log‘2)) ∈ ℂ
352	351	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (log‘2)) ∈ ℂ)
353		subcl 10964	. . . . . . . . . . . 12 ⊢ (((log‘𝑁) ∈ ℂ ∧ (5 · (log‘2)) ∈ ℂ) → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
354	168, 266, 353	sylancl 589	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝑁) − (5 · (log‘2))) ∈ ℂ)
355	352, 283, 354	addassd 10742	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))) = ((2 · (log‘2)) + ((2 · (log‘𝑁)) + ((log‘𝑁) − (5 · (log‘2))))))
356	294, 349, 355	3eqtr4d 2783	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) = (((2 · (log‘2)) + (2 · (log‘𝑁))) + ((log‘𝑁) − (5 · (log‘2)))))
357	356	oveq2d 7187	. . . . . . . 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 10700	. . . . . . . . . . 11 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
359	251, 196, 358	sylancl 589	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘2)) ∈ ℂ)
360	251, 168	mulcld 10740	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) ∈ ℂ)
361	87	recnd 10748	. . . . . . . . . . 11 ⊢ (𝜑 → ((9 / 4) · (𝐺‘(𝑁 / 2))) ∈ ℂ)
362	214, 361	mulcld 10740	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
363	359, 360, 362	addassd 10742	. . . . . . . . 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 7187	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))))
365	251, 245, 168	adddid 10744	. . . . . . . . . . 11 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((log‘2) + (log‘𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
366	364, 365	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + (((√‘(2 · 𝑁)) / 3) · (log‘𝑁))))
367	366	oveq1d 7186	. . . . . . . . 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 7187	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((2 · 𝑁) / 3) · ((((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) + ((log‘2) / (√‘(2 · 𝑁))))))
369	88	recnd 10748	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2)))) ∈ ℂ)
370	96	recnd 10748	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) / (√‘(2 · 𝑁))) ∈ ℂ)
371	214, 369, 370	adddid 10744	. . . . . . . . . . 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 2773	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) + (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁))))))
373	71	recnd 10748	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘2) · (𝐺‘(√‘𝑁))) ∈ ℂ)
374	214, 373, 361	adddid 10744	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
375	93	rpge0d 12519	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
376		remsqsqrt 14707	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
377	237, 375, 376	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) = (2 · 𝑁))
378	377	oveq1d 7186	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = ((2 · 𝑁) / 3))
379	112	recnd 10748	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℂ)
380	224	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≠ 0)
381	379, 379, 334, 380	div23d 11532	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘(2 · 𝑁)) · (√‘(2 · 𝑁))) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
382	378, 381	eqtr3d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝑁) / 3) = (((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))))
383	382	oveq1d 7186	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))))
384	251, 379, 373	mulassd 10743	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))))
385		0le2 11819	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ≤ 2
386	116, 385	pm3.2i 474	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ ∧ 0 ≤ 2)
387	59	rprege0d 12522	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
388		sqrtmul 14710	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁)) → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
389	386, 387, 388	sylancr 590	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(2 · 𝑁)) = ((√‘2) · (√‘𝑁)))
390	389	oveq1d 7186	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))))
391	58	recni 10734	. . . . . . . . . . . . . . . . . 18 ⊢ (√‘2) ∈ ℂ
392	391	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘2) ∈ ℂ)
393	60	rpcnd 12517	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘𝑁) ∈ ℂ)
394	69	recnd 10748	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘(√‘𝑁)) ∈ ℂ)
395	392, 393, 392, 394	mul4d 10931	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))))
396		remsqsqrt 14707	. . . . . . . . . . . . . . . . . . . 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 7187	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))))
400	67	recnd 10748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (log‘(√‘𝑁)) ∈ ℂ)
401	60	rpne0d 12520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑁) ≠ 0)
402	400, 393, 401	divcan2d 11497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · ((log‘(√‘𝑁)) / (√‘𝑁))) = (log‘(√‘𝑁)))
403	399, 402	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘𝑁) · (𝐺‘(√‘𝑁))) = (log‘(√‘𝑁)))
404	398, 403	oveq12d 7189	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (2 · (log‘(√‘𝑁))))
405	400	2timesd 11960	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (log‘(√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
406	60, 60	relogmuld 25368	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = ((log‘(√‘𝑁)) + (log‘(√‘𝑁))))
407		remsqsqrt 14707	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
408	387, 407	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((√‘𝑁) · (√‘𝑁)) = 𝑁)
409	408	fveq2d 6679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (log‘((√‘𝑁) · (√‘𝑁))) = (log‘𝑁))
410	406, 409	eqtr3d 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘(√‘𝑁)) + (log‘(√‘𝑁))) = (log‘𝑁))
411	404, 405, 410	3eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((√‘2) · (√‘2)) · ((√‘𝑁) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
412	390, 395, 411	3eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (log‘𝑁))
413	412	oveq2d 7187	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((√‘2) · (𝐺‘(√‘𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
414	383, 384, 413	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘𝑁)))
415	414	oveq1d 7186	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · 𝑁) / 3) · ((√‘2) · (𝐺‘(√‘𝑁)))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
416	374, 415	eqtrd 2773	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (((√‘2) · (𝐺‘(√‘𝑁))) + ((9 / 4) · (𝐺‘(𝑁 / 2))))) = ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
417	382	oveq1d 7186	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))))
418	251, 379, 370	mulassd 10743	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (√‘(2 · 𝑁))) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))))
419	94	rpne0d 12520	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(2 · 𝑁)) ≠ 0)
420	245, 379, 419	divcan2d 11497	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁)))) = (log‘2))
421	420	oveq2d 7187	. . . . . . . . . . . 12 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · ((√‘(2 · 𝑁)) · ((log‘2) / (√‘(2 · 𝑁))))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
422	417, 418, 421	3eqtrd 2777	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝑁) / 3) · ((log‘2) / (√‘(2 · 𝑁)))) = (((√‘(2 · 𝑁)) / 3) · (log‘2)))
423	416, 422	oveq12d 7189	. . . . . . . . . 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 10739	. . . . . . . . . . 11 ⊢ (𝜑 → ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))) ∈ ℂ)
425	424, 359	addcomd 10921	. . . . . . . . . 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 2777	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘2)) + ((((√‘(2 · 𝑁)) / 3) · (log‘𝑁)) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2)))))))
427	363, 367, 426	3eqtr4rd 2784	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + (((2 · 𝑁) / 3) · ((9 / 4) · (𝐺‘(𝑁 / 2))))))
428	251, 253	mulcld 10740	. . . . . . . . 9 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) ∈ ℂ)
429		addcl 10698	. . . . . . . . . 10 ⊢ (((2 · (log‘2)) ∈ ℂ ∧ (2 · (log‘𝑁)) ∈ ℂ) → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
430	351, 283, 429	sylancr 590	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (log‘2)) + (2 · (log‘𝑁))) ∈ ℂ)
431	428, 430, 354	addassd 10742	. . . . . . . 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 2783	. . . . . . 7 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = (((((√‘(2 · 𝑁)) / 3) · (log‘(2 · 𝑁))) + ((2 · (log‘2)) + (2 · (log‘𝑁)))) + ((log‘𝑁) − (5 · (log‘2)))))
433	270, 272, 432	3eqtr4rd 2784	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (𝐹‘𝑁)) = ((((((√‘(2 · 𝑁)) / 3) + 2) · (log‘(2 · 𝑁))) + ((((4 · 𝑁) / 3) − 5) · (log‘2))) − ((((4 · 𝑁) / 3) · (log‘2)) − (log‘𝑁))))
434	191, 250, 433	3brtr4d 5063	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁)))
435	99, 98, 213	ltmul2d 12557	. . . . 5 ⊢ (𝜑 → ((log‘2) < (𝐹‘𝑁) ↔ (((2 · 𝑁) / 3) · (log‘2)) < (((2 · 𝑁) / 3) · (𝐹‘𝑁))))
436	434, 435	mpbird 260	. . . 4 ⊢ (𝜑 → (log‘2) < (𝐹‘𝑁))
437	45, 99, 98, 100, 436	lttrd 10880	. . 3 ⊢ (𝜑 → (𝐹‘;64) < (𝐹‘𝑁))
438	45, 98, 437	ltnsymd 10868	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝑁) < (𝐹‘;64))
439	42, 438	pm2.21dd 198	1 ⊢ (𝜑 → 𝜓)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2113 ≠ wne 2934 ∃wrex 3054 ifcif 4415 class class class wbr 5031 ↦ cmpt 5111 ‘cfv 6340 (class class class)co 7171 ℂcc 10614 ℝcr 10615 0cc0 10616 1c1 10617 + caddc 10619 · cmul 10621 < clt 10754 ≤ cle 10755 − cmin 10949 / cdiv 11376 ℕcn 11717 2c2 11772 3c3 11773 4c4 11774 5c5 11775 6c6 11776 8c8 11778 9c9 11779 ℤcz 12063 cdc 12180 ℤ_≥cuz 12325 ℝ⁺crp 12473 ⌊cfl 13252 ↑cexp 13522 Ccbc 13755 √csqrt 14683 expce 15508 eceu 15509 ℙcprime 16113 pCnt cpc 16274 logclog 25298 ↑_𝑐ccxp 25299

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-inf2 9178 ax-cnex 10672 ax-resscn 10673 ax-1cn 10674 ax-icn 10675 ax-addcl 10676 ax-addrcl 10677 ax-mulcl 10678 ax-mulrcl 10679 ax-mulcom 10680 ax-addass 10681 ax-mulass 10682 ax-distr 10683 ax-i2m1 10684 ax-1ne0 10685 ax-1rid 10686 ax-rnegex 10687 ax-rrecex 10688 ax-cnre 10689 ax-pre-lttri 10690 ax-pre-lttrn 10691 ax-pre-ltadd 10692 ax-pre-mulgt0 10693 ax-pre-sup 10694 ax-addf 10695 ax-mulf 10696

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-iin 4885 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-se 5485 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7128 df-ov 7174 df-oprab 7175 df-mpo 7176 df-of 7426 df-om 7601 df-1st 7715 df-2nd 7716 df-supp 7858 df-wrecs 7977 df-recs 8038 df-rdg 8076 df-1o 8132 df-2o 8133 df-oadd 8136 df-er 8321 df-map 8440 df-pm 8441 df-ixp 8509 df-en 8557 df-dom 8558 df-sdom 8559 df-fin 8560 df-fsupp 8908 df-fi 8949 df-sup 8980 df-inf 8981 df-oi 9048 df-dju 9404 df-card 9442 df-pnf 10756 df-mnf 10757 df-xr 10758 df-ltxr 10759 df-le 10760 df-sub 10951 df-neg 10952 df-div 11377 df-nn 11718 df-2 11780 df-3 11781 df-4 11782 df-5 11783 df-6 11784 df-7 11785 df-8 11786 df-9 11787 df-n0 11978 df-xnn0 12050 df-z 12064 df-dec 12181 df-uz 12326 df-q 12432 df-rp 12474 df-xneg 12591 df-xadd 12592 df-xmul 12593 df-ioo 12826 df-ioc 12827 df-ico 12828 df-icc 12829 df-fz 12983 df-fzo 13126 df-fl 13254 df-mod 13330 df-seq 13462 df-exp 13523 df-fac 13727 df-bc 13756 df-hash 13784 df-shft 14517 df-cj 14549 df-re 14550 df-im 14551 df-sqrt 14685 df-abs 14686 df-limsup 14919 df-clim 14936 df-rlim 14937 df-sum 15137 df-ef 15514 df-e 15515 df-sin 15516 df-cos 15517 df-pi 15519 df-dvds 15701 df-gcd 15939 df-prm 16114 df-pc 16275 df-struct 16589 df-ndx 16590 df-slot 16591 df-base 16593 df-sets 16594 df-ress 16595 df-plusg 16682 df-mulr 16683 df-starv 16684 df-sca 16685 df-vsca 16686 df-ip 16687 df-tset 16688 df-ple 16689 df-ds 16691 df-unif 16692 df-hom 16693 df-cco 16694 df-rest 16800 df-topn 16801 df-0g 16819 df-gsum 16820 df-topgen 16821 df-pt 16822 df-prds 16825 df-xrs 16879 df-qtop 16884 df-imas 16885 df-xps 16887 df-mre 16961 df-mrc 16962 df-acs 16964 df-mgm 17969 df-sgrp 18018 df-mnd 18029 df-submnd 18074 df-mulg 18344 df-cntz 18566 df-cmn 19027 df-psmet 20210 df-xmet 20211 df-met 20212 df-bl 20213 df-mopn 20214 df-fbas 20215 df-fg 20216 df-cnfld 20219 df-top 21646 df-topon 21663 df-topsp 21685 df-bases 21698 df-cld 21771 df-ntr 21772 df-cls 21773 df-nei 21850 df-lp 21888 df-perf 21889 df-cn 21979 df-cnp 21980 df-haus 22067 df-tx 22314 df-hmeo 22507 df-fil 22598 df-fm 22690 df-flim 22691 df-flf 22692 df-xms 23074 df-ms 23075 df-tms 23076 df-cncf 23631 df-limc 24618 df-dv 24619 df-log 25300 df-cxp 25301 df-cht 25834 df-ppi 25837

This theorem is referenced by: bpos 26029

W3C validator