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 ∈ A y ≤ x
supsubc.b ⊢ φ → B ∈ ℝ
supsubc.c ⊢ C = z | ∃ v ∈ A z = v − B
Assertion supsubc ⊢ φ → sup A ℝ < − B = sup C ℝ <

Proof

Step Hyp Ref Expression
1 supsubc.a1 ⊢ φ → A ⊆ ℝ
2 supsubc.a2 ⊢ φ → A ≠ ∅
3 supsubc.a3 ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
4 supsubc.b ⊢ φ → B ∈ ℝ
5 supsubc.c ⊢ C = z | ∃ v ∈ A z = v − B
6 5 a1i ⊢ φ → C = z | ∃ v ∈ A z = 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 ∈ A z = v − B ↔ ∃ v ∈ A z = v + − B
15 14 abbidv ⊢ φ → z | ∃ v ∈ A z = v − B = z | ∃ v ∈ A z = v + − B
16 eqidd ⊢ φ → z | ∃ v ∈ A z = v + − B = z | ∃ v ∈ A z = v + − B
17 6 15 16 3eqtrd ⊢ φ → C = z | ∃ v ∈ A z = v + − B
18 17 supeq1d ⊢ φ → sup C ℝ < = sup z | ∃ v ∈ A z = v + − B ℝ <
19 4 renegcld ⊢ φ → − B ∈ ℝ
20 eqid ⊢ z | ∃ v ∈ A z = v + − B = z | ∃ v ∈ A z = v + − B
21 1 2 3 19 20 supaddc ⊢ φ → sup A ℝ < + − B = sup z | ∃ v ∈ A z = v + − B ℝ <
22 21 eqcomd ⊢ φ → sup z | ∃ v ∈ A z = v + − B ℝ < = sup A ℝ < + − B
23 suprcl ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → sup A ℝ < ∈ ℝ
24 1 2 3 23 syl3anc ⊢ φ → sup A ℝ < ∈ ℝ
25 24 recnd ⊢ φ → sup A ℝ < ∈ ℂ
26 25 9 negsubd ⊢ φ → sup A ℝ < + − B = sup A ℝ < − B
27 18 22 26 3eqtrrd ⊢ φ → sup A ℝ < − B = sup C ℝ <