Metamath Proof Explorer

Theorem resubidaddid1lem

Description: Lemma for resubidaddid1 . A special case of npncan . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses resubidaddid1lem.a ⊢ φ → A ∈ ℝ
resubidaddid1lem.b ⊢ φ → B ∈ ℝ
resubidaddid1lem.c ⊢ φ → C ∈ ℝ
resubidaddid1lem.1 ⊢ φ → A - ℝ B = B - ℝ C
Assertion resubidaddid1lem ⊢ φ → A - ℝ B + B - ℝ C = A - ℝ C

Proof

Step Hyp Ref Expression
1 resubidaddid1lem.a ⊢ φ → A ∈ ℝ
2 resubidaddid1lem.b ⊢ φ → B ∈ ℝ
3 resubidaddid1lem.c ⊢ φ → C ∈ ℝ
4 resubidaddid1lem.1 ⊢ φ → A - ℝ B = B - ℝ C
5 rersubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B ∈ ℝ
6 1 2 5 syl2anc ⊢ φ → A - ℝ B ∈ ℝ
7 rersubcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
8 2 3 7 syl2anc ⊢ φ → B - ℝ C ∈ ℝ
9 6 8 readdcld ⊢ φ → A - ℝ B + B - ℝ C ∈ ℝ
10 4 eqcomd ⊢ φ → B - ℝ C = A - ℝ B
11 2 3 6 resubaddd ⊢ φ → B - ℝ C = A - ℝ B ↔ C + A - ℝ B = B
12 10 11 mpbid ⊢ φ → C + A - ℝ B = B
13 12 oveq1d ⊢ φ → C + A - ℝ B + B - ℝ C = B + B - ℝ C
14 3 recnd ⊢ φ → C ∈ ℂ
15 6 recnd ⊢ φ → A - ℝ B ∈ ℂ
16 8 recnd ⊢ φ → B - ℝ C ∈ ℂ
17 14 15 16 addassd ⊢ φ → C + A - ℝ B + B - ℝ C = C + A - ℝ B + B - ℝ C
18 1 2 8 resubaddd ⊢ φ → A - ℝ B = B - ℝ C ↔ B + B - ℝ C = A
19 4 18 mpbid ⊢ φ → B + B - ℝ C = A
20 13 17 19 3eqtr3d ⊢ φ → C + A - ℝ B + B - ℝ C = A
21 3 9 20 reladdrsub ⊢ φ → A - ℝ B + B - ℝ C = A - ℝ C