This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem readdcan2

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

Ref Expression
Assertion readdcan2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

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