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
|
syl6bb |
|- ( 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
|
syl6bb |
|- ( 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
|
ffvelrnda |
|- ( ( 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
|
syl6bb |
|- ( 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
|
syl6bb |
|- ( 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 ) ) |