Metamath Proof Explorer

Theorem resubsub4

Description: Law for double subtraction. Compare subsub4 . (Contributed by Steven Nguyen, 14-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 readdcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
2 1 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C ∈ ℝ
3 rersubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B ∈ ℝ
4 3 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B ∈ ℝ
5 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
6 rersubcl ⊢ A - ℝ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B - ℝ C ∈ ℝ
7 4 5 6 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B - ℝ C ∈ ℝ
8 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
9 8 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
10 5 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
11 7 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B - ℝ C ∈ ℂ
12 9 10 11 addassd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C + A - ℝ B - ℝ C = B + C + A - ℝ B - ℝ C
13 repncan3 ⊢ C ∈ ℝ ∧ A - ℝ B ∈ ℝ → C + A - ℝ B - ℝ C = A - ℝ B
14 5 4 13 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A - ℝ B - ℝ C = A - ℝ B
15 14 oveq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C + A - ℝ B - ℝ C = B + A - ℝ B
16 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
17 repncan3 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B + A - ℝ B = A
18 8 16 17 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + A - ℝ B = A
19 12 15 18 3eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C + A - ℝ B - ℝ C = A
20 2 7 19 reladdrsub ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B - ℝ C = A - ℝ B + C