Theorem chtqub 16215

Description: An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014.) (Revised 22-Sep-2014.)

Assertion

Ref	Expression
chtqub	⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))

Proof of Theorem chtqub

Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 9376	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
2		1lt2 9478	. . . . . . . . . . 11 ⊢ 1 < 2
3		rplogcl 16031	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
4	1, 2, 3	mp2an 430	. . . . . . . . . 10 ⊢ (log‘2) ∈ ℝ+
5		elrp 10066	. . . . . . . . . 10 ⊢ ((log‘2) ∈ ℝ+ ↔ ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
6	4, 5	mpbi 145	. . . . . . . . 9 ⊢ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))
7	6	simpli 111	. . . . . . . 8 ⊢ (log‘2) ∈ ℝ
8	7	recni 8338	. . . . . . 7 ⊢ (log‘2) ∈ ℂ
9	8	mulridi 8328	. . . . . 6 ⊢ ((log‘2) · 1) = (log‘2)
10		cht2 16195	. . . . . 6 ⊢ (θ‘2) = (log‘2)
11	9, 10	eqtr4i 2262	. . . . 5 ⊢ ((log‘2) · 1) = (θ‘2)
12		fveq2 5695	. . . . 5 ⊢ ((⌊‘𝑁) = 2 → (θ‘(⌊‘𝑁)) = (θ‘2))
13	11, 12	eqtr4id 2290	. . . 4 ⊢ ((⌊‘𝑁) = 2 → ((log‘2) · 1) = (θ‘(⌊‘𝑁)))
14		chtqfl 16177	. . . . 5 ⊢ (𝑁 ∈ ℚ → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
15	14	adantr 276	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
16	13, 15	sylan9eqr 2293	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) = (θ‘𝑁))
17		qre 10034	. . . 4 ⊢ (𝑁 ∈ ℚ → 𝑁 ∈ ℝ)
18		2t2e4 9461	. . . . . . . 8 ⊢ (2 · 2) = 4
19		df-4 9367	. . . . . . . 8 ⊢ 4 = (3 + 1)
20	18, 19	eqtri 2259	. . . . . . 7 ⊢ (2 · 2) = (3 + 1)
21		simplr 533	. . . . . . . 8 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 2 < 𝑁)
22		simpl 109	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 𝑁 ∈ ℝ)
23		2pos 9397	. . . . . . . . . . 11 ⊢ 0 < 2
24	1, 23	pm3.2i 272	. . . . . . . . . 10 ⊢ (2 ∈ ℝ ∧ 0 < 2)
25	24	a1i 9	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 ∈ ℝ ∧ 0 < 2))
26		ltmul2 9188	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑁 ↔ (2 · 2) < (2 · 𝑁)))
27	1, 22, 25, 26	mp3an2ani 1385	. . . . . . . 8 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 < 𝑁 ↔ (2 · 2) < (2 · 𝑁)))
28	21, 27	mpbid 147	. . . . . . 7 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 · 2) < (2 · 𝑁))
29	20, 28	eqbrtrrid 4166	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (3 + 1) < (2 · 𝑁))
30		3re 9380	. . . . . . . 8 ⊢ 3 ∈ ℝ
31	30	a1i 9	. . . . . . 7 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 3 ∈ ℝ)
32		1red 8341	. . . . . . 7 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 1 ∈ ℝ)
33		remulcl 8307	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
34	1, 22, 33	sylancr 418	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (2 · 𝑁) ∈ ℝ)
35	34	adantr 276	. . . . . . 7 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 · 𝑁) ∈ ℝ)
36	31, 32, 35	ltaddsub2d 8875	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((3 + 1) < (2 · 𝑁) ↔ 1 < ((2 · 𝑁) − 3)))
37	29, 36	mpbid 147	. . . . 5 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 1 < ((2 · 𝑁) − 3))
38		resubcl 8591	. . . . . . . 8 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · 𝑁) − 3) ∈ ℝ)
39	34, 30, 38	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → ((2 · 𝑁) − 3) ∈ ℝ)
40	39	adantr 276	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((2 · 𝑁) − 3) ∈ ℝ)
41	6	a1i 9	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
42		ltmul2 9188	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3))))
43	32, 40, 41, 42	syl3anc 1278	. . . . 5 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3))))
44	37, 43	mpbid 147	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3)))
45	17, 44	sylanl1 406	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3)))
46	16, 45	eqbrtrrd 4154	. 2 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
47		chtqcl 16163	. . . 4 ⊢ (𝑁 ∈ ℚ → (θ‘𝑁) ∈ ℝ)
48	47	ad2antrr 492	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (θ‘𝑁) ∈ ℝ)
49		flqcl 10718	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ∈ ℤ)
50	49	zred 9772	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ∈ ℝ)
51	50	ad2antrr 492	. . . . . 6 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ ℝ)
52		remulcl 8307	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ (⌊‘𝑁) ∈ ℝ) → (2 · (⌊‘𝑁)) ∈ ℝ)
53	1, 51, 52	sylancr 418	. . . . 5 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (2 · (⌊‘𝑁)) ∈ ℝ)
54		resubcl 8591	. . . . 5 ⊢ (((2 · (⌊‘𝑁)) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
55	53, 30, 54	sylancl 417	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
56		remulcl 8307	. . . 4 ⊢ (((log‘2) ∈ ℝ ∧ ((2 · (⌊‘𝑁)) − 3) ∈ ℝ) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈ ℝ)
57	7, 55, 56	sylancr 418	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈ ℝ)
58	39	adantr 276	. . . . 5 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((2 · 𝑁) − 3) ∈ ℝ)
59		remulcl 8307	. . . . 5 ⊢ (((log‘2) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
60	7, 58, 59	sylancr 418	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
61	17, 60	sylanl1 406	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
62	14	ad2antrr 492	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
63		simpr 110	. . . . . . 7 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1)))
64		df-3 9366	. . . . . . . 8 ⊢ 3 = (2 + 1)
65	64	fveq2i 5698	. . . . . . 7 ⊢ (ℤ≥‘3) = (ℤ≥‘(2 + 1))
66	63, 65	eleqtrrdi 2332	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ≥‘3))
67		fveq2 5695	. . . . . . . 8 ⊢ (𝑘 = (⌊‘𝑁) → (θ‘𝑘) = (θ‘(⌊‘𝑁)))
68		oveq2 6093	. . . . . . . . . 10 ⊢ (𝑘 = (⌊‘𝑁) → (2 · 𝑘) = (2 · (⌊‘𝑁)))
69	68	oveq1d 6100	. . . . . . . . 9 ⊢ (𝑘 = (⌊‘𝑁) → ((2 · 𝑘) − 3) = ((2 · (⌊‘𝑁)) − 3))
70	69	oveq2d 6101	. . . . . . . 8 ⊢ (𝑘 = (⌊‘𝑁) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
71	67, 70	breq12d 4143	. . . . . . 7 ⊢ (𝑘 = (⌊‘𝑁) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3))))
72		oveq2 6093	. . . . . . . . 9 ⊢ (𝑥 = 3 → (3...𝑥) = (3...3))
73	72	raleqdv 2755	. . . . . . . 8 ⊢ (𝑥 = 3 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...3)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
74		oveq2 6093	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (3...𝑥) = (3...𝑛))
75	74	raleqdv 2755	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
76		oveq2 6093	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (3...𝑥) = (3...(𝑛 + 1)))
77	76	raleqdv 2755	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
78		oveq2 6093	. . . . . . . . 9 ⊢ (𝑥 = (⌊‘𝑁) → (3...𝑥) = (3...(⌊‘𝑁)))
79	78	raleqdv 2755	. . . . . . . 8 ⊢ (𝑥 = (⌊‘𝑁) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
80		6lt8 9500	. . . . . . . . . . . 12 ⊢ 6 < 8
81		6re 9387	. . . . . . . . . . . . . 14 ⊢ 6 ∈ ℝ
82		6pos 9407	. . . . . . . . . . . . . 14 ⊢ 0 < 6
83	81, 82	elrpii 10067	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℝ+
84		8re 9391	. . . . . . . . . . . . . 14 ⊢ 8 ∈ ℝ
85		8pos 9409	. . . . . . . . . . . . . 14 ⊢ 0 < 8
86	84, 85	elrpii 10067	. . . . . . . . . . . . 13 ⊢ 8 ∈ ℝ+
87		logltb 16026	. . . . . . . . . . . . 13 ⊢ ((6 ∈ ℝ+ ∧ 8 ∈ ℝ+) → (6 < 8 ↔ (log‘6) < (log‘8)))
88	83, 86, 87	mp2an 430	. . . . . . . . . . . 12 ⊢ (6 < 8 ↔ (log‘6) < (log‘8))
89	80, 88	mpbi 145	. . . . . . . . . . 11 ⊢ (log‘6) < (log‘8)
90	89	a1i 9	. . . . . . . . . 10 ⊢ (𝑘 ∈ (3...3) → (log‘6) < (log‘8))
91		elfz1eq 10449	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (3...3) → 𝑘 = 3)
92	91	fveq2d 5699	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (3...3) → (θ‘𝑘) = (θ‘3))
93		cht3 16196	. . . . . . . . . . 11 ⊢ (θ‘3) = (log‘6)
94	92, 93	eqtrdi 2287	. . . . . . . . . 10 ⊢ (𝑘 ∈ (3...3) → (θ‘𝑘) = (log‘6))
95	91	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (3...3) → (2 · 𝑘) = (2 · 3))
96	95	oveq1d 6100	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (3...3) → ((2 · 𝑘) − 3) = ((2 · 3) − 3))
97		3cn 9381	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
98	97	2timesi 9436	. . . . . . . . . . . . . 14 ⊢ (2 · 3) = (3 + 3)
99	97, 97, 98	mvrraddi 8544	. . . . . . . . . . . . 13 ⊢ ((2 · 3) − 3) = 3
100	96, 99	eqtrdi 2287	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (3...3) → ((2 · 𝑘) − 3) = 3)
101	100	oveq2d 6101	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (3...3) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · 3))
102		2rp 10069	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ+
103		relogcl 16013	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
104	102, 103	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (log‘2) ∈ ℝ
105	104	recni 8338	. . . . . . . . . . . . . 14 ⊢ (log‘2) ∈ ℂ
106	105, 97	mulcomi 8332	. . . . . . . . . . . . 13 ⊢ ((log‘2) · 3) = (3 · (log‘2))
107		3z 9677	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℤ
108		relogexp 16024	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
109	102, 107, 108	mp2an 430	. . . . . . . . . . . . 13 ⊢ (log‘(2↑3)) = (3 · (log‘2))
110	106, 109	eqtr4i 2262	. . . . . . . . . . . 12 ⊢ ((log‘2) · 3) = (log‘(2↑3))
111		cu2 11088	. . . . . . . . . . . . 13 ⊢ (2↑3) = 8
112	111	fveq2i 5698	. . . . . . . . . . . 12 ⊢ (log‘(2↑3)) = (log‘8)
113	110, 112	eqtri 2259	. . . . . . . . . . 11 ⊢ ((log‘2) · 3) = (log‘8)
114	101, 113	eqtrdi 2287	. . . . . . . . . 10 ⊢ (𝑘 ∈ (3...3) → ((log‘2) · ((2 · 𝑘) − 3)) = (log‘8))
115	90, 94, 114	3brtr4d 4162	. . . . . . . . 9 ⊢ (𝑘 ∈ (3...3) → (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
116	115	rgen 2603	. . . . . . . 8 ⊢ ∀𝑘 ∈ (3...3)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))
117		df-2 9365	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
118		2div2e1 9439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 / 2) = 1
119		eluzle 9943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (ℤ≥‘3) → 3 ≤ 𝑛)
120	64, 119	eqbrtrrid 4166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 + 1) ≤ 𝑛)
121		2z 9676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℤ
122		eluzelz 9940	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (ℤ≥‘3) → 𝑛 ∈ ℤ)
123		zltp1le 9703	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛))
124	121, 122, 123	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛))
125	120, 124	mpbird 167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘3) → 2 < 𝑛)
126		eluzelre 9941	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (ℤ≥‘3) → 𝑛 ∈ ℝ)
127		ltdiv1 9200	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
128	1, 24, 127	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
129	126, 128	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
130	125, 129	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 / 2) < (𝑛 / 2))
131	118, 130	eqbrtrrid 4166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ≥‘3) → 1 < (𝑛 / 2))
132	126	rehalfcld 9556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 / 2) ∈ ℝ)
133		1re 8325	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ
134		ltadd1 8758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (𝑛 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
135	133, 133, 134	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 / 2) ∈ ℝ → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
136	132, 135	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ≥‘3) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
137	131, 136	mpbid 147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → (1 + 1) < ((𝑛 / 2) + 1))
138	117, 137	eqbrtrid 4165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → 2 < ((𝑛 / 2) + 1))
139	138	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 < ((𝑛 / 2) + 1))
140		peano2z 9684	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 / 2) ∈ ℤ → ((𝑛 / 2) + 1) ∈ ℤ)
141	140	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℤ)
142		zltp1le 9703	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ ((𝑛 / 2) + 1) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1)))
143	121, 141, 142	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1)))
144	139, 143	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 + 1) ≤ ((𝑛 / 2) + 1))
145	64, 144	eqbrtrid 4165	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 3 ≤ ((𝑛 / 2) + 1))
146		1red 8341	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → 1 ∈ ℝ)
147		ltle 8413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ (𝑛 / 2) ∈ ℝ) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2)))
148	133, 132, 147	sylancr 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2)))
149	131, 148	mpd 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → 1 ≤ (𝑛 / 2))
150	146, 132, 132, 149	leadd2dd 8889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((𝑛 / 2) + 1) ≤ ((𝑛 / 2) + (𝑛 / 2)))
151	126	recnd 8354	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → 𝑛 ∈ ℂ)
152	151	2halvesd 9555	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((𝑛 / 2) + (𝑛 / 2)) = 𝑛)
153	150, 152	breqtrd 4156	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((𝑛 / 2) + 1) ≤ 𝑛)
154	153	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ≤ 𝑛)
155		elfz 10427	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑛 / 2) + 1) ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
156	107, 155	mp3an2 1366	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 / 2) + 1) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
157	140, 122, 156	syl2anr 290	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
158	145, 154, 157	mpbir2and 957	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (3...𝑛))
159		fveq2 5695	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = ((𝑛 / 2) + 1) → (θ‘𝑘) = (θ‘((𝑛 / 2) + 1)))
160		oveq2 6093	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = ((𝑛 / 2) + 1) → (2 · 𝑘) = (2 · ((𝑛 / 2) + 1)))
161	160	oveq1d 6100	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑛 / 2) + 1) → ((2 · 𝑘) − 3) = ((2 · ((𝑛 / 2) + 1)) − 3))
162	161	oveq2d 6101	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = ((𝑛 / 2) + 1) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))
163	159, 162	breq12d 4143	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = ((𝑛 / 2) + 1) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
164	163	rspcv 2925	. . . . . . . . . . . . . 14 ⊢ (((𝑛 / 2) + 1) ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
165	158, 164	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
166	132	recnd 8354	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 / 2) ∈ ℂ)
167	166	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 / 2) ∈ ℂ)
168		2cn 9377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℂ
169		ax-1cn 8272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
170		adddi 8311	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ (𝑛 / 2) ∈ ℂ ∧ 1 ∈ ℂ) → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
171	168, 169, 170	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 / 2) ∈ ℂ → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
172	167, 171	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
173	151	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈ ℂ)
174		id 19	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℂ → 𝑛 ∈ ℂ)
175		2cnd 9379	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℂ → 2 ∈ ℂ)
176		2ap0 9399	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 # 0
177	176	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℂ → 2 # 0)
178	174, 175, 177	divcanap2d 9124	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℂ → (2 · (𝑛 / 2)) = 𝑛)
179	173, 178	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 / 2)) = 𝑛)
180	168	mulridi 8328	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 · 1) = 2
181	180	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 1) = 2)
182	179, 181	oveq12d 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 / 2)) + (2 · 1)) = (𝑛 + 2))
183	172, 182	eqtrd 2271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · ((𝑛 / 2) + 1)) = (𝑛 + 2))
184	183	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 3) = ((𝑛 + 2) − 3))
185		subsub3 8559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
186	97, 168, 185	mp3an23 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℂ → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
187	173, 186	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
188		2p1e3 9440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 + 1) = 3
189	97, 168, 169, 188	subaddrii 8616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (3 − 2) = 1
190	189	oveq2i 6096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 − (3 − 2)) = (𝑛 − 1)
191	187, 190	eqtr3di 2286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 3) = (𝑛 − 1))
192	184, 191	eqtrd 2271	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 3) = (𝑛 − 1))
193	192	oveq2d 6101	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) = ((log‘2) · (𝑛 − 1)))
194	193	breq2d 4142	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔ (θ‘((𝑛 / 2) + 1)) < ((log‘2) · (𝑛 − 1))))
195		zq 10035	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 / 2) + 1) ∈ ℤ → ((𝑛 / 2) + 1) ∈ ℚ)
196	141, 195	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℚ)
197		chtqcl 16163	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 / 2) + 1) ∈ ℚ → (θ‘((𝑛 / 2) + 1)) ∈ ℝ)
198	196, 197	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((𝑛 / 2) + 1)) ∈ ℝ)
199	126	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈ ℝ)
200		peano2rem 8594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
201	199, 200	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈ ℝ)
202		remulcl 8307	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘2) ∈ ℝ ∧ (𝑛 − 1) ∈ ℝ) → ((log‘2) · (𝑛 − 1)) ∈ ℝ)
203	104, 201, 202	sylancr 418	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · (𝑛 − 1)) ∈ ℝ)
204		remulcl 8307	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘2) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((log‘2) · 𝑛) ∈ ℝ)
205	104, 199, 204	sylancr 418	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · 𝑛) ∈ ℝ)
206	198, 203, 205	ltadd1d 8867	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · (𝑛 − 1)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛))))
207	105	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (log‘2) ∈ ℂ)
208	201	recnd 8354	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈ ℂ)
209	207, 208, 173	adddid 8350	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((𝑛 − 1) + 𝑛)) = (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)))
210		adddi 8311	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
211	168, 169, 210	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℂ → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
212	173, 211	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
213	180	oveq2i 6096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 𝑛) + (2 · 1)) = ((2 · 𝑛) + 2)
214	212, 213	eqtrdi 2287	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + 2))
215	214	oveq1d 6100	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 + 1)) − 3) = (((2 · 𝑛) + 2) − 3))
216		zmulcl 9702	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
217	121, 122, 216	sylancr 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 · 𝑛) ∈ ℤ)
218	217	zcnd 9773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 · 𝑛) ∈ ℂ)
219	218	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 𝑛) ∈ ℂ)
220		subsub3 8559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑛) ∈ ℂ ∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
221	97, 168, 220	mp3an23 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
222	219, 221	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
223	189	oveq2i 6096	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑛) − (3 − 2)) = ((2 · 𝑛) − 1)
224	173	2timesd 9552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 𝑛) = (𝑛 + 𝑛))
225	224	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − 1) = ((𝑛 + 𝑛) − 1))
226	169	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 1 ∈ ℂ)
227	173, 173, 226	addsubd 8659	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 𝑛) − 1) = ((𝑛 − 1) + 𝑛))
228	225, 227	eqtrd 2271	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − 1) = ((𝑛 − 1) + 𝑛))
229	223, 228	eqtrid 2283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − (3 − 2)) = ((𝑛 − 1) + 𝑛))
230	215, 222, 229	3eqtr2rd 2278	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 − 1) + 𝑛) = ((2 · (𝑛 + 1)) − 3))
231	230	oveq2d 6101	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((𝑛 − 1) + 𝑛)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
232	209, 231	eqtr3d 2273	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
233	232	breq2d 4142	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
234	194, 206, 233	3bitrd 214	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
235		3nn 9471	. . . . . . . . . . . . . . . . . 18 ⊢ 3 ∈ ℕ
236		elfzuz 10434	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 / 2) + 1) ∈ (3...𝑛) → ((𝑛 / 2) + 1) ∈ (ℤ≥‘3))
237	158, 236	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (ℤ≥‘3))
238		eluznn 10009	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 ∈ ℕ ∧ ((𝑛 / 2) + 1) ∈ (ℤ≥‘3)) → ((𝑛 / 2) + 1) ∈ ℕ)
239	235, 237, 238	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℕ)
240		chtublem 16214	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 / 2) + 1) ∈ ℕ → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))))
241	239, 240	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))))
242	183	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 1) = ((𝑛 + 2) − 1))
243		addsubass 8537	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
244	168, 169, 243	mp3an23 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℂ → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
245	173, 244	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
246		2m1e1 9424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 − 1) = 1
247	246	oveq2i 6096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 + (2 − 1)) = (𝑛 + 1)
248	245, 247	eqtrdi 2287	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + 1))
249	242, 248	eqtrd 2271	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 1) = (𝑛 + 1))
250	249	fveq2d 5699	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) = (θ‘(𝑛 + 1)))
251		pncan 8533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 / 2) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2))
252	167, 169, 251	sylancl 417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2))
253	252	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (((𝑛 / 2) + 1) − 1)) = ((log‘4) · (𝑛 / 2)))
254		relogexp 16024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℝ+ ∧ 2 ∈ ℤ) → (log‘(2↑2)) = (2 · (log‘2)))
255	102, 121, 254	mp2an 430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (log‘(2↑2)) = (2 · (log‘2))
256		sq2 11085	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2↑2) = 4
257	256	fveq2i 5698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (log‘(2↑2)) = (log‘4)
258	168, 105	mulcomi 8332	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · (log‘2)) = ((log‘2) · 2)
259	255, 257, 258	3eqtr3i 2267	. . . . . . . . . . . . . . . . . . . 20 ⊢ (log‘4) = ((log‘2) · 2)
260	259	oveq1i 6095	. . . . . . . . . . . . . . . . . . 19 ⊢ ((log‘4) · (𝑛 / 2)) = (((log‘2) · 2) · (𝑛 / 2))
261		2cnd 9379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 ∈ ℂ)
262	207, 261, 167	mulassd 8349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2) · 2) · (𝑛 / 2)) = ((log‘2) · (2 · (𝑛 / 2))))
263	260, 262	eqtrid 2283	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (𝑛 / 2)) = ((log‘2) · (2 · (𝑛 / 2))))
264	179	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · (2 · (𝑛 / 2))) = ((log‘2) · 𝑛))
265	253, 263, 264	3eqtrd 2275	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (((𝑛 / 2) + 1) − 1)) = ((log‘2) · 𝑛))
266	265	oveq2d 6101	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))) = ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)))
267	241, 250, 266	3brtr3d 4161	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)))
268		peano2uz 9992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 + 1) ∈ (ℤ≥‘3))
269		eluzelz 9940	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 + 1) ∈ (ℤ≥‘3) → (𝑛 + 1) ∈ ℤ)
270	268, 269	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 + 1) ∈ ℤ)
271		zq 10035	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 + 1) ∈ ℤ → (𝑛 + 1) ∈ ℚ)
272	270, 271	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 + 1) ∈ ℚ)
273	272	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 + 1) ∈ ℚ)
274		chtqcl 16163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 + 1) ∈ ℚ → (θ‘(𝑛 + 1)) ∈ ℝ)
275	273, 274	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) ∈ ℝ)
276	198, 205	readdcld 8355	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∈ ℝ)
277		zmulcl 9702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℤ ∧ (𝑛 + 1) ∈ ℤ) → (2 · (𝑛 + 1)) ∈ ℤ)
278	121, 270, 277	sylancr 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 · (𝑛 + 1)) ∈ ℤ)
279	278	zred 9772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 · (𝑛 + 1)) ∈ ℝ)
280		resubcl 8591	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · (𝑛 + 1)) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
281	279, 30, 280	sylancl 417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
282	281	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
283		remulcl 8307	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘2) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
284	104, 282, 283	sylancr 418	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
285		lelttr 8414	. . . . . . . . . . . . . . . 16 ⊢ (((θ‘(𝑛 + 1)) ∈ ℝ ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∈ ℝ ∧ ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ) → (((θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
286	275, 276, 284, 285	syl3anc 1278	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
287	267, 286	mpand 433	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
288	234, 287	sylbid 150	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
289	165, 288	syld 45	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
290		eluzfz2 10446	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ≥‘3) → 𝑛 ∈ (3...𝑛))
291		fveq2 5695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (θ‘𝑘) = (θ‘𝑛))
292		oveq2 6093	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
293	292	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((2 · 𝑘) − 3) = ((2 · 𝑛) − 3))
294	293	oveq2d 6101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · 𝑛) − 3)))
295	291, 294	breq12d 4143	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
296	295	rspcv 2925	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
297	290, 296	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
298	297	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
299	217	zred 9772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 · 𝑛) ∈ ℝ)
300	30	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → 3 ∈ ℝ)
301	126	ltp1d 9262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → 𝑛 < (𝑛 + 1))
302	270	zred 9772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 + 1) ∈ ℝ)
303	24	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 ∈ ℝ ∧ 0 < 2))
304		ltmul2 9188	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1))))
305	126, 302, 303, 304	syl3anc 1278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1))))
306	301, 305	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 · 𝑛) < (2 · (𝑛 + 1)))
307	299, 279, 300, 306	ltsub1dd 8886	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3))
308		resubcl 8591	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · 𝑛) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · 𝑛) − 3) ∈ ℝ)
309	299, 30, 308	sylancl 417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((2 · 𝑛) − 3) ∈ ℝ)
310	6	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
311		ltmul2 9188	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2 · 𝑛) − 3) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
312	309, 281, 310, 311	syl3anc 1278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
313	307, 312	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
314		zq 10035	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℚ)
315	122, 314	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → 𝑛 ∈ ℚ)
316		chtqcl 16163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℚ → (θ‘𝑛) ∈ ℝ)
317	315, 316	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → (θ‘𝑛) ∈ ℝ)
318		remulcl 8307	. . . . . . . . . . . . . . . . . 18 ⊢ (((log‘2) ∈ ℝ ∧ ((2 · 𝑛) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ)
319	104, 309, 318	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ)
320	104, 281, 283	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
321		lttr 8399	. . . . . . . . . . . . . . . . 17 ⊢ (((θ‘𝑛) ∈ ℝ ∧ ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ ∧ ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ) → (((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) ∧ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
322	317, 319, 320, 321	syl3anc 1278	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ℤ≥‘3) → (((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) ∧ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
323	313, 322	mpan2d 432	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
324	323	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
325		evend2 12672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 + 1) ∈ ℤ → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
326	270, 325	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
327		2lt3 9479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 3
328		zltnle 9694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ 3 ∈ ℤ) → (2 < 3 ↔ ¬ 3 ≤ 2))
329	121, 107, 328	mp2an 430	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2 < 3 ↔ ¬ 3 ≤ 2)
330	327, 329	mpbi 145	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ 3 ≤ 2
331		breq2 4134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 = (𝑛 + 1) → (3 ≤ 2 ↔ 3 ≤ (𝑛 + 1)))
332	330, 331	mtbii 685	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 = (𝑛 + 1) → ¬ 3 ≤ (𝑛 + 1))
333		eluzle 9943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 + 1) ∈ (ℤ≥‘3) → 3 ≤ (𝑛 + 1))
334	268, 333	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (ℤ≥‘3) → 3 ≤ (𝑛 + 1))
335	332, 334	nsyl3 635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ℤ≥‘3) → ¬ 2 = (𝑛 + 1))
336	335	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 = (𝑛 + 1))
337		uzid 9945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ≥‘2))
338	121, 337	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ (ℤ≥‘2)
339		simpr 110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → (𝑛 + 1) ∈ ℙ)
340		dvdsprm 12932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ (ℤ≥‘2) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥ (𝑛 + 1) ↔ 2 = (𝑛 + 1)))
341	338, 339, 340	sylancr 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥ (𝑛 + 1) ↔ 2 = (𝑛 + 1)))
342	336, 341	mtbird 684	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 ∥ (𝑛 + 1))
343	342	ex 115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((𝑛 + 1) ∈ ℙ → ¬ 2 ∥ (𝑛 + 1)))
344	343	con2d 633	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘3) → (2 ∥ (𝑛 + 1) → ¬ (𝑛 + 1) ∈ ℙ))
345	326, 344	sylbird 170	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ≥‘3) → (((𝑛 + 1) / 2) ∈ ℤ → ¬ (𝑛 + 1) ∈ ℙ))
346	345	imp 124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ¬ (𝑛 + 1) ∈ ℙ)
347		chtnprm 16181	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℤ ∧ ¬ (𝑛 + 1) ∈ ℙ) → (θ‘(𝑛 + 1)) = (θ‘𝑛))
348	122, 346, 347	syl2an2r 603	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) = (θ‘𝑛))
349	348	breq1d 4140	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ↔ (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
350	324, 349	sylibrd 169	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
351	298, 350	syld 45	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ (ℤ≥‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
352		zeo 9755	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℤ → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈ ℤ))
353	122, 352	syl 14	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈ ℤ))
354	289, 351, 353	mpjaodan 810	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
355	122	peano2zd 9775	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ℤ≥‘3) → (𝑛 + 1) ∈ ℤ)
356		fveq2 5695	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑛 + 1) → (θ‘𝑘) = (θ‘(𝑛 + 1)))
357		oveq2 6093	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (2 · 𝑘) = (2 · (𝑛 + 1)))
358	357	oveq1d 6100	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑛 + 1) → ((2 · 𝑘) − 3) = ((2 · (𝑛 + 1)) − 3))
359	358	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑛 + 1) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
360	356, 359	breq12d 4143	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 + 1) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
361	360	ralsng 3749	. . . . . . . . . . . 12 ⊢ ((𝑛 + 1) ∈ ℤ → (∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
362	355, 361	syl 14	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
363	354, 362	sylibrd 169	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
364	363	ancld 325	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))))
365		ralun 3411	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
366		fzsuc 10485	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘3) → (3...(𝑛 + 1)) = ((3...𝑛) ∪ {(𝑛 + 1)}))
367	366	raleqdv 2755	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
368	365, 367	imbitrrid 156	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘3) → ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
369	364, 368	syld 45	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ≥‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
370	73, 75, 77, 79, 116, 369	uzind4i 10001	. . . . . . 7 ⊢ ((⌊‘𝑁) ∈ (ℤ≥‘3) → ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
371		eluzfz2 10446	. . . . . . 7 ⊢ ((⌊‘𝑁) ∈ (ℤ≥‘3) → (⌊‘𝑁) ∈ (3...(⌊‘𝑁)))
372	71, 370, 371	rspcdva 2934	. . . . . 6 ⊢ ((⌊‘𝑁) ∈ (ℤ≥‘3) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
373	66, 372	syl 14	. . . . 5 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
374	17, 373	sylanl1 406	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
375	62, 374	eqbrtrrd 4154	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
376	34	adantr 276	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (2 · 𝑁) ∈ ℝ)
377	17, 376	sylanl1 406	. . . . 5 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (2 · 𝑁) ∈ ℝ)
378	30	a1i 9	. . . . 5 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → 3 ∈ ℝ)
379		flqle 10725	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ≤ 𝑁)
380	379	ad2antrr 492	. . . . . 6 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (⌊‘𝑁) ≤ 𝑁)
381	17	ad2antrr 492	. . . . . . 7 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → 𝑁 ∈ ℝ)
382	24	a1i 9	. . . . . . 7 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (2 ∈ ℝ ∧ 0 < 2))
383		lemul2 9189	. . . . . . 7 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)))
384	51, 381, 382, 383	syl3anc 1278	. . . . . 6 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)))
385	380, 384	mpbid 147	. . . . 5 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (2 · (⌊‘𝑁)) ≤ (2 · 𝑁))
386	53, 377, 378, 385	lesub1dd 8890	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3))
387	17, 58	sylanl1 406	. . . . 5 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((2 · 𝑁) − 3) ∈ ℝ)
388	6	a1i 9	. . . . 5 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
389		lemul2 9189	. . . . 5 ⊢ ((((2 · (⌊‘𝑁)) − 3) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))))
390	55, 387, 388, 389	syl3anc 1278	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))))
391	386, 390	mpbid 147	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3)))
392	48, 57, 61, 375, 391	ltletrd 8752	. 2 ⊢ (((𝑁 ∈ ℚ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
393	121	a1i 9	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → 2 ∈ ℤ)
394	49	adantr 276	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → (⌊‘𝑁) ∈ ℤ)
395		ltle 8413	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁))
396	1, 17, 395	sylancr 418	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (2 < 𝑁 → 2 ≤ 𝑁))
397		flqge 10729	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 2 ∈ ℤ) → (2 ≤ 𝑁 ↔ 2 ≤ (⌊‘𝑁)))
398	121, 397	mpan2 429	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (2 ≤ 𝑁 ↔ 2 ≤ (⌊‘𝑁)))
399	396, 398	sylibd 149	. . . . 5 ⊢ (𝑁 ∈ ℚ → (2 < 𝑁 → 2 ≤ (⌊‘𝑁)))
400	399	imp 124	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → 2 ≤ (⌊‘𝑁))
401		eluz2 9936	. . . 4 ⊢ ((⌊‘𝑁) ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 2 ≤ (⌊‘𝑁)))
402	393, 394, 400, 401	syl3anbrc 1212	. . 3 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → (⌊‘𝑁) ∈ (ℤ≥‘2))
403		uzp1 9965	. . 3 ⊢ ((⌊‘𝑁) ∈ (ℤ≥‘2) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))))
404	402, 403	syl 14	. 2 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈ (ℤ≥‘(2 + 1))))
405	46, 392, 404	mpjaodan 810	1 ⊢ ((𝑁 ∈ ℚ ∧ 2 < 𝑁) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 720   = wceq 1402   ∈ wcel 2209  ∀wral 2528   ∪ cun 3218  {csn 3709   class class class wbr 4130  ‘cfv 5377  (class class class)co 6085  ℂcc 8177  ℝcr 8178  0cc0 8179  1c1 8180   + caddc 8182   · cmul 8184   < clt 8360   ≤ cle 8361   − cmin 8498   # cap 8911   / cdiv 9004  ℕcn 9306  2c2 9357  3c3 9358  4c4 9359  6c6 9361  8c8 9363  ℤcz 9648  ℤ_≥cuz 9930  ℚcq 10028  ℝ⁺crp 10064  ...cfz 10421  ⌊cfl 10713  ↑cexp 10988   ∥ cdvds 12570  ℙcprime 12901  logclog 16007  θccht 16152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-mulrcl 8278  ax-addcom 8279  ax-mulcom 8280  ax-addass 8281  ax-mulass 8282  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-1rid 8286  ax-0id 8287  ax-rnegex 8288  ax-precex 8289  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-apti 8294  ax-pre-ltadd 8295  ax-pre-mulgt0 8296  ax-pre-mulext 8297  ax-arch 8298  ax-caucvg 8299  ax-pre-suploc 8300  ax-addf 8301  ax-mulf 8302

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-disj 4107  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-of 6302  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6807  df-map 6924  df-pm 6925  df-en 7023  df-dom 7024  df-fin 7025  df-sup 7324  df-inf 7325  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8500  df-neg 8501  df-reap 8905  df-ap 8912  df-div 9005  df-inn 9307  df-2 9365  df-3 9366  df-4 9367  df-5 9368  df-6 9369  df-7 9370  df-8 9371  df-n0 9568  df-xnn0 9635  df-z 9649  df-uz 9931  df-q 10029  df-rp 10065  df-xneg 10184  df-xadd 10185  df-ioo 10304  df-ico 10306  df-icc 10307  df-fz 10422  df-fzo 10560  df-fl 10715  df-mod 10773  df-seqfrec 10898  df-exp 10989  df-fac 11178  df-bc 11200  df-ihash 11229  df-shft 11594  df-cj 11621  df-re 11622  df-im 11623  df-rsqrt 11778  df-abs 11779  df-clim 12061  df-sumdc 12136  df-ef 12431  df-e 12432  df-dvds 12571  df-gcd 12747  df-prm 12902  df-pc 13084  df-rest 13644  df-topgen 13663  df-psmet 14929  df-xmet 14930  df-met 14931  df-bl 14932  df-mopn 14933  df-top 15148  df-topon 15161  df-bases 15193  df-ntr 15246  df-cn 15338  df-cnp 15339  df-tx 15403  df-cncf 15721  df-limced 15806  df-dvap 15807  df-relog 16009  df-cht 16155

This theorem is used by: (None)