Metamath Proof Explorer

Theorem sn-addid1

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

Ref Expression
Assertion sn-addid1 
|- ( A e. CC -> ( A + 0 ) = A )

Proof

Step Hyp Ref Expression
1 sn-negex2 
 |-  ( A e. CC -> E. x e. CC ( x + A ) = 0 )
2 simprr 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( x + A ) = 0 )
3 2 oveq1d 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + 0 ) = ( 0 + 0 ) )
4 sn-00id 
 |-  ( 0 + 0 ) = 0
5 3 4 eqtrdi 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + 0 ) = 0 )
6 simprl 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> x e. CC )
7 simpl 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> A e. CC )
8 0cnd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> 0 e. CC )
9 6 7 8 addassd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + 0 ) = ( x + ( A + 0 ) ) )
10 2 5 9 3eqtr2rd 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( x + ( A + 0 ) ) = ( x + A ) )
11 7 8 addcld 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( A + 0 ) e. CC )
12 6 11 7 sn-addcand 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + ( A + 0 ) ) = ( x + A ) <-> ( A + 0 ) = A ) )
13 10 12 mpbid 
 |-  ( ( A e. CC /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( A + 0 ) = A )
14 1 13 rexlimddv 
 |-  ( A e. CC -> ( A + 0 ) = A )