Theorem pntlem3 24175

Description: Lemma for pnt 24180. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.)

Hypotheses

Ref	Expression
pntlem3.r	|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
pntlem3.a	|- ( ph -> A e. RR+ )
pntlem3.A	|- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
pntlem3.1	|- T = { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t }
pntlem3.2	|- ( ph -> C e. RR+ )
pntlem3.3	|- ( ( ph /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )

Assertion

Ref	Expression
pntlem3	|- ( ph -> ( x e. RR+ |-> ( (ψ ` x ) / x ) ) ~~> r 1 )

Distinct variable groups:   x, t, y, z, A   u, a, x, y, z   u, C   u, t, R, x, y, z   t, a   u, T, x   ph, t, x, y, u, z

Allowed substitution hints:   ph( a)   A( u, a)   C( x, y, z, t, a)   R( a)   T( y, z, t, a)

Proof of Theorem pntlem3

Dummy variables s w p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpssre 11275	. . . 4 |- RR+ C_ RR
2		eqid 2402	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
3	2	subcn 21662	. . . . . . . . . . . 12 |- - e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) )
4	3	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> - e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) ) )
5		ssid 3461	. . . . . . . . . . . . 13 |- CC C_ CC
6		cncfmptid 21708	. . . . . . . . . . . . 13 |- ( ( CC C_ CC /\ CC C_ CC ) -> ( p e. CC |-> p ) e. ( CC -cn-> CC ) )
7	5, 5, 6	mp2an 670	. . . . . . . . . . . 12 |- ( p e. CC |-> p ) e. ( CC -cn-> CC )
8	7	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> p ) e. ( CC -cn-> CC ) )
9		pntlem3.2	. . . . . . . . . . . . . . 15 |- ( ph -> C e. RR+ )
10	9	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> C e. RR+ )
11	10	rpcnd 11306	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> C e. CC )
12	5	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> CC C_ CC )
13		cncfmptc 21707	. . . . . . . . . . . . 13 |- ( ( C e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( p e. CC |-> C ) e. ( CC -cn-> CC ) )
14	11, 12, 12, 13	syl3anc 1230	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> C ) e. ( CC -cn-> CC ) )
15		3nn0 10854	. . . . . . . . . . . . . 14 |- 3 e. NN0
16	2	expcn 21668	. . . . . . . . . . . . . 14 |- ( 3 e. NN0 -> ( p e. CC |-> ( p ^ 3 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
17	15, 16	mp1i 13	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( p ^ 3 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
18	2	cncfcn1 21706	. . . . . . . . . . . . 13 |- ( CC -cn-> CC ) = ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) )
19	17, 18	syl6eleqr 2501	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( p ^ 3 ) ) e. ( CC -cn-> CC ) )
20	14, 19	mulcncf 22151	. . . . . . . . . . 11 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( C x. ( p ^ 3 ) ) ) e. ( CC -cn-> CC ) )
21	2, 4, 8, 20	cncfmpt2f 21710	. . . . . . . . . 10 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) e. ( CC -cn-> CC ) )
22		pntlem3.1	. . . . . . . . . . . . . . 15 |- T = { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t }
23		ssrab2 3524	. . . . . . . . . . . . . . 15 |- { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } C_ ( 0 [,] A )
24	22, 23	eqsstri 3472	. . . . . . . . . . . . . 14 |- T C_ ( 0 [,] A )
25		0re 9626	. . . . . . . . . . . . . . 15 |- 0 e. RR
26		pntlem3.a	. . . . . . . . . . . . . . . 16 |- ( ph -> A e. RR+ )
27	26	rpred 11304	. . . . . . . . . . . . . . 15 |- ( ph -> A e. RR )
28		iccssre 11660	. . . . . . . . . . . . . . 15 |- ( ( 0 e. RR /\ A e. RR ) -> ( 0 [,] A ) C_ RR )
29	25, 27, 28	sylancr 661	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 [,] A ) C_ RR )
30	24, 29	syl5ss 3453	. . . . . . . . . . . . 13 |- ( ph -> T C_ RR )
31		0xr 9670	. . . . . . . . . . . . . . . . 17 |- 0 e. RR*
32	31	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 e. RR* )
33	26	rpxrd 11305	. . . . . . . . . . . . . . . 16 |- ( ph -> A e. RR* )
34	26	rpge0d 11308	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ A )
35		ubicc2 11691	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR* /\ A e. RR* /\ 0 <_ A ) -> A e. ( 0 [,] A ) )
36	32, 33, 34, 35	syl3anc 1230	. . . . . . . . . . . . . . 15 |- ( ph -> A e. ( 0 [,] A ) )
37		1rp 11269	. . . . . . . . . . . . . . . 16 |- 1 e. RR+
38		1re 9625	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. RR
39		elicopnf 11674	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR -> ( z e. ( 1 [,) +oo ) <-> ( z e. RR /\ 1 <_ z ) ) )
40	38, 39	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( z e. ( 1 [,) +oo ) <-> ( z e. RR /\ 1 <_ z ) ) )
41	40	simprbda 621	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> z e. RR )
42		0red 9627	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 e. RR )
43	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 1 e. RR )
44		0lt1 10115	. . . . . . . . . . . . . . . . . . . . 21 |- 0 < 1
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 < 1 )
46	40	simplbda 622	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 1 <_ z )
47	42, 43, 41, 45, 46	ltletrd 9776	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 < z )
48	41, 47	elrpd 11301	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> z e. RR+ )
49		pntlem3.A	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
50	49	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
51		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( R ` x ) = ( R ` z ) )
52		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> x = z )
53	51, 52	oveq12d 6296	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( R ` x ) / x ) = ( ( R ` z ) / z ) )
54	53	fveq2d 5853	. . . . . . . . . . . . . . . . . . . 20 |- ( x = z -> ( abs ` ( ( R ` x ) / x ) ) = ( abs ` ( ( R ` z ) / z ) ) )
55	54	breq1d 4405	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> ( ( abs ` ( ( R ` x ) / x ) ) <_ A <-> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
56	55	rspcv 3156	. . . . . . . . . . . . . . . . . 18 |- ( z e. RR+ -> ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A -> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
57	48, 50, 56	sylc 59	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> ( abs ` ( ( R ` z ) / z ) ) <_ A )
58	57	ralrimiva 2818	. . . . . . . . . . . . . . . 16 |- ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
59		oveq1 6285	. . . . . . . . . . . . . . . . . 18 |- ( y = 1 -> ( y [,) +oo ) = ( 1 [,) +oo ) )
60	59	raleqdv 3010	. . . . . . . . . . . . . . . . 17 |- ( y = 1 -> ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A <-> A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
61	60	rspcev 3160	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) -> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
62	37, 58, 61	sylancr 661	. . . . . . . . . . . . . . 15 |- ( ph -> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
63		breq2 4399	. . . . . . . . . . . . . . . . 17 |- ( t = A -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
64	63	rexralbidv 2926	. . . . . . . . . . . . . . . 16 |- ( t = A -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t <-> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
65	64, 22	elrab2 3209	. . . . . . . . . . . . . . 15 |- ( A e. T <-> ( A e. ( 0 [,] A ) /\ E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
66	36, 62, 65	sylanbrc 662	. . . . . . . . . . . . . 14 |- ( ph -> A e. T )
67		ne0i 3744	. . . . . . . . . . . . . 14 |- ( A e. T -> T =/= (/) )
68	66, 67	syl 17	. . . . . . . . . . . . 13 |- ( ph -> T =/= (/) )
69		elicc2 11643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR /\ A e. RR ) -> ( t e. ( 0 [,] A ) <-> ( t e. RR /\ 0 <_ t /\ t <_ A ) ) )
70	25, 27, 69	sylancr 661	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( t e. ( 0 [,] A ) <-> ( t e. RR /\ 0 <_ t /\ t <_ A ) ) )
71	70	biimpa 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ t e. ( 0 [,] A ) ) -> ( t e. RR /\ 0 <_ t /\ t <_ A ) )
72	71	simp2d 1010	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. ( 0 [,] A ) ) -> 0 <_ t )
73	72	a1d 25	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ t e. ( 0 [,] A ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
74	73	ralrimiva 2818	. . . . . . . . . . . . . . 15 |- ( ph -> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
75	22	raleqi 3008	. . . . . . . . . . . . . . . 16 |- ( A. w e. T 0 <_ w <-> A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } 0 <_ w )
76		breq2 4399	. . . . . . . . . . . . . . . . 17 |- ( w = t -> ( 0 <_ w <-> 0 <_ t ) )
77	76	ralrab2 3215	. . . . . . . . . . . . . . . 16 |- ( A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } 0 <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
78	75, 77	bitri 249	. . . . . . . . . . . . . . 15 |- ( A. w e. T 0 <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> 0 <_ t ) )
79	74, 78	sylibr 212	. . . . . . . . . . . . . 14 |- ( ph -> A. w e. T 0 <_ w )
80		breq1 4398	. . . . . . . . . . . . . . . 16 |- ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
81	80	ralbidv 2843	. . . . . . . . . . . . . . 15 |- ( x = 0 -> ( A. w e. T x <_ w <-> A. w e. T 0 <_ w ) )
82	81	rspcev 3160	. . . . . . . . . . . . . 14 |- ( ( 0 e. RR /\ A. w e. T 0 <_ w ) -> E. x e. RR A. w e. T x <_ w )
83	25, 79, 82	sylancr 661	. . . . . . . . . . . . 13 |- ( ph -> E. x e. RR A. w e. T x <_ w )
84		infmrcl 10562	. . . . . . . . . . . . 13 |- ( ( T C_ RR /\ T =/= (/) /\ E. x e. RR A. w e. T x <_ w ) -> sup ( T , RR , `' < ) e. RR )
85	30, 68, 83, 84	syl3anc 1230	. . . . . . . . . . . 12 |- ( ph -> sup ( T , RR , `' < ) e. RR )
86	85	recnd 9652	. . . . . . . . . . 11 |- ( ph -> sup ( T , RR , `' < ) e. CC )
87	86	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> sup ( T , RR , `' < ) e. CC )
88		elrp 11267	. . . . . . . . . . . . . 14 |- ( sup ( T , RR , `' < ) e. RR+ <-> ( sup ( T , RR , `' < ) e. RR /\ 0 < sup ( T , RR , `' < ) ) )
89	88	biimpri 206	. . . . . . . . . . . . 13 |- ( ( sup ( T , RR , `' < ) e. RR /\ 0 < sup ( T , RR , `' < ) ) -> sup ( T , RR , `' < ) e. RR+ )
90	85, 89	sylan 469	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> sup ( T , RR , `' < ) e. RR+ )
91		3z 10938	. . . . . . . . . . . 12 |- 3 e. ZZ
92		rpexpcl 12229	. . . . . . . . . . . 12 |- ( ( sup ( T , RR , `' < ) e. RR+ /\ 3 e. ZZ ) -> ( sup ( T , RR , `' < ) ^ 3 ) e. RR+ )
93	90, 91, 92	sylancl 660	. . . . . . . . . . 11 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( sup ( T , RR , `' < ) ^ 3 ) e. RR+ )
94	10, 93	rpmulcld 11320	. . . . . . . . . 10 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. RR+ )
95		cncfi 21690	. . . . . . . . . 10 |- ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) e. ( CC -cn-> CC ) /\ sup ( T , RR , `' < ) e. CC /\ ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. RR+ ) -> E. s e. RR+ A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
96	21, 87, 94, 95	syl3anc 1230	. . . . . . . . 9 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> E. s e. RR+ A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
97	85	ad2antrr 724	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> sup ( T , RR , `' < ) e. RR )
98		rphalfcl 11290	. . . . . . . . . . . . . 14 |- ( s e. RR+ -> ( s / 2 ) e. RR+ )
99	98	adantl 464	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR+ )
100	97, 99	ltaddrpd 11333	. . . . . . . . . . . 12 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> sup ( T , RR , `' < ) < ( sup ( T , RR , `' < ) + ( s / 2 ) ) )
101	99	rpred 11304	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR )
102	97, 101	readdcld 9653	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) e. RR )
103	97, 102	ltnled 9764	. . . . . . . . . . . 12 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( sup ( T , RR , `' < ) < ( sup ( T , RR , `' < ) + ( s / 2 ) ) <-> -. ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ sup ( T , RR , `' < ) ) )
104	100, 103	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> -. ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ sup ( T , RR , `' < ) )
105		ax-resscn 9579	. . . . . . . . . . . . . . 15 |- RR C_ CC
106	30, 105	syl6ss 3454	. . . . . . . . . . . . . 14 |- ( ph -> T C_ CC )
107	106	ad2antrr 724	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> T C_ CC )
108		ssralv 3503	. . . . . . . . . . . . 13 |- ( T C_ CC -> ( A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> A. u e. T ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) )
109	107, 108	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> A. u e. T ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) )
110	30	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> T C_ RR )
111	110	sselda 3442	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. RR )
112	102	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) e. RR )
113	111, 112	ltnled 9764	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u < ( sup ( T , RR , `' < ) + ( s / 2 ) ) <-> -. ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
114	85	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) e. RR )
115	101	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( s / 2 ) e. RR )
116	114, 115	resubcld 10028	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) e. RR )
117	97, 99	ltsubrpd 11332	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) < sup ( T , RR , `' < ) )
118	117	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) < sup ( T , RR , `' < ) )
119	30	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> T C_ RR )
120	83	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> E. x e. RR A. w e. T x <_ w )
121		simpr 459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. T )
122		infmrlb 10564	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T C_ RR /\ E. x e. RR A. w e. T x <_ w /\ u e. T ) -> sup ( T , RR , `' < ) <_ u )
123	119, 120, 121, 122	syl3anc 1230	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) <_ u )
124	116, 114, 111, 118, 123	ltletrd 9776	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) < u )
125	111, 114, 115	absdifltd 13414	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < ( s / 2 ) <-> ( ( sup ( T , RR , `' < ) - ( s / 2 ) ) < u /\ u < ( sup ( T , RR , `' < ) + ( s / 2 ) ) ) ) )
126	125	biimprd 223	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( sup ( T , RR , `' < ) - ( s / 2 ) ) < u /\ u < ( sup ( T , RR , `' < ) + ( s / 2 ) ) ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < ( s / 2 ) ) )
127	124, 126	mpand 673	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u < ( sup ( T , RR , `' < ) + ( s / 2 ) ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < ( s / 2 ) ) )
128		rphalflt 11292	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. RR+ -> ( s / 2 ) < s )
129	128	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( s / 2 ) < s )
130	111, 114	resubcld 10028	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - sup ( T , RR , `' < ) ) e. RR )
131	130	recnd 9652	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - sup ( T , RR , `' < ) ) e. CC )
132	131	abscld 13416	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) e. RR )
133		rpre 11271	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. RR+ -> s e. RR )
134	133	ad2antlr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> s e. RR )
135		lttr 9692	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) e. RR /\ ( s / 2 ) e. RR /\ s e. RR ) -> ( ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < ( s / 2 ) /\ ( s / 2 ) < s ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s ) )
136	132, 115, 134, 135	syl3anc 1230	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < ( s / 2 ) /\ ( s / 2 ) < s ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s ) )
137	129, 136	mpan2d 672	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < ( s / 2 ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s ) )
138	127, 137	syld 42	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u < ( sup ( T , RR , `' < ) + ( s / 2 ) ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s ) )
139	113, 138	sylbird 235	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( -. ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s ) )
140	139	con1d 124	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( -. ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
141	111	recnd 9652	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. CC )
142		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = u -> p = u )
143		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( p = u -> ( p ^ 3 ) = ( u ^ 3 ) )
144	143	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = u -> ( C x. ( p ^ 3 ) ) = ( C x. ( u ^ 3 ) ) )
145	142, 144	oveq12d 6296	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = u -> ( p - ( C x. ( p ^ 3 ) ) ) = ( u - ( C x. ( u ^ 3 ) ) ) )
146		eqid 2402	. . . . . . . . . . . . . . . . . . . . 21 |- ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) = ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) )
147		ovex 6306	. . . . . . . . . . . . . . . . . . . . 21 |- ( u - ( C x. ( u ^ 3 ) ) ) e. _V
148	145, 146, 147	fvmpt 5932	. . . . . . . . . . . . . . . . . . . 20 |- ( u e. CC -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) = ( u - ( C x. ( u ^ 3 ) ) ) )
149	141, 148	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) = ( u - ( C x. ( u ^ 3 ) ) ) )
150	87	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) e. CC )
151		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = sup ( T , RR , `' < ) -> p = sup ( T , RR , `' < ) )
152		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( p = sup ( T , RR , `' < ) -> ( p ^ 3 ) = ( sup ( T , RR , `' < ) ^ 3 ) )
153	152	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = sup ( T , RR , `' < ) -> ( C x. ( p ^ 3 ) ) = ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) )
154	151, 153	oveq12d 6296	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = sup ( T , RR , `' < ) -> ( p - ( C x. ( p ^ 3 ) ) ) = ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
155		ovex 6306	. . . . . . . . . . . . . . . . . . . . 21 |- ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) e. _V
156	154, 146, 155	fvmpt 5932	. . . . . . . . . . . . . . . . . . . 20 |- ( sup ( T , RR , `' < ) e. CC -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) = ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
157	150, 156	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) = ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
158	149, 157	oveq12d 6296	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) = ( ( u - ( C x. ( u ^ 3 ) ) ) - ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) )
159	158	fveq2d 5853	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) = ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) ) )
160	159	breq1d 4405	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) <-> ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
161	9	rpred 11304	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. RR )
162	161	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> C e. RR )
163		reexpcl 12227	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( u e. RR /\ 3 e. NN0 ) -> ( u ^ 3 ) e. RR )
164	111, 15, 163	sylancl 660	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u ^ 3 ) e. RR )
165	162, 164	remulcld 9654	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( u ^ 3 ) ) e. RR )
166	111, 165	resubcld 10028	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. RR )
167	15	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> 3 e. NN0 )
168	114, 167	reexpcld 12371	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) ^ 3 ) e. RR )
169	162, 168	remulcld 9654	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. RR )
170	114, 169	resubcld 10028	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) e. RR )
171	166, 170, 169	absdifltd 13414	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) <-> ( ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) < ( u - ( C x. ( u ^ 3 ) ) ) /\ ( u - ( C x. ( u ^ 3 ) ) ) < ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) + ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) ) )
172	169	recnd 9652	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. CC )
173	150, 172	npcand 9971	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) + ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) = sup ( T , RR , `' < ) )
174	173	breq2d 4407	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( u - ( C x. ( u ^ 3 ) ) ) < ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) + ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) <-> ( u - ( C x. ( u ^ 3 ) ) ) < sup ( T , RR , `' < ) ) )
175		simpll 752	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ph )
176		pntlem3.3	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )
177	175, 176	sylan 469	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )
178		infmrlb 10564	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T C_ RR /\ E. x e. RR A. w e. T x <_ w /\ ( u - ( C x. ( u ^ 3 ) ) ) e. T ) -> sup ( T , RR , `' < ) <_ ( u - ( C x. ( u ^ 3 ) ) ) )
179	119, 120, 177, 178	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) <_ ( u - ( C x. ( u ^ 3 ) ) ) )
180	114, 166	lenltd 9763	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) <_ ( u - ( C x. ( u ^ 3 ) ) ) <-> -. ( u - ( C x. ( u ^ 3 ) ) ) < sup ( T , RR , `' < ) ) )
181	179, 180	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> -. ( u - ( C x. ( u ^ 3 ) ) ) < sup ( T , RR , `' < ) )
182	181	pm2.21d 106	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( u - ( C x. ( u ^ 3 ) ) ) < sup ( T , RR , `' < ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
183	174, 182	sylbid 215	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( u - ( C x. ( u ^ 3 ) ) ) < ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) + ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
184	183	adantld 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) < ( u - ( C x. ( u ^ 3 ) ) ) /\ ( u - ( C x. ( u ^ 3 ) ) ) < ( ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) + ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
185	171, 184	sylbid 215	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( u - ( C x. ( u ^ 3 ) ) ) - ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
186	160, 185	sylbid 215	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
187	140, 186	jad 162	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
188	187	ralimdva 2812	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( A. u e. T ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> A. u e. T ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
189	68	ad2antrr 724	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> T =/= (/) )
190	83	ad2antrr 724	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> E. x e. RR A. w e. T x <_ w )
191		infmrgelb 10563	. . . . . . . . . . . . . 14 |- ( ( ( T C_ RR /\ T =/= (/) /\ E. x e. RR A. w e. T x <_ w ) /\ ( sup ( T , RR , `' < ) + ( s / 2 ) ) e. RR ) -> ( ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ sup ( T , RR , `' < ) <-> A. u e. T ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
192	110, 189, 190, 102, 191	syl31anc 1233	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ sup ( T , RR , `' < ) <-> A. u e. T ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ u ) )
193	188, 192	sylibrd 234	. . . . . . . . . . . 12 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( A. u e. T ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ sup ( T , RR , `' < ) ) )
194	109, 193	syld 42	. . . . . . . . . . 11 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) <_ sup ( T , RR , `' < ) ) )
195	104, 194	mtod 177	. . . . . . . . . 10 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> -. A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
196	195	nrexdv 2860	. . . . . . . . 9 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> -. E. s e. RR+ A. u e. CC ( ( abs ` ( u - sup ( T , RR , `' < ) ) ) < s -> ( abs ` ( ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) - ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` sup ( T , RR , `' < ) ) ) ) < ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
197	96, 196	pm2.65da 574	. . . . . . . 8 |- ( ph -> -. 0 < sup ( T , RR , `' < ) )
198	197	adantr 463	. . . . . . 7 |- ( ( ph /\ s e. RR+ ) -> -. 0 < sup ( T , RR , `' < ) )
199	30	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> T C_ RR )
200	68	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> T =/= (/) )
201	83	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> E. x e. RR A. w e. T x <_ w )
202	133	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> s e. RR )
203		infmrgelb 10563	. . . . . . . . . 10 |- ( ( ( T C_ RR /\ T =/= (/) /\ E. x e. RR A. w e. T x <_ w ) /\ s e. RR ) -> ( s <_ sup ( T , RR , `' < ) <-> A. w e. T s <_ w ) )
204	199, 200, 201, 202, 203	syl31anc 1233	. . . . . . . . 9 |- ( ( ph /\ s e. RR+ ) -> ( s <_ sup ( T , RR , `' < ) <-> A. w e. T s <_ w ) )
205	22	raleqi 3008	. . . . . . . . . 10 |- ( A. w e. T s <_ w <-> A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } s <_ w )
206		breq2 4399	. . . . . . . . . . 11 |- ( w = t -> ( s <_ w <-> s <_ t ) )
207	206	ralrab2 3215	. . . . . . . . . 10 |- ( A. w e. { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t } s <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
208	205, 207	bitri 249	. . . . . . . . 9 |- ( A. w e. T s <_ w <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
209	204, 208	syl6bb 261	. . . . . . . 8 |- ( ( ph /\ s e. RR+ ) -> ( s <_ sup ( T , RR , `' < ) <-> A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) ) )
210		rpgt0 11276	. . . . . . . . . 10 |- ( s e. RR+ -> 0 < s )
211	210	adantl 464	. . . . . . . . 9 |- ( ( ph /\ s e. RR+ ) -> 0 < s )
212		0red 9627	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> 0 e. RR )
213	85	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> sup ( T , RR , `' < ) e. RR )
214		ltletr 9707	. . . . . . . . . 10 |- ( ( 0 e. RR /\ s e. RR /\ sup ( T , RR , `' < ) e. RR ) -> ( ( 0 < s /\ s <_ sup ( T , RR , `' < ) ) -> 0 < sup ( T , RR , `' < ) ) )
215	212, 202, 213, 214	syl3anc 1230	. . . . . . . . 9 |- ( ( ph /\ s e. RR+ ) -> ( ( 0 < s /\ s <_ sup ( T , RR , `' < ) ) -> 0 < sup ( T , RR , `' < ) ) )
216	211, 215	mpand 673	. . . . . . . 8 |- ( ( ph /\ s e. RR+ ) -> ( s <_ sup ( T , RR , `' < ) -> 0 < sup ( T , RR , `' < ) ) )
217	209, 216	sylbird 235	. . . . . . 7 |- ( ( ph /\ s e. RR+ ) -> ( A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) -> 0 < sup ( T , RR , `' < ) ) )
218	198, 217	mtod 177	. . . . . 6 |- ( ( ph /\ s e. RR+ ) -> -. A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
219		rexanali 2857	. . . . . 6 |- ( E. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) <-> -. A. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> s <_ t ) )
220	218, 219	sylibr 212	. . . . 5 |- ( ( ph /\ s e. RR+ ) -> E. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) )
221		fveq2 5849	. . . . . . . . . . . . . . 15 |- ( z = x -> ( R ` z ) = ( R ` x ) )
222		id 22	. . . . . . . . . . . . . . 15 |- ( z = x -> z = x )
223	221, 222	oveq12d 6296	. . . . . . . . . . . . . 14 |- ( z = x -> ( ( R ` z ) / z ) = ( ( R ` x ) / x ) )
224	223	fveq2d 5853	. . . . . . . . . . . . 13 |- ( z = x -> ( abs ` ( ( R ` z ) / z ) ) = ( abs ` ( ( R ` x ) / x ) ) )
225	224	breq1d 4405	. . . . . . . . . . . 12 |- ( z = x -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` x ) / x ) ) <_ t ) )
226	225	cbvralv 3034	. . . . . . . . . . 11 |- ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t <-> A. x e. ( y [,) +oo ) ( abs ` ( ( R ` x ) / x ) ) <_ t )
227		rpre 11271	. . . . . . . . . . . . . . . . 17 |- ( x e. RR+ -> x e. RR )
228	227	ad2antll 727	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. RR )
229		simprl 756	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y <_ x )
230		simplr 754	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y e. RR+ )
231	230	rpred 11304	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y e. RR )
232		elicopnf 11674	. . . . . . . . . . . . . . . . 17 |- ( y e. RR -> ( x e. ( y [,) +oo ) <-> ( x e. RR /\ y <_ x ) ) )
233	231, 232	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( x e. ( y [,) +oo ) <-> ( x e. RR /\ y <_ x ) ) )
234	228, 229, 233	mpbir2and 923	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. ( y [,) +oo ) )
235		pntlem3.r	. . . . . . . . . . . . . . . . . . . . . 22 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
236	235	pntrval 24128	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. RR+ -> ( R ` x ) = ( (ψ ` x ) - x ) )
237	236	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( R ` x ) = ( (ψ ` x ) - x ) )
238	237	oveq1d 6293	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( R ` x ) / x ) = ( ( (ψ ` x ) - x ) / x ) )
239		chpcl 23779	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> (ψ ` x ) e. RR )
240	228, 239	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> (ψ ` x ) e. RR )
241	240	recnd 9652	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> (ψ ` x ) e. CC )
242		rpcn 11273	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. RR+ -> x e. CC )
243	242	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. CC )
244		rpne0 11280	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. RR+ -> x =/= 0 )
245	244	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x =/= 0 )
246	241, 243, 243, 245	divsubdird 10400	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( (ψ ` x ) - x ) / x ) = ( ( (ψ ` x ) / x ) - ( x / x ) ) )
247	243, 245	dividd 10359	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( x / x ) = 1 )
248	247	oveq2d 6294	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( (ψ ` x ) / x ) - ( x / x ) ) = ( ( (ψ ` x ) / x ) - 1 ) )
249	238, 246, 248	3eqtrrd 2448	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( (ψ ` x ) / x ) - 1 ) = ( ( R ` x ) / x ) )
250	249	fveq2d 5853	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) = ( abs ` ( ( R ` x ) / x ) ) )
251	250	breq1d 4405	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) <_ t <-> ( abs ` ( ( R ` x ) / x ) ) <_ t ) )
252		simprr 758	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> -. s <_ t )
253	252	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> -. s <_ t )
254	29	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> ( 0 [,] A ) C_ RR )
255	254	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( 0 [,] A ) C_ RR )
256		simplrl 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> t e. ( 0 [,] A ) )
257	256	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> t e. ( 0 [,] A ) )
258	255, 257	sseldd 3443	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> t e. RR )
259		simp-4r 769	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> s e. RR+ )
260	259	rpred 11304	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> s e. RR )
261	258, 260	ltnled 9764	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( t < s <-> -. s <_ t ) )
262	253, 261	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> t < s )
263	227, 239	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. RR+ -> (ψ ` x ) e. RR )
264		rerpdivcl 11293	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( (ψ ` x ) e. RR /\ x e. RR+ ) -> ( (ψ ` x ) / x ) e. RR )
265	263, 264	mpancom 667	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR+ -> ( (ψ ` x ) / x ) e. RR )
266	265	ad2antll 727	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( (ψ ` x ) / x ) e. RR )
267		resubcl 9919	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( (ψ ` x ) / x ) e. RR /\ 1 e. RR ) -> ( ( (ψ ` x ) / x ) - 1 ) e. RR )
268	266, 38, 267	sylancl 660	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( (ψ ` x ) / x ) - 1 ) e. RR )
269	268	recnd 9652	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( (ψ ` x ) / x ) - 1 ) e. CC )
270	269	abscld 13416	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) e. RR )
271		lelttr 9706	. . . . . . . . . . . . . . . . . 18 |- ( ( ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) e. RR /\ t e. RR /\ s e. RR ) -> ( ( ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) <_ t /\ t < s ) -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
272	270, 258, 260, 271	syl3anc 1230	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) <_ t /\ t < s ) -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
273	262, 272	mpan2d 672	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) <_ t -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
274	251, 273	sylbird 235	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( abs ` ( ( R ` x ) / x ) ) <_ t -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
275	234, 274	embantd 53	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> ( ( x e. ( y [,) +oo ) -> ( abs ` ( ( R ` x ) / x ) ) <_ t ) -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
276	275	exp32 603	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( y <_ x -> ( x e. RR+ -> ( ( x e. ( y [,) +oo ) -> ( abs ` ( ( R ` x ) / x ) ) <_ t ) -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) ) )
277	276	com24 87	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( ( x e. ( y [,) +oo ) -> ( abs ` ( ( R ` x ) / x ) ) <_ t ) -> ( x e. RR+ -> ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) ) )
278	277	ralimdv2 2811	. . . . . . . . . . 11 |- ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( A. x e. ( y [,) +oo ) ( abs ` ( ( R ` x ) / x ) ) <_ t -> A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
279	226, 278	syl5bi 217	. . . . . . . . . 10 |- ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
280	279	reximdva 2879	. . . . . . . . 9 |- ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
281	280	anassrs 646	. . . . . . . 8 |- ( ( ( ( ph /\ s e. RR+ ) /\ t e. ( 0 [,] A ) ) /\ -. s <_ t ) -> ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
282	281	impancom 438	. . . . . . 7 |- ( ( ( ( ph /\ s e. RR+ ) /\ t e. ( 0 [,] A ) ) /\ E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t ) -> ( -. s <_ t -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
283	282	expimpd 601	. . . . . 6 |- ( ( ( ph /\ s e. RR+ ) /\ t e. ( 0 [,] A ) ) -> ( ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
284	283	rexlimdva 2896	. . . . 5 |- ( ( ph /\ s e. RR+ ) -> ( E. t e. ( 0 [,] A ) ( E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t /\ -. s <_ t ) -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
285	220, 284	mpd 15	. . . 4 |- ( ( ph /\ s e. RR+ ) -> E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
286		ssrexv 3504	. . . 4 |- ( RR+ C_ RR -> ( E. y e. RR+ A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) -> E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
287	1, 285, 286	mpsyl 62	. . 3 |- ( ( ph /\ s e. RR+ ) -> E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
288	287	ralrimiva 2818	. 2 |- ( ph -> A. s e. RR+ E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
289	265	recnd 9652	. . . . 5 |- ( x e. RR+ -> ( (ψ ` x ) / x ) e. CC )
290	289	rgen 2764	. . . 4 |- A. x e. RR+ ( (ψ ` x ) / x ) e. CC
291	290	a1i 11	. . 3 |- ( ph -> A. x e. RR+ ( (ψ ` x ) / x ) e. CC )
292	1	a1i 11	. . 3 |- ( ph -> RR+ C_ RR )
293		1cnd 9642	. . 3 |- ( ph -> 1 e. CC )
294	291, 292, 293	rlim2 13468	. 2 |- ( ph -> ( ( x e. RR+ |-> ( (ψ ` x ) / x ) ) ~~> r 1 <-> A. s e. RR+ E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) ) )
295	288, 294	mpbird 232	1 |- ( ph -> ( x e. RR+ |-> ( (ψ ` x ) / x ) ) ~~> r 1 )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2754   E.wrex 2755   {crab 2758   C_ wss 3414   (/)c0 3738   class class class wbr 4395   |-> cmpt 4453   `'ccnv 4822   ` cfv 5569  (class class class)co 6278   supcsup 7934   CCcc 9520   RRcr 9521   0cc0 9522   1c1 9523   + caddc 9525   x. cmul 9527   +oocpnf 9655   RR*cxr 9657   < clt 9658   <_ cle 9659   - cmin 9841   / cdiv 10247   2c2 10626   3c3 10627   NN0cn0 10836   ZZcz 10905   RR+crp 11265   [,)cico 11584   [,]cicc 11585   ^cexp 12210   abscabs 13216   ~~> r crli 13457   TopOpenctopn 15036  ℂ_fldccnfld 18740   Cn ccn 20018   tX ctx 20353   -cn->ccncf 21672  ψcchp 23747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-inf2 8091  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599  ax-pre-sup 9600  ax-addf 9601  ax-mulf 9602

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-iin 4274  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6521  df-om 6684  df-1st 6784  df-2nd 6785  df-supp 6903  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-2o 7168  df-oadd 7171  df-er 7348  df-map 7459  df-pm 7460  df-ixp 7508  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-fsupp 7864  df-fi 7905  df-sup 7935  df-oi 7969  df-card 8352  df-cda 8580  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-div 10248  df-nn 10577  df-2 10635  df-3 10636  df-4 10637  df-5 10638  df-6 10639  df-7 10640  df-8 10641  df-9 10642  df-10 10643  df-n0 10837  df-z 10906  df-dec 11020  df-uz 11128  df-q 11228  df-rp 11266  df-xneg 11371  df-xadd 11372  df-xmul 11373  df-ioo 11586  df-ioc 11587  df-ico 11588  df-icc 11589  df-fz 11727  df-fzo 11855  df-fl 11966  df-mod 12035  df-seq 12152  df-exp 12211  df-fac 12398  df-bc 12425  df-hash 12453  df-shft 13049  df-cj 13081  df-re 13082  df-im 13083  df-sqrt 13217  df-abs 13218  df-limsup 13443  df-clim 13460  df-rlim 13461  df-sum 13658  df-ef 14012  df-sin 14014  df-cos 14015  df-pi 14017  df-dvds 14196  df-gcd 14354  df-prm 14427  df-pc 14570  df-struct 14843  df-ndx 14844  df-slot 14845  df-base 14846  df-sets 14847  df-ress 14848  df-plusg 14922  df-mulr 14923  df-starv 14924  df-sca 14925  df-vsca 14926  df-ip 14927  df-tset 14928  df-ple 14929  df-ds 14931  df-unif 14932  df-hom 14933  df-cco 14934  df-rest 15037  df-topn 15038  df-0g 15056  df-gsum 15057  df-topgen 15058  df-pt 15059  df-prds 15062  df-xrs 15116  df-qtop 15121  df-imas 15122  df-xps 15124  df-mre 15200  df-mrc 15201  df-acs 15203  df-mgm 16196  df-sgrp 16235  df-mnd 16245  df-submnd 16291  df-mulg 16384  df-cntz 16679  df-cmn 17124  df-psmet 18731  df-xmet 18732  df-met 18733  df-bl 18734  df-mopn 18735  df-fbas 18736  df-fg 18737  df-cnfld 18741  df-top 19691  df-bases 19693  df-topon 19694  df-topsp 19695  df-cld 19812  df-ntr 19813  df-cls 19814  df-nei 19892  df-lp 19930  df-perf 19931  df-cn 20021  df-cnp 20022  df-haus 20109  df-tx 20355  df-hmeo 20548  df-fil 20639  df-fm 20731  df-flim 20732  df-flf 20733  df-xms 21115  df-ms 21116  df-tms 21117  df-cncf 21674  df-limc 22562  df-dv 22563  df-log 23236  df-vma 23752  df-chp 23753

This theorem is referenced by:  pntleml  24177