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		readdid1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 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		readdid1	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) ↔ 𝐴 = 𝐵 ) )