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 ⊢ φ → inf 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 → inf ran ⁡ x ∈ A ⟼ B ℝ < = − sup w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ℝ <
10 6 7 8 9 syl3anc ⊢ φ → inf 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 ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ < = − sup ran ⁡ x ∈ A ⟼ − B ℝ <