Metamath Proof Explorer

Theorem zmulcomlem

Description: Lemma for zmulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion zmulcomlem 
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( A x. B ) = ( B x. A ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
2 renegneg 
 |-  ( A e. RR -> ( 0 -R ( 0 -R A ) ) = A )
3 2 oveq1d 
 |-  ( A e. RR -> ( ( 0 -R ( 0 -R A ) ) x. B ) = ( A x. B ) )
4 3 ad2antrr 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( ( 0 -R ( 0 -R A ) ) x. B ) = ( A x. B ) )
5 rernegcl 
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
6 5 ad2antrr 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( 0 -R A ) e. RR )
7 simpr 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> B e. NN )
8 6 7 renegmulnnass 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( ( 0 -R ( 0 -R A ) ) x. B ) = ( 0 -R ( ( 0 -R A ) x. B ) ) )
9 nnmulcom 
 |-  ( ( ( 0 -R A ) e. NN /\ B e. NN ) -> ( ( 0 -R A ) x. B ) = ( B x. ( 0 -R A ) ) )
10 9 adantll 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( ( 0 -R A ) x. B ) = ( B x. ( 0 -R A ) ) )
11 10 oveq2d 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( 0 -R ( ( 0 -R A ) x. B ) ) = ( 0 -R ( B x. ( 0 -R A ) ) ) )
12 nnre 
 |-  ( B e. NN -> B e. RR )
13 12 adantl 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> B e. RR )
14 0red 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> 0 e. RR )
15 resubdi 
 |-  ( ( B e. RR /\ 0 e. RR /\ ( 0 -R A ) e. RR ) -> ( B x. ( 0 -R ( 0 -R A ) ) ) = ( ( B x. 0 ) -R ( B x. ( 0 -R A ) ) ) )
16 13 14 6 15 syl3anc 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( B x. ( 0 -R ( 0 -R A ) ) ) = ( ( B x. 0 ) -R ( B x. ( 0 -R A ) ) ) )
17 remul01 
 |-  ( B e. RR -> ( B x. 0 ) = 0 )
18 12 17 syl 
 |-  ( B e. NN -> ( B x. 0 ) = 0 )
19 18 adantl 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( B x. 0 ) = 0 )
20 19 oveq1d 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( ( B x. 0 ) -R ( B x. ( 0 -R A ) ) ) = ( 0 -R ( B x. ( 0 -R A ) ) ) )
21 16 20 eqtrd 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( B x. ( 0 -R ( 0 -R A ) ) ) = ( 0 -R ( B x. ( 0 -R A ) ) ) )
22 2 ad2antrr 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( 0 -R ( 0 -R A ) ) = A )
23 22 oveq2d 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( B x. ( 0 -R ( 0 -R A ) ) ) = ( B x. A ) )
24 11 21 23 3eqtr2d 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( 0 -R ( ( 0 -R A ) x. B ) ) = ( B x. A ) )
25 8 4 24 3eqtr3d 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )
26 4 4 25 3eqtr3d 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )
27 remul01 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
28 remul02 
 |-  ( A e. RR -> ( 0 x. A ) = 0 )
29 27 28 eqtr4d 
 |-  ( A e. RR -> ( A x. 0 ) = ( 0 x. A ) )
30 29 adantr 
 |-  ( ( A e. RR /\ ( 0 -R A ) e. NN ) -> ( A x. 0 ) = ( 0 x. A ) )
31 oveq2 
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
32 oveq1 
 |-  ( B = 0 -> ( B x. A ) = ( 0 x. A ) )
33 31 32 eqeq12d 
 |-  ( B = 0 -> ( ( A x. B ) = ( B x. A ) <-> ( A x. 0 ) = ( 0 x. A ) ) )
34 30 33 syl5ibrcom 
 |-  ( ( A e. RR /\ ( 0 -R A ) e. NN ) -> ( B = 0 -> ( A x. B ) = ( B x. A ) ) )
35 34 imp 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B = 0 ) -> ( A x. B ) = ( B x. A ) )
36 26 35 jaodan 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. NN \/ B = 0 ) ) -> ( A x. B ) = ( B x. A ) )
37 1 36 sylan2b 
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( A x. B ) = ( B x. A ) )