Metamath Proof Explorer

Theorem readdcan2

Description: Commuted version of readdcan without ax-mulcom . (Contributed by SN, 21-Feb-2024)

Ref Expression
Assertion readdcan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C = B + C ↔ A = B

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A + C = B + C → A + C + 0 - ℝ C = B + C + 0 - ℝ C
2 1 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A + C = B + C → A + C + 0 - ℝ C = B + C + 0 - ℝ C
3 simpl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
4 3 recnd ⊢ A ∈ ℝ ∧ C ∈ ℝ → A ∈ ℂ
5 simpr ⊢ A ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
6 5 recnd ⊢ A ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
7 rernegcl ⊢ C ∈ ℝ → 0 - ℝ C ∈ ℝ
8 7 adantl ⊢ A ∈ ℝ ∧ C ∈ ℝ → 0 - ℝ C ∈ ℝ
9 8 recnd ⊢ A ∈ ℝ ∧ C ∈ ℝ → 0 - ℝ C ∈ ℂ
10 4 6 9 addassd ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + C + 0 - ℝ C = A + C + 0 - ℝ C
11 renegid ⊢ C ∈ ℝ → C + 0 - ℝ C = 0
12 11 oveq2d ⊢ C ∈ ℝ → A + C + 0 - ℝ C = A + 0
13 12 adantl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + C + 0 - ℝ C = A + 0
14 readdrid ⊢ A ∈ ℝ → A + 0 = A
15 14 adantr ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + 0 = A
16 10 13 15 3eqtrd ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + C + 0 - ℝ C = A
17 16 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C + 0 - ℝ C = A
18 17 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A + C = B + C → A + C + 0 - ℝ C = A
19 simpl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
20 19 recnd ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
21 simpr ⊢ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
22 21 recnd ⊢ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
23 7 adantl ⊢ B ∈ ℝ ∧ C ∈ ℝ → 0 - ℝ C ∈ ℝ
24 23 recnd ⊢ B ∈ ℝ ∧ C ∈ ℝ → 0 - ℝ C ∈ ℂ
25 20 22 24 addassd ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C + 0 - ℝ C = B + C + 0 - ℝ C
26 11 oveq2d ⊢ C ∈ ℝ → B + C + 0 - ℝ C = B + 0
27 26 adantl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C + 0 - ℝ C = B + 0
28 readdrid ⊢ B ∈ ℝ → B + 0 = B
29 28 adantr ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + 0 = B
30 25 27 29 3eqtrd ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + C + 0 - ℝ C = B
31 30 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C + 0 - ℝ C = B
32 31 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A + C = B + C → B + C + 0 - ℝ C = B
33 2 18 32 3eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A + C = B + C → A = B
34 33 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C = B + C → A = B
35 oveq1 ⊢ A = B → A + C = B + C
36 34 35 impbid1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C = B + C ↔ A = B