Theorem chtqub 16262

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 9377	. . . . . . . . . . 11 |- 2 e. RR
2		1lt2 9479	. . . . . . . . . . 11 |- 1 < 2
3		rplogcl 16075	. . . . . . . . . . 11 |- ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
4	1, 2, 3	mp2an 430	. . . . . . . . . 10 |- ( log ` 2 ) e. RR+
5		elrp 10067	. . . . . . . . . 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 8339	. . . . . . 7 |- ( log ` 2 ) e. CC
9	8	mulridi 8329	. . . . . 6 |- ( ( log ` 2 ) x. 1 ) = ( log ` 2 )
10		cht2 16242	. . . . . 6 |- ( theta ` 2 ) = ( log ` 2 )
11	9, 10	eqtr4i 2262	. . . . 5 |- ( ( log ` 2 ) x. 1 ) = ( theta ` 2 )
12		fveq2 5695	. . . . 5 |- ( ( |_ ` N ) = 2 -> ( theta ` ( |_ ` N ) ) = ( theta ` 2 ) )
13	11, 12	eqtr4id 2290	. . . 4 |- ( ( |_ ` N ) = 2 -> ( ( log ` 2 ) x. 1 ) = ( theta ` ( |_ ` N ) ) )
14		chtqfl 16224	. . . . 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 10035	. . . 4 |- ( N e. QQ -> N e. RR )
18		2t2e4 9462	. . . . . . . 8 |- ( 2 x. 2 ) = 4
19		df-4 9368	. . . . . . . 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 9398	. . . . . . . . . . 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 9189	. . . . . . . . 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 4166	. . . . . 6 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( 3 + 1 ) < ( 2 x. N ) )
30		3re 9381	. . . . . . . 8 |- 3 e. RR
31	30	a1i 9	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 3 e. RR )
32		1red 8342	. . . . . . 7 |- ( ( ( N e. RR /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> 1 e. RR )
33		remulcl 8308	. . . . . . . . 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 8876	. . . . . 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 8592	. . . . . . . 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 9189	. . . . . 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 4154	. 2 |- ( ( ( N e. QQ /\ 2 < N ) /\ ( |_ ` N ) = 2 ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
47		chtqcl 16210	. . . 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 10719	. . . . . . . 8 |- ( N e. QQ -> ( |_ ` N ) e. ZZ )
50	49	zred 9773	. . . . . . 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 8308	. . . . . 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 8592	. . . . 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 8308	. . . 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 8308	. . . . 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 9367	. . . . . . . 8 |- 3 = ( 2 + 1 )
65	64	fveq2i 5698	. . . . . . 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 5695	. . . . . . . 8 |- ( k = ( |_ ` N ) -> ( theta ` k ) = ( theta ` ( |_ ` N ) ) )
68		oveq2 6093	. . . . . . . . . 10 |- ( k = ( |_ ` N ) -> ( 2 x. k ) = ( 2 x. ( |_ ` N ) ) )
69	68	oveq1d 6100	. . . . . . . . 9 |- ( k = ( |_ ` N ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( |_ ` N ) ) - 3 ) )
70	69	oveq2d 6101	. . . . . . . 8 |- ( k = ( |_ ` N ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) )
71	67, 70	breq12d 4143	. . . . . . 7 |- ( k = ( |_ ` N ) -> ( ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) <-> ( theta ` ( |_ ` N ) ) < ( ( log ` 2 ) x. ( ( 2 x. ( |_ ` N ) ) - 3 ) ) ) )
72		oveq2 6093	. . . . . . . . 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 6093	. . . . . . . . 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 6093	. . . . . . . . 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 6093	. . . . . . . . 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 9501	. . . . . . . . . . . 12 |- 6 < 8
81		6re 9388	. . . . . . . . . . . . . 14 |- 6 e. RR
82		6pos 9408	. . . . . . . . . . . . . 14 |- 0 < 6
83	81, 82	elrpii 10068	. . . . . . . . . . . . 13 |- 6 e. RR+
84		8re 9392	. . . . . . . . . . . . . 14 |- 8 e. RR
85		8pos 9410	. . . . . . . . . . . . . 14 |- 0 < 8
86	84, 85	elrpii 10068	. . . . . . . . . . . . 13 |- 8 e. RR+
87		logltb 16070	. . . . . . . . . . . . 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 10450	. . . . . . . . . . . 12 |- ( k e. ( 3 ... 3 ) -> k = 3 )
92	91	fveq2d 5699	. . . . . . . . . . 11 |- ( k e. ( 3 ... 3 ) -> ( theta ` k ) = ( theta ` 3 ) )
93		cht3 16243	. . . . . . . . . . 11 |- ( theta ` 3 ) = ( log ` 6 )
94	92, 93	eqtrdi 2287	. . . . . . . . . 10 |- ( k e. ( 3 ... 3 ) -> ( theta ` k ) = ( log ` 6 ) )
95	91	oveq2d 6101	. . . . . . . . . . . . . 14 |- ( k e. ( 3 ... 3 ) -> ( 2 x. k ) = ( 2 x. 3 ) )
96	95	oveq1d 6100	. . . . . . . . . . . . 13 |- ( k e. ( 3 ... 3 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. 3 ) - 3 ) )
97		3cn 9382	. . . . . . . . . . . . . 14 |- 3 e. CC
98	97	2timesi 9437	. . . . . . . . . . . . . 14 |- ( 2 x. 3 ) = ( 3 + 3 )
99	97, 97, 98	mvrraddi 8545	. . . . . . . . . . . . 13 |- ( ( 2 x. 3 ) - 3 ) = 3
100	96, 99	eqtrdi 2287	. . . . . . . . . . . 12 |- ( k e. ( 3 ... 3 ) -> ( ( 2 x. k ) - 3 ) = 3 )
101	100	oveq2d 6101	. . . . . . . . . . 11 |- ( k e. ( 3 ... 3 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. 3 ) )
102		2rp 10070	. . . . . . . . . . . . . . . 16 |- 2 e. RR+
103		relogcl 16057	. . . . . . . . . . . . . . . 16 |- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
104	102, 103	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( log ` 2 ) e. RR
105	104	recni 8339	. . . . . . . . . . . . . 14 |- ( log ` 2 ) e. CC
106	105, 97	mulcomi 8333	. . . . . . . . . . . . 13 |- ( ( log ` 2 ) x. 3 ) = ( 3 x. ( log ` 2 ) )
107		3z 9678	. . . . . . . . . . . . . 14 |- 3 e. ZZ
108		relogexp 16068	. . . . . . . . . . . . . 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 11090	. . . . . . . . . . . . 13 |- ( 2 ^ 3 ) = 8
112	111	fveq2i 5698	. . . . . . . . . . . 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 4162	. . . . . . . . 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 9366	. . . . . . . . . . . . . . . . . . 19 |- 2 = ( 1 + 1 )
118		2div2e1 9440	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 / 2 ) = 1
119		eluzle 9944	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. ( ZZ>= ` 3 ) -> 3 <_ n )
120	64, 119	eqbrtrrid 4166	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) <_ n )
121		2z 9677	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 e. ZZ
122		eluzelz 9941	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. ( ZZ>= ` 3 ) -> n e. ZZ )
123		zltp1le 9704	. . . . . . . . . . . . . . . . . . . . . . . 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 9942	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( ZZ>= ` 3 ) -> n e. RR )
127		ltdiv1 9201	. . . . . . . . . . . . . . . . . . . . . . . 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 4166	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> 1 < ( n / 2 ) )
132	126	rehalfcld 9557	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. ( ZZ>= ` 3 ) -> ( n / 2 ) e. RR )
133		1re 8326	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. RR
134		ltadd1 8759	. . . . . . . . . . . . . . . . . . . . . 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 4165	. . . . . . . . . . . . . . . . . 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 9685	. . . . . . . . . . . . . . . . . . 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 9704	. . . . . . . . . . . . . . . . . 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 4165	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 3 <_ ( ( n / 2 ) + 1 ) )
146		1red 8342	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> 1 e. RR )
147		ltle 8414	. . . . . . . . . . . . . . . . . . . 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 8890	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + 1 ) <_ ( ( n / 2 ) + ( n / 2 ) ) )
151	126	recnd 8355	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> n e. CC )
152	151	2halvesd 9556	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( n / 2 ) + ( n / 2 ) ) = n )
153	150, 152	breqtrd 4156	. . . . . . . . . . . . . . . 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 10428	. . . . . . . . . . . . . . . . 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 5695	. . . . . . . . . . . . . . . 16 |- ( k = ( ( n / 2 ) + 1 ) -> ( theta ` k ) = ( theta ` ( ( n / 2 ) + 1 ) ) )
160		oveq2 6093	. . . . . . . . . . . . . . . . . 18 |- ( k = ( ( n / 2 ) + 1 ) -> ( 2 x. k ) = ( 2 x. ( ( n / 2 ) + 1 ) ) )
161	160	oveq1d 6100	. . . . . . . . . . . . . . . . 17 |- ( k = ( ( n / 2 ) + 1 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) )
162	161	oveq2d 6101	. . . . . . . . . . . . . . . 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 4143	. . . . . . . . . . . . . . 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 8355	. . . . . . . . . . . . . . . . . . . . . 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 9378	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. CC
169		ax-1cn 8273	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
170		adddi 8312	. . . . . . . . . . . . . . . . . . . . . 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 9380	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. CC -> 2 e. CC )
176		2ap0 9400	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 # 0
177	176	a1i 9	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. CC -> 2 # 0 )
178	174, 175, 177	divcanap2d 9125	. . . . . . . . . . . . . . . . . . . . . 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 8329	. . . . . . . . . . . . . . . . . . . . . 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 6103	. . . . . . . . . . . . . . . . . . . 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 6100	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 3 ) = ( ( n + 2 ) - 3 ) )
185		subsub3 8560	. . . . . . . . . . . . . . . . . . . . 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 9441	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2 + 1 ) = 3
189	97, 168, 169, 188	subaddrii 8617	. . . . . . . . . . . . . . . . . . . 20 |- ( 3 - 2 ) = 1
190	189	oveq2i 6096	. . . . . . . . . . . . . . . . . . 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 6101	. . . . . . . . . . . . . . . 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 4142	. . . . . . . . . . . . . . 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 10036	. . . . . . . . . . . . . . . . . 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 16210	. . . . . . . . . . . . . . . . 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 8595	. . . . . . . . . . . . . . . . . 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 8308	. . . . . . . . . . . . . . . . 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 8308	. . . . . . . . . . . . . . . . 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 8868	. . . . . . . . . . . . . . 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 8355	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( n - 1 ) e. CC )
209	207, 208, 173	adddid 8351	. . . . . . . . . . . . . . . . 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 8312	. . . . . . . . . . . . . . . . . . . . . . 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 6096	. . . . . . . . . . . . . . . . . . . . 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 6100	. . . . . . . . . . . . . . . . . . 19 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( n + 1 ) ) - 3 ) = ( ( ( 2 x. n ) + 2 ) - 3 ) )
216		zmulcl 9703	. . . . . . . . . . . . . . . . . . . . . . 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 9774	. . . . . . . . . . . . . . . . . . . . 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 8560	. . . . . . . . . . . . . . . . . . . . 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 6096	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 x. n ) - ( 3 - 2 ) ) = ( ( 2 x. n ) - 1 )
224	173	2timesd 9553	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( 2 x. n ) = ( n + n ) )
225	224	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . 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 8660	. . . . . . . . . . . . . . . . . . . . 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 6101	. . . . . . . . . . . . . . . . 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 4142	. . . . . . . . . . . . . . 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 9472	. . . . . . . . . . . . . . . . . 18 |- 3 e. NN
236		elfzuz 10435	. . . . . . . . . . . . . . . . . . 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 10010	. . . . . . . . . . . . . . . . . 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 16261	. . . . . . . . . . . . . . . . 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 6100	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) = ( ( n + 2 ) - 1 ) )
243		addsubass 8538	. . . . . . . . . . . . . . . . . . . . 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 9425	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 - 1 ) = 1
247	246	oveq2i 6096	. . . . . . . . . . . . . . . . . . 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 5699	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( ( 2 x. ( ( n / 2 ) + 1 ) ) - 1 ) ) = ( theta ` ( n + 1 ) ) )
251		pncan 8534	. . . . . . . . . . . . . . . . . . . 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 6101	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( log ` 4 ) x. ( ( ( n / 2 ) + 1 ) - 1 ) ) = ( ( log ` 4 ) x. ( n / 2 ) ) )
254		relogexp 16068	. . . . . . . . . . . . . . . . . . . . . 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 11087	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 2 ^ 2 ) = 4
257	256	fveq2i 5698	. . . . . . . . . . . . . . . . . . . . 21 |- ( log ` ( 2 ^ 2 ) ) = ( log ` 4 )
258	168, 105	mulcomi 8333	. . . . . . . . . . . . . . . . . . . . 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 6095	. . . . . . . . . . . . . . . . . . 19 |- ( ( log ` 4 ) x. ( n / 2 ) ) = ( ( ( log ` 2 ) x. 2 ) x. ( n / 2 ) )
261		2cnd 9380	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> 2 e. CC )
262	207, 261, 167	mulassd 8350	. . . . . . . . . . . . . . . . . . 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 6101	. . . . . . . . . . . . . . . . . 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 6101	. . . . . . . . . . . . . . . 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 4161	. . . . . . . . . . . . . . 15 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( theta ` ( n + 1 ) ) <_ ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) )
268		peano2uz 9993	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ( ZZ>= ` 3 ) )
269		eluzelz 9941	. . . . . . . . . . . . . . . . . . . 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 10036	. . . . . . . . . . . . . . . . . . 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 16210	. . . . . . . . . . . . . . . . 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 8356	. . . . . . . . . . . . . . . 16 |- ( ( n e. ( ZZ>= ` 3 ) /\ ( n / 2 ) e. ZZ ) -> ( ( theta ` ( ( n / 2 ) + 1 ) ) + ( ( log ` 2 ) x. n ) ) e. RR )
277		zmulcl 9703	. . . . . . . . . . . . . . . . . . . . 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 9773	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> ( 2 x. ( n + 1 ) ) e. RR )
280		resubcl 8592	. . . . . . . . . . . . . . . . . . 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 8308	. . . . . . . . . . . . . . . . 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 8415	. . . . . . . . . . . . . . . 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 10447	. . . . . . . . . . . . . . 15 |- ( n e. ( ZZ>= ` 3 ) -> n e. ( 3 ... n ) )
291		fveq2 5695	. . . . . . . . . . . . . . . . 17 |- ( k = n -> ( theta ` k ) = ( theta ` n ) )
292		oveq2 6093	. . . . . . . . . . . . . . . . . . 19 |- ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
293	292	oveq1d 6100	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. n ) - 3 ) )
294	293	oveq2d 6101	. . . . . . . . . . . . . . . . 17 |- ( k = n -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. n ) - 3 ) ) )
295	291, 294	breq12d 4143	. . . . . . . . . . . . . . . 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 9773	. . . . . . . . . . . . . . . . . 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 9263	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 3 ) -> n < ( n + 1 ) )
302	270	zred 9773	. . . . . . . . . . . . . . . . . . . 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 9189	. . . . . . . . . . . . . . . . . . . 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 8887	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( ( 2 x. n ) - 3 ) < ( ( 2 x. ( n + 1 ) ) - 3 ) )
308		resubcl 8592	. . . . . . . . . . . . . . . . . . 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 9189	. . . . . . . . . . . . . . . . . 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 10036	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ZZ -> n e. QQ )
315	122, 314	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( ZZ>= ` 3 ) -> n e. QQ )
316		chtqcl 16210	. . . . . . . . . . . . . . . . . 18 |- ( n e. QQ -> ( theta ` n ) e. RR )
317	315, 316	syl 14	. . . . . . . . . . . . . . . . 17 |- ( n e. ( ZZ>= ` 3 ) -> ( theta ` n ) e. RR )
318		remulcl 8308	. . . . . . . . . . . . . . . . . 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 8400	. . . . . . . . . . . . . . . . 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 12675	. . . . . . . . . . . . . . . . . . 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 9480	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 < 3
328		zltnle 9695	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4134	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 2 = ( n + 1 ) -> ( 3 <_ 2 <-> 3 <_ ( n + 1 ) ) )
332	330, 331	mtbii 685	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 = ( n + 1 ) -> -. 3 <_ ( n + 1 ) )
333		eluzle 9944	. . . . . . . . . . . . . . . . . . . . . . . 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 9946	. . . . . . . . . . . . . . . . . . . . . . 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 12935	. . . . . . . . . . . . . . . . . . . . . 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 16228	. . . . . . . . . . . . . . . 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 4140	. . . . . . . . . . . . . 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 9756	. . . . . . . . . . . . 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 9776	. . . . . . . . . . . 12 |- ( n e. ( ZZ>= ` 3 ) -> ( n + 1 ) e. ZZ )
356		fveq2 5695	. . . . . . . . . . . . . 14 |- ( k = ( n + 1 ) -> ( theta ` k ) = ( theta ` ( n + 1 ) ) )
357		oveq2 6093	. . . . . . . . . . . . . . . 16 |- ( k = ( n + 1 ) -> ( 2 x. k ) = ( 2 x. ( n + 1 ) ) )
358	357	oveq1d 6100	. . . . . . . . . . . . . . 15 |- ( k = ( n + 1 ) -> ( ( 2 x. k ) - 3 ) = ( ( 2 x. ( n + 1 ) ) - 3 ) )
359	358	oveq2d 6101	. . . . . . . . . . . . . 14 |- ( k = ( n + 1 ) -> ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) = ( ( log ` 2 ) x. ( ( 2 x. ( n + 1 ) ) - 3 ) ) )
360	356, 359	breq12d 4143	. . . . . . . . . . . . 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 10486	. . . . . . . . . . 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 10002	. . . . . . 7 |- ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> A. k e. ( 3 ... ( |_ ` N ) ) ( theta ` k ) < ( ( log ` 2 ) x. ( ( 2 x. k ) - 3 ) ) )
371		eluzfz2 10447	. . . . . . 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 4154	. . 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 10726	. . . . . . 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 9190	. . . . . . 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 8891	. . . 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 9190	. . . . 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 8753	. 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 8414	. . . . . . 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 10730	. . . . . . 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 9937	. . . 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 9966	. . 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 4130   ` cfv 5377  (class class class)co 6085   CCcc 8178   RRcr 8179   0cc0 8180   1c1 8181   + caddc 8183   x. cmul 8185   < clt 8361   <_ cle 8362   - cmin 8499   # cap 8912   / cdiv 9005   NNcn 9307   2c2 9358   3c3 9359   4c4 9360   6c6 9362   8c8 9364   ZZcz 9649   ZZ>=cuz 9931   QQcq 10029   RR+crp 10065   ...cfz 10422   |_cfl 10714   ^cexp 10990   || cdvds 12573   Primecprime 12904   logclog 16051   thetaccht 16199

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 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300  ax-pre-suploc 8301  ax-addf 8302  ax-mulf 8303

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 7325  df-inf 7326  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-5 9369  df-6 9370  df-7 9371  df-8 9372  df-n0 9569  df-xnn0 9636  df-z 9650  df-uz 9932  df-q 10030  df-rp 10066  df-xneg 10185  df-xadd 10186  df-ioo 10305  df-ico 10307  df-icc 10308  df-fz 10423  df-fzo 10561  df-fl 10716  df-mod 10775  df-seqfrec 10900  df-exp 10991  df-fac 11180  df-bc 11202  df-ihash 11231  df-shft 11596  df-cj 11623  df-re 11624  df-im 11625  df-rsqrt 11780  df-abs 11781  df-clim 12064  df-sumdc 12139  df-ef 12434  df-e 12435  df-dvds 12574  df-gcd 12750  df-prm 12905  df-pc 13087  df-rest 13648  df-topgen 13667  df-psmet 14964  df-xmet 14965  df-met 14966  df-bl 14967  df-mopn 14968  df-top 15190  df-topon 15203  df-bases 15235  df-ntr 15288  df-cn 15380  df-cnp 15381  df-tx 15445  df-cncf 15763  df-limced 15848  df-dvap 15849  df-relog 16053  df-cht 16202

This theorem is used by:  bposlem6  16282