Theorem chtqub 16308

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

Assertion

Ref	Expression
chtqub	|- ( ( N e. QQ /\ 2 < N ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )

Proof of Theorem chtqub

Dummy variables k n x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 9384	. . . . . . . . . . 11 |- 2 e. RR
2		1lt2 9486	. . . . . . . . . . 11 |- 1 < 2
3		rplogcl 16121	. . . . . . . . . . 11 |- ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
4	1, 2, 3	mp2an 430	. . . . . . . . . 10 |- ( log ` 2 ) e. RR+
5		elrp 10074	. . . . . . . . . 10 |- ( ( log ` 2 ) e. RR+ <-> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
6	4, 5	mpbi 145	. . . . . . . . 9 |- ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) )
7	6	simpli 111	. . . . . . . 8 |- ( log ` 2 ) e. RR
8	7	recni 8345	. . . . . . 7 |- ( log ` 2 ) e. CC
9	8	mulridi 8335	. . . . . 6 |- ( ( log ` 2 ) x. 1 ) = ( log ` 2 )
10		cht2 16288	. . . . . 6 |- ( theta ` 2 ) = ( log ` 2 )
11	9, 10	eqtr4i 2262	. . . . 5 |- ( ( log ` 2 ) x. 1 ) = ( theta ` 2 )
12		fveq2 5698	. . . . 5 |- ( ( |_ ` N ) = 2 -> ( theta ` ( |_ ` N ) ) = ( theta ` 2 ) )
13	11, 12	eqtr4id 2290	. . . 4 |- ( ( |_ ` N ) = 2 -> ( ( log ` 2 ) x. 1 ) = ( theta ` ( |_ ` N ) ) )
14		chtqfl 16270	. . . . 5 |- ( N e. QQ -> ( theta ` ( |_ ` N ) ) = ( theta ` N ) )
15	14	adantr 276	. . . 4 |- ( ( N e. QQ /\ 2 < N ) -> ( theta ` ( |_ ` N ) ) = ( theta ` N ) )
16	13, 15	sylan9eqr 2293	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) x. 1 ) = ( theta ` N ) )
17		qre 10042	. . . 4 |- ( N e. QQ -> N e. RR )
18		2t2e4 9469	. . . . . . . 8 |- ( 2 x. 2 ) = 4
19		df-4 9375	. . . . . . . 8 |- 4 = ( 3 + 1 )
20	18, 19	eqtri 2259	. . . . . . 7 |- ( 2 x. 2 ) = ( 3 + 1 )
21		simplr 533	. . . . . . . 8 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 2 < N )
22		simpl 109	. . . . . . . . 9 |- ( ( N e. RR /\ 2 < N ) -> N e. RR )
23		2pos 9405	. . . . . . . . . . 11 |- 0 < 2
24	1, 23	pm3.2i 272	. . . . . . . . . 10 |- ( 2 e. RR /\ 0 < 2 )
25	24	a1i 9	. . . . . . . . 9 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 e. RR /\ 0 < 2 ) )
26		ltmul2 9195	. . . . . . . . 9 |- ( ( 2 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 2 < N <-> ( 2 x. 2 ) < ( 2 x. N ) ) )
27	1, 22, 25, 26	mp3an2ani 1385	. . . . . . . 8 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 < N <-> ( 2 x. 2 ) < ( 2 x. N ) ) )
28	21, 27	mpbid 147	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 x. 2 ) < ( 2 x. N ) )
29	20, 28	eqbrtrrid 4167	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 3 + 1 ) < ( 2 x. N ) )
30		3re 9388	. . . . . . . 8 |- 3 e. RR
31	30	a1i 9	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 3 e. RR )
32		1red 8348	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 1 e. RR )
33		remulcl 8314	. . . . . . . . 9 |- ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
34	1, 22, 33	sylancr 418	. . . . . . . 8 |- ( ( N e. RR /\ 2 < N ) -> ( 2 x. N ) e. RR )
35	34	adantr 276	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 2 x. N ) e. RR )
36	31, 32, 35	ltaddsub2d 8882	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( 3 + 1 ) < ( 2 x. N ) <-> 1 < ( ( 2 x. N ) - 3 ) ) )
37	29, 36	mpbid 147	. . . . 5 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 1 < ( ( 2 x. N ) - 3 ) )
38		resubcl 8598	. . . . . . . 8 |- ( ( ( 2 x. N ) e. RR /\ 3 e. RR ) -> ( ( 2 x. N ) - 3 ) e. RR )
39	34, 30, 38	sylancl 417	. . . . . . 7 |- ( ( N e. RR /\ 2 < N ) -> ( ( 2 x. N ) - 3 ) e. RR )
40	39	adantr 276	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( 2 x. N ) - 3 ) e. RR )
41	6	a1i 9	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
42		ltmul2 9195	. . . . . 6 |- ( ( 1 e. RR /\ ( ( 2 x. N ) - 3 ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( 1 < ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
43	32, 40, 41, 42	syl3anc 1278	. . . . 5 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 1 < ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
44	37, 43	mpbid 147	. . . 4 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
45	17, 44	sylanl1 406	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( ( log ` 2 ) x. 1 ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
46	16, 45	eqbrtrrd 4155	. 2 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
47		chtqcl 16256	. . . 4 |- ( N e. QQ -> ( theta ` N ) e. RR )
48	47	ad2antrr 492	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` N ) e. RR )
49		flqcl 10726	. . . . . . . 8 |- ( N e. QQ -> ( |_ ` N ) e. ZZ )
50	49	zred 9780	. . . . . . 7 |- ( N e. QQ -> ( |_ ` N ) e. RR )
51	50	ad2antrr 492	. . . . . 6 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) e. RR )
52		remulcl 8314	. . . . . 6 |- ( ( 2 e. RR /\ ( |_ ` N ) e. RR ) -> ( 2 x. ( |_ ` N ) ) e. RR )
53	1, 51, 52	sylancr 418	. . . . 5 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. ( |_ ` N ) ) e. RR )
54		resubcl 8598	. . . . 5 |- ( ( ( 2 x. ( |_ ` N ) ) e. RR /\ 3 e. RR ) -> ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR )
55	53, 30, 54	sylancl 417	. . . 4 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR )
56		remulcl 8314	. . . 4 |- ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) e. RR )
57	7, 55, 56	sylancr 418	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) e. RR )
58	39	adantr 276	. . . . 5 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. N ) - 3 ) e. RR )
59		remulcl 8314	. . . . 5 |- ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. N ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) e. RR )
60	7, 58, 59	sylancr 418	. . . 4 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) e. RR )
61	17, 60	sylanl1 406	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) e. RR )
62	14	ad2antrr 492	. . . 4 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` ( |_ ` N ) ) = ( theta ` N ) )
63		simpr 110	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) )
64		df-3 9374	. . . . . . . 8 |- 3 = ( 2 + 1 )
65	64	fveq2i 5701	. . . . . . 7 |- ( ZZ>= ` 3 ) = ( ZZ>= ` ( 2 + 1 ) )
66	63, 65	eleqtrrdi 2332	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) e. ( ZZ>= ` 3 ) )
67		fveq2 5698	. . . . . . . 8 |- ( k = ( |_ ` N ) -> ( theta ` k ) = ( theta ` ( |_ ` N ) ) )
68		oveq2 6096	. . . . . . . . . 10 |- ( k = ( |_ ` N ) -> ( 2 x. k ) = ( 2 x. ( |_ ` N ) ) )
69	68	oveq1d 6103	. . . . . . . . 9 |- ( k = ( |_ ` N ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( |_ ` N ) ) - 3 ) )
70	69	oveq2d 6104	. . . . . . . 8 |- ( k = ( |_ ` N ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
71	67, 70	breq12d 4144	. . . . . . 7 |- ( k = ( |_ ` N ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) ) )
72		oveq2 6096	. . . . . . . . 9 |- ( x = 3 -> ( 3 ... x ) = ( 3 ... 3 ) )
73	72	raleqdv 2755	. . . . . . . 8 |- ( x = 3 -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... 3 ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
74		oveq2 6096	. . . . . . . . 9 |- ( x = n -> ( 3 ... x ) = ( 3 ... n ) )
75	74	raleqdv 2755	. . . . . . . 8 |- ( x = n -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
76		oveq2 6096	. . . . . . . . 9 |- ( x = ( n + 1 ) -> ( 3 ... x ) = ( 3 ... ( n + 1 ) ) )
77	76	raleqdv 2755	. . . . . . . 8 |- ( x = ( n + 1 ) -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
78		oveq2 6096	. . . . . . . . 9 |- ( x = ( |_ ` N ) -> ( 3 ... x ) = ( 3 ... ( |_ ` N ) ) )
79	78	raleqdv 2755	. . . . . . . 8 |- ( x = ( |_ ` N ) -> ( A. k e. ( 3 ... x ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( 3 ... ( |_ ` N ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
80		6lt8 9508	. . . . . . . . . . . 12 |- 6 < 8
81		6re 9395	. . . . . . . . . . . . . 14 |- 6 e. RR
82		6pos 9415	. . . . . . . . . . . . . 14 |- 0 < 6
83	81, 82	elrpii 10075	. . . . . . . . . . . . 13 |- 6 e. RR+
84		8re 9399	. . . . . . . . . . . . . 14 |- 8 e. RR
85		8pos 9417	. . . . . . . . . . . . . 14 |- 0 < 8
86	84, 85	elrpii 10075	. . . . . . . . . . . . 13 |- 8 e. RR+
87		logltb 16116	. . . . . . . . . . . . 13 |- ( ( 6 e. RR+ /\ 8 e. RR+ ) -> ( 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 |- ( k e. ( 3 ... 3 ) -> ( log ` 6 ) < ( log ` 8 ) )
91		elfz1eq 10457	. . . . . . . . . . . 12 |- ( k e. ( 3 ... 3 ) -> k = 3 )
92	91	fveq2d 5702	. . . . . . . . . . 11 |- ( k e. ( 3 ... 3 ) -> ( theta ` k ) = ( theta ` 3 ) )
93		cht3 16289	. . . . . . . . . . 11 |- ( theta ` 3 ) = ( log ` 6 )
94	92, 93	eqtrdi 2287	. . . . . . . . . 10 |- ( k e. ( 3 ... 3 ) -> ( theta ` k ) = ( log ` 6 ) )
95	91	oveq2d 6104	. . . . . . . . . . . . . 14 |- ( k e. ( 3 ... 3 ) -> ( 2 x. k ) = ( 2 x. 3 ) )
96	95	oveq1d 6103	. . . . . . . . . . . . 13 |- ( k e. ( 3 ... 3 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. 3 ) - 3 ) )
97		3cn 9389	. . . . . . . . . . . . . 14 |- 3 e. CC
98	97	2timesi 9444	. . . . . . . . . . . . . 14 |- ( 2 x. 3 ) = ( 3 + 3 )
99	97, 97, 98	mvrraddi 8551	. . . . . . . . . . . . 13 |- ( ( 2 x. 3 ) - 3 ) = 3
100	96, 99	eqtrdi 2287	. . . . . . . . . . . 12 |- ( k e. ( 3 ... 3 ) -> ( ( 2 x. k ) - 3 ) = 3 )
101	100	oveq2d 6104	. . . . . . . . . . 11 |- ( k e. ( 3 ... 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. 3 ) )
102		2rp 10077	. . . . . . . . . . . . . . . 16 |- 2 e. RR+
103		relogcl 16103	. . . . . . . . . . . . . . . 16 |- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
104	102, 103	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( log ` 2 ) e. RR
105	104	recni 8345	. . . . . . . . . . . . . 14 |- ( log ` 2 ) e. CC
106	105, 97	mulcomi 8339	. . . . . . . . . . . . 13 |- ( ( log ` 2 ) x. 3 ) = ( 3 x. ( log ` 2 ) )
107		3z 9685	. . . . . . . . . . . . . 14 |- 3 e. ZZ
108		relogexp 16114	. . . . . . . . . . . . . 14 |- ( ( 2 e. RR+ /\ 3 e. ZZ ) -> ( log ` ( 2 ^ 3 ) ) = ( 3 x. ( log ` 2 ) ) )
109	102, 107, 108	mp2an 430	. . . . . . . . . . . . 13 |- ( log ` ( 2 ^ 3 ) ) = ( 3 x. ( log ` 2 ) )
110	106, 109	eqtr4i 2262	. . . . . . . . . . . 12 |- ( ( log ` 2 ) x. 3 ) = ( log ` ( 2 ^ 3 ) )
111		cu2 11097	. . . . . . . . . . . . 13 |- ( 2 ^ 3 ) = 8
112	111	fveq2i 5701	. . . . . . . . . . . 12 |- ( log ` ( 2 ^ 3 ) ) = ( log ` 8 )
113	110, 112	eqtri 2259	. . . . . . . . . . 11 |- ( ( log ` 2 ) x. 3 ) = ( log ` 8 )
114	101, 113	eqtrdi 2287	. . . . . . . . . 10 |- ( k e. ( 3 ... 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( log ` 8 ) )
115	90, 94, 114	3brtr4d 4163	. . . . . . . . 9 |- ( k e. ( 3 ... 3 ) -> ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
116	115	rgen 2603	. . . . . . . 8 |- A. k e. ( 3 ... 3 ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) )
117		df-2 9373	. . . . . . . . . . . . . . . . . . 19 |- 2 = ( 1 + 1 )
118		2div2e1 9447	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 2 ) = 1
119		eluzle 9951	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. ( ZZ>= ` 3 ) -> 3 <_ n )
120	64, 119	eqbrtrrid 4167	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) <_ n )
121		2z 9684	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 e. ZZ
122		eluzelz 9948	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. ( ZZ>= ` 3 ) -> n e. ZZ )
123		zltp1le 9711	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 < n <-> ( 2 + 1 ) <_ n ) )
124	121, 122, 123	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 < n <-> ( 2 + 1 ) <_ n ) )
125	120, 124	mpbird 167	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 3 ) -> 2 < n )
126		eluzelre 9949	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( ZZ>= ` 3 ) -> n e. RR )
127		ltdiv1 9207	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 2 e. RR /\ n e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 2 < n <-> ( 2 / 2 ) < ( n / 2 ) ) )
128	1, 24, 127	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. RR -> ( 2 < n <-> ( 2 / 2 ) < ( n / 2 ) ) )
129	126, 128	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 < n <-> ( 2 / 2 ) < ( n / 2 ) ) )
130	125, 129	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 / 2 ) < ( n / 2 ) )
131	118, 130	eqbrtrrid 4167	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> 1 < ( n / 2 ) )
132	126	rehalfcld 9564	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. ( ZZ>= ` 3 ) -> ( n / 2 ) e. RR )
133		1re 8332	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. RR
134		ltadd1 8765	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 1 e. RR /\ ( n / 2 ) e. RR /\ 1 e. RR ) -> ( 1 < ( n / 2 ) <-> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) ) )
135	133, 133, 134	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n / 2 ) e. RR -> ( 1 < ( n / 2 ) <-> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) ) )
136	132, 135	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> ( 1 < ( n / 2 ) <-> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) ) )
137	131, 136	mpbid 147	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( 1 + 1 ) < ( ( n / 2 ) + 1 ) )
138	117, 137	eqbrtrid 4166	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> 2 < ( ( n / 2 ) + 1 ) )
139	138	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 2 < ( ( n / 2 ) + 1 ) )
140		peano2z 9692	. . . . . . . . . . . . . . . . . . 19 |- ( ( n / 2 ) e. ZZ -> ( ( n / 2 ) + 1 ) e. ZZ )
141	140	adantl 277	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. ZZ )
142		zltp1le 9711	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. ZZ /\ ( ( n / 2 ) + 1 ) e. ZZ ) -> ( 2 < ( ( n / 2 ) + 1 ) <-> ( 2 + 1 ) <_ ( ( n / 2 ) + 1 ) ) )
143	121, 141, 142	sylancr 418	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 < ( ( n / 2 ) + 1 ) <-> ( 2 + 1 ) <_ ( ( n / 2 ) + 1 ) ) )
144	139, 143	mpbid 147	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 + 1 ) <_ ( ( n / 2 ) + 1 ) )
145	64, 144	eqbrtrid 4166	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 3 <_ ( ( n / 2 ) + 1 ) )
146		1red 8348	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> 1 e. RR )
147		ltle 8420	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 e. RR /\ ( n / 2 ) e. RR ) -> ( 1 < ( n / 2 ) -> 1 <_ ( n / 2 ) ) )
148	133, 132, 147	sylancr 418	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( 1 < ( n / 2 ) -> 1 <_ ( n / 2 ) ) )
149	131, 148	mpd 13	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> 1 <_ ( n / 2 ) )
150	146, 132, 132, 149	leadd2dd 8896	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + 1 ) <_ ( ( n / 2 ) + ( n / 2 ) ) )
151	126	recnd 8361	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> n e. CC )
152	151	2halvesd 9563	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + ( n / 2 ) ) = n )
153	150, 152	breqtrd 4157	. . . . . . . . . . . . . . . 16 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + 1 ) <_ n )
154	153	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) <_ n )
155		elfz 10435	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( n / 2 ) + 1 ) e. ZZ /\ 3 e. ZZ /\ n e. ZZ ) -> ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) <-> ( 3 <_ ( ( n / 2 ) + 1 ) /\ ( ( n / 2 ) + 1 ) <_ n ) ) )
156	107, 155	mp3an2 1366	. . . . . . . . . . . . . . . 16 |- ( ( ( ( n / 2 ) + 1 ) e. ZZ /\ n e. ZZ ) -> ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) <-> ( 3 <_ ( ( n / 2 ) + 1 ) /\ ( ( n / 2 ) + 1 ) <_ n ) ) )
157	140, 122, 156	syl2anr 290	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) <-> ( 3 <_ ( ( n / 2 ) + 1 ) /\ ( ( n / 2 ) + 1 ) <_ n ) ) )
158	145, 154, 157	mpbir2and 957	. . . . . . . . . . . . . 14 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. ( 3 ... n ) )
159		fveq2 5698	. . . . . . . . . . . . . . . 16 |- ( k = ( ( n / 2 ) + 1 ) -> ( theta ` k ) = ( theta ` ( ( n / 2 ) + 1 ) ) )
160		oveq2 6096	. . . . . . . . . . . . . . . . . 18 |- ( k = ( ( n / 2 ) + 1 ) -> ( 2 x. k ) = ( 2 x. ( ( n / 2 ) + 1 ) ) )
161	160	oveq1d 6103	. . . . . . . . . . . . . . . . 17 |- ( k = ( ( n / 2 ) + 1 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) )
162	161	oveq2d 6104	. . . . . . . . . . . . . . . 16 |- ( k = ( ( n / 2 ) + 1 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) )
163	159, 162	breq12d 4144	. . . . . . . . . . . . . . 15 |- ( k = ( ( n / 2 ) + 1 ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) ) )
164	163	rspcv 2925	. . . . . . . . . . . . . 14 |- ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) ) )
165	158, 164	syl 14	. . . . . . . . . . . . 13 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) ) )
166	132	recnd 8361	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 3 ) -> ( n / 2 ) e. CC )
167	166	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n / 2 ) e. CC )
168		2cn 9385	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. CC
169		ax-1cn 8279	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
170		adddi 8318	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. CC /\ ( n / 2 ) e. CC /\ 1 e. CC ) -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) )
171	168, 169, 170	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n / 2 ) e. CC -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) )
172	167, 171	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) )
173	151	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> n e. CC )
174		id 19	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. CC -> n e. CC )
175		2cnd 9387	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. CC -> 2 e. CC )
176		2ap0 9407	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 # 0
177	176	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. CC -> 2 # 0 )
178	174, 175, 177	divcanap2d 9131	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. CC -> ( 2 x. ( n / 2 ) ) = n )
179	173, 178	syl 14	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( n / 2 ) ) = n )
180	168	mulridi 8335	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 2 x. 1 ) = 2
181	180	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. 1 ) = 2 )
182	179, 181	oveq12d 6106	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n / 2 ) ) + ( 2 x. 1 ) ) = ( n + 2 ) )
183	172, 182	eqtrd 2271	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( ( n / 2 ) + 1 ) ) = ( n + 2 ) )
184	183	oveq1d 6103	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) = ( ( n + 2 ) - 3 ) )
185		subsub3 8566	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. CC /\ 3 e. CC /\ 2 e. CC ) -> ( n - ( 3 - 2 ) ) = ( ( n + 2 ) - 3 ) )
186	97, 168, 185	mp3an23 1370	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. CC -> ( n - ( 3 - 2 ) ) = ( ( n + 2 ) - 3 ) )
187	173, 186	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - ( 3 - 2 ) ) = ( ( n + 2 ) - 3 ) )
188		2p1e3 9448	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 + 1 ) = 3
189	97, 168, 169, 188	subaddrii 8623	. . . . . . . . . . . . . . . . . . . 20 |- ( 3 - 2 ) = 1
190	189	oveq2i 6099	. . . . . . . . . . . . . . . . . . 19 |- ( n - ( 3 - 2 ) ) = ( n - 1 )
191	187, 190	eqtr3di 2286	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + 2 ) - 3 ) = ( n - 1 ) )
192	184, 191	eqtrd 2271	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) = ( n - 1 ) )
193	192	oveq2d 6104	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) = ( ( log ` 2 ) x. ( n - 1 ) ) )
194	193	breq2d 4143	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) <-> ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( n - 1 ) ) ) )
195		zq 10043	. . . . . . . . . . . . . . . . . 18 |- ( ( ( n / 2 ) + 1 ) e. ZZ -> ( ( n / 2 ) + 1 ) e. QQ )
196	141, 195	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. QQ )
197		chtqcl 16256	. . . . . . . . . . . . . . . . 17 |- ( ( ( n / 2 ) + 1 ) e. QQ -> ( theta ` ( ( n / 2 ) + 1 ) ) e. RR )
198	196, 197	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( n / 2 ) + 1 ) ) e. RR )
199	126	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> n e. RR )
200		peano2rem 8601	. . . . . . . . . . . . . . . . . 18 |- ( n e. RR -> ( n - 1 ) e. RR )
201	199, 200	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - 1 ) e. RR )
202		remulcl 8314	. . . . . . . . . . . . . . . . 17 |- ( ( ( log ` 2 ) e. RR /\ ( n - 1 ) e. RR ) -> ( ( log ` 2 ) x. ( n - 1 ) ) e. RR )
203	104, 201, 202	sylancr 418	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( n - 1 ) ) e. RR )
204		remulcl 8314	. . . . . . . . . . . . . . . . 17 |- ( ( ( log ` 2 ) e. RR /\ n e. RR ) -> ( ( log ` 2 ) x. n ) e. RR )
205	104, 199, 204	sylancr 418	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. n ) e. RR )
206	198, 203, 205	ltadd1d 8874	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( n - 1 ) ) <-> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) ) )
207	105	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( log ` 2 ) e. CC )
208	201	recnd 8361	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - 1 ) e. CC )
209	207, 208, 173	adddid 8357	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( n - 1 ) + n ) ) = ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) )
210		adddi 8318	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 e. CC /\ n e. CC /\ 1 e. CC ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
211	168, 169, 210	mp3an13 1369	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. CC -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
212	173, 211	syl 14	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
213	180	oveq2i 6099	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 x. n ) + ( 2 x. 1 ) ) = ( ( 2 x. n ) + 2 )
214	212, 213	eqtrdi 2287	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + 2 ) )
215	214	oveq1d 6103	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
216		zmulcl 9710	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
217	121, 122, 216	sylancr 418	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) e. ZZ )
218	217	zcnd 9781	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) e. CC )
219	218	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. n ) e. CC )
220		subsub3 8566	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2 x. n ) e. CC /\ 3 e. CC /\ 2 e. CC ) -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
221	97, 168, 220	mp3an23 1370	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. n ) e. CC -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
222	219, 221	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
223	189	oveq2i 6099	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( 2 x. n ) - 1 )
224	173	2timesd 9560	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. n ) = ( n + n ) )
225	224	oveq1d 6103	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - 1 ) = ( ( n + n ) - 1 ) )
226	169	a1i 9	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 1 e. CC )
227	173, 173, 226	addsubd 8666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + n ) - 1 ) = ( ( n - 1 ) + n ) )
228	225, 227	eqtrd 2271	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - 1 ) = ( ( n - 1 ) + n ) )
229	223, 228	eqtrid 2283	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( n - 1 ) + n ) )
230	215, 222, 229	3eqtr2rd 2278	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n - 1 ) + n ) = ( ( 2 x. ( n + 1 ) ) - 3 ) )
231	230	oveq2d 6104	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( n - 1 ) + n ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
232	209, 231	eqtr3d 2273	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
233	232	breq2d 4143	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( ( log ` 2 ) x. ( n - 1 ) ) + ( ( log ` 2 ) x. n ) ) <-> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
234	194, 206, 233	3bitrd 214	. . . . . . . . . . . . . 14 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) <-> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
235		3nn 9479	. . . . . . . . . . . . . . . . . 18 |- 3 e. NN
236		elfzuz 10442	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( n / 2 ) + 1 ) e. ( 3 ... n ) -> ( ( n / 2 ) + 1 ) e. ( ZZ>= ` 3 ) )
237	158, 236	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. ( ZZ>= ` 3 ) )
238		eluznn 10017	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 e. NN /\ ( ( n / 2 ) + 1 ) e. ( ZZ>= ` 3 ) ) -> ( ( n / 2 ) + 1 ) e. NN )
239	235, 237, 238	sylancr 418	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n / 2 ) + 1 ) e. NN )
240		chtublem 16307	. . . . . . . . . . . . . . . . 17 |- ( ( ( n / 2 ) + 1 ) e. NN -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) ) )
241	239, 240	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) ) )
242	183	oveq1d 6103	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) = ( ( n + 2 ) - 1 ) )
243		addsubass 8544	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( n + 2 ) - 1 ) = ( n + ( 2 - 1 ) ) )
244	168, 169, 243	mp3an23 1370	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. CC -> ( ( n + 2 ) - 1 ) = ( n + ( 2 - 1 ) ) )
245	173, 244	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + 2 ) - 1 ) = ( n + ( 2 - 1 ) ) )
246		2m1e1 9432	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 - 1 ) = 1
247	246	oveq2i 6099	. . . . . . . . . . . . . . . . . . 19 |- ( n + ( 2 - 1 ) ) = ( n + 1 )
248	245, 247	eqtrdi 2287	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( n + 2 ) - 1 ) = ( n + 1 ) )
249	242, 248	eqtrd 2271	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) = ( n + 1 ) )
250	249	fveq2d 5702	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) = ( theta ` ( n + 1 ) ) )
251		pncan 8540	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( n / 2 ) e. CC /\ 1 e. CC ) -> ( ( ( n / 2 ) + 1 ) - 1 ) = ( n / 2 ) )
252	167, 169, 251	sylancl 417	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( n / 2 ) + 1 ) - 1 ) = ( n / 2 ) )
253	252	oveq2d 6104	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) = ( ( log ` 4 ) x. ( n / 2 ) ) )
254		relogexp 16114	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. RR+ /\ 2 e. ZZ ) -> ( log ` ( 2 ^ 2 ) ) = ( 2 x. ( log ` 2 ) ) )
255	102, 121, 254	mp2an 430	. . . . . . . . . . . . . . . . . . . . 21 |- ( log ` ( 2 ^ 2 ) ) = ( 2 x. ( log ` 2 ) )
256		sq2 11094	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 2 ^ 2 ) = 4
257	256	fveq2i 5701	. . . . . . . . . . . . . . . . . . . . 21 |- ( log ` ( 2 ^ 2 ) ) = ( log ` 4 )
258	168, 105	mulcomi 8339	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 x. ( log ` 2 ) ) = ( ( log ` 2 ) x. 2 )
259	255, 257, 258	3eqtr3i 2267	. . . . . . . . . . . . . . . . . . . 20 |- ( log ` 4 ) = ( ( log ` 2 ) x. 2 )
260	259	oveq1i 6098	. . . . . . . . . . . . . . . . . . 19 |- ( ( log ` 4 ) x. ( n / 2 ) ) = ( ( ( log ` 2 ) x. 2 ) x. ( n / 2 ) )
261		2cnd 9387	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 2 e. CC )
262	207, 261, 167	mulassd 8356	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( log ` 2 ) x. 2 ) x. ( n / 2 ) ) = ( ( log ` 2 ) x. ( 2 x. ( n / 2 ) ) ) )
263	260, 262	eqtrid 2283	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( n / 2 ) ) = ( ( log ` 2 ) x. ( 2 x. ( n / 2 ) ) ) )
264	179	oveq2d 6104	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( 2 x. ( n / 2 ) ) ) = ( ( log ` 2 ) x. n ) )
265	253, 263, 264	3eqtrd 2275	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) = ( ( log ` 2 ) x. n ) )
266	265	oveq2d 6104	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) ) = ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) )
267	241, 250, 266	3brtr3d 4162	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) )
268		peano2uz 10000	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ( ZZ>= ` 3 ) )
269		eluzelz 9948	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n + 1 ) e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ZZ )
270	268, 269	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ZZ )
271		zq 10043	. . . . . . . . . . . . . . . . . . 19 |- ( ( n + 1 ) e. ZZ -> ( n + 1 ) e. QQ )
272	270, 271	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. QQ )
273	272	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n + 1 ) e. QQ )
274		chtqcl 16256	. . . . . . . . . . . . . . . . 17 |- ( ( n + 1 ) e. QQ -> ( theta ` ( n + 1 ) ) e. RR )
275	273, 274	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) e. RR )
276	198, 205	readdcld 8362	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) e. RR )
277		zmulcl 9710	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. ZZ /\ ( n + 1 ) e. ZZ ) -> ( 2 x. ( n + 1 ) ) e. ZZ )
278	121, 270, 277	sylancr 418	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. ( n + 1 ) ) e. ZZ )
279	278	zred 9780	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. ( n + 1 ) ) e. RR )
280		resubcl 8598	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 2 x. ( n + 1 ) ) e. RR /\ 3 e. RR ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR )
281	279, 30, 280	sylancl 417	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR )
282	281	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR )
283		remulcl 8314	. . . . . . . . . . . . . . . . 17 |- ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR )
284	104, 282, 283	sylancr 418	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR )
285		lelttr 8421	. . . . . . . . . . . . . . . 16 |- ( ( ( theta ` ( n + 1 ) ) e. RR /\ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR ) -> ( ( ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) /\ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
286	275, 276, 284, 285	syl3anc 1278	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) /\ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
287	267, 286	mpand 433	. . . . . . . . . . . . . 14 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
288	234, 287	sylbid 150	. . . . . . . . . . . . 13 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
289	165, 288	syld 45	. . . . . . . . . . . 12 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
290		eluzfz2 10454	. . . . . . . . . . . . . . 15 |- ( n e. ( ZZ>= ` 3 ) -> n e. ( 3 ... n ) )
291		fveq2 5698	. . . . . . . . . . . . . . . . 17 |- ( k = n -> ( theta ` k ) = ( theta ` n ) )
292		oveq2 6096	. . . . . . . . . . . . . . . . . . 19 |- ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
293	292	oveq1d 6103	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. n ) - 3 ) )
294	293	oveq2d 6104	. . . . . . . . . . . . . . . . 17 |- ( k = n -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) )
295	291, 294	breq12d 4144	. . . . . . . . . . . . . . . 16 |- ( k = n -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
296	295	rspcv 2925	. . . . . . . . . . . . . . 15 |- ( n e. ( 3 ... n ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
297	290, 296	syl 14	. . . . . . . . . . . . . 14 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
298	297	adantr 276	. . . . . . . . . . . . 13 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) ) )
299	217	zred 9780	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) e. RR )
300	30	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> 3 e. RR )
301	126	ltp1d 9269	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> n < ( n + 1 ) )
302	270	zred 9780	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. RR )
303	24	a1i 9	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 e. RR /\ 0 < 2 ) )
304		ltmul2 9195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. RR /\ ( n + 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( n < ( n + 1 ) <-> ( 2 x. n ) < ( 2 x. ( n + 1 ) ) ) )
305	126, 302, 303, 304	syl3anc 1278	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( n < ( n + 1 ) <-> ( 2 x. n ) < ( 2 x. ( n + 1 ) ) ) )
306	301, 305	mpbid 147	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. n ) < ( 2 x. ( n + 1 ) ) )
307	299, 279, 300, 306	ltsub1dd 8893	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) )
308		resubcl 8598	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 2 x. n ) e. RR /\ 3 e. RR ) -> ( ( 2 x. n ) - 3 ) e. RR )
309	299, 30, 308	sylancl 417	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. n ) - 3 ) e. RR )
310	6	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
311		ltmul2 9195	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 2 x. n ) - 3 ) e. RR /\ ( ( 2 x. ( n + 1 ) ) - 3 ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
312	309, 281, 310, 311	syl3anc 1278	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
313	307, 312	mpbid 147	. . . . . . . . . . . . . . . 16 |- ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
314		zq 10043	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ZZ -> n e. QQ )
315	122, 314	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> n e. QQ )
316		chtqcl 16256	. . . . . . . . . . . . . . . . . 18 |- ( n e. QQ -> ( theta ` n ) e. RR )
317	315, 316	syl 14	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( theta ` n ) e. RR )
318		remulcl 8314	. . . . . . . . . . . . . . . . . 18 |- ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. n ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) e. RR )
319	104, 309, 318	sylancr 418	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) e. RR )
320	104, 281, 283	sylancr 418	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR )
321		lttr 8406	. . . . . . . . . . . . . . . . 17 |- ( ( ( theta ` n ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) e. RR ) -> ( ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) /\ ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
322	317, 319, 320, 321	syl3anc 1278	. . . . . . . . . . . . . . . 16 |- ( n e. ( ZZ>= ` 3 ) -> ( ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) /\ ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
323	313, 322	mpan2d 432	. . . . . . . . . . . . . . 15 |- ( n e. ( ZZ>= ` 3 ) -> ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
324	323	adantr 276	. . . . . . . . . . . . . 14 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) -> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
325		evend2 12682	. . . . . . . . . . . . . . . . . . 19 |- ( ( n + 1 ) e. ZZ -> ( 2 || ( n + 1 ) <-> ( ( n + 1 ) / 2 ) e. ZZ ) )
326	270, 325	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 || ( n + 1 ) <-> ( ( n + 1 ) / 2 ) e. ZZ ) )
327		2lt3 9487	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 < 3
328		zltnle 9702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 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 4135	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 2 = ( n + 1 ) -> ( 3 <_ 2 <-> 3 <_ ( n + 1 ) ) )
332	330, 331	mtbii 685	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 = ( n + 1 ) -> -. 3 <_ ( n + 1 ) )
333		eluzle 9951	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( n + 1 ) e. ( ZZ>= ` 3 ) -> 3 <_ ( n + 1 ) )
334	268, 333	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( ZZ>= ` 3 ) -> 3 <_ ( n + 1 ) )
335	332, 334	nsyl3 635	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 3 ) -> -. 2 = ( n + 1 ) )
336	335	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> -. 2 = ( n + 1 ) )
337		uzid 9953	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
338	121, 337	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. ( ZZ>= ` 2 )
339		simpr 110	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> ( n + 1 ) e. Prime )
340		dvdsprm 12942	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. ( ZZ>= ` 2 ) /\ ( n + 1 ) e. Prime ) -> ( 2 || ( n + 1 ) <-> 2 = ( n + 1 ) ) )
341	338, 339, 340	sylancr 418	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> ( 2 || ( n + 1 ) <-> 2 = ( n + 1 ) ) )
342	336, 341	mtbird 684	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n + 1 ) e. Prime ) -> -. 2 || ( n + 1 ) )
343	342	ex 115	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n + 1 ) e. Prime -> -. 2 || ( n + 1 ) ) )
344	343	con2d 633	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 || ( n + 1 ) -> -. ( n + 1 ) e. Prime ) )
345	326, 344	sylbird 170	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( ( n + 1 ) / 2 ) e. ZZ -> -. ( n + 1 ) e. Prime ) )
346	345	imp 124	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> -. ( n + 1 ) e. Prime )
347		chtnprm 16274	. . . . . . . . . . . . . . . 16 |- ( ( n e. ZZ /\ -. ( n + 1 ) e. Prime ) -> ( theta ` ( n + 1 ) ) = ( theta ` n ) )
348	122, 346, 347	syl2an2r 603	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) = ( theta ` n ) )
349	348	breq1d 4141	. . . . . . . . . . . . . 14 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) <-> ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
350	324, 349	sylibrd 169	. . . . . . . . . . . . 13 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( ( theta ` n ) < ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
351	298, 350	syld 45	. . . . . . . . . . . 12 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( ( n + 1 ) / 2 ) e. ZZ ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
352		zeo 9763	. . . . . . . . . . . . 13 |- ( n e. ZZ -> ( ( n / 2 ) e. ZZ \/ ( ( n + 1 ) / 2 ) e. ZZ ) )
353	122, 352	syl 14	. . . . . . . . . . . 12 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) e. ZZ \/ ( ( n + 1 ) / 2 ) e. ZZ ) )
354	289, 351, 353	mpjaodan 810	. . . . . . . . . . 11 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
355	122	peano2zd 9783	. . . . . . . . . . . 12 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ZZ )
356		fveq2 5698	. . . . . . . . . . . . . 14 |- ( k = ( n + 1 ) -> ( theta ` k ) = ( theta ` ( n + 1 ) ) )
357		oveq2 6096	. . . . . . . . . . . . . . . 16 |- ( k = ( n + 1 ) -> ( 2 x. k ) = ( 2 x. ( n + 1 ) ) )
358	357	oveq1d 6103	. . . . . . . . . . . . . . 15 |- ( k = ( n + 1 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( n + 1 ) ) - 3 ) )
359	358	oveq2d 6104	. . . . . . . . . . . . . 14 |- ( k = ( n + 1 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
360	356, 359	breq12d 4144	. . . . . . . . . . . . 13 |- ( k = ( n + 1 ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
361	360	ralsng 3749	. . . . . . . . . . . 12 |- ( ( n + 1 ) e. ZZ -> ( A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
362	355, 361	syl 14	. . . . . . . . . . 11 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( n + 1 ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) ) )
363	354, 362	sylibrd 169	. . . . . . . . . 10 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
364	363	ancld 325	. . . . . . . . 9 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) /\ A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) ) )
365		ralun 3411	. . . . . . . . . 10 |- ( ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) /\ A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) -> A. k e. ( ( 3 ... n ) u. { ( n + 1 ) } ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
366		fzsuc 10493	. . . . . . . . . . 11 |- ( n e. ( ZZ>= ` 3 ) -> ( 3 ... ( n + 1 ) ) = ( ( 3 ... n ) u. { ( n + 1 ) } ) )
367	366	raleqdv 2755	. . . . . . . . . 10 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> A. k e. ( ( 3 ... n ) u. { ( n + 1 ) } ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
368	365, 367	imbitrrid 156	. . . . . . . . 9 |- ( n e. ( ZZ>= ` 3 ) -> ( ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) /\ A. k e. { ( n + 1 ) } ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) -> A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
369	364, 368	syld 45	. . . . . . . 8 |- ( n e. ( ZZ>= ` 3 ) -> ( A. k e. ( 3 ... n ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) -> A. k e. ( 3 ... ( n + 1 ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) ) )
370	73, 75, 77, 79, 116, 369	uzind4i 10009	. . . . . . 7 |- ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> A. k e. ( 3 ... ( |_ ` N ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
371		eluzfz2 10454	. . . . . . 7 |- ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> ( |_ ` N ) e. ( 3 ... ( |_ ` N ) ) )
372	71, 370, 371	rspcdva 2934	. . . . . 6 |- ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
373	66, 372	syl 14	. . . . 5 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
374	17, 373	sylanl1 406	. . . 4 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
375	62, 374	eqbrtrrd 4155	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
376	34	adantr 276	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. N ) e. RR )
377	17, 376	sylanl1 406	. . . . 5 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. N ) e. RR )
378	30	a1i 9	. . . . 5 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> 3 e. RR )
379		flqle 10733	. . . . . . 7 |- ( N e. QQ -> ( |_ ` N ) <_ N )
380	379	ad2antrr 492	. . . . . 6 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( |_ ` N ) <_ N )
381	17	ad2antrr 492	. . . . . . 7 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> N e. RR )
382	24	a1i 9	. . . . . . 7 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 e. RR /\ 0 < 2 ) )
383		lemul2 9196	. . . . . . 7 |- ( ( ( |_ ` N ) e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( |_ ` N ) <_ N <-> ( 2 x. ( |_ ` N ) ) <_ ( 2 x. N ) ) )
384	51, 381, 382, 383	syl3anc 1278	. . . . . 6 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( |_ ` N ) <_ N <-> ( 2 x. ( |_ ` N ) ) <_ ( 2 x. N ) ) )
385	380, 384	mpbid 147	. . . . 5 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( 2 x. ( |_ ` N ) ) <_ ( 2 x. N ) )
386	53, 377, 378, 385	lesub1dd 8897	. . . 4 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. ( |_ ` N ) ) - 3 ) <_ ( ( 2 x. N ) - 3 ) )
387	17, 58	sylanl1 406	. . . . 5 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( 2 x. N ) - 3 ) e. RR )
388	6	a1i 9	. . . . 5 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
389		lemul2 9196	. . . . 5 |- ( ( ( ( 2 x. ( |_ ` N ) ) - 3 ) e. RR /\ ( ( 2 x. N ) - 3 ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( ( ( 2 x. ( |_ ` N ) ) - 3 ) <_ ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) <_ ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
390	55, 387, 388, 389	syl3anc 1278	. . . 4 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( ( 2 x. ( |_ ` N ) ) - 3 ) <_ ( ( 2 x. N ) - 3 ) <-> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) <_ ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) ) )
391	386, 390	mpbid 147	. . 3 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) <_ ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
392	48, 57, 61, 375, 391	ltletrd 8759	. 2 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
393	121	a1i 9	. . . 4 |- ( ( N e. QQ /\ 2 < N ) -> 2 e. ZZ )
394	49	adantr 276	. . . 4 |- ( ( N e. QQ /\ 2 < N ) -> ( |_ ` N ) e. ZZ )
395		ltle 8420	. . . . . . 7 |- ( ( 2 e. RR /\ N e. RR ) -> ( 2 < N -> 2 <_ N ) )
396	1, 17, 395	sylancr 418	. . . . . 6 |- ( N e. QQ -> ( 2 < N -> 2 <_ N ) )
397		flqge 10737	. . . . . . 7 |- ( ( N e. QQ /\ 2 e. ZZ ) -> ( 2 <_ N <-> 2 <_ ( |_ ` N ) ) )
398	121, 397	mpan2 429	. . . . . 6 |- ( N e. QQ -> ( 2 <_ N <-> 2 <_ ( |_ ` N ) ) )
399	396, 398	sylibd 149	. . . . 5 |- ( N e. QQ -> ( 2 < N -> 2 <_ ( |_ ` N ) ) )
400	399	imp 124	. . . 4 |- ( ( N e. QQ /\ 2 < N ) -> 2 <_ ( |_ ` N ) )
401		eluz2 9944	. . . 4 |- ( ( |_ ` N ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( |_ ` N ) e. ZZ /\ 2 <_ ( |_ ` N ) ) )
402	393, 394, 400, 401	syl3anbrc 1212	. . 3 |- ( ( N e. QQ /\ 2 < N ) -> ( |_ ` N ) e. ( ZZ>= ` 2 ) )
403		uzp1 9973	. . 3 |- ( ( |_ ` N ) e. ( ZZ>= ` 2 ) -> ( ( |_ ` N ) = 2 \/ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) )
404	402, 403	syl 14	. 2 |- ( ( N e. QQ /\ 2 < N ) -> ( ( |_ ` N ) = 2 \/ ( |_ ` N ) e. ( ZZ>= ` ( 2 + 1 ) ) ) )
405	46, 392, 404	mpjaodan 810	1 |- ( ( N e. QQ /\ 2 < N ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720   = wceq 1402   e. wcel 2209   A.wral 2528   u. cun 3218   {csn 3709   class class class wbr 4131   ` cfv 5380  (class class class)co 6088   CCcc 8184   RRcr 8185   0cc0 8186   1c1 8187   + caddc 8189   x. cmul 8191   < clt 8367   <_ cle 8368   - cmin 8505   # cap 8918   / cdiv 9011   NNcn 9314   2c2 9365   3c3 9366   4c4 9367   6c6 9369   8c8 9371   ZZcz 9656   ZZ>=cuz 9938   QQcq 10036   RR+crp 10072   ...cfz 10429   |_cfl 10721   ^cexp 10997   || cdvds 12580   Primecprime 12911   logclog 16097   thetaccht 16245

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 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-mulrcl 8285  ax-addcom 8286  ax-mulcom 8287  ax-addass 8288  ax-mulass 8289  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-1rid 8293  ax-0id 8294  ax-rnegex 8295  ax-precex 8296  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-ltwlin 8299  ax-pre-lttrn 8300  ax-pre-apti 8301  ax-pre-ltadd 8302  ax-pre-mulgt0 8303  ax-pre-mulext 8304  ax-arch 8305  ax-caucvg 8306  ax-pre-suploc 8307  ax-addf 8308  ax-mulf 8309

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 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-po 4443  df-iso 4444  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-isom 5389  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-of 6305  df-1st 6378  df-2nd 6379  df-recs 6580  df-irdg 6645  df-frec 6666  df-1o 6691  df-2o 6692  df-oadd 6695  df-er 6811  df-map 6928  df-pm 6929  df-en 7028  df-dom 7029  df-fin 7030  df-sup 7331  df-inf 7332  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-sub 8507  df-neg 8508  df-reap 8912  df-ap 8919  df-div 9012  df-inn 9315  df-2 9373  df-3 9374  df-4 9375  df-5 9376  df-6 9377  df-7 9378  df-8 9379  df-n0 9576  df-xnn0 9643  df-z 9657  df-uz 9939  df-q 10037  df-rp 10073  df-xneg 10192  df-xadd 10193  df-ioo 10312  df-ico 10314  df-icc 10315  df-fz 10430  df-fzo 10568  df-fl 10723  df-mod 10782  df-seqfrec 10907  df-exp 10998  df-fac 11187  df-bc 11209  df-ihash 11238  df-shft 11603  df-cj 11630  df-re 11631  df-im 11632  df-rsqrt 11787  df-abs 11788  df-clim 12071  df-sumdc 12146  df-ef 12441  df-e 12442  df-dvds 12581  df-gcd 12757  df-prm 12912  df-pc 13094  df-rest 13655  df-topgen 13674  df-psmet 14990  df-xmet 14991  df-met 14992  df-bl 14993  df-mopn 14994  df-top 15236  df-topon 15249  df-bases 15281  df-ntr 15334  df-cn 15426  df-cnp 15427  df-tx 15491  df-cncf 15809  df-limced 15894  df-dvap 15895  df-relog 16099  df-cht 16248

This theorem is used by:  bposlem6  16328