Metamath Proof Explorer

Theorem supsubc

Description: The supremum function distributes over subtraction in a sense similar to that in supaddc . (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses supsubc.a1 ⊢φ→A⊆ℝ
supsubc.a2 ⊢φ→A≠∅
supsubc.a3 ⊢φ→∃x∈ℝ∀y∈Ay≤x
supsubc.b ⊢φ→B∈ℝ
supsubc.c ⊢C=z|∃v∈Az=v−B
Assertion supsubc ⊢φ→supAℝ<−B=supCℝ<

Proof

Step Hyp Ref Expression
1 supsubc.a1 ⊢φ→A⊆ℝ
2 supsubc.a2 ⊢φ→A≠∅
3 supsubc.a3 ⊢φ→∃x∈ℝ∀y∈Ay≤x
4 supsubc.b ⊢φ→B∈ℝ
5 supsubc.c ⊢C=z|∃v∈Az=v−B
6 5 a1i ⊢φ→C=z|∃v∈Az=v−B
7 1 sselda ⊢φ∧v∈A→v∈ℝ
8 7 recnd ⊢φ∧v∈A→v∈ℂ
9 4 recnd ⊢φ→B∈ℂ
10 9 adantr ⊢φ∧v∈A→B∈ℂ
11 8 10 negsubd ⊢φ∧v∈A→v+−B=v−B
12 11 eqcomd ⊢φ∧v∈A→v−B=v+−B
13 12 eqeq2d ⊢φ∧v∈A→z=v−B↔z=v+−B
14 13 rexbidva ⊢φ→∃v∈Az=v−B↔∃v∈Az=v+−B
15 14 abbidv ⊢φ→z|∃v∈Az=v−B=z|∃v∈Az=v+−B
16 eqidd ⊢φ→z|∃v∈Az=v+−B=z|∃v∈Az=v+−B
17 6 15 16 3eqtrd ⊢φ→C=z|∃v∈Az=v+−B
18 17 supeq1d ⊢φ→supCℝ<=supz|∃v∈Az=v+−Bℝ<
19 4 renegcld ⊢φ→−B∈ℝ
20 eqid ⊢z|∃v∈Az=v+−B=z|∃v∈Az=v+−B
21 1 2 3 19 20 supaddc ⊢φ→supAℝ<+−B=supz|∃v∈Az=v+−Bℝ<
22 21 eqcomd ⊢φ→supz|∃v∈Az=v+−Bℝ<=supAℝ<+−B
23 suprcl ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x→supAℝ<∈ℝ
24 1 2 3 23 syl3anc ⊢φ→supAℝ<∈ℝ
25 24 recnd ⊢φ→supAℝ<∈ℂ
26 25 9 negsubd ⊢φ→supAℝ<+−B=supAℝ<−B
27 18 22 26 3eqtrrd ⊢φ→supAℝ<−B=supCℝ<