Metamath Proof Explorer

Theorem nnmulcom

Description: Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024)

Ref Expression
Assertion nnmulcom 
|- ( ( A e. NN /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = 1 -> ( x x. B ) = ( 1 x. B ) )
2 oveq2 
 |-  ( x = 1 -> ( B x. x ) = ( B x. 1 ) )
3 1 2 eqeq12d 
 |-  ( x = 1 -> ( ( x x. B ) = ( B x. x ) <-> ( 1 x. B ) = ( B x. 1 ) ) )
4 3 imbi2d 
 |-  ( x = 1 -> ( ( B e. NN -> ( x x. B ) = ( B x. x ) ) <-> ( B e. NN -> ( 1 x. B ) = ( B x. 1 ) ) ) )
5 oveq1 
 |-  ( x = y -> ( x x. B ) = ( y x. B ) )
6 oveq2 
 |-  ( x = y -> ( B x. x ) = ( B x. y ) )
7 5 6 eqeq12d 
 |-  ( x = y -> ( ( x x. B ) = ( B x. x ) <-> ( y x. B ) = ( B x. y ) ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( B e. NN -> ( x x. B ) = ( B x. x ) ) <-> ( B e. NN -> ( y x. B ) = ( B x. y ) ) ) )
9 oveq1 
 |-  ( x = ( y + 1 ) -> ( x x. B ) = ( ( y + 1 ) x. B ) )
10 oveq2 
 |-  ( x = ( y + 1 ) -> ( B x. x ) = ( B x. ( y + 1 ) ) )
11 9 10 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x x. B ) = ( B x. x ) <-> ( ( y + 1 ) x. B ) = ( B x. ( y + 1 ) ) ) )
12 11 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( B e. NN -> ( x x. B ) = ( B x. x ) ) <-> ( B e. NN -> ( ( y + 1 ) x. B ) = ( B x. ( y + 1 ) ) ) ) )
13 oveq1 
 |-  ( x = A -> ( x x. B ) = ( A x. B ) )
14 oveq2 
 |-  ( x = A -> ( B x. x ) = ( B x. A ) )
15 13 14 eqeq12d 
 |-  ( x = A -> ( ( x x. B ) = ( B x. x ) <-> ( A x. B ) = ( B x. A ) ) )
16 15 imbi2d 
 |-  ( x = A -> ( ( B e. NN -> ( x x. B ) = ( B x. x ) ) <-> ( B e. NN -> ( A x. B ) = ( B x. A ) ) ) )
17 nnmul1com 
 |-  ( B e. NN -> ( 1 x. B ) = ( B x. 1 ) )
18 simp3 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> ( y x. B ) = ( B x. y ) )
19 17 3ad2ant2 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> ( 1 x. B ) = ( B x. 1 ) )
20 18 19 oveq12d 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> ( ( y x. B ) + ( 1 x. B ) ) = ( ( B x. y ) + ( B x. 1 ) ) )
21 simp1 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> y e. NN )
22 1nn 
 |-  1 e. NN
23 22 a1i 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> 1 e. NN )
24 simp2 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> B e. NN )
25 nnadddir 
 |-  ( ( y e. NN /\ 1 e. NN /\ B e. NN ) -> ( ( y + 1 ) x. B ) = ( ( y x. B ) + ( 1 x. B ) ) )
26 21 23 24 25 syl3anc 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> ( ( y + 1 ) x. B ) = ( ( y x. B ) + ( 1 x. B ) ) )
27 24 nncnd 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> B e. CC )
28 21 nncnd 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> y e. CC )
29 1cnd 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> 1 e. CC )
30 27 28 29 adddid 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> ( B x. ( y + 1 ) ) = ( ( B x. y ) + ( B x. 1 ) ) )
31 20 26 30 3eqtr4d 
 |-  ( ( y e. NN /\ B e. NN /\ ( y x. B ) = ( B x. y ) ) -> ( ( y + 1 ) x. B ) = ( B x. ( y + 1 ) ) )
32 31 3exp 
 |-  ( y e. NN -> ( B e. NN -> ( ( y x. B ) = ( B x. y ) -> ( ( y + 1 ) x. B ) = ( B x. ( y + 1 ) ) ) ) )
33 32 a2d 
 |-  ( y e. NN -> ( ( B e. NN -> ( y x. B ) = ( B x. y ) ) -> ( B e. NN -> ( ( y + 1 ) x. B ) = ( B x. ( y + 1 ) ) ) ) )
34 4 8 12 16 17 33 nnind 
 |-  ( A e. NN -> ( B e. NN -> ( A x. B ) = ( B x. A ) ) )
35 34 imp 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )