Metamath Proof Explorer

Theorem sn-addid2

Description: addid2 without ax-mulcom . (Contributed by SN, 23-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cnre 
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
2 0cnd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> 0 e. CC )
3 simp2l 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> x e. RR )
4 3 recnd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> x e. CC )
5 ax-icn 
 |-  _i e. CC
6 5 a1i 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> _i e. CC )
7 simp2r 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> y e. RR )
8 7 recnd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> y e. CC )
9 6 8 mulcld 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( _i x. y ) e. CC )
10 2 4 9 addassd 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( 0 + x ) + ( _i x. y ) ) = ( 0 + ( x + ( _i x. y ) ) ) )
11 readdid2 
 |-  ( x e. RR -> ( 0 + x ) = x )
12 11 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 0 + x ) = x )
13 12 3ad2ant2 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( 0 + x ) = x )
14 13 oveq1d 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( ( 0 + x ) + ( _i x. y ) ) = ( x + ( _i x. y ) ) )
15 10 14 eqtr3d 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( 0 + ( x + ( _i x. y ) ) ) = ( x + ( _i x. y ) ) )
16 simp3 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> A = ( x + ( _i x. y ) ) )
17 16 oveq2d 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( 0 + A ) = ( 0 + ( x + ( _i x. y ) ) ) )
18 15 17 16 3eqtr4d 
 |-  ( ( A e. CC /\ ( x e. RR /\ y e. RR ) /\ A = ( x + ( _i x. y ) ) ) -> ( 0 + A ) = A )
19 18 3exp 
 |-  ( A e. CC -> ( ( x e. RR /\ y e. RR ) -> ( A = ( x + ( _i x. y ) ) -> ( 0 + A ) = A ) ) )
20 19 rexlimdvv 
 |-  ( A e. CC -> ( E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) -> ( 0 + A ) = A ) )
21 1 20 mpd 
 |-  ( A e. CC -> ( 0 + A ) = A )