Metamath Proof Explorer

Theorem sn-addcan2d

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

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

Proof

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