Metamath Proof Explorer

Theorem remulcan2d

Description: mulcan2d for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023)

Ref Expression
Hypotheses remulcan2d.1 
|- ( ph -> A e. RR )
remulcan2d.2 
|- ( ph -> B e. RR )
remulcan2d.3 
|- ( ph -> C e. RR )
remulcan2d.4 
|- ( ph -> C =/= 0 )
Assertion remulcan2d 
|- ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 remulcan2d.1 
 |-  ( ph -> A e. RR )
2 remulcan2d.2 
 |-  ( ph -> B e. RR )
3 remulcan2d.3 
 |-  ( ph -> C e. RR )
4 remulcan2d.4 
 |-  ( ph -> C =/= 0 )
5 ax-rrecex 
 |-  ( ( C e. RR /\ C =/= 0 ) -> E. x e. RR ( C x. x ) = 1 )
6 3 4 5 syl2anc 
 |-  ( ph -> E. x e. RR ( C x. x ) = 1 )
7 oveq1 
 |-  ( ( A x. C ) = ( B x. C ) -> ( ( A x. C ) x. x ) = ( ( B x. C ) x. x ) )
8 1 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> A e. RR )
9 8 recnd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> A e. CC )
10 3 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> C e. RR )
11 10 recnd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> C e. CC )
12 simprl 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> x e. RR )
13 12 recnd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> x e. CC )
14 9 11 13 mulassd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( ( A x. C ) x. x ) = ( A x. ( C x. x ) ) )
15 simprr 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( C x. x ) = 1 )
16 15 oveq2d 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( A x. ( C x. x ) ) = ( A x. 1 ) )
17 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
18 8 17 syl 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( A x. 1 ) = A )
19 14 16 18 3eqtrd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( ( A x. C ) x. x ) = A )
20 2 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> B e. RR )
21 20 recnd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> B e. CC )
22 21 11 13 mulassd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( ( B x. C ) x. x ) = ( B x. ( C x. x ) ) )
23 15 oveq2d 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( B x. ( C x. x ) ) = ( B x. 1 ) )
24 ax-1rid 
 |-  ( B e. RR -> ( B x. 1 ) = B )
25 20 24 syl 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( B x. 1 ) = B )
26 22 23 25 3eqtrd 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( ( B x. C ) x. x ) = B )
27 19 26 eqeq12d 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( ( ( A x. C ) x. x ) = ( ( B x. C ) x. x ) <-> A = B ) )
28 7 27 syl5ib 
 |-  ( ( ph /\ ( x e. RR /\ ( C x. x ) = 1 ) ) -> ( ( A x. C ) = ( B x. C ) -> A = B ) )
29 6 28 rexlimddv 
 |-  ( ph -> ( ( A x. C ) = ( B x. C ) -> A = B ) )
30 oveq1 
 |-  ( A = B -> ( A x. C ) = ( B x. C ) )
31 29 30 impbid1 
 |-  ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )