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 bilani ⊢ φ ∧ w ∈ ran ⁡ x ∈ A ⟼ − B → ∃ x ∈ A w = − B
48 18 23 nfel ⊢ Ⅎ x w ∈ ℝ
49 48 22 nfan ⊢ Ⅎ x w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
50 simp3 ⊢ φ ∧ x ∈ A ∧ w = − B → w = − B
51 3 renegcld ⊢ φ ∧ x ∈ A → − B ∈ ℝ
52 51 3adant3 ⊢ φ ∧ x ∈ A ∧ w = − B → − B ∈ ℝ
53 50 52 eqeltrd ⊢ φ ∧ x ∈ A ∧ w = − B → w ∈ ℝ
54 simp2 ⊢ φ ∧ x ∈ A ∧ w = − B → x ∈ A
55 50 negeqd ⊢ φ ∧ x ∈ A ∧ w = − B → − w = − − B
56 3 recnd ⊢ φ ∧ x ∈ A → B ∈ ℂ
57 56 negnegd ⊢ φ ∧ x ∈ A → − − B = B
58 57 3adant3 ⊢ φ ∧ x ∈ A ∧ w = − B → − − B = B
59 55 58 eqtrd ⊢ φ ∧ x ∈ A ∧ w = − B → − w = B
60 rspe ⊢ x ∈ A ∧ − w = B → ∃ x ∈ A − w = B
61 54 59 60 syl2anc ⊢ φ ∧ x ∈ A ∧ w = − B → ∃ x ∈ A − w = B
62 14 a1i ⊢ φ ∧ x ∈ A ∧ w = − B → − w ∈ V
63 5 61 62 elrnmptd ⊢ φ ∧ x ∈ A ∧ w = − B → − w ∈ ran ⁡ x ∈ A ⟼ B
64 53 63 jca ⊢ φ ∧ x ∈ A ∧ w = − B → w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
65 64 3exp ⊢ φ → x ∈ A → w = − B → w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
66 1 49 65 rexlimd ⊢ φ → ∃ x ∈ A w = − B → w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
67 66 imp ⊢ φ ∧ ∃ x ∈ A w = − B → w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
68 47 67 syldan ⊢ φ ∧ w ∈ ran ⁡ x ∈ A ⟼ − B → w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
69 rabid ⊢ w ∈ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ↔ w ∈ ℝ ∧ − w ∈ ran ⁡ x ∈ A ⟼ B
70 68 69 sylibr ⊢ φ ∧ w ∈ ran ⁡ x ∈ A ⟼ − B → w ∈ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B
71 70 ex ⊢ φ → w ∈ ran ⁡ x ∈ A ⟼ − B → w ∈ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B
72 43 71 impbid ⊢ φ → w ∈ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ↔ w ∈ ran ⁡ x ∈ A ⟼ − B
73 72 alrimiv ⊢ φ → ∀ w w ∈ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ↔ w ∈ ran ⁡ x ∈ A ⟼ − B
74 nfrab1 ⊢ Ⅎ _ w w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B
75 nfcv ⊢ Ⅎ _ w ran ⁡ x ∈ A ⟼ − B
76 74 75 cleqf ⊢ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B = ran ⁡ x ∈ A ⟼ − B ↔ ∀ w w ∈ w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ↔ w ∈ ran ⁡ x ∈ A ⟼ − B
77 73 76 sylibr ⊢ φ → w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B = ran ⁡ x ∈ A ⟼ − B
78 77 supeq1d ⊢ φ → sup w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ℝ < = sup ran ⁡ x ∈ A ⟼ − B ℝ <
79 78 negeqd ⊢ φ → − sup w ∈ ℝ | − w ∈ ran ⁡ x ∈ A ⟼ B ℝ < = − sup ran ⁡ x ∈ A ⟼ − B ℝ <
80 eqidd ⊢ φ → − sup ran ⁡ x ∈ A ⟼ − B ℝ < = − sup ran ⁡ x ∈ A ⟼ − B ℝ <
81 10 79 80 3eqtrd ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ < = − sup ran ⁡ x ∈ A ⟼ − B ℝ <