xlimpnfxnegmnf

Description: A sequence converges to +oo if and only if its negation converges to -oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	xlimpnfxnegmnf.1	\|- F/_ j F
	xlimpnfxnegmnf.2	\|- Z = ( ZZ>= ` M )
	xlimpnfxnegmnf.3	\|- ( ph -> F : Z --> RR* )
Assertion	xlimpnfxnegmnf	\|- ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )

Proof

Step	Hyp	Ref	Expression
1		xlimpnfxnegmnf.1	\|- F/_ j F
2		xlimpnfxnegmnf.2	\|- Z = ( ZZ>= ` M )
3		xlimpnfxnegmnf.3	\|- ( ph -> F : Z --> RR* )
4		breq1	\|- ( x = y -> ( x <_ ( F ` j ) <-> y <_ ( F ` j ) ) )
5	4	rexralbidv	\|- ( x = y -> ( E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> E. k e. Z A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) ) )
6		fveq2	\|- ( k = i -> ( ZZ>= ` k ) = ( ZZ>= ` i ) )
7	6	raleqdv	\|- ( k = i -> ( A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) <-> A. j e. ( ZZ>= ` i ) y <_ ( F ` j ) ) )
8		nfv	\|- F/ l y <_ ( F ` j )
9		nfcv	\|- F/_ j y
10		nfcv	\|- F/_ j <_
11		nfcv	\|- F/_ j l
12	1 11	nffv	\|- F/_ j ( F ` l )
13	9 10 12	nfbr	\|- F/ j y <_ ( F ` l )
14		fveq2	\|- ( j = l -> ( F ` j ) = ( F ` l ) )
15	14	breq2d	\|- ( j = l -> ( y <_ ( F ` j ) <-> y <_ ( F ` l ) ) )
16	8 13 15	cbvralw	\|- ( A. j e. ( ZZ>= ` i ) y <_ ( F ` j ) <-> A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
17	7 16	bitrdi	\|- ( k = i -> ( A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) <-> A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
18	17	cbvrexvw	\|- ( E. k e. Z A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
19	5 18	bitrdi	\|- ( x = y -> ( E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
20	19	cbvralvw	\|- ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
21	20	a1i	\|- ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
22		simpll	\|- ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> ph )
23		simpr	\|- ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> w e. RR )
24		xnegrecl	\|- ( w e. RR -> -e w e. RR )
25		simpl	\|- ( ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ w e. RR ) -> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
26		breq1	\|- ( y = -e w -> ( y <_ ( F ` l ) <-> -e w <_ ( F ` l ) ) )
27	26	rexralbidv	\|- ( y = -e w -> ( E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) ) )
28	27	rspcva	\|- ( ( -e w e. RR /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) )
29	24 25 28	syl2an2	\|- ( ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ w e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) )
30	29	adantll	\|- ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) )
31		simpll	\|- ( ( ( ( ph /\ w e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( ph /\ w e. RR ) )
32	2	uztrn2	\|- ( ( i e. Z /\ l e. ( ZZ>= ` i ) ) -> l e. Z )
33	32	adantll	\|- ( ( ( ( ph /\ w e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> l e. Z )
34		rexr	\|- ( w e. RR -> w e. RR* )
35	34	ad2antlr	\|- ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> w e. RR* )
36	3	ffvelcdmda	\|- ( ( ph /\ l e. Z ) -> ( F ` l ) e. RR* )
37	36	adantlr	\|- ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> ( F ` l ) e. RR* )
38		xlenegcon1	\|- ( ( w e. RR* /\ ( F ` l ) e. RR* ) -> ( -e w <_ ( F ` l ) <-> -e ( F ` l ) <_ w ) )
39	35 37 38	syl2anc	\|- ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> ( -e w <_ ( F ` l ) <-> -e ( F ` l ) <_ w ) )
40	39	biimpd	\|- ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> ( -e w <_ ( F ` l ) -> -e ( F ` l ) <_ w ) )
41	31 33 40	syl2anc	\|- ( ( ( ( ph /\ w e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( -e w <_ ( F ` l ) -> -e ( F ` l ) <_ w ) )
42	41	ralimdva	\|- ( ( ( ph /\ w e. RR ) /\ i e. Z ) -> ( A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) -> A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) )
43	42	reximdva	\|- ( ( ph /\ w e. RR ) -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) )
44	43	imp	\|- ( ( ( ph /\ w e. RR ) /\ E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
45	22 23 30 44	syl21anc	\|- ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
46	45	ralrimiva	\|- ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) -> A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
47		simpll	\|- ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> ph )
48		simpr	\|- ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> y e. RR )
49		xnegrecl	\|- ( y e. RR -> -e y e. RR )
50		simpl	\|- ( ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w /\ y e. RR ) -> A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
51		breq2	\|- ( w = -e y -> ( -e ( F ` l ) <_ w <-> -e ( F ` l ) <_ -e y ) )
52	51	rexralbidv	\|- ( w = -e y -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y ) )
53	52	rspcva	\|- ( ( -e y e. RR /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y )
54	49 50 53	syl2an2	\|- ( ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w /\ y e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y )
55	54	adantll	\|- ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y )
56		simpll	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( ph /\ y e. RR ) )
57	32	adantll	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> l e. Z )
58		rexr	\|- ( y e. RR -> y e. RR* )
59	58	ad2antlr	\|- ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> y e. RR* )
60	36	adantlr	\|- ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> ( F ` l ) e. RR* )
61		xleneg	\|- ( ( y e. RR* /\ ( F ` l ) e. RR* ) -> ( y <_ ( F ` l ) <-> -e ( F ` l ) <_ -e y ) )
62	59 60 61	syl2anc	\|- ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> ( y <_ ( F ` l ) <-> -e ( F ` l ) <_ -e y ) )
63	62	biimprd	\|- ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> ( -e ( F ` l ) <_ -e y -> y <_ ( F ` l ) ) )
64	56 57 63	syl2anc	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( -e ( F ` l ) <_ -e y -> y <_ ( F ` l ) ) )
65	64	ralimdva	\|- ( ( ( ph /\ y e. RR ) /\ i e. Z ) -> ( A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y -> A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
66	65	reximdva	\|- ( ( ph /\ y e. RR ) -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y -> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
67	66	imp	\|- ( ( ( ph /\ y e. RR ) /\ E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y ) -> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
68	47 48 55 67	syl21anc	\|- ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
69	68	ralrimiva	\|- ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) -> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
70	46 69	impbida	\|- ( ph -> ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) )
71		breq2	\|- ( w = x -> ( -e ( F ` l ) <_ w <-> -e ( F ` l ) <_ x ) )
72	71	rexralbidv	\|- ( w = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x ) )
73		fveq2	\|- ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
74	73	raleqdv	\|- ( i = k -> ( A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` k ) -e ( F ` l ) <_ x ) )
75	12	nfxneg	\|- F/_ j -e ( F ` l )
76		nfcv	\|- F/_ j x
77	75 10 76	nfbr	\|- F/ j -e ( F ` l ) <_ x
78		nfv	\|- F/ l -e ( F ` j ) <_ x
79		fveq2	\|- ( l = j -> ( F ` l ) = ( F ` j ) )
80	79	xnegeqd	\|- ( l = j -> -e ( F ` l ) = -e ( F ` j ) )
81	80	breq1d	\|- ( l = j -> ( -e ( F ` l ) <_ x <-> -e ( F ` j ) <_ x ) )
82	77 78 81	cbvralw	\|- ( A. l e. ( ZZ>= ` k ) -e ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
83	74 82	bitrdi	\|- ( i = k -> ( A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
84	83	cbvrexvw	\|- ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
85	72 84	bitrdi	\|- ( w = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
86	85	cbvralvw	\|- ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
87	86	a1i	\|- ( ph -> ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
88	21 70 87	3bitrd	\|- ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )

Metamath Proof Explorer

Theorem xlimpnfxnegmnf

Proof