Metamath Proof Explorer

Theorem sn-addid1

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

Ref Expression
Assertion sn-addid1 ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 sn-negex2 ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝑥 + 𝐴 ) = 0 )
2 simprr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( 𝑥 + 𝐴 ) = 0 )
3 2 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( ( 𝑥 + 𝐴 ) + 0 ) = ( 0 + 0 ) )
4 sn-00id ⊢ ( 0 + 0 ) = 0
5 3 4 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( ( 𝑥 + 𝐴 ) + 0 ) = 0 )
6 simprl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → 𝑥 ∈ ℂ )
7 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → 𝐴 ∈ ℂ )
8 0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → 0 ∈ ℂ )
9 6 7 8 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( ( 𝑥 + 𝐴 ) + 0 ) = ( 𝑥 + ( 𝐴 + 0 ) ) )
10 2 5 9 3eqtr2rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( 𝑥 + ( 𝐴 + 0 ) ) = ( 𝑥 + 𝐴 ) )
11 7 8 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( 𝐴 + 0 ) ∈ ℂ )
12 6 11 7 sn-addcand ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( ( 𝑥 + ( 𝐴 + 0 ) ) = ( 𝑥 + 𝐴 ) ↔ ( 𝐴 + 0 ) = 𝐴 ) )
13 10 12 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑥 + 𝐴 ) = 0 ) ) → ( 𝐴 + 0 ) = 𝐴 )
14 1 13 rexlimddv ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )