Metamath Proof Explorer

Theorem sn-addcand

Description: addcand without ax-mulcom . Note how the proof is almost identical to addcan . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses sn-addcand.a 
|- ( ph -> A e. CC )
sn-addcand.b 
|- ( ph -> B e. CC )
sn-addcand.c 
|- ( ph -> C e. CC )
Assertion sn-addcand 
|- ( ph -> ( ( A + B ) = ( A + C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 sn-addcand.a 
 |-  ( ph -> A e. CC )
2 sn-addcand.b 
 |-  ( ph -> B e. CC )
3 sn-addcand.c 
 |-  ( ph -> C e. CC )
4 sn-negex2 
 |-  ( A e. CC -> E. x e. CC ( x + A ) = 0 )
5 1 4 syl 
 |-  ( ph -> E. x e. CC ( x + A ) = 0 )
6 oveq2 
 |-  ( ( A + B ) = ( A + C ) -> ( x + ( A + B ) ) = ( x + ( A + C ) ) )
7 simprr 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( x + A ) = 0 )
8 7 oveq1d 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + B ) = ( 0 + B ) )
9 simprl 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> x e. CC )
10 1 adantr 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> A e. CC )
11 2 adantr 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> B e. CC )
12 9 10 11 addassd 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + B ) = ( x + ( A + B ) ) )
13 sn-addid2 
 |-  ( B e. CC -> ( 0 + B ) = B )
14 11 13 syl 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( 0 + B ) = B )
15 8 12 14 3eqtr3d 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( x + ( A + B ) ) = B )
16 7 oveq1d 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + C ) = ( 0 + C ) )
17 3 adantr 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> C e. CC )
18 9 10 17 addassd 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + A ) + C ) = ( x + ( A + C ) ) )
19 sn-addid2 
 |-  ( C e. CC -> ( 0 + C ) = C )
20 17 19 syl 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( 0 + C ) = C )
21 16 18 20 3eqtr3d 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( x + ( A + C ) ) = C )
22 15 21 eqeq12d 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( x + ( A + B ) ) = ( x + ( A + C ) ) <-> B = C ) )
23 6 22 syl5ib 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( A + B ) = ( A + C ) -> B = C ) )
24 oveq2 
 |-  ( B = C -> ( A + B ) = ( A + C ) )
25 23 24 impbid1 
 |-  ( ( ph /\ ( x e. CC /\ ( x + A ) = 0 ) ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
26 5 25 rexlimddv 
 |-  ( ph -> ( ( A + B ) = ( A + C ) <-> B = C ) )