Theorem chtppilim 24369

Description: The theta function is asymptotic to π ( x ) log ( x ), so it is sufficient to prove theta ( x ) / x ~~> r 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014.)

Assertion

Ref	Expression
chtppilim	|- ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) ~~> r 1

Proof of Theorem chtppilim

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		halfre 10862	. . . . . . . . 9 |- ( 1 / 2 ) e. RR
2		1re 9673	. . . . . . . . . 10 |- 1 e. RR
3		rpre 11342	. . . . . . . . . 10 |- ( y e. RR+ -> y e. RR )
4		resubcl 9969	. . . . . . . . . 10 |- ( ( 1 e. RR /\ y e. RR ) -> ( 1 - y ) e. RR )
5	2, 3, 4	sylancr 674	. . . . . . . . 9 |- ( y e. RR+ -> ( 1 - y ) e. RR )
6		ifcl 3935	. . . . . . . . 9 |- ( ( ( 1 / 2 ) e. RR /\ ( 1 - y ) e. RR ) -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR )
7	1, 5, 6	sylancr 674	. . . . . . . 8 |- ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR )
8		0red 9675	. . . . . . . . 9 |- ( y e. RR+ -> 0 e. RR )
9	1	a1i 11	. . . . . . . . 9 |- ( y e. RR+ -> ( 1 / 2 ) e. RR )
10		halfgt0 10864	. . . . . . . . . 10 |- 0 < ( 1 / 2 )
11	10	a1i 11	. . . . . . . . 9 |- ( y e. RR+ -> 0 < ( 1 / 2 ) )
12		max2 11516	. . . . . . . . . 10 |- ( ( ( 1 - y ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( 1 / 2 ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
13	5, 1, 12	sylancl 673	. . . . . . . . 9 |- ( y e. RR+ -> ( 1 / 2 ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
14	8, 9, 7, 11, 13	ltletrd 9826	. . . . . . . 8 |- ( y e. RR+ -> 0 < if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
15	7, 14	elrpd 11372	. . . . . . 7 |- ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR+ )
16	15	rpsqrtcld 13528	. . . . . 6 |- ( y e. RR+ -> ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) e. RR+ )
17		halflt1 10865	. . . . . . . . 9 |- ( 1 / 2 ) < 1
18		ltsubrp 11369	. . . . . . . . . 10 |- ( ( 1 e. RR /\ y e. RR+ ) -> ( 1 - y ) < 1 )
19	2, 18	mpan 681	. . . . . . . . 9 |- ( y e. RR+ -> ( 1 - y ) < 1 )
20		breq1 4421	. . . . . . . . . 10 |- ( ( 1 / 2 ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) -> ( ( 1 / 2 ) < 1 <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 ) )
21		breq1 4421	. . . . . . . . . 10 |- ( ( 1 - y ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) -> ( ( 1 - y ) < 1 <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 ) )
22	20, 21	ifboth 3929	. . . . . . . . 9 |- ( ( ( 1 / 2 ) < 1 /\ ( 1 - y ) < 1 ) -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 )
23	17, 19, 22	sylancr 674	. . . . . . . 8 |- ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 )
24	15	rpge0d 11379	. . . . . . . . 9 |- ( y e. RR+ -> 0 <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
25	2	a1i 11	. . . . . . . . 9 |- ( y e. RR+ -> 1 e. RR )
26		0le1 10170	. . . . . . . . . 10 |- 0 <_ 1
27	26	a1i 11	. . . . . . . . 9 |- ( y e. RR+ -> 0 <_ 1 )
28	7, 24, 25, 27	sqrtltd 13544	. . . . . . . 8 |- ( y e. RR+ -> ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 <-> ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) < ( sqr ` 1 ) ) )
29	23, 28	mpbid 215	. . . . . . 7 |- ( y e. RR+ -> ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) < ( sqr ` 1 ) )
30		sqrt1 13390	. . . . . . 7 |- ( sqr ` 1 ) = 1
31	29, 30	syl6breq 4458	. . . . . 6 |- ( y e. RR+ -> ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) < 1 )
32	16, 31	chtppilimlem2 24368	. . . . 5 |- ( y e. RR+ -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )
33	5	adantr 471	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( 1 - y ) e. RR )
34		max1 11514	. . . . . . . . . . 11 |- ( ( ( 1 - y ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
35	33, 1, 34	sylancl 673	. . . . . . . . . 10 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
36	7	adantr 471	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR )
37		2re 10712	. . . . . . . . . . . . . . . 16 |- 2 e. RR
38		elicopnf 11764	. . . . . . . . . . . . . . . 16 |- ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
39	37, 38	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
40	39	simplbi 466	. . . . . . . . . . . . . 14 |- ( x e. ( 2 [,) +oo ) -> x e. RR )
41		chtcl 24092	. . . . . . . . . . . . . 14 |- ( x e. RR -> ( theta ` x ) e. RR )
42	40, 41	syl 17	. . . . . . . . . . . . 13 |- ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. RR )
43		ppinncl 24157	. . . . . . . . . . . . . . . 16 |- ( ( x e. RR /\ 2 <_ x ) -> (π ` x ) e. NN )
44	39, 43	sylbi 200	. . . . . . . . . . . . . . 15 |- ( x e. ( 2 [,) +oo ) -> (π ` x ) e. NN )
45	44	nnrpd 11373	. . . . . . . . . . . . . 14 |- ( x e. ( 2 [,) +oo ) -> (π ` x ) e. RR+ )
46	2	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. ( 2 [,) +oo ) -> 1 e. RR )
47	37	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. ( 2 [,) +oo ) -> 2 e. RR )
48		1lt2 10810	. . . . . . . . . . . . . . . . 17 |- 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. ( 2 [,) +oo ) -> 1 < 2 )
50	39	simprbi 470	. . . . . . . . . . . . . . . 16 |- ( x e. ( 2 [,) +oo ) -> 2 <_ x )
51	46, 47, 40, 49, 50	ltletrd 9826	. . . . . . . . . . . . . . 15 |- ( x e. ( 2 [,) +oo ) -> 1 < x )
52	40, 51	rplogcld 23634	. . . . . . . . . . . . . 14 |- ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. RR+ )
53	45, 52	rpmulcld 11391	. . . . . . . . . . . . 13 |- ( x e. ( 2 [,) +oo ) -> ( (π ` x ) x. ( log ` x ) ) e. RR+ )
54	42, 53	rerpdivcld 11403	. . . . . . . . . . . 12 |- ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. RR )
55	54	adantl 472	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. RR )
56		lelttr 9755	. . . . . . . . . . 11 |- ( ( ( 1 - y ) e. RR /\ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR /\ ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. RR ) -> ( ( ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) /\ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) -> ( 1 - y ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
57	33, 36, 55, 56	syl3anc 1276	. . . . . . . . . 10 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) /\ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) -> ( 1 - y ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
58	35, 57	mpand 686	. . . . . . . . 9 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) -> ( 1 - y ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
59	7	recnd 9700	. . . . . . . . . . . . . 14 |- ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. CC )
60	59	sqsqrtd 13556	. . . . . . . . . . . . 13 |- ( y e. RR+ -> ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
61	60	adantr 471	. . . . . . . . . . . 12 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
62	61	oveq1d 6335	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) = ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( (π ` x ) x. ( log ` x ) ) ) )
63	62	breq1d 4428	. . . . . . . . . 10 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )
64	42	adantl 472	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) e. RR )
65	53	rpregt0d 11381	. . . . . . . . . . . 12 |- ( x e. ( 2 [,) +oo ) -> ( ( (π ` x ) x. ( log ` x ) ) e. RR /\ 0 < ( (π ` x ) x. ( log ` x ) ) ) )
66	65	adantl 472	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( (π ` x ) x. ( log ` x ) ) e. RR /\ 0 < ( (π ` x ) x. ( log ` x ) ) ) )
67		ltmuldiv 10511	. . . . . . . . . . 11 |- ( ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR /\ ( theta ` x ) e. RR /\ ( ( (π ` x ) x. ( log ` x ) ) e. RR /\ 0 < ( (π ` x ) x. ( log ` x ) ) ) ) -> ( ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
68	36, 64, 66, 67	syl3anc 1276	. . . . . . . . . 10 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
69	63, 68	bitrd 261	. . . . . . . . 9 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
70		0red 9675	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 2 [,) +oo ) -> 0 e. RR )
71		2pos 10734	. . . . . . . . . . . . . . . . . . 19 |- 0 < 2
72	71	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 2 [,) +oo ) -> 0 < 2 )
73	70, 47, 40, 72, 50	ltletrd 9826	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 2 [,) +oo ) -> 0 < x )
74	40, 73	elrpd 11372	. . . . . . . . . . . . . . . 16 |- ( x e. ( 2 [,) +oo ) -> x e. RR+ )
75		chtleppi 24194	. . . . . . . . . . . . . . . 16 |- ( x e. RR+ -> ( theta ` x ) <_ ( (π ` x ) x. ( log ` x ) ) )
76	74, 75	syl 17	. . . . . . . . . . . . . . 15 |- ( x e. ( 2 [,) +oo ) -> ( theta ` x ) <_ ( (π ` x ) x. ( log ` x ) ) )
77	53	rpcnd 11377	. . . . . . . . . . . . . . . 16 |- ( x e. ( 2 [,) +oo ) -> ( (π ` x ) x. ( log ` x ) ) e. CC )
78	77	mulid1d 9691	. . . . . . . . . . . . . . 15 |- ( x e. ( 2 [,) +oo ) -> ( ( (π ` x ) x. ( log ` x ) ) x. 1 ) = ( (π ` x ) x. ( log ` x ) ) )
79	76, 78	breqtrrd 4445	. . . . . . . . . . . . . 14 |- ( x e. ( 2 [,) +oo ) -> ( theta ` x ) <_ ( ( (π ` x ) x. ( log ` x ) ) x. 1 ) )
80	42, 46, 53	ledivmuld 11425	. . . . . . . . . . . . . 14 |- ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) <_ 1 <-> ( theta ` x ) <_ ( ( (π ` x ) x. ( log ` x ) ) x. 1 ) ) )
81	79, 80	mpbird 240	. . . . . . . . . . . . 13 |- ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) <_ 1 )
82	54, 46, 81	abssuble0d 13549	. . . . . . . . . . . 12 |- ( x e. ( 2 [,) +oo ) -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) = ( 1 - ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
83	82	breq1d 4428	. . . . . . . . . . 11 |- ( x e. ( 2 [,) +oo ) -> ( ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y <-> ( 1 - ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) < y ) )
84	83	adantl 472	. . . . . . . . . 10 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y <-> ( 1 - ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) < y ) )
85	2	a1i 11	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> 1 e. RR )
86	3	adantr 471	. . . . . . . . . . 11 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> y e. RR )
87		ltsub23 10127	. . . . . . . . . . 11 |- ( ( 1 e. RR /\ ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. RR /\ y e. RR ) -> ( ( 1 - ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) < y <-> ( 1 - y ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
88	85, 55, 86, 87	syl3anc 1276	. . . . . . . . . 10 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( 1 - ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) < y <-> ( 1 - y ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
89	84, 88	bitrd 261	. . . . . . . . 9 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y <-> ( 1 - y ) < ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) )
90	58, 69, 89	3imtr4d 276	. . . . . . . 8 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) )
91	90	imim2d 54	. . . . . . 7 |- ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( z <_ x -> ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) -> ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
92	91	ralimdva 2808	. . . . . 6 |- ( y e. RR+ -> ( A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) -> A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
93	92	reximdv 2873	. . . . 5 |- ( y e. RR+ -> ( E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( ( sqr ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( (π ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
94	32, 93	mpd 15	. . . 4 |- ( y e. RR+ -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) )
95	94	rgen 2759	. . 3 |- A. y e. RR+ E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y )
96	54	recnd 9700	. . . . . 6 |- ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. CC )
97	96	adantl 472	. . . . 5 |- ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. CC )
98	97	ralrimiva 2814	. . . 4 |- ( T. -> A. x e. ( 2 [,) +oo ) ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) e. CC )
99	40	ssriv 3448	. . . . 5 |- ( 2 [,) +oo ) C_ RR
100	99	a1i 11	. . . 4 |- ( T. -> ( 2 [,) +oo ) C_ RR )
101		1cnd 9690	. . . 4 |- ( T. -> 1 e. CC )
102	98, 100, 101	rlim2 13615	. . 3 |- ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) ~~> r 1 <-> A. y e. RR+ E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
103	95, 102	mpbiri 241	. 2 |- ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) ~~> r 1 )
104	103	trud 1464	1 |- ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( (π ` x ) x. ( log ` x ) ) ) ) ~~> r 1

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   T. wtru 1456   e. wcel 1898   A.wral 2749   E.wrex 2750   C_ wss 3416   ifcif 3893   class class class wbr 4418   |-> cmpt 4477   ` cfv 5605  (class class class)co 6320   CCcc 9568   RRcr 9569   0cc0 9570   1c1 9571   x. cmul 9575   +oocpnf 9703   < clt 9706   <_ cle 9707   - cmin 9891   / cdiv 10302   NNcn 10642   2c2 10692   RR+crp 11336   [,)cico 11671   ^cexp 12310   sqrcsqrt 13351   abscabs 13352   ~~> r crli 13604   logclog 23560   thetaccht 24073  πcppi 24076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648  ax-addf 9649  ax-mulf 9650

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-of 6563  df-om 6725  df-1st 6825  df-2nd 6826  df-supp 6947  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-2o 7214  df-oadd 7217  df-er 7394  df-map 7505  df-pm 7506  df-ixp 7554  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fsupp 7915  df-fi 7956  df-sup 7987  df-inf 7988  df-oi 8056  df-card 8404  df-cda 8629  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-dec 11086  df-uz 11194  df-q 11299  df-rp 11337  df-xneg 11443  df-xadd 11444  df-xmul 11445  df-ioo 11673  df-ioc 11674  df-ico 11675  df-icc 11676  df-fz 11820  df-fzo 11953  df-fl 12066  df-mod 12135  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13185  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-limsup 13581  df-clim 13607  df-rlim 13608  df-o1 13609  df-lo1 13610  df-sum 13808  df-ef 14176  df-e 14177  df-sin 14178  df-cos 14179  df-pi 14181  df-dvds 14361  df-gcd 14524  df-prm 14678  df-pc 14842  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-starv 15260  df-sca 15261  df-vsca 15262  df-ip 15263  df-tset 15264  df-ple 15265  df-ds 15267  df-unif 15268  df-hom 15269  df-cco 15270  df-rest 15376  df-topn 15377  df-0g 15395  df-gsum 15396  df-topgen 15397  df-pt 15398  df-prds 15401  df-xrs 15455  df-qtop 15461  df-imas 15462  df-xps 15465  df-mre 15547  df-mrc 15548  df-acs 15550  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-submnd 16638  df-mulg 16731  df-cntz 17026  df-cmn 17487  df-psmet 19017  df-xmet 19018  df-met 19019  df-bl 19020  df-mopn 19021  df-fbas 19022  df-fg 19023  df-cnfld 19026  df-top 19976  df-bases 19977  df-topon 19978  df-topsp 19979  df-cld 20089  df-ntr 20090  df-cls 20091  df-nei 20169  df-lp 20207  df-perf 20208  df-cn 20298  df-cnp 20299  df-haus 20386  df-tx 20632  df-hmeo 20825  df-fil 20916  df-fm 21008  df-flim 21009  df-flf 21010  df-xms 21390  df-ms 21391  df-tms 21392  df-cncf 21965  df-limc 22877  df-dv 22878  df-log 23562  df-cxp 23563  df-cht 24079  df-ppi 24082

This theorem is referenced by:  chebbnd2  24371  chto1lb  24372  pnt  24508