Metamath Proof Explorer

Theorem sn-addcand

Description: addcand without ax-mulcom . Note how the proof is almost identical to addcan . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses sn-addcand.a ⊢φ→A∈ℂ
sn-addcand.b ⊢φ→B∈ℂ
sn-addcand.c ⊢φ→C∈ℂ
Assertion sn-addcand ⊢φ→A+B=A+C↔B=C

Proof

Step Hyp Ref Expression
1 sn-addcand.a ⊢φ→A∈ℂ
2 sn-addcand.b ⊢φ→B∈ℂ
3 sn-addcand.c ⊢φ→C∈ℂ
4 sn-negex2 ⊢A∈ℂ→∃x∈ℂx+A=0
5 1 4 syl ⊢φ→∃x∈ℂx+A=0
6 oveq2 ⊢A+B=A+C→x+A+B=x+A+C
7 simprr ⊢φ∧x∈ℂ∧x+A=0→x+A=0
8 7 oveq1d ⊢φ∧x∈ℂ∧x+A=0→x+A+B=0+B
9 simprl ⊢φ∧x∈ℂ∧x+A=0→x∈ℂ
10 1 adantr ⊢φ∧x∈ℂ∧x+A=0→A∈ℂ
11 2 adantr ⊢φ∧x∈ℂ∧x+A=0→B∈ℂ
12 9 10 11 addassd ⊢φ∧x∈ℂ∧x+A=0→x+A+B=x+A+B
13 sn-addlid ⊢B∈ℂ→0+B=B
14 11 13 syl ⊢φ∧x∈ℂ∧x+A=0→0+B=B
15 8 12 14 3eqtr3d ⊢φ∧x∈ℂ∧x+A=0→x+A+B=B
16 7 oveq1d ⊢φ∧x∈ℂ∧x+A=0→x+A+C=0+C
17 3 adantr ⊢φ∧x∈ℂ∧x+A=0→C∈ℂ
18 9 10 17 addassd ⊢φ∧x∈ℂ∧x+A=0→x+A+C=x+A+C
19 sn-addlid ⊢C∈ℂ→0+C=C
20 17 19 syl ⊢φ∧x∈ℂ∧x+A=0→0+C=C
21 16 18 20 3eqtr3d ⊢φ∧x∈ℂ∧x+A=0→x+A+C=C
22 15 21 eqeq12d ⊢φ∧x∈ℂ∧x+A=0→x+A+B=x+A+C↔B=C
23 6 22 imbitrid ⊢φ∧x∈ℂ∧x+A=0→A+B=A+C→B=C
24 oveq2 ⊢B=C→A+B=A+C
25 23 24 impbid1 ⊢φ∧x∈ℂ∧x+A=0→A+B=A+C↔B=C
26 5 25 rexlimddv ⊢φ→A+B=A+C↔B=C