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 𝑥 𝜑
infnsuprnmpt.a ( 𝜑𝐴 ≠ ∅ )
infnsuprnmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
infnsuprnmpt.l ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝑦𝐵 )
Assertion infnsuprnmpt ( 𝜑 → inf ( ran ( 𝑥𝐴𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑥𝐴 ↦ - 𝐵 ) , ℝ , < ) )

Proof

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