This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-subeu

Description: negeu without ax-mulcom and complex number version of resubeu . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-subeu 
|- ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( A + x ) = B )

Proof

Step Hyp Ref Expression
1 sn-negex 
 |-  ( A e. CC -> E. y e. CC ( A + y ) = 0 )
2 1 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> E. y e. CC ( A + y ) = 0 )
3 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> y e. CC )
4 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> B e. CC )
5 3 4 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> ( y + B ) e. CC )
6 simplrr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( A + y ) = 0 )
7 6 oveq1d 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + y ) + B ) = ( 0 + B ) )
8 simplll 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> A e. CC )
9 simplrl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> y e. CC )
10 simpllr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> B e. CC )
11 8 9 10 addassd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + y ) + B ) = ( A + ( y + B ) ) )
12 sn-addlid 
 |-  ( B e. CC -> ( 0 + B ) = B )
13 10 12 syl 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( 0 + B ) = B )
14 7 11 13 3eqtr3rd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> B = ( A + ( y + B ) ) )
15 14 eqeq2d 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + x ) = B <-> ( A + x ) = ( A + ( y + B ) ) ) )
16 simpr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> x e. CC )
17 9 10 addcld 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( y + B ) e. CC )
18 8 16 17 sn-addcand 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + x ) = ( A + ( y + B ) ) <-> x = ( y + B ) ) )
19 15 18 bitrd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) /\ x e. CC ) -> ( ( A + x ) = B <-> x = ( y + B ) ) )
20 19 ralrimiva 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> A. x e. CC ( ( A + x ) = B <-> x = ( y + B ) ) )
21 reu6i 
 |-  ( ( ( y + B ) e. CC /\ A. x e. CC ( ( A + x ) = B <-> x = ( y + B ) ) ) -> E! x e. CC ( A + x ) = B )
22 5 20 21 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( y e. CC /\ ( A + y ) = 0 ) ) -> E! x e. CC ( A + x ) = B )
23 2 22 rexlimddv 
 |-  ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( A + x ) = B )