Metamath Proof Explorer

Theorem addinvcom

Description: A number commutes with its additive inverse. Compare remulinvcom . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses addinvcom.a 
|- ( ph -> A e. CC )
addinvcom.b 
|- ( ph -> B e. CC )
addinvcom.1 
|- ( ph -> ( A + B ) = 0 )
Assertion addinvcom 
|- ( ph -> ( B + A ) = 0 )

Proof

Step Hyp Ref Expression
1 addinvcom.a 
 |-  ( ph -> A e. CC )
2 addinvcom.b 
 |-  ( ph -> B e. CC )
3 addinvcom.1 
 |-  ( ph -> ( A + B ) = 0 )
4 ssidd 
 |-  ( ph -> CC C_ CC )
5 simpl 
 |-  ( ( ( A + x ) = 0 /\ ( x + A ) = 0 ) -> ( A + x ) = 0 )
6 5 rgenw 
 |-  A. x e. CC ( ( ( A + x ) = 0 /\ ( x + A ) = 0 ) -> ( A + x ) = 0 )
7 6 a1i 
 |-  ( ph -> A. x e. CC ( ( ( A + x ) = 0 /\ ( x + A ) = 0 ) -> ( A + x ) = 0 ) )
8 sn-negex12 
 |-  ( A e. CC -> E. x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) )
9 1 8 syl 
 |-  ( ph -> E. x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) )
10 0cn 
 |-  0 e. CC
11 sn-subeu 
 |-  ( ( A e. CC /\ 0 e. CC ) -> E! x e. CC ( A + x ) = 0 )
12 1 10 11 sylancl 
 |-  ( ph -> E! x e. CC ( A + x ) = 0 )
13 riotass2 
 |-  ( ( ( CC C_ CC /\ A. x e. CC ( ( ( A + x ) = 0 /\ ( x + A ) = 0 ) -> ( A + x ) = 0 ) ) /\ ( E. x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) /\ E! x e. CC ( A + x ) = 0 ) ) -> ( iota_ x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) = ( iota_ x e. CC ( A + x ) = 0 ) )
14 4 7 9 12 13 syl22anc 
 |-  ( ph -> ( iota_ x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) = ( iota_ x e. CC ( A + x ) = 0 ) )
15 oveq2 
 |-  ( x = B -> ( A + x ) = ( A + B ) )
16 15 eqeq1d 
 |-  ( x = B -> ( ( A + x ) = 0 <-> ( A + B ) = 0 ) )
17 16 riota2 
 |-  ( ( B e. CC /\ E! x e. CC ( A + x ) = 0 ) -> ( ( A + B ) = 0 <-> ( iota_ x e. CC ( A + x ) = 0 ) = B ) )
18 2 12 17 syl2anc 
 |-  ( ph -> ( ( A + B ) = 0 <-> ( iota_ x e. CC ( A + x ) = 0 ) = B ) )
19 3 18 mpbid 
 |-  ( ph -> ( iota_ x e. CC ( A + x ) = 0 ) = B )
20 14 19 eqtrd 
 |-  ( ph -> ( iota_ x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) = B )
21 reurmo 
 |-  ( E! x e. CC ( A + x ) = 0 -> E* x e. CC ( A + x ) = 0 )
22 5 rmoimi 
 |-  ( E* x e. CC ( A + x ) = 0 -> E* x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) )
23 12 21 22 3syl 
 |-  ( ph -> E* x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) )
24 reu5 
 |-  ( E! x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) <-> ( E. x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) /\ E* x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) )
25 9 23 24 sylanbrc 
 |-  ( ph -> E! x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) )
26 oveq1 
 |-  ( x = B -> ( x + A ) = ( B + A ) )
27 26 eqeq1d 
 |-  ( x = B -> ( ( x + A ) = 0 <-> ( B + A ) = 0 ) )
28 16 27 anbi12d 
 |-  ( x = B -> ( ( ( A + x ) = 0 /\ ( x + A ) = 0 ) <-> ( ( A + B ) = 0 /\ ( B + A ) = 0 ) ) )
29 28 riota2 
 |-  ( ( B e. CC /\ E! x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) -> ( ( ( A + B ) = 0 /\ ( B + A ) = 0 ) <-> ( iota_ x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) = B ) )
30 2 25 29 syl2anc 
 |-  ( ph -> ( ( ( A + B ) = 0 /\ ( B + A ) = 0 ) <-> ( iota_ x e. CC ( ( A + x ) = 0 /\ ( x + A ) = 0 ) ) = B ) )
31 20 30 mpbird 
 |-  ( ph -> ( ( A + B ) = 0 /\ ( B + A ) = 0 ) )
32 31 simprd 
 |-  ( ph -> ( B + A ) = 0 )