chtub

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

		Ref	Expression
	Assertion	chtub	$⊢ (N \in ℝ \land 2 < N) \to θ (N) < \log 2 (2 \cdot N - 3)$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		1lt2	$⊢ 1 < 2$
3		rplogcl	$⊢ (2 \in ℝ \land 1 < 2) \to \log 2 \in ℝ^{+}$
4	1 2 3	mp2an	$⊢ \log 2 \in ℝ^{+}$
5		elrp	$⊢ \log 2 \in ℝ^{+} \leftrightarrow (\log 2 \in ℝ \land 0 < \log 2)$
6	4 5	mpbi	$⊢ (\log 2 \in ℝ \land 0 < \log 2)$
7	6	simpli	$⊢ \log 2 \in ℝ$
8	7	recni	$⊢ \log 2 \in ℂ$
9	8	mulridi	$⊢ \log 2 \cdot 1 = \log 2$
10		cht2	$⊢ θ (2) = \log 2$
11	9 10	eqtr4i	$⊢ \log 2 \cdot 1 = θ (2)$
12		fveq2	$⊢ ⌊N⌋ = 2 \to θ (⌊N⌋) = θ (2)$
13	11 12	eqtr4id	$⊢ ⌊N⌋ = 2 \to \log 2 \cdot 1 = θ (⌊N⌋)$
14		chtfl	$⊢ N \in ℝ \to θ (⌊N⌋) = θ (N)$
15	14	adantr	$⊢ (N \in ℝ \land 2 < N) \to θ (⌊N⌋) = θ (N)$
16	13 15	sylan9eqr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to \log 2 \cdot 1 = θ (N)$
17		2t2e4	$⊢ 2 \cdot 2 = 4$
18		df-4	$⊢ 4 = 3 + 1$
19	17 18	eqtri	$⊢ 2 \cdot 2 = 3 + 1$
20		simplr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 2 < N$
21		simpl	$⊢ (N \in ℝ \land 2 < N) \to N \in ℝ$
22		2pos	$⊢ 0 < 2$
23	1 22	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
24	23	a1i	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to (2 \in ℝ \land 0 < 2)$
25		ltmul2	$⊢ (2 \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 < N \leftrightarrow 2 \cdot 2 < 2 \cdot N)$
26	1 21 24 25	mp3an2ani	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to (2 < N \leftrightarrow 2 \cdot 2 < 2 \cdot N)$
27	20 26	mpbid	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 2 \cdot 2 < 2 \cdot N$
28	19 27	eqbrtrrid	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 3 + 1 < 2 \cdot N$
29		3re	$⊢ 3 \in ℝ$
30	29	a1i	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 3 \in ℝ$
31		1red	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 1 \in ℝ$
32		remulcl	$⊢ (2 \in ℝ \land N \in ℝ) \to 2 \cdot N \in ℝ$
33	1 21 32	sylancr	$⊢ (N \in ℝ \land 2 < N) \to 2 \cdot N \in ℝ$
34	33	adantr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 2 \cdot N \in ℝ$
35	30 31 34	ltaddsub2d	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to (3 + 1 < 2 \cdot N \leftrightarrow 1 < 2 \cdot N - 3)$
36	28 35	mpbid	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 1 < 2 \cdot N - 3$
37		resubcl	$⊢ (2 \cdot N \in ℝ \land 3 \in ℝ) \to 2 \cdot N - 3 \in ℝ$
38	33 29 37	sylancl	$⊢ (N \in ℝ \land 2 < N) \to 2 \cdot N - 3 \in ℝ$
39	38	adantr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to 2 \cdot N - 3 \in ℝ$
40	6	a1i	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to (\log 2 \in ℝ \land 0 < \log 2)$
41		ltmul2	$⊢ (1 \in ℝ \land 2 \cdot N - 3 \in ℝ \land (\log 2 \in ℝ \land 0 < \log 2)) \to (1 < 2 \cdot N - 3 \leftrightarrow \log 2 \cdot 1 < \log 2 (2 \cdot N - 3))$
42	31 39 40 41	syl3anc	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to (1 < 2 \cdot N - 3 \leftrightarrow \log 2 \cdot 1 < \log 2 (2 \cdot N - 3))$
43	36 42	mpbid	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to \log 2 \cdot 1 < \log 2 (2 \cdot N - 3)$
44	16 43	eqbrtrrd	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ = 2) \to θ (N) < \log 2 (2 \cdot N - 3)$
45		chtcl	$⊢ N \in ℝ \to θ (N) \in ℝ$
46	45	ad2antrr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to θ (N) \in ℝ$
47		reflcl	$⊢ N \in ℝ \to ⌊N⌋ \in ℝ$
48	47	ad2antrr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to ⌊N⌋ \in ℝ$
49		remulcl	$⊢ (2 \in ℝ \land ⌊N⌋ \in ℝ) \to 2 ⌊N⌋ \in ℝ$
50	1 48 49	sylancr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 2 ⌊N⌋ \in ℝ$
51		resubcl	$⊢ (2 ⌊N⌋ \in ℝ \land 3 \in ℝ) \to 2 ⌊N⌋ - 3 \in ℝ$
52	50 29 51	sylancl	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 2 ⌊N⌋ - 3 \in ℝ$
53		remulcl	$⊢ (\log 2 \in ℝ \land 2 ⌊N⌋ - 3 \in ℝ) \to \log 2 (2 ⌊N⌋ - 3) \in ℝ$
54	7 52 53	sylancr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to \log 2 (2 ⌊N⌋ - 3) \in ℝ$
55	38	adantr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 2 \cdot N - 3 \in ℝ$
56		remulcl	$⊢ (\log 2 \in ℝ \land 2 \cdot N - 3 \in ℝ) \to \log 2 (2 \cdot N - 3) \in ℝ$
57	7 55 56	sylancr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to \log 2 (2 \cdot N - 3) \in ℝ$
58	15	adantr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to θ (⌊N⌋) = θ (N)$
59		simpr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to ⌊N⌋ \in ℤ_{\geq (2 + 1)}$
60		df-3	$⊢ 3 = 2 + 1$
61	60	fveq2i	$⊢ ℤ_{\geq 3} = ℤ_{\geq (2 + 1)}$
62	59 61	eleqtrrdi	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to ⌊N⌋ \in ℤ_{\geq 3}$
63		fveq2	$⊢ k = ⌊N⌋ \to θ (k) = θ (⌊N⌋)$
64		oveq2	$⊢ k = ⌊N⌋ \to 2 k = 2 ⌊N⌋$
65	64	oveq1d	$⊢ k = ⌊N⌋ \to 2 k - 3 = 2 ⌊N⌋ - 3$
66	65	oveq2d	$⊢ k = ⌊N⌋ \to \log 2 (2 k - 3) = \log 2 (2 ⌊N⌋ - 3)$
67	63 66	breq12d	$⊢ k = ⌊N⌋ \to (θ (k) < \log 2 (2 k - 3) \leftrightarrow θ (⌊N⌋) < \log 2 (2 ⌊N⌋ - 3))$
68		oveq2	$⊢ x = 3 \to (3 \dots x) = (3 \dots 3)$
69	68	raleqdv	$⊢ x = 3 \to (\forall k \in (3 \dots x) θ (k) < \log 2 (2 k - 3) \leftrightarrow \forall k \in (3 \dots 3) θ (k) < \log 2 (2 k - 3))$
70		oveq2	$⊢ x = n \to (3 \dots x) = (3 \dots n)$
71	70	raleqdv	$⊢ x = n \to (\forall k \in (3 \dots x) θ (k) < \log 2 (2 k - 3) \leftrightarrow \forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3))$
72		oveq2	$⊢ x = n + 1 \to (3 \dots x) = (3 \dots n + 1)$
73	72	raleqdv	$⊢ x = n + 1 \to (\forall k \in (3 \dots x) θ (k) < \log 2 (2 k - 3) \leftrightarrow \forall k \in (3 \dots n + 1) θ (k) < \log 2 (2 k - 3))$
74		oveq2	$⊢ x = ⌊N⌋ \to (3 \dots x) = (3 \dots ⌊N⌋)$
75	74	raleqdv	$⊢ x = ⌊N⌋ \to (\forall k \in (3 \dots x) θ (k) < \log 2 (2 k - 3) \leftrightarrow \forall k \in (3 \dots ⌊N⌋) θ (k) < \log 2 (2 k - 3))$
76		6lt8	$⊢ 6 < 8$
77		6re	$⊢ 6 \in ℝ$
78		6pos	$⊢ 0 < 6$
79	77 78	elrpii	$⊢ 6 \in ℝ^{+}$
80		8re	$⊢ 8 \in ℝ$
81		8pos	$⊢ 0 < 8$
82	80 81	elrpii	$⊢ 8 \in ℝ^{+}$
83		logltb	$⊢ (6 \in ℝ^{+} \land 8 \in ℝ^{+}) \to (6 < 8 \leftrightarrow \log 6 < \log 8)$
84	79 82 83	mp2an	$⊢ 6 < 8 \leftrightarrow \log 6 < \log 8$
85	76 84	mpbi	$⊢ \log 6 < \log 8$
86	85	a1i	$⊢ k \in (3 \dots 3) \to \log 6 < \log 8$
87		elfz1eq	$⊢ k \in (3 \dots 3) \to k = 3$
88	87	fveq2d	$⊢ k \in (3 \dots 3) \to θ (k) = θ (3)$
89		cht3	$⊢ θ (3) = \log 6$
90	88 89	eqtrdi	$⊢ k \in (3 \dots 3) \to θ (k) = \log 6$
91	87	oveq2d	$⊢ k \in (3 \dots 3) \to 2 k = 2 \cdot 3$
92	91	oveq1d	$⊢ k \in (3 \dots 3) \to 2 k - 3 = 2 \cdot 3 - 3$
93		3cn	$⊢ 3 \in ℂ$
94	93	2timesi	$⊢ 2 \cdot 3 = 3 + 3$
95	93 93 94	mvrraddi	$⊢ 2 \cdot 3 - 3 = 3$
96	92 95	eqtrdi	$⊢ k \in (3 \dots 3) \to 2 k - 3 = 3$
97	96	oveq2d	$⊢ k \in (3 \dots 3) \to \log 2 (2 k - 3) = \log 2 \cdot 3$
98		2rp	$⊢ 2 \in ℝ^{+}$
99		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
100	98 99	ax-mp	$⊢ \log 2 \in ℝ$
101	100	recni	$⊢ \log 2 \in ℂ$
102	101 93	mulcomi	$⊢ \log 2 \cdot 3 = 3 \log 2$
103		3z	$⊢ 3 \in ℤ$
104		relogexp	$⊢ (2 \in ℝ^{+} \land 3 \in ℤ) \to \log 2^{3} = 3 \log 2$
105	98 103 104	mp2an	$⊢ \log 2^{3} = 3 \log 2$
106	102 105	eqtr4i	$⊢ \log 2 \cdot 3 = \log 2^{3}$
107		cu2	$⊢ 2^{3} = 8$
108	107	fveq2i	$⊢ \log 2^{3} = \log 8$
109	106 108	eqtri	$⊢ \log 2 \cdot 3 = \log 8$
110	97 109	eqtrdi	$⊢ k \in (3 \dots 3) \to \log 2 (2 k - 3) = \log 8$
111	86 90 110	3brtr4d	$⊢ k \in (3 \dots 3) \to θ (k) < \log 2 (2 k - 3)$
112	111	rgen	$⊢ \forall k \in (3 \dots 3) θ (k) < \log 2 (2 k - 3)$
113		df-2	$⊢ 2 = 1 + 1$
114		2div2e1	$⊢ \frac{2}{2} = 1$
115		eluzle	$⊢ n \in ℤ_{\geq 3} \to 3 \leq n$
116	60 115	eqbrtrrid	$⊢ n \in ℤ_{\geq 3} \to 2 + 1 \leq n$
117		2z	$⊢ 2 \in ℤ$
118		eluzelz	$⊢ n \in ℤ_{\geq 3} \to n \in ℤ$
119		zltp1le	$⊢ (2 \in ℤ \land n \in ℤ) \to (2 < n \leftrightarrow 2 + 1 \leq n)$
120	117 118 119	sylancr	$⊢ n \in ℤ_{\geq 3} \to (2 < n \leftrightarrow 2 + 1 \leq n)$
121	116 120	mpbird	$⊢ n \in ℤ_{\geq 3} \to 2 < n$
122		eluzelre	$⊢ n \in ℤ_{\geq 3} \to n \in ℝ$
123		ltdiv1	$⊢ (2 \in ℝ \land n \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 < n \leftrightarrow \frac{2}{2} < \frac{n}{2})$
124	1 23 123	mp3an13	$⊢ n \in ℝ \to (2 < n \leftrightarrow \frac{2}{2} < \frac{n}{2})$
125	122 124	syl	$⊢ n \in ℤ_{\geq 3} \to (2 < n \leftrightarrow \frac{2}{2} < \frac{n}{2})$
126	121 125	mpbid	$⊢ n \in ℤ_{\geq 3} \to \frac{2}{2} < \frac{n}{2}$
127	114 126	eqbrtrrid	$⊢ n \in ℤ_{\geq 3} \to 1 < \frac{n}{2}$
128	122	rehalfcld	$⊢ n \in ℤ_{\geq 3} \to \frac{n}{2} \in ℝ$
129		1re	$⊢ 1 \in ℝ$
130		ltadd1	$⊢ (1 \in ℝ \land \frac{n}{2} \in ℝ \land 1 \in ℝ) \to (1 < \frac{n}{2} \leftrightarrow 1 + 1 < (\frac{n}{2}) + 1)$
131	129 129 130	mp3an13	$⊢ \frac{n}{2} \in ℝ \to (1 < \frac{n}{2} \leftrightarrow 1 + 1 < (\frac{n}{2}) + 1)$
132	128 131	syl	$⊢ n \in ℤ_{\geq 3} \to (1 < \frac{n}{2} \leftrightarrow 1 + 1 < (\frac{n}{2}) + 1)$
133	127 132	mpbid	$⊢ n \in ℤ_{\geq 3} \to 1 + 1 < (\frac{n}{2}) + 1$
134	113 133	eqbrtrid	$⊢ n \in ℤ_{\geq 3} \to 2 < (\frac{n}{2}) + 1$
135	134	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 < (\frac{n}{2}) + 1$
136		peano2z	$⊢ \frac{n}{2} \in ℤ \to (\frac{n}{2}) + 1 \in ℤ$
137	136	adantl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 \in ℤ$
138		zltp1le	$⊢ (2 \in ℤ \land (\frac{n}{2}) + 1 \in ℤ) \to (2 < (\frac{n}{2}) + 1 \leftrightarrow 2 + 1 \leq (\frac{n}{2}) + 1)$
139	117 137 138	sylancr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (2 < (\frac{n}{2}) + 1 \leftrightarrow 2 + 1 \leq (\frac{n}{2}) + 1)$
140	135 139	mpbid	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 + 1 \leq (\frac{n}{2}) + 1$
141	60 140	eqbrtrid	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 3 \leq (\frac{n}{2}) + 1$
142		1red	$⊢ n \in ℤ_{\geq 3} \to 1 \in ℝ$
143		ltle	$⊢ (1 \in ℝ \land \frac{n}{2} \in ℝ) \to (1 < \frac{n}{2} \to 1 \leq \frac{n}{2})$
144	129 128 143	sylancr	$⊢ n \in ℤ_{\geq 3} \to (1 < \frac{n}{2} \to 1 \leq \frac{n}{2})$
145	127 144	mpd	$⊢ n \in ℤ_{\geq 3} \to 1 \leq \frac{n}{2}$
146	142 128 128 145	leadd2dd	$⊢ n \in ℤ_{\geq 3} \to (\frac{n}{2}) + 1 \leq (\frac{n}{2}) + (\frac{n}{2})$
147	122	recnd	$⊢ n \in ℤ_{\geq 3} \to n \in ℂ$
148	147	2halvesd	$⊢ n \in ℤ_{\geq 3} \to (\frac{n}{2}) + (\frac{n}{2}) = n$
149	146 148	breqtrd	$⊢ n \in ℤ_{\geq 3} \to (\frac{n}{2}) + 1 \leq n$
150	149	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 \leq n$
151		elfz	$⊢ ((\frac{n}{2}) + 1 \in ℤ \land 3 \in ℤ \land n \in ℤ) \to ((\frac{n}{2}) + 1 \in (3 \dots n) \leftrightarrow (3 \leq (\frac{n}{2}) + 1 \land (\frac{n}{2}) + 1 \leq n))$
152	103 151	mp3an2	$⊢ ((\frac{n}{2}) + 1 \in ℤ \land n \in ℤ) \to ((\frac{n}{2}) + 1 \in (3 \dots n) \leftrightarrow (3 \leq (\frac{n}{2}) + 1 \land (\frac{n}{2}) + 1 \leq n))$
153	136 118 152	syl2anr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to ((\frac{n}{2}) + 1 \in (3 \dots n) \leftrightarrow (3 \leq (\frac{n}{2}) + 1 \land (\frac{n}{2}) + 1 \leq n))$
154	141 150 153	mpbir2and	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 \in (3 \dots n)$
155		fveq2	$⊢ k = (\frac{n}{2}) + 1 \to θ (k) = θ ((\frac{n}{2}) + 1)$
156		oveq2	$⊢ k = (\frac{n}{2}) + 1 \to 2 k = 2 ((\frac{n}{2}) + 1)$
157	156	oveq1d	$⊢ k = (\frac{n}{2}) + 1 \to 2 k - 3 = 2 ((\frac{n}{2}) + 1) - 3$
158	157	oveq2d	$⊢ k = (\frac{n}{2}) + 1 \to \log 2 (2 k - 3) = \log 2 (2 ((\frac{n}{2}) + 1) - 3)$
159	155 158	breq12d	$⊢ k = (\frac{n}{2}) + 1 \to (θ (k) < \log 2 (2 k - 3) \leftrightarrow θ ((\frac{n}{2}) + 1) < \log 2 (2 ((\frac{n}{2}) + 1) - 3))$
160	159	rspcv	$⊢ (\frac{n}{2}) + 1 \in (3 \dots n) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ ((\frac{n}{2}) + 1) < \log 2 (2 ((\frac{n}{2}) + 1) - 3))$
161	154 160	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ ((\frac{n}{2}) + 1) < \log 2 (2 ((\frac{n}{2}) + 1) - 3))$
162	128	recnd	$⊢ n \in ℤ_{\geq 3} \to \frac{n}{2} \in ℂ$
163	162	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \frac{n}{2} \in ℂ$
164		2cn	$⊢ 2 \in ℂ$
165		ax-1cn	$⊢ 1 \in ℂ$
166		adddi	$⊢ (2 \in ℂ \land \frac{n}{2} \in ℂ \land 1 \in ℂ) \to 2 ((\frac{n}{2}) + 1) = 2 (\frac{n}{2}) + 2 \cdot 1$
167	164 165 166	mp3an13	$⊢ \frac{n}{2} \in ℂ \to 2 ((\frac{n}{2}) + 1) = 2 (\frac{n}{2}) + 2 \cdot 1$
168	163 167	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 ((\frac{n}{2}) + 1) = 2 (\frac{n}{2}) + 2 \cdot 1$
169	147	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n \in ℂ$
170		2ne0	$⊢ 2 \neq 0$
171		divcan2	$⊢ (n \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{n}{2}) = n$
172	164 170 171	mp3an23	$⊢ n \in ℂ \to 2 (\frac{n}{2}) = n$
173	169 172	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 (\frac{n}{2}) = n$
174	164	mulridi	$⊢ 2 \cdot 1 = 2$
175	174	a1i	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 \cdot 1 = 2$
176	173 175	oveq12d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 (\frac{n}{2}) + 2 \cdot 1 = n + 2$
177	168 176	eqtrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 ((\frac{n}{2}) + 1) = n + 2$
178	177	oveq1d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 ((\frac{n}{2}) + 1) - 3 = n + 2 - 3$
179		subsub3	$⊢ (n \in ℂ \land 3 \in ℂ \land 2 \in ℂ) \to n - (3 - 2) = n + 2 - 3$
180	93 164 179	mp3an23	$⊢ n \in ℂ \to n - (3 - 2) = n + 2 - 3$
181	169 180	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n - (3 - 2) = n + 2 - 3$
182		2p1e3	$⊢ 2 + 1 = 3$
183	93 164 165 182	subaddrii	$⊢ 3 - 2 = 1$
184	183	oveq2i	$⊢ n - (3 - 2) = n - 1$
185	181 184	eqtr3di	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n + 2 - 3 = n - 1$
186	178 185	eqtrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 ((\frac{n}{2}) + 1) - 3 = n - 1$
187	186	oveq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 (2 ((\frac{n}{2}) + 1) - 3) = \log 2 (n - 1)$
188	187	breq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (θ ((\frac{n}{2}) + 1) < \log 2 (2 ((\frac{n}{2}) + 1) - 3) \leftrightarrow θ ((\frac{n}{2}) + 1) < \log 2 (n - 1))$
189	137	zred	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 \in ℝ$
190		chtcl	$⊢ (\frac{n}{2}) + 1 \in ℝ \to θ ((\frac{n}{2}) + 1) \in ℝ$
191	189 190	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ ((\frac{n}{2}) + 1) \in ℝ$
192	122	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n \in ℝ$
193		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
194	192 193	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n - 1 \in ℝ$
195		remulcl	$⊢ (\log 2 \in ℝ \land n - 1 \in ℝ) \to \log 2 (n - 1) \in ℝ$
196	100 194 195	sylancr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 (n - 1) \in ℝ$
197		remulcl	$⊢ (\log 2 \in ℝ \land n \in ℝ) \to \log 2 n \in ℝ$
198	100 192 197	sylancr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 n \in ℝ$
199	191 196 198	ltadd1d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (θ ((\frac{n}{2}) + 1) < \log 2 (n - 1) \leftrightarrow θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (n - 1) + \log 2 n)$
200	101	a1i	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 \in ℂ$
201	194	recnd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n - 1 \in ℂ$
202	200 201 169	adddid	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 (n - 1 + n) = \log 2 (n - 1) + \log 2 n$
203		adddi	$⊢ (2 \in ℂ \land n \in ℂ \land 1 \in ℂ) \to 2 (n + 1) = 2 n + 2 \cdot 1$
204	164 165 203	mp3an13	$⊢ n \in ℂ \to 2 (n + 1) = 2 n + 2 \cdot 1$
205	169 204	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 (n + 1) = 2 n + 2 \cdot 1$
206	174	oveq2i	$⊢ 2 n + 2 \cdot 1 = 2 n + 2$
207	205 206	eqtrdi	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 (n + 1) = 2 n + 2$
208	207	oveq1d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 (n + 1) - 3 = 2 n + 2 - 3$
209		zmulcl	$⊢ (2 \in ℤ \land n \in ℤ) \to 2 n \in ℤ$
210	117 118 209	sylancr	$⊢ n \in ℤ_{\geq 3} \to 2 n \in ℤ$
211	210	zcnd	$⊢ n \in ℤ_{\geq 3} \to 2 n \in ℂ$
212	211	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 n \in ℂ$
213		subsub3	$⊢ (2 n \in ℂ \land 3 \in ℂ \land 2 \in ℂ) \to 2 n - (3 - 2) = 2 n + 2 - 3$
214	93 164 213	mp3an23	$⊢ 2 n \in ℂ \to 2 n - (3 - 2) = 2 n + 2 - 3$
215	212 214	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 n - (3 - 2) = 2 n + 2 - 3$
216	183	oveq2i	$⊢ 2 n - (3 - 2) = 2 n - 1$
217	169	2timesd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 n = n + n$
218	217	oveq1d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 n - 1 = n + n - 1$
219	165	a1i	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 1 \in ℂ$
220	169 169 219	addsubd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n + n - 1 = n - 1 + n$
221	218 220	eqtrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 n - 1 = n - 1 + n$
222	216 221	eqtrid	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 n - (3 - 2) = n - 1 + n$
223	208 215 222	3eqtr2rd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n - 1 + n = 2 (n + 1) - 3$
224	223	oveq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 (n - 1 + n) = \log 2 (2 (n + 1) - 3)$
225	202 224	eqtr3d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 (n - 1) + \log 2 n = \log 2 (2 (n + 1) - 3)$
226	225	breq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (n - 1) + \log 2 n \leftrightarrow θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (2 (n + 1) - 3))$
227	188 199 226	3bitrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (θ ((\frac{n}{2}) + 1) < \log 2 (2 ((\frac{n}{2}) + 1) - 3) \leftrightarrow θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (2 (n + 1) - 3))$
228		3nn	$⊢ 3 \in ℕ$
229		elfzuz	$⊢ (\frac{n}{2}) + 1 \in (3 \dots n) \to (\frac{n}{2}) + 1 \in ℤ_{\geq 3}$
230	154 229	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 \in ℤ_{\geq 3}$
231		eluznn	$⊢ (3 \in ℕ \land (\frac{n}{2}) + 1 \in ℤ_{\geq 3}) \to (\frac{n}{2}) + 1 \in ℕ$
232	228 230 231	sylancr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 \in ℕ$
233		chtublem	$⊢ (\frac{n}{2}) + 1 \in ℕ \to θ (2 ((\frac{n}{2}) + 1) - 1) \leq θ ((\frac{n}{2}) + 1) + \log 4 ((\frac{n}{2}) + 1 - 1)$
234	232 233	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ (2 ((\frac{n}{2}) + 1) - 1) \leq θ ((\frac{n}{2}) + 1) + \log 4 ((\frac{n}{2}) + 1 - 1)$
235	177	oveq1d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 ((\frac{n}{2}) + 1) - 1 = n + 2 - 1$
236		addsubass	$⊢ (n \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \to n + 2 - 1 = n + 2 - 1$
237	164 165 236	mp3an23	$⊢ n \in ℂ \to n + 2 - 1 = n + 2 - 1$
238	169 237	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n + 2 - 1 = n + 2 - 1$
239		2m1e1	$⊢ 2 - 1 = 1$
240	239	oveq2i	$⊢ n + 2 - 1 = n + 1$
241	238 240	eqtrdi	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n + 2 - 1 = n + 1$
242	235 241	eqtrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 ((\frac{n}{2}) + 1) - 1 = n + 1$
243	242	fveq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ (2 ((\frac{n}{2}) + 1) - 1) = θ (n + 1)$
244		pncan	$⊢ (\frac{n}{2} \in ℂ \land 1 \in ℂ) \to (\frac{n}{2}) + 1 - 1 = \frac{n}{2}$
245	163 165 244	sylancl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\frac{n}{2}) + 1 - 1 = \frac{n}{2}$
246	245	oveq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 4 ((\frac{n}{2}) + 1 - 1) = \log 4 (\frac{n}{2})$
247		relogexp	$⊢ (2 \in ℝ^{+} \land 2 \in ℤ) \to \log 2^{2} = 2 \log 2$
248	98 117 247	mp2an	$⊢ \log 2^{2} = 2 \log 2$
249		sq2	$⊢ 2^{2} = 4$
250	249	fveq2i	$⊢ \log 2^{2} = \log 4$
251	164 101	mulcomi	$⊢ 2 \log 2 = \log 2 \cdot 2$
252	248 250 251	3eqtr3i	$⊢ \log 4 = \log 2 \cdot 2$
253	252	oveq1i	$⊢ \log 4 (\frac{n}{2}) = \log 2 \cdot 2 (\frac{n}{2})$
254	164	a1i	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 \in ℂ$
255	200 254 163	mulassd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 \cdot 2 (\frac{n}{2}) = \log 2 2 (\frac{n}{2})$
256	253 255	eqtrid	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 4 (\frac{n}{2}) = \log 2 2 (\frac{n}{2})$
257	173	oveq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 2 (\frac{n}{2}) = \log 2 n$
258	246 256 257	3eqtrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 4 ((\frac{n}{2}) + 1 - 1) = \log 2 n$
259	258	oveq2d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ ((\frac{n}{2}) + 1) + \log 4 ((\frac{n}{2}) + 1 - 1) = θ ((\frac{n}{2}) + 1) + \log 2 n$
260	234 243 259	3brtr3d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ (n + 1) \leq θ ((\frac{n}{2}) + 1) + \log 2 n$
261		peano2uz	$⊢ n \in ℤ_{\geq 3} \to n + 1 \in ℤ_{\geq 3}$
262		eluzelz	$⊢ n + 1 \in ℤ_{\geq 3} \to n + 1 \in ℤ$
263	261 262	syl	$⊢ n \in ℤ_{\geq 3} \to n + 1 \in ℤ$
264	263	zred	$⊢ n \in ℤ_{\geq 3} \to n + 1 \in ℝ$
265	264	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to n + 1 \in ℝ$
266		chtcl	$⊢ n + 1 \in ℝ \to θ (n + 1) \in ℝ$
267	265 266	syl	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ (n + 1) \in ℝ$
268	191 198	readdcld	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to θ ((\frac{n}{2}) + 1) + \log 2 n \in ℝ$
269		zmulcl	$⊢ (2 \in ℤ \land n + 1 \in ℤ) \to 2 (n + 1) \in ℤ$
270	117 263 269	sylancr	$⊢ n \in ℤ_{\geq 3} \to 2 (n + 1) \in ℤ$
271	270	zred	$⊢ n \in ℤ_{\geq 3} \to 2 (n + 1) \in ℝ$
272		resubcl	$⊢ (2 (n + 1) \in ℝ \land 3 \in ℝ) \to 2 (n + 1) - 3 \in ℝ$
273	271 29 272	sylancl	$⊢ n \in ℤ_{\geq 3} \to 2 (n + 1) - 3 \in ℝ$
274	273	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to 2 (n + 1) - 3 \in ℝ$
275		remulcl	$⊢ (\log 2 \in ℝ \land 2 (n + 1) - 3 \in ℝ) \to \log 2 (2 (n + 1) - 3) \in ℝ$
276	100 274 275	sylancr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to \log 2 (2 (n + 1) - 3) \in ℝ$
277		lelttr	$⊢ (θ (n + 1) \in ℝ \land θ ((\frac{n}{2}) + 1) + \log 2 n \in ℝ \land \log 2 (2 (n + 1) - 3) \in ℝ) \to ((θ (n + 1) \leq θ ((\frac{n}{2}) + 1) + \log 2 n \land θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (2 (n + 1) - 3)) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
278	267 268 276 277	syl3anc	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to ((θ (n + 1) \leq θ ((\frac{n}{2}) + 1) + \log 2 n \land θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (2 (n + 1) - 3)) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
279	260 278	mpand	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (θ ((\frac{n}{2}) + 1) + \log 2 n < \log 2 (2 (n + 1) - 3) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
280	227 279	sylbid	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (θ ((\frac{n}{2}) + 1) < \log 2 (2 ((\frac{n}{2}) + 1) - 3) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
281	161 280	syld	$⊢ (n \in ℤ_{\geq 3} \land \frac{n}{2} \in ℤ) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
282		eluzfz2	$⊢ n \in ℤ_{\geq 3} \to n \in (3 \dots n)$
283		fveq2	$⊢ k = n \to θ (k) = θ (n)$
284		oveq2	$⊢ k = n \to 2 k = 2 n$
285	284	oveq1d	$⊢ k = n \to 2 k - 3 = 2 n - 3$
286	285	oveq2d	$⊢ k = n \to \log 2 (2 k - 3) = \log 2 (2 n - 3)$
287	283 286	breq12d	$⊢ k = n \to (θ (k) < \log 2 (2 k - 3) \leftrightarrow θ (n) < \log 2 (2 n - 3))$
288	287	rspcv	$⊢ n \in (3 \dots n) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ (n) < \log 2 (2 n - 3))$
289	282 288	syl	$⊢ n \in ℤ_{\geq 3} \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ (n) < \log 2 (2 n - 3))$
290	289	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ (n) < \log 2 (2 n - 3))$
291	210	zred	$⊢ n \in ℤ_{\geq 3} \to 2 n \in ℝ$
292	29	a1i	$⊢ n \in ℤ_{\geq 3} \to 3 \in ℝ$
293	122	ltp1d	$⊢ n \in ℤ_{\geq 3} \to n < n + 1$
294	23	a1i	$⊢ n \in ℤ_{\geq 3} \to (2 \in ℝ \land 0 < 2)$
295		ltmul2	$⊢ (n \in ℝ \land n + 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (n < n + 1 \leftrightarrow 2 n < 2 (n + 1))$
296	122 264 294 295	syl3anc	$⊢ n \in ℤ_{\geq 3} \to (n < n + 1 \leftrightarrow 2 n < 2 (n + 1))$
297	293 296	mpbid	$⊢ n \in ℤ_{\geq 3} \to 2 n < 2 (n + 1)$
298	291 271 292 297	ltsub1dd	$⊢ n \in ℤ_{\geq 3} \to 2 n - 3 < 2 (n + 1) - 3$
299		resubcl	$⊢ (2 n \in ℝ \land 3 \in ℝ) \to 2 n - 3 \in ℝ$
300	291 29 299	sylancl	$⊢ n \in ℤ_{\geq 3} \to 2 n - 3 \in ℝ$
301	6	a1i	$⊢ n \in ℤ_{\geq 3} \to (\log 2 \in ℝ \land 0 < \log 2)$
302		ltmul2	$⊢ (2 n - 3 \in ℝ \land 2 (n + 1) - 3 \in ℝ \land (\log 2 \in ℝ \land 0 < \log 2)) \to (2 n - 3 < 2 (n + 1) - 3 \leftrightarrow \log 2 (2 n - 3) < \log 2 (2 (n + 1) - 3))$
303	300 273 301 302	syl3anc	$⊢ n \in ℤ_{\geq 3} \to (2 n - 3 < 2 (n + 1) - 3 \leftrightarrow \log 2 (2 n - 3) < \log 2 (2 (n + 1) - 3))$
304	298 303	mpbid	$⊢ n \in ℤ_{\geq 3} \to \log 2 (2 n - 3) < \log 2 (2 (n + 1) - 3)$
305		chtcl	$⊢ n \in ℝ \to θ (n) \in ℝ$
306	122 305	syl	$⊢ n \in ℤ_{\geq 3} \to θ (n) \in ℝ$
307		remulcl	$⊢ (\log 2 \in ℝ \land 2 n - 3 \in ℝ) \to \log 2 (2 n - 3) \in ℝ$
308	100 300 307	sylancr	$⊢ n \in ℤ_{\geq 3} \to \log 2 (2 n - 3) \in ℝ$
309	100 273 275	sylancr	$⊢ n \in ℤ_{\geq 3} \to \log 2 (2 (n + 1) - 3) \in ℝ$
310		lttr	$⊢ (θ (n) \in ℝ \land \log 2 (2 n - 3) \in ℝ \land \log 2 (2 (n + 1) - 3) \in ℝ) \to ((θ (n) < \log 2 (2 n - 3) \land \log 2 (2 n - 3) < \log 2 (2 (n + 1) - 3)) \to θ (n) < \log 2 (2 (n + 1) - 3))$
311	306 308 309 310	syl3anc	$⊢ n \in ℤ_{\geq 3} \to ((θ (n) < \log 2 (2 n - 3) \land \log 2 (2 n - 3) < \log 2 (2 (n + 1) - 3)) \to θ (n) < \log 2 (2 (n + 1) - 3))$
312	304 311	mpan2d	$⊢ n \in ℤ_{\geq 3} \to (θ (n) < \log 2 (2 n - 3) \to θ (n) < \log 2 (2 (n + 1) - 3))$
313	312	adantr	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to (θ (n) < \log 2 (2 n - 3) \to θ (n) < \log 2 (2 (n + 1) - 3))$
314		evend2	$⊢ n + 1 \in ℤ \to (2 ∥ (n + 1) \leftrightarrow \frac{n + 1}{2} \in ℤ)$
315	263 314	syl	$⊢ n \in ℤ_{\geq 3} \to (2 ∥ (n + 1) \leftrightarrow \frac{n + 1}{2} \in ℤ)$
316		2lt3	$⊢ 2 < 3$
317	1 29	ltnlei	$⊢ 2 < 3 \leftrightarrow \neg 3 \leq 2$
318	316 317	mpbi	$⊢ \neg 3 \leq 2$
319		breq2	$⊢ 2 = n + 1 \to (3 \leq 2 \leftrightarrow 3 \leq n + 1)$
320	318 319	mtbii	$⊢ 2 = n + 1 \to \neg 3 \leq n + 1$
321		eluzle	$⊢ n + 1 \in ℤ_{\geq 3} \to 3 \leq n + 1$
322	261 321	syl	$⊢ n \in ℤ_{\geq 3} \to 3 \leq n + 1$
323	320 322	nsyl3	$⊢ n \in ℤ_{\geq 3} \to \neg 2 = n + 1$
324	323	adantr	$⊢ (n \in ℤ_{\geq 3} \land n + 1 \in ℙ) \to \neg 2 = n + 1$
325		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
326	117 325	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
327		simpr	$⊢ (n \in ℤ_{\geq 3} \land n + 1 \in ℙ) \to n + 1 \in ℙ$
328		dvdsprm	$⊢ (2 \in ℤ_{\geq 2} \land n + 1 \in ℙ) \to (2 ∥ (n + 1) \leftrightarrow 2 = n + 1)$
329	326 327 328	sylancr	$⊢ (n \in ℤ_{\geq 3} \land n + 1 \in ℙ) \to (2 ∥ (n + 1) \leftrightarrow 2 = n + 1)$
330	324 329	mtbird	$⊢ (n \in ℤ_{\geq 3} \land n + 1 \in ℙ) \to \neg 2 ∥ (n + 1)$
331	330	ex	$⊢ n \in ℤ_{\geq 3} \to (n + 1 \in ℙ \to \neg 2 ∥ (n + 1))$
332	331	con2d	$⊢ n \in ℤ_{\geq 3} \to (2 ∥ (n + 1) \to \neg n + 1 \in ℙ)$
333	315 332	sylbird	$⊢ n \in ℤ_{\geq 3} \to (\frac{n + 1}{2} \in ℤ \to \neg n + 1 \in ℙ)$
334	333	imp	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to \neg n + 1 \in ℙ$
335		chtnprm	$⊢ (n \in ℤ \land \neg n + 1 \in ℙ) \to θ (n + 1) = θ (n)$
336	118 334 335	syl2an2r	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to θ (n + 1) = θ (n)$
337	336	breq1d	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to (θ (n + 1) < \log 2 (2 (n + 1) - 3) \leftrightarrow θ (n) < \log 2 (2 (n + 1) - 3))$
338	313 337	sylibrd	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to (θ (n) < \log 2 (2 n - 3) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
339	290 338	syld	$⊢ (n \in ℤ_{\geq 3} \land \frac{n + 1}{2} \in ℤ) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
340		zeo	$⊢ n \in ℤ \to (\frac{n}{2} \in ℤ \lor \frac{n + 1}{2} \in ℤ)$
341	118 340	syl	$⊢ n \in ℤ_{\geq 3} \to (\frac{n}{2} \in ℤ \lor \frac{n + 1}{2} \in ℤ)$
342	281 339 341	mpjaodan	$⊢ n \in ℤ_{\geq 3} \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to θ (n + 1) < \log 2 (2 (n + 1) - 3))$
343		ovex	$⊢ n + 1 \in V$
344		fveq2	$⊢ k = n + 1 \to θ (k) = θ (n + 1)$
345		oveq2	$⊢ k = n + 1 \to 2 k = 2 (n + 1)$
346	345	oveq1d	$⊢ k = n + 1 \to 2 k - 3 = 2 (n + 1) - 3$
347	346	oveq2d	$⊢ k = n + 1 \to \log 2 (2 k - 3) = \log 2 (2 (n + 1) - 3)$
348	344 347	breq12d	$⊢ k = n + 1 \to (θ (k) < \log 2 (2 k - 3) \leftrightarrow θ (n + 1) < \log 2 (2 (n + 1) - 3))$
349	343 348	ralsn	$⊢ \forall k \in \{n + 1\} θ (k) < \log 2 (2 k - 3) \leftrightarrow θ (n + 1) < \log 2 (2 (n + 1) - 3)$
350	342 349	imbitrrdi	$⊢ n \in ℤ_{\geq 3} \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to \forall k \in \{n + 1\} θ (k) < \log 2 (2 k - 3))$
351	350	ancld	$⊢ n \in ℤ_{\geq 3} \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \land \forall k \in \{n + 1\} θ (k) < \log 2 (2 k - 3)))$
352		ralun	$⊢ (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \land \forall k \in \{n + 1\} θ (k) < \log 2 (2 k - 3)) \to \forall k \in ((3 \dots n) \cup \{n + 1\}) θ (k) < \log 2 (2 k - 3)$
353		fzsuc	$⊢ n \in ℤ_{\geq 3} \to (3 \dots n + 1) = (3 \dots n) \cup \{n + 1\}$
354	353	raleqdv	$⊢ n \in ℤ_{\geq 3} \to (\forall k \in (3 \dots n + 1) θ (k) < \log 2 (2 k - 3) \leftrightarrow \forall k \in ((3 \dots n) \cup \{n + 1\}) θ (k) < \log 2 (2 k - 3))$
355	352 354	imbitrrid	$⊢ n \in ℤ_{\geq 3} \to ((\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \land \forall k \in \{n + 1\} θ (k) < \log 2 (2 k - 3)) \to \forall k \in (3 \dots n + 1) θ (k) < \log 2 (2 k - 3))$
356	351 355	syld	$⊢ n \in ℤ_{\geq 3} \to (\forall k \in (3 \dots n) θ (k) < \log 2 (2 k - 3) \to \forall k \in (3 \dots n + 1) θ (k) < \log 2 (2 k - 3))$
357	69 71 73 75 112 356	uzind4i	$⊢ ⌊N⌋ \in ℤ_{\geq 3} \to \forall k \in (3 \dots ⌊N⌋) θ (k) < \log 2 (2 k - 3)$
358		eluzfz2	$⊢ ⌊N⌋ \in ℤ_{\geq 3} \to ⌊N⌋ \in (3 \dots ⌊N⌋)$
359	67 357 358	rspcdva	$⊢ ⌊N⌋ \in ℤ_{\geq 3} \to θ (⌊N⌋) < \log 2 (2 ⌊N⌋ - 3)$
360	62 359	syl	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to θ (⌊N⌋) < \log 2 (2 ⌊N⌋ - 3)$
361	58 360	eqbrtrrd	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to θ (N) < \log 2 (2 ⌊N⌋ - 3)$
362	33	adantr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 2 \cdot N \in ℝ$
363	29	a1i	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 3 \in ℝ$
364		flle	$⊢ N \in ℝ \to ⌊N⌋ \leq N$
365	364	ad2antrr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to ⌊N⌋ \leq N$
366	21	adantr	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to N \in ℝ$
367	23	a1i	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to (2 \in ℝ \land 0 < 2)$
368		lemul2	$⊢ (⌊N⌋ \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (⌊N⌋ \leq N \leftrightarrow 2 ⌊N⌋ \leq 2 \cdot N)$
369	48 366 367 368	syl3anc	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to (⌊N⌋ \leq N \leftrightarrow 2 ⌊N⌋ \leq 2 \cdot N)$
370	365 369	mpbid	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 2 ⌊N⌋ \leq 2 \cdot N$
371	50 362 363 370	lesub1dd	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to 2 ⌊N⌋ - 3 \leq 2 \cdot N - 3$
372	6	a1i	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to (\log 2 \in ℝ \land 0 < \log 2)$
373		lemul2	$⊢ (2 ⌊N⌋ - 3 \in ℝ \land 2 \cdot N - 3 \in ℝ \land (\log 2 \in ℝ \land 0 < \log 2)) \to (2 ⌊N⌋ - 3 \leq 2 \cdot N - 3 \leftrightarrow \log 2 (2 ⌊N⌋ - 3) \leq \log 2 (2 \cdot N - 3))$
374	52 55 372 373	syl3anc	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to (2 ⌊N⌋ - 3 \leq 2 \cdot N - 3 \leftrightarrow \log 2 (2 ⌊N⌋ - 3) \leq \log 2 (2 \cdot N - 3))$
375	371 374	mpbid	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to \log 2 (2 ⌊N⌋ - 3) \leq \log 2 (2 \cdot N - 3)$
376	46 54 57 361 375	ltletrd	$⊢ ((N \in ℝ \land 2 < N) \land ⌊N⌋ \in ℤ_{\geq (2 + 1)}) \to θ (N) < \log 2 (2 \cdot N - 3)$
377	117	a1i	$⊢ (N \in ℝ \land 2 < N) \to 2 \in ℤ$
378		flcl	$⊢ N \in ℝ \to ⌊N⌋ \in ℤ$
379	378	adantr	$⊢ (N \in ℝ \land 2 < N) \to ⌊N⌋ \in ℤ$
380		ltle	$⊢ (2 \in ℝ \land N \in ℝ) \to (2 < N \to 2 \leq N)$
381	1 380	mpan	$⊢ N \in ℝ \to (2 < N \to 2 \leq N)$
382		flge	$⊢ (N \in ℝ \land 2 \in ℤ) \to (2 \leq N \leftrightarrow 2 \leq ⌊N⌋)$
383	117 382	mpan2	$⊢ N \in ℝ \to (2 \leq N \leftrightarrow 2 \leq ⌊N⌋)$
384	381 383	sylibd	$⊢ N \in ℝ \to (2 < N \to 2 \leq ⌊N⌋)$
385	384	imp	$⊢ (N \in ℝ \land 2 < N) \to 2 \leq ⌊N⌋$
386		eluz2	$⊢ ⌊N⌋ \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land ⌊N⌋ \in ℤ \land 2 \leq ⌊N⌋)$
387	377 379 385 386	syl3anbrc	$⊢ (N \in ℝ \land 2 < N) \to ⌊N⌋ \in ℤ_{\geq 2}$
388		uzp1	$⊢ ⌊N⌋ \in ℤ_{\geq 2} \to (⌊N⌋ = 2 \lor ⌊N⌋ \in ℤ_{\geq (2 + 1)})$
389	387 388	syl	$⊢ (N \in ℝ \land 2 < N) \to (⌊N⌋ = 2 \lor ⌊N⌋ \in ℤ_{\geq (2 + 1)})$
390	44 376 389	mpjaodan	$⊢ (N \in ℝ \land 2 < N) \to θ (N) < \log 2 (2 \cdot N - 3)$

Metamath Proof Explorer

Theorem chtub

Proof