Theorem sn-addcan2d

Description: addcan2d without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Hypotheses	sn-addcan2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	sn-addcan2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	sn-addcan2d.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	sn-addcan2d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sn-addcan2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		sn-addcan2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		sn-addcan2d.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		sn-negex	⊢ ( 𝐶 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝐶 + 𝑥 ) = 0 )
5	3 4	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( 𝐶 + 𝑥 ) = 0 )
6		oveq1	⊢ ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) → ( ( 𝐴 + 𝐶 ) + 𝑥 ) = ( ( 𝐵 + 𝐶 ) + 𝑥 ) )
7	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → 𝐴 ∈ ℂ )
8	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → 𝐶 ∈ ℂ )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → 𝑥 ∈ ℂ )
10	7 8 9	addassd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( 𝐴 + 𝐶 ) + 𝑥 ) = ( 𝐴 + ( 𝐶 + 𝑥 ) ) )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( 𝐶 + 𝑥 ) = 0 )
12	11	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( 𝐴 + ( 𝐶 + 𝑥 ) ) = ( 𝐴 + 0 ) )
13		sn-addid1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )
14	7 13	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( 𝐴 + 0 ) = 𝐴 )
15	10 12 14	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( 𝐴 + 𝐶 ) + 𝑥 ) = 𝐴 )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → 𝐵 ∈ ℂ )
17	16 8 9	addassd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( 𝐵 + 𝐶 ) + 𝑥 ) = ( 𝐵 + ( 𝐶 + 𝑥 ) ) )
18	11	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( 𝐵 + ( 𝐶 + 𝑥 ) ) = ( 𝐵 + 0 ) )
19		sn-addid1	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 + 0 ) = 𝐵 )
20	16 19	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( 𝐵 + 0 ) = 𝐵 )
21	17 18 20	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( 𝐵 + 𝐶 ) + 𝑥 ) = 𝐵 )
22	15 21	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( ( 𝐴 + 𝐶 ) + 𝑥 ) = ( ( 𝐵 + 𝐶 ) + 𝑥 ) ↔ 𝐴 = 𝐵 ) )
23	6 22	syl5ib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) → 𝐴 = 𝐵 ) )
24		oveq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) )
25	23 24	impbid1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐶 + 𝑥 ) = 0 ) ) → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) ↔ 𝐴 = 𝐵 ) )
26	5 25	rexlimddv	⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) ↔ 𝐴 = 𝐵 ) )