Theorem pntlem3 23920

Description: Lemma for pnt 23925. 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 11255	. . . 4 |- RR+ C_ RR
2		eqid 2457	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
3	2	subcn 21496	. . . . . . . . . . . 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 3518	. . . . . . . . . . . . 13 |- CC C_ CC
6		cncfmptid 21542	. . . . . . . . . . . . 13 |- ( ( CC C_ CC /\ CC C_ CC ) -> ( p e. CC |-> p ) e. ( CC -cn-> CC ) )
7	5, 5, 6	mp2an 672	. . . . . . . . . . . 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 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> C e. RR+ )
11	10	rpcnd 11283	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> C e. CC )
12	5	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> CC C_ CC )
13		cncfmptc 21541	. . . . . . . . . . . . 13 |- ( ( C e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( p e. CC |-> C ) e. ( CC -cn-> CC ) )
14	11, 12, 12, 13	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> C ) e. ( CC -cn-> CC ) )
15		3nn0 10834	. . . . . . . . . . . . . 14 |- 3 e. NN0
16	2	expcn 21502	. . . . . . . . . . . . . 14 |- ( 3 e. NN0 -> ( p e. CC |-> ( p ^ 3 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
17	15, 16	mp1i 12	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( p ^ 3 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
18	2	cncfcn1 21540	. . . . . . . . . . . . 13 |- ( CC -cn-> CC ) = ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) )
19	17, 18	syl6eleqr 2556	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( p ^ 3 ) ) e. ( CC -cn-> CC ) )
20	14, 19	mulcncf 21985	. . . . . . . . . . 11 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( p e. CC |-> ( C x. ( p ^ 3 ) ) ) e. ( CC -cn-> CC ) )
21	2, 4, 8, 20	cncfmpt2f 21544	. . . . . . . . . 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 3581	. . . . . . . . . . . . . . 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 3529	. . . . . . . . . . . . . 14 |- T C_ ( 0 [,] A )
25		0re 9613	. . . . . . . . . . . . . . 15 |- 0 e. RR
26		pntlem3.a	. . . . . . . . . . . . . . . 16 |- ( ph -> A e. RR+ )
27	26	rpred 11281	. . . . . . . . . . . . . . 15 |- ( ph -> A e. RR )
28		iccssre 11631	. . . . . . . . . . . . . . 15 |- ( ( 0 e. RR /\ A e. RR ) -> ( 0 [,] A ) C_ RR )
29	25, 27, 28	sylancr 663	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 [,] A ) C_ RR )
30	24, 29	syl5ss 3510	. . . . . . . . . . . . 13 |- ( ph -> T C_ RR )
31		0xr 9657	. . . . . . . . . . . . . . . . 17 |- 0 e. RR*
32	31	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 e. RR* )
33	26	rpxrd 11282	. . . . . . . . . . . . . . . 16 |- ( ph -> A e. RR* )
34	26	rpge0d 11285	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ A )
35		ubicc2 11662	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR* /\ A e. RR* /\ 0 <_ A ) -> A e. ( 0 [,] A ) )
36	32, 33, 34, 35	syl3anc 1228	. . . . . . . . . . . . . . 15 |- ( ph -> A e. ( 0 [,] A ) )
37		1rp 11249	. . . . . . . . . . . . . . . 16 |- 1 e. RR+
38		1re 9612	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. RR
39		elicopnf 11645	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 e. RR -> ( z e. ( 1 [,) +oo ) <-> ( z e. RR /\ 1 <_ z ) ) )
40	38, 39	mp1i 12	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( z e. ( 1 [,) +oo ) <-> ( z e. RR /\ 1 <_ z ) ) )
41	40	simprbda 623	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> z e. RR )
42		0red 9614	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 e. RR )
43	38	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 1 e. RR )
44		0lt1 10096	. . . . . . . . . . . . . . . . . . . . 21 |- 0 < 1
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 < 1 )
46	40	simplbda 624	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 1 <_ z )
47	42, 43, 41, 45, 46	ltletrd 9759	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> 0 < z )
48	41, 47	elrpd 11279	. . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
51		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( R ` x ) = ( R ` z ) )
52		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> x = z )
53	51, 52	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( R ` x ) / x ) = ( ( R ` z ) / z ) )
54	53	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( x = z -> ( abs ` ( ( R ` x ) / x ) ) = ( abs ` ( ( R ` z ) / z ) ) )
55	54	breq1d 4466	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> ( ( abs ` ( ( R ` x ) / x ) ) <_ A <-> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
56	55	rspcv 3206	. . . . . . . . . . . . . . . . . 18 |- ( z e. RR+ -> ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A -> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
57	48, 50, 56	sylc 60	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ( 1 [,) +oo ) ) -> ( abs ` ( ( R ` z ) / z ) ) <_ A )
58	57	ralrimiva 2871	. . . . . . . . . . . . . . . 16 |- ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
59		oveq1 6303	. . . . . . . . . . . . . . . . . 18 |- ( y = 1 -> ( y [,) +oo ) = ( 1 [,) +oo ) )
60	59	raleqdv 3060	. . . . . . . . . . . . . . . . 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 3210	. . . . . . . . . . . . . . . 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 663	. . . . . . . . . . . . . . 15 |- ( ph -> E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ A )
63		breq2 4460	. . . . . . . . . . . . . . . . 17 |- ( t = A -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` z ) / z ) ) <_ A ) )
64	63	rexralbidv 2976	. . . . . . . . . . . . . . . 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 3259	. . . . . . . . . . . . . . 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 664	. . . . . . . . . . . . . 14 |- ( ph -> A e. T )
67		ne0i 3799	. . . . . . . . . . . . . 14 |- ( A e. T -> T =/= (/) )
68	66, 67	syl 16	. . . . . . . . . . . . 13 |- ( ph -> T =/= (/) )
69		elicc2 11614	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR /\ A e. RR ) -> ( t e. ( 0 [,] A ) <-> ( t e. RR /\ 0 <_ t /\ t <_ A ) ) )
70	25, 27, 69	sylancr 663	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( t e. ( 0 [,] A ) <-> ( t e. RR /\ 0 <_ t /\ t <_ A ) ) )
71	70	biimpa 484	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ t e. ( 0 [,] A ) ) -> ( t e. RR /\ 0 <_ t /\ t <_ A ) )
72	71	simp2d 1009	. . . . . . . . . . . . . . . . 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 2871	. . . . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . 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 4460	. . . . . . . . . . . . . . . . 17 |- ( w = t -> ( 0 <_ w <-> 0 <_ t ) )
77	76	ralrab2 3265	. . . . . . . . . . . . . . . 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 4459	. . . . . . . . . . . . . . . 16 |- ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
81	80	ralbidv 2896	. . . . . . . . . . . . . . 15 |- ( x = 0 -> ( A. w e. T x <_ w <-> A. w e. T 0 <_ w ) )
82	81	rspcev 3210	. . . . . . . . . . . . . 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 663	. . . . . . . . . . . . 13 |- ( ph -> E. x e. RR A. w e. T x <_ w )
84		infmrcl 10542	. . . . . . . . . . . . 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 1228	. . . . . . . . . . . 12 |- ( ph -> sup ( T , RR , `' < ) e. RR )
86	85	recnd 9639	. . . . . . . . . . 11 |- ( ph -> sup ( T , RR , `' < ) e. CC )
87	86	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> sup ( T , RR , `' < ) e. CC )
88		elrp 11247	. . . . . . . . . . . . . 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 471	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> sup ( T , RR , `' < ) e. RR+ )
91		3z 10918	. . . . . . . . . . . 12 |- 3 e. ZZ
92		rpexpcl 12188	. . . . . . . . . . . 12 |- ( ( sup ( T , RR , `' < ) e. RR+ /\ 3 e. ZZ ) -> ( sup ( T , RR , `' < ) ^ 3 ) e. RR+ )
93	90, 91, 92	sylancl 662	. . . . . . . . . . 11 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( sup ( T , RR , `' < ) ^ 3 ) e. RR+ )
94	10, 93	rpmulcld 11297	. . . . . . . . . 10 |- ( ( ph /\ 0 < sup ( T , RR , `' < ) ) -> ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. RR+ )
95		cncfi 21524	. . . . . . . . . 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 1228	. . . . . . . . 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 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> sup ( T , RR , `' < ) e. RR )
98		rphalfcl 11269	. . . . . . . . . . . . . 14 |- ( s e. RR+ -> ( s / 2 ) e. RR+ )
99	98	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR+ )
100	97, 99	ltaddrpd 11310	. . . . . . . . . . . 12 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> sup ( T , RR , `' < ) < ( sup ( T , RR , `' < ) + ( s / 2 ) ) )
101	99	rpred 11281	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR )
102	97, 101	readdcld 9640	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) e. RR )
103	97, 102	ltnled 9749	. . . . . . . . . . . 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 9566	. . . . . . . . . . . . . . 15 |- RR C_ CC
106	30, 105	syl6ss 3511	. . . . . . . . . . . . . 14 |- ( ph -> T C_ CC )
107	106	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> T C_ CC )
108		ssralv 3560	. . . . . . . . . . . . 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 16	. . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> T C_ RR )
111	110	sselda 3499	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. RR )
112	102	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) + ( s / 2 ) ) e. RR )
113	111, 112	ltnled 9749	. . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) e. RR )
115	101	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( s / 2 ) e. RR )
116	114, 115	resubcld 10008	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) e. RR )
117	97, 99	ltsubrpd 11309	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) < sup ( T , RR , `' < ) )
118	117	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) < sup ( T , RR , `' < ) )
119	30	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> T C_ RR )
120	83	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> E. x e. RR A. w e. T x <_ w )
121		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> u e. T )
122		infmrlb 10544	. . . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) <_ u )
124	116, 114, 111, 118, 123	ltletrd 9759	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) - ( s / 2 ) ) < u )
125	111, 114, 115	absdifltd 13277	. . . . . . . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . . . . . 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 11271	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. RR+ -> ( s / 2 ) < s )
129	128	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( s / 2 ) < s )
130	111, 114	resubcld 10008	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - sup ( T , RR , `' < ) ) e. RR )
131	130	recnd 9639	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - sup ( T , RR , `' < ) ) e. CC )
132	131	abscld 13279	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( abs ` ( u - sup ( T , RR , `' < ) ) ) e. RR )
133		rpre 11251	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. RR+ -> s e. RR )
134	133	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> s e. RR )
135		lttr 9678	. . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . 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 674	. . . . . . . . . . . . . . . . . 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 44	. . . . . . . . . . . . . . . . 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 9639	. . . . . . . . . . . . . . . . . . . 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 6303	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( p = u -> ( p ^ 3 ) = ( u ^ 3 ) )
144	143	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = u -> ( C x. ( p ^ 3 ) ) = ( C x. ( u ^ 3 ) ) )
145	142, 144	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = u -> ( p - ( C x. ( p ^ 3 ) ) ) = ( u - ( C x. ( u ^ 3 ) ) ) )
146		eqid 2457	. . . . . . . . . . . . . . . . . . . . 21 |- ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) = ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) )
147		ovex 6324	. . . . . . . . . . . . . . . . . . . . 21 |- ( u - ( C x. ( u ^ 3 ) ) ) e. _V
148	145, 146, 147	fvmpt 5956	. . . . . . . . . . . . . . . . . . . 20 |- ( u e. CC -> ( ( p e. CC |-> ( p - ( C x. ( p ^ 3 ) ) ) ) ` u ) = ( u - ( C x. ( u ^ 3 ) ) ) )
149	141, 148	syl 16	. . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . 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 6303	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( p = sup ( T , RR , `' < ) -> ( p ^ 3 ) = ( sup ( T , RR , `' < ) ^ 3 ) )
153	152	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p = sup ( T , RR , `' < ) -> ( C x. ( p ^ 3 ) ) = ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) )
154	151, 153	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = sup ( T , RR , `' < ) -> ( p - ( C x. ( p ^ 3 ) ) ) = ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) )
155		ovex 6324	. . . . . . . . . . . . . . . . . . . . 21 |- ( sup ( T , RR , `' < ) - ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) ) e. _V
156	154, 146, 155	fvmpt 5956	. . . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . 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 6314	. . . . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . . . . 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 4466	. . . . . . . . . . . . . . . 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 11281	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. RR )
162	161	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> C e. RR )
163		reexpcl 12186	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( u e. RR /\ 3 e. NN0 ) -> ( u ^ 3 ) e. RR )
164	111, 15, 163	sylancl 662	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u ^ 3 ) e. RR )
165	162, 164	remulcld 9641	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( u ^ 3 ) ) e. RR )
166	111, 165	resubcld 10008	. . . . . . . . . . . . . . . . . 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 12330	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( sup ( T , RR , `' < ) ^ 3 ) e. RR )
169	162, 168	remulcld 9641	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. RR )
170	114, 169	resubcld 10008	. . . . . . . . . . . . . . . . . 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 13277	. . . . . . . . . . . . . . . . 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 9639	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( C x. ( sup ( T , RR , `' < ) ^ 3 ) ) e. CC )
173	150, 172	npcand 9954	. . . . . . . . . . . . . . . . . . . 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 4468	. . . . . . . . . . . . . . . . . . 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 753	. . . . . . . . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )
178		infmrlb 10544	. . . . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) /\ u e. T ) -> sup ( T , RR , `' < ) <_ ( u - ( C x. ( u ^ 3 ) ) ) )
180	114, 166	lenltd 9748	. . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . 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 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> T =/= (/) )
190	83	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 0 < sup ( T , RR , `' < ) ) /\ s e. RR+ ) -> E. x e. RR A. w e. T x <_ w )
191		infmrgelb 10543	. . . . . . . . . . . . . 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 1231	. . . . . . . . . . . . 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 44	. . . . . . . . . . 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 2913	. . . . . . . . 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 576	. . . . . . . 8 |- ( ph -> -. 0 < sup ( T , RR , `' < ) )
198	197	adantr 465	. . . . . . 7 |- ( ( ph /\ s e. RR+ ) -> -. 0 < sup ( T , RR , `' < ) )
199	30	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> T C_ RR )
200	68	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> T =/= (/) )
201	83	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> E. x e. RR A. w e. T x <_ w )
202	133	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> s e. RR )
203		infmrgelb 10543	. . . . . . . . . 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 1231	. . . . . . . . 9 |- ( ( ph /\ s e. RR+ ) -> ( s <_ sup ( T , RR , `' < ) <-> A. w e. T s <_ w ) )
205	22	raleqi 3058	. . . . . . . . . 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 4460	. . . . . . . . . . 11 |- ( w = t -> ( s <_ w <-> s <_ t ) )
207	206	ralrab2 3265	. . . . . . . . . 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 11256	. . . . . . . . . 10 |- ( s e. RR+ -> 0 < s )
211	210	adantl 466	. . . . . . . . 9 |- ( ( ph /\ s e. RR+ ) -> 0 < s )
212		0red 9614	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> 0 e. RR )
213	85	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. RR+ ) -> sup ( T , RR , `' < ) e. RR )
214		ltletr 9693	. . . . . . . . . 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 1228	. . . . . . . . 9 |- ( ( ph /\ s e. RR+ ) -> ( ( 0 < s /\ s <_ sup ( T , RR , `' < ) ) -> 0 < sup ( T , RR , `' < ) ) )
216	211, 215	mpand 675	. . . . . . . 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 2910	. . . . . 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 5872	. . . . . . . . . . . . . . 15 |- ( z = x -> ( R ` z ) = ( R ` x ) )
222		id 22	. . . . . . . . . . . . . . 15 |- ( z = x -> z = x )
223	221, 222	oveq12d 6314	. . . . . . . . . . . . . 14 |- ( z = x -> ( ( R ` z ) / z ) = ( ( R ` x ) / x ) )
224	223	fveq2d 5876	. . . . . . . . . . . . 13 |- ( z = x -> ( abs ` ( ( R ` z ) / z ) ) = ( abs ` ( ( R ` x ) / x ) ) )
225	224	breq1d 4466	. . . . . . . . . . . 12 |- ( z = x -> ( ( abs ` ( ( R ` z ) / z ) ) <_ t <-> ( abs ` ( ( R ` x ) / x ) ) <_ t ) )
226	225	cbvralv 3084	. . . . . . . . . . 11 |- ( A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t <-> A. x e. ( y [,) +oo ) ( abs ` ( ( R ` x ) / x ) ) <_ t )
227		rpre 11251	. . . . . . . . . . . . . . . . 17 |- ( x e. RR+ -> x e. RR )
228	227	ad2antll 728	. . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . 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 11281	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> y e. RR )
232		elicopnf 11645	. . . . . . . . . . . . . . . . 17 |- ( y e. RR -> ( x e. ( y [,) +oo ) <-> ( x e. RR /\ y <_ x ) ) )
233	231, 232	syl 16	. . . . . . . . . . . . . . . 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 922	. . . . . . . . . . . . . . 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 23873	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. RR+ -> ( R ` x ) = ( (ψ ` x ) - x ) )
237	236	ad2antll 728	. . . . . . . . . . . . . . . . . . . 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 6311	. . . . . . . . . . . . . . . . . . 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 23524	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> (ψ ` x ) e. RR )
240	228, 239	syl 16	. . . . . . . . . . . . . . . . . . . . 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 9639	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> (ψ ` x ) e. CC )
242		rpcn 11253	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. RR+ -> x e. CC )
243	242	ad2antll 728	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> x e. CC )
244		rpne0 11260	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. RR+ -> x =/= 0 )
245	244	ad2antll 728	. . . . . . . . . . . . . . . . . . . 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 10380	. . . . . . . . . . . . . . . . . . 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 10339	. . . . . . . . . . . . . . . . . . . 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 6312	. . . . . . . . . . . . . . . . . . 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 2503	. . . . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . . . . 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 4466	. . . . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> -. s <_ t )
253	252	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) /\ ( y <_ x /\ x e. RR+ ) ) -> -. s <_ t )
254	29	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) -> ( 0 [,] A ) C_ RR )
255	254	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 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 761	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ s e. RR+ ) /\ ( t e. ( 0 [,] A ) /\ -. s <_ t ) ) /\ y e. RR+ ) -> t e. ( 0 [,] A ) )
257	256	adantr 465	. . . . . . . . . . . . . . . . . . . 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 3500	. . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . 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 11281	. . . . . . . . . . . . . . . . . . 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 9749	. . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. RR+ -> (ψ ` x ) e. RR )
264		rerpdivcl 11272	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( (ψ ` x ) e. RR /\ x e. RR+ ) -> ( (ψ ` x ) / x ) e. RR )
265	263, 264	mpancom 669	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR+ -> ( (ψ ` x ) / x ) e. RR )
266	265	ad2antll 728	. . . . . . . . . . . . . . . . . . . . 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 9902	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( (ψ ` x ) / x ) e. RR /\ 1 e. RR ) -> ( ( (ψ ` x ) / x ) - 1 ) e. RR )
268	266, 38, 267	sylancl 662	. . . . . . . . . . . . . . . . . . . 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 9639	. . . . . . . . . . . . . . . . . . 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 13279	. . . . . . . . . . . . . . . . . 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 9692	. . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . 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 674	. . . . . . . . . . . . . . . 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 54	. . . . . . . . . . . . . 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 605	. . . . . . . . . . . . 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 2864	. . . . . . . . . . 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 2932	. . . . . . . . 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 648	. . . . . . . 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 440	. . . . . . 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 603	. . . . . 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 2949	. . . . 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 3561	. . . 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 63	. . 3 |- ( ( ph /\ s e. RR+ ) -> E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
288	287	ralrimiva 2871	. 2 |- ( ph -> A. s e. RR+ E. y e. RR A. x e. RR+ ( y <_ x -> ( abs ` ( ( (ψ ` x ) / x ) - 1 ) ) < s ) )
289	265	recnd 9639	. . . . 5 |- ( x e. RR+ -> ( (ψ ` x ) / x ) e. CC )
290	289	rgen 2817	. . . 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 9629	. . 3 |- ( ph -> 1 e. CC )
294	291, 292, 293	rlim2 13331	. 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 369   /\ w3a 973   = wceq 1395   e. wcel 1819   =/= wne 2652   A.wral 2807   E.wrex 2808   {crab 2811   C_ wss 3471   (/)c0 3793   class class class wbr 4456   |-> cmpt 4515   `'ccnv 5007   ` cfv 5594  (class class class)co 6296   supcsup 7918   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510   + caddc 9512   x. cmul 9514   +oocpnf 9642   RR*cxr 9644   < clt 9645   <_ cle 9646   - cmin 9824   / cdiv 10227   2c2 10606   3c3 10607   NN0cn0 10816   ZZcz 10885   RR+crp 11245   [,)cico 11556   [,]cicc 11557   ^cexp 12169   abscabs 13079   ~~> r crli 13320   TopOpenctopn 14839  ℂ_fldccnfld 18547   Cn ccn 19852   tX ctx 20187   -cn->ccncf 21506  ψcchp 23492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587  ax-addf 9588  ax-mulf 9589

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-ixp 7489  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-fi 7889  df-sup 7919  df-oi 7953  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-q 11208  df-rp 11246  df-xneg 11343  df-xadd 11344  df-xmul 11345  df-ioo 11558  df-ioc 11559  df-ico 11560  df-icc 11561  df-fz 11698  df-fzo 11822  df-fl 11932  df-mod 12000  df-seq 12111  df-exp 12170  df-fac 12357  df-bc 12384  df-hash 12409  df-shft 12912  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-limsup 13306  df-clim 13323  df-rlim 13324  df-sum 13521  df-ef 13815  df-sin 13817  df-cos 13818  df-pi 13820  df-dvds 13999  df-gcd 14157  df-prm 14230  df-pc 14373  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-starv 14727  df-sca 14728  df-vsca 14729  df-ip 14730  df-tset 14731  df-ple 14732  df-ds 14734  df-unif 14735  df-hom 14736  df-cco 14737  df-rest 14840  df-topn 14841  df-0g 14859  df-gsum 14860  df-topgen 14861  df-pt 14862  df-prds 14865  df-xrs 14919  df-qtop 14924  df-imas 14925  df-xps 14927  df-mre 15003  df-mrc 15004  df-acs 15006  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-submnd 16094  df-mulg 16187  df-cntz 16482  df-cmn 16927  df-psmet 18538  df-xmet 18539  df-met 18540  df-bl 18541  df-mopn 18542  df-fbas 18543  df-fg 18544  df-cnfld 18548  df-top 19526  df-bases 19528  df-topon 19529  df-topsp 19530  df-cld 19647  df-ntr 19648  df-cls 19649  df-nei 19726  df-lp 19764  df-perf 19765  df-cn 19855  df-cnp 19856  df-haus 19943  df-tx 20189  df-hmeo 20382  df-fil 20473  df-fm 20565  df-flim 20566  df-flf 20567  df-xms 20949  df-ms 20950  df-tms 20951  df-cncf 21508  df-limc 22396  df-dv 22397  df-log 23070  df-vma 23497  df-chp 23498

This theorem is referenced by:  pntleml  23922