Metamath Proof Explorer

Theorem sn-addcan2d

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

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

Proof

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