Theorem lmxrge0 28807

Description: Express "sequence F converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.)

Hypotheses

Ref	Expression
lmxrge0.j	|- J = ( TopOpen ` ( RR*s ↾s ( 0 [,] +oo ) ) )
lmxrge0.6	|- ( ph -> F : NN --> ( 0 [,] +oo ) )
lmxrge0.7	|- ( ( ph /\ k e. NN ) -> ( F ` k ) = A )

Assertion

Ref	Expression
lmxrge0	|- ( ph -> ( F ( ~~> t ` J ) +oo <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )

Distinct variable groups:   x, j, A   j, k, F, x   k, J, x   ph, k, x

Allowed substitution hints:   ph( j)   A( k)   J( j)

Proof of Theorem lmxrge0

Dummy variables a l are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmxrge0.j	. . . . . . 7 |- J = ( TopOpen ` ( RR*s ↾s ( 0 [,] +oo ) ) )
2		eqid 2462	. . . . . . . 8 |- ( RR*s ↾s ( 0 [,] +oo ) ) = ( RR*s ↾s ( 0 [,] +oo ) )
3		xrstopn 20273	. . . . . . . 8 |- (ordTop ` <_ ) = ( TopOpen ` RR*s )
4	2, 3	resstopn 20251	. . . . . . 7 |- ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) ) = ( TopOpen ` ( RR*s ↾s ( 0 [,] +oo ) ) )
5	1, 4	eqtr4i 2487	. . . . . 6 |- J = ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) )
6		letopon 20270	. . . . . . 7 |- (ordTop ` <_ ) e. (TopOn ` RR* )
7		iccssxr 11746	. . . . . . 7 |- ( 0 [,] +oo ) C_ RR*
8		resttopon 20226	. . . . . . 7 |- ( ( (ordTop ` <_ ) e. (TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) ) e. (TopOn ` ( 0 [,] +oo ) ) )
9	6, 7, 8	mp2an 683	. . . . . 6 |- ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) ) e. (TopOn ` ( 0 [,] +oo ) )
10	5, 9	eqeltri 2536	. . . . 5 |- J e. (TopOn ` ( 0 [,] +oo ) )
11	10	a1i 11	. . . 4 |- ( ph -> J e. (TopOn ` ( 0 [,] +oo ) ) )
12		nnuz 11223	. . . 4 |- NN = ( ZZ>= ` 1 )
13		1zzd 10997	. . . 4 |- ( ph -> 1 e. ZZ )
14		lmxrge0.6	. . . 4 |- ( ph -> F : NN --> ( 0 [,] +oo ) )
15		lmxrge0.7	. . . 4 |- ( ( ph /\ k e. NN ) -> ( F ` k ) = A )
16	11, 12, 13, 14, 15	lmbrf 20325	. . 3 |- ( ph -> ( F ( ~~> t ` J ) +oo <-> ( +oo e. ( 0 [,] +oo ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) ) )
17		0xr 9713	. . . . 5 |- 0 e. RR*
18		pnfxr 11441	. . . . 5 |- +oo e. RR*
19		0lepnf 11462	. . . . 5 |- 0 <_ +oo
20		ubicc2 11778	. . . . 5 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
21	17, 18, 19, 20	mp3an 1373	. . . 4 |- +oo e. ( 0 [,] +oo )
22	21	biantrur 513	. . 3 |- ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) <-> ( +oo e. ( 0 [,] +oo ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) )
23	16, 22	syl6bbr 271	. 2 |- ( ph -> ( F ( ~~> t ` J ) +oo <-> A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) )
24		rexr 9712	. . . . . . . . . 10 |- ( x e. RR -> x e. RR* )
25	18	a1i 11	. . . . . . . . . 10 |- ( x e. RR -> +oo e. RR* )
26		ltpnf 11451	. . . . . . . . . 10 |- ( x e. RR -> x < +oo )
27		ubioc1 11717	. . . . . . . . . 10 |- ( ( x e. RR* /\ +oo e. RR* /\ x < +oo ) -> +oo e. ( x (,] +oo ) )
28	24, 25, 26, 27	syl3anc 1276	. . . . . . . . 9 |- ( x e. RR -> +oo e. ( x (,] +oo ) )
29		0ltpnf 11453	. . . . . . . . . 10 |- 0 < +oo
30		ubioc1 11717	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> +oo e. ( 0 (,] +oo ) )
31	17, 18, 29, 30	mp3an 1373	. . . . . . . . 9 |- +oo e. ( 0 (,] +oo )
32	28, 31	jctir 545	. . . . . . . 8 |- ( x e. RR -> ( +oo e. ( x (,] +oo ) /\ +oo e. ( 0 (,] +oo ) ) )
33		elin 3629	. . . . . . . 8 |- ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) <-> ( +oo e. ( x (,] +oo ) /\ +oo e. ( 0 (,] +oo ) ) )
34	32, 33	sylibr 217	. . . . . . 7 |- ( x e. RR -> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) )
35	34	ad2antlr 738	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) -> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) )
36		letop 20271	. . . . . . . . . . 11 |- (ordTop ` <_ ) e. Top
37		ovex 6343	. . . . . . . . . . 11 |- ( 0 [,] +oo ) e. _V
38		iocpnfordt 20280	. . . . . . . . . . . 12 |- ( x (,] +oo ) e. (ordTop ` <_ )
39		iocpnfordt 20280	. . . . . . . . . . . 12 |- ( 0 (,] +oo ) e. (ordTop ` <_ )
40		inopn 19978	. . . . . . . . . . . 12 |- ( ( (ordTop ` <_ ) e. Top /\ ( x (,] +oo ) e. (ordTop ` <_ ) /\ ( 0 (,] +oo ) e. (ordTop ` <_ ) ) -> ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. (ordTop ` <_ ) )
41	36, 38, 39, 40	mp3an 1373	. . . . . . . . . . 11 |- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. (ordTop ` <_ )
42		elrestr 15376	. . . . . . . . . . 11 |- ( ( (ordTop ` <_ ) e. Top /\ ( 0 [,] +oo ) e. _V /\ ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. (ordTop ` <_ ) ) -> ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) ) e. ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) ) )
43	36, 37, 41, 42	mp3an 1373	. . . . . . . . . 10 |- ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) ) e. ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) )
44		inss2 3665	. . . . . . . . . . . . 13 |- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( 0 (,] +oo )
45		iocssicc 11751	. . . . . . . . . . . . 13 |- ( 0 (,] +oo ) C_ ( 0 [,] +oo )
46	44, 45	sstri 3453	. . . . . . . . . . . 12 |- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( 0 [,] +oo )
47		sseqin2 3663	. . . . . . . . . . . 12 |- ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( 0 [,] +oo ) <-> ( ( 0 [,] +oo ) i^i ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) )
48	46, 47	mpbi 213	. . . . . . . . . . 11 |- ( ( 0 [,] +oo ) i^i ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) )
49		incom 3637	. . . . . . . . . . 11 |- ( ( 0 [,] +oo ) i^i ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) = ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) )
50	48, 49	eqtr3i 2486	. . . . . . . . . 10 |- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) = ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) )
51	43, 50, 5	3eltr4i 2553	. . . . . . . . 9 |- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. J
52	51	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. J )
53		eleq2 2529	. . . . . . . . . . 11 |- ( a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> ( +oo e. a <-> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) )
54	53	adantl 472	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( +oo e. a <-> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) )
55	54	biimprd 231	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> +oo e. a ) )
56		simp-5r 784	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> x e. RR )
57	56	rexrd 9716	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> x e. RR* )
58		simpr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> A e. a )
59		simp-4r 782	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) )
60	58, 59	eleqtrd 2542	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> A e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) )
61		elin 3629	. . . . . . . . . . . . . . . 16 |- ( A e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) <-> ( A e. ( x (,] +oo ) /\ A e. ( 0 (,] +oo ) ) )
62	61	simplbi 466	. . . . . . . . . . . . . . 15 |- ( A e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> A e. ( x (,] +oo ) )
63	60, 62	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> A e. ( x (,] +oo ) )
64		elioc1 11707	. . . . . . . . . . . . . . . . 17 |- ( ( x e. RR* /\ +oo e. RR* ) -> ( A e. ( x (,] +oo ) <-> ( A e. RR* /\ x < A /\ A <_ +oo ) ) )
65	18, 64	mpan2 682	. . . . . . . . . . . . . . . 16 |- ( x e. RR* -> ( A e. ( x (,] +oo ) <-> ( A e. RR* /\ x < A /\ A <_ +oo ) ) )
66	65	biimpa 491	. . . . . . . . . . . . . . 15 |- ( ( x e. RR* /\ A e. ( x (,] +oo ) ) -> ( A e. RR* /\ x < A /\ A <_ +oo ) )
67	66	simp2d 1027	. . . . . . . . . . . . . 14 |- ( ( x e. RR* /\ A e. ( x (,] +oo ) ) -> x < A )
68	57, 63, 67	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> x < A )
69	68	ex 440	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( A e. a -> x < A ) )
70	69	ralimdva 2808	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) -> ( A. k e. ( ZZ>= ` l ) A e. a -> A. k e. ( ZZ>= ` l ) x < A ) )
71	70	reximdva 2874	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( E. l e. NN A. k e. ( ZZ>= ` l ) A e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) x < A ) )
72		fveq2 5888	. . . . . . . . . . . 12 |- ( j = l -> ( ZZ>= ` j ) = ( ZZ>= ` l ) )
73	72	raleqdv 3005	. . . . . . . . . . 11 |- ( j = l -> ( A. k e. ( ZZ>= ` j ) x < A <-> A. k e. ( ZZ>= ` l ) x < A ) )
74	73	cbvrexv 3032	. . . . . . . . . 10 |- ( E. j e. NN A. k e. ( ZZ>= ` j ) x < A <-> E. l e. NN A. k e. ( ZZ>= ` l ) x < A )
75	71, 74	syl6ibr 235	. . . . . . . . 9 |- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( E. l e. NN A. k e. ( ZZ>= ` l ) A e. a -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )
76	55, 75	imim12d 77	. . . . . . . 8 |- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) )
77	52, 76	rspcimdv 3163	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) )
78	77	imp 435	. . . . . 6 |- ( ( ( ph /\ x e. RR ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )
79	35, 78	mpd 15	. . . . 5 |- ( ( ( ph /\ x e. RR ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A )
80	79	ex 440	. . . 4 |- ( ( ph /\ x e. RR ) -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )
81	80	ralrimdva 2818	. . 3 |- ( ph -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )
82		simplll 773	. . . . . 6 |- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> ph )
83		simpllr 774	. . . . . . 7 |- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> a e. J )
84		simpr 467	. . . . . . 7 |- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> +oo e. a )
85	1	pnfneige0 28806	. . . . . . 7 |- ( ( a e. J /\ +oo e. a ) -> E. x e. RR ( x (,] +oo ) C_ a )
86	83, 84, 85	syl2anc 671	. . . . . 6 |- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> E. x e. RR ( x (,] +oo ) C_ a )
87		simplr 767	. . . . . 6 |- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A )
88		r19.29r 2938	. . . . . . . 8 |- ( ( E. x e. RR ( x (,] +oo ) C_ a /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. x e. RR ( ( x (,] +oo ) C_ a /\ E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )
89		simp-4l 781	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ph )
90		uznnssnn 11235	. . . . . . . . . . . . . . . . 17 |- ( l e. NN -> ( ZZ>= ` l ) C_ NN )
91	90	ad2antlr 738	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( ZZ>= ` l ) C_ NN )
92		simpr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> k e. ( ZZ>= ` l ) )
93	91, 92	sseldd 3445	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> k e. NN )
94	89, 93	jca 539	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( ph /\ k e. NN ) )
95		simp-4r 782	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> x e. RR )
96		simpllr 774	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( x (,] +oo ) C_ a )
97		simplr 767	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ x < A ) -> ( x (,] +oo ) C_ a )
98		simplr 767	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> x e. RR )
99	98	rexrd 9716	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> x e. RR* )
100	14	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( 0 [,] +oo ) )
101	15, 100	eqeltrrd 2541	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
102	7, 101	sseldi 3442	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN ) -> A e. RR* )
103	102	ad2antrr 737	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> A e. RR* )
104		simpr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> x < A )
105		pnfge 11461	. . . . . . . . . . . . . . . . . . 19 |- ( A e. RR* -> A <_ +oo )
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> A <_ +oo )
107	65	biimpar 492	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. RR* /\ ( A e. RR* /\ x < A /\ A <_ +oo ) ) -> A e. ( x (,] +oo ) )
108	99, 103, 104, 106, 107	syl13anc 1278	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> A e. ( x (,] +oo ) )
109	108	adantlr 726	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ x < A ) -> A e. ( x (,] +oo ) )
110	97, 109	sseldd 3445	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ x < A ) -> A e. a )
111	110	ex 440	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) -> ( x < A -> A e. a ) )
112	94, 95, 96, 111	syl21anc 1275	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( x < A -> A e. a ) )
113	112	ralimdva 2808	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) -> ( A. k e. ( ZZ>= ` l ) x < A -> A. k e. ( ZZ>= ` l ) A e. a ) )
114	113	reximdva 2874	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) -> ( E. l e. NN A. k e. ( ZZ>= ` l ) x < A -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) )
115	74, 114	syl5bi 225	. . . . . . . . . 10 |- ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) x < A -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) )
116	115	expimpd 612	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( ( ( x (,] +oo ) C_ a /\ E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) )
117	116	rexlimdva 2891	. . . . . . . 8 |- ( ph -> ( E. x e. RR ( ( x (,] +oo ) C_ a /\ E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) )
118	88, 117	syl5 33	. . . . . . 7 |- ( ph -> ( ( E. x e. RR ( x (,] +oo ) C_ a /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) )
119	118	imp 435	. . . . . 6 |- ( ( ph /\ ( E. x e. RR ( x (,] +oo ) C_ a /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a )
120	82, 86, 87, 119	syl12anc 1274	. . . . 5 |- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a )
121	120	exp31 613	. . . 4 |- ( ( ph /\ a e. J ) -> ( A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A -> ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) )
122	121	ralrimdva 2818	. . 3 |- ( ph -> ( A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A -> A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) )
123	81, 122	impbid 195	. 2 |- ( ph -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )
124	23, 123	bitrd 261	1 |- ( ph -> ( F ( ~~> t ` J ) +oo <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   _Vcvv 3057   i^i cin 3415   C_ wss 3416   class class class wbr 4416   -->wf 5597   ` cfv 5601  (class class class)co 6315   RRcr 9564   0cc0 9565   1c1 9566   +oocpnf 9698   RR*cxr 9700   < clt 9701   <_ cle 9702   NNcn 10637   ZZ>=cuz 11188   (,]cioc 11665   [,]cicc 11667   ↾_s cress 15171   ↾_t crest 15368   TopOpenctopn 15369  ordTopcordt 15446   RR*scxrs 15447   Topctop 19966  TopOnctopon 19967   ~~> tclm 20291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fi 7951  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-ioo 11668  df-ioc 11669  df-ico 11670  df-icc 11671  df-fz 11814  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-tset 15258  df-ple 15259  df-ds 15261  df-rest 15370  df-topn 15371  df-topgen 15391  df-ordt 15448  df-xrs 15449  df-ps 16495  df-tsr 16496  df-top 19970  df-bases 19971  df-topon 19972  df-lm 20294

This theorem is referenced by:  lmdvglim  28809