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