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-addid2 ⊢ 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-addid2 ⊢ 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 syl5ib ⊢ φ ∧ 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