Metamath Proof Explorer

Theorem readdsub

Description: Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
2 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
3 2 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ∈ ℝ
4 repncan3 ⊢ C ∈ ℝ ∧ A + B ∈ ℝ → C + A + B - ℝ C = A + B
5 1 3 4 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A + B - ℝ C = A + B
6 repncan3 ⊢ C ∈ ℝ ∧ A ∈ ℝ → C + A - ℝ C = A
7 6 ancoms ⊢ A ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C = A
8 7 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C = A
9 8 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C + B = A + B
10 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
11 rersubcl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A - ℝ C ∈ ℝ
12 11 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C ∈ ℝ
13 12 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C ∈ ℂ
14 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
15 14 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
16 10 13 15 addassd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ C + B = C + A - ℝ C + B
17 5 9 16 3eqtr2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A + B - ℝ C = C + A - ℝ C + B
18 rersubcl ⊢ A + B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ C ∈ ℝ
19 3 1 18 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ C ∈ ℝ
20 12 14 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C + B ∈ ℝ
21 readdcan ⊢ A + B - ℝ C ∈ ℝ ∧ A - ℝ C + B ∈ ℝ ∧ C ∈ ℝ → C + A + B - ℝ C = C + A - ℝ C + B ↔ A + B - ℝ C = A - ℝ C + B
22 19 20 1 21 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A + B - ℝ C = C + A - ℝ C + B ↔ A + B - ℝ C = A - ℝ C + B
23 17 22 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ C = A - ℝ C + B