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∈Ay≤B
Assertion infnsuprnmpt ⊢φ→supran⁡x∈A⟼Bℝ<=−supran⁡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∈Ay≤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⟼By≤z
9 infrenegsup ⊢ran⁡x∈A⟼B⊆ℝ∧ran⁡x∈A⟼B≠∅∧∃y∈ℝ∀z∈ran⁡x∈A⟼By≤z→supran⁡x∈A⟼Bℝ<=−supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<
10 6 7 8 9 syl3anc ⊢φ→supran⁡x∈A⟼Bℝ<=−supw∈ℝ|−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 ⊢Ⅎ_xw
19 18 nfneg ⊢Ⅎ_x−w
20 nfmpt1 ⊢Ⅎ_xx∈A⟼B
21 20 nfrn ⊢Ⅎ_xran⁡x∈A⟼B
22 19 21 nfel ⊢Ⅎx−w∈ran⁡x∈A⟼B
23 nfcv ⊢Ⅎ_xℝ
24 22 23 nfrabw ⊢Ⅎ_xw∈ℝ|−w∈ran⁡x∈A⟼B
25 18 24 nfel ⊢Ⅎxw∈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∈Aw=−B
40 17 39 mpd ⊢φ∧w∈w∈ℝ|−w∈ran⁡x∈A⟼B→∃x∈Aw=−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∈Aw=−B
46 44 45 ax-mp ⊢w∈ran⁡x∈A⟼−B↔∃x∈Aw=−B
47 46 biimpi ⊢w∈ran⁡x∈A⟼−B→∃x∈Aw=−B
48 47 adantl ⊢φ∧w∈ran⁡x∈A⟼−B→∃x∈Aw=−B
49 18 23 nfel ⊢Ⅎxw∈ℝ
50 49 22 nfan ⊢Ⅎxw∈ℝ∧−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∈Aw=−B→w∈ℝ∧−w∈ran⁡x∈A⟼B
68 67 imp ⊢φ∧∃x∈Aw=−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 ⊢φ→∀ww∈w∈ℝ|−w∈ran⁡x∈A⟼B↔w∈ran⁡x∈A⟼−B
75 nfrab1 ⊢Ⅎ_ww∈ℝ|−w∈ran⁡x∈A⟼B
76 nfcv ⊢Ⅎ_wran⁡x∈A⟼−B
77 75 76 cleqf ⊢w∈ℝ|−w∈ran⁡x∈A⟼B=ran⁡x∈A⟼−B↔∀ww∈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 ⊢φ→supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<=supran⁡x∈A⟼−Bℝ<
80 79 negeqd ⊢φ→−supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<=−supran⁡x∈A⟼−Bℝ<
81 eqidd ⊢φ→−supran⁡x∈A⟼−Bℝ<=−supran⁡x∈A⟼−Bℝ<
82 10 80 81 3eqtrd ⊢φ→supran⁡x∈A⟼Bℝ<=−supran⁡x∈A⟼−Bℝ<