Metamath Proof Explorer

Theorem renpncan3

Description: Cancellation law for real subtraction. Compare npncan3 . (Contributed by Steven Nguyen, 28-Jan-2023)

Ref Expression
Assertion renpncan3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B + C - ℝ A = C - ℝ B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
2 rersubcl ⊢ C ∈ ℝ ∧ A ∈ ℝ → C - ℝ A ∈ ℝ
3 2 ancoms ⊢ A ∈ ℝ ∧ C ∈ ℝ → C - ℝ A ∈ ℝ
4 3 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C - ℝ A ∈ ℝ
5 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
6 readdsub ⊢ A ∈ ℝ ∧ C - ℝ A ∈ ℝ ∧ B ∈ ℝ → A + C - ℝ A - ℝ B = A - ℝ B + C - ℝ A
7 1 4 5 6 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C - ℝ A - ℝ B = A - ℝ B + C - ℝ A
8 repncan3 ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + C - ℝ A = C
9 8 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C - ℝ A = C
10 9 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C - ℝ A - ℝ B = C - ℝ B
11 7 10 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B + C - ℝ A = C - ℝ B