Metamath Proof Explorer


Theorem infnsuprnmpt

Description: The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infnsuprnmpt.x x φ
infnsuprnmpt.a φ A
infnsuprnmpt.b φ x A B
infnsuprnmpt.l φ y x A y B
Assertion infnsuprnmpt φ sup ran x A B < = sup ran x A B <

Proof

Step Hyp Ref Expression
1 infnsuprnmpt.x x φ
2 infnsuprnmpt.a φ A
3 infnsuprnmpt.b φ x A B
4 infnsuprnmpt.l φ y x A y B
5 eqid x A B = x A B
6 1 5 3 rnmptssd φ ran x A B
7 1 3 5 2 rnmptn0 φ ran x A B
8 4 rnmptlb φ y z ran x A B y z
9 infrenegsup ran x A B ran x A B y z ran x A B y z sup ran x A B < = sup w | w ran x A B <
10 6 7 8 9 syl3anc φ sup ran x A B < = sup w | w ran x A B <
11 eqid x A B = x A B
12 rabidim2 w w | w ran x A B w ran x A B
13 12 adantl φ w w | w ran x A B w ran x A B
14 negex w V
15 5 elrnmpt w V w ran x A B x A w = B
16 14 15 ax-mp w ran x A B x A w = B
17 13 16 sylib φ w w | w ran x A B x A w = B
18 nfcv _ x w
19 18 nfneg _ x w
20 nfmpt1 _ x x A B
21 20 nfrn _ x ran x A B
22 19 21 nfel x w ran x A B
23 nfcv _ x
24 22 23 nfrabw _ x w | w ran x A B
25 18 24 nfel x w w | w ran x A B
26 1 25 nfan x φ w w | w ran x A B
27 rabidim1 w w | w ran x A B w
28 27 adantl φ w w | w ran x A B w
29 negeq w = B w = B
30 29 eqcomd w = B B = w
31 30 3ad2ant3 φ w x A w = B B = w
32 simp1r φ w x A w = B w
33 recn w w
34 33 negnegd w w = w
35 32 34 syl φ w x A w = B w = w
36 31 35 eqtr2d φ w x A w = B w = B
37 36 3exp φ w x A w = B w = B
38 28 37 syldan φ w w | w ran x A B x A w = B w = B
39 26 38 reximdai φ w w | w ran x A B x A w = B x A w = B
40 17 39 mpd φ w w | w ran x A B x A w = B
41 simpr φ w w | w ran x A B w w | w ran x A B
42 11 40 41 elrnmptd φ w w | w ran x A B w ran x A B
43 42 ex φ w w | w ran x A B w ran x A B
44 vex w V
45 11 elrnmpt w V w ran x A B x A w = B
46 44 45 ax-mp w ran x A B x A w = B
47 46 biimpi w ran x A B x A w = B
48 47 adantl φ w ran x A B x A w = B
49 18 23 nfel x w
50 49 22 nfan x w w ran x A B
51 simp3 φ x A w = B w = B
52 3 renegcld φ x A B
53 52 3adant3 φ x A w = B B
54 51 53 eqeltrd φ x A w = B w
55 simp2 φ x A w = B x A
56 51 negeqd φ x A w = B w = B
57 3 recnd φ x A B
58 57 negnegd φ x A B = B
59 58 3adant3 φ x A w = B B = B
60 56 59 eqtrd φ x A w = B w = B
61 rspe x A w = B x A w = B
62 55 60 61 syl2anc φ x A w = B x A w = B
63 14 a1i φ x A w = B w V
64 5 62 63 elrnmptd φ x A w = B w ran x A B
65 54 64 jca φ x A w = B w w ran x A B
66 65 3exp φ x A w = B w w ran x A B
67 1 50 66 rexlimd φ x A w = B w w ran x A B
68 67 imp φ x A w = B w w ran x A B
69 48 68 syldan φ w ran x A B w w ran x A B
70 rabid w w | w ran x A B w w ran x A B
71 69 70 sylibr φ w ran x A B w w | w ran x A B
72 71 ex φ w ran x A B w w | w ran x A B
73 43 72 impbid φ w w | w ran x A B w ran x A B
74 73 alrimiv φ w w w | w ran x A B w ran x A B
75 nfrab1 _ w w | w ran x A B
76 nfcv _ w ran x A B
77 75 76 cleqf w | w ran x A B = ran x A B w w w | w ran x A B w ran x A B
78 74 77 sylibr φ w | w ran x A B = ran x A B
79 78 supeq1d φ sup w | w ran x A B < = sup ran x A B <
80 79 negeqd φ sup w | w ran x A B < = sup ran x A B <
81 eqidd φ sup ran x A B < = sup ran x A B <
82 10 80 81 3eqtrd φ sup ran x A B < = sup ran x A B <