Metamath Proof Explorer

Theorem nnmul1com

Description: Multiplication with 1 is commutative for natural numbers, without ax-mulcom . Since ( A x. 1 ) is A by ax-1rid , this is equivalent to remulid2 for natural numbers, but using fewer axioms (avoiding ax-resscn , ax-addass , ax-mulass , ax-rnegex , ax-pre-lttri , ax-pre-lttrn , ax-pre-ltadd ). (Contributed by SN, 5-Feb-2024)

Ref Expression
Assertion nnmul1com 
|- ( A e. NN -> ( 1 x. A ) = ( A x. 1 ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 1 -> ( 1 x. x ) = ( 1 x. 1 ) )
2 id 
 |-  ( x = 1 -> x = 1 )
3 1 2 eqeq12d 
 |-  ( x = 1 -> ( ( 1 x. x ) = x <-> ( 1 x. 1 ) = 1 ) )
4 oveq2 
 |-  ( x = y -> ( 1 x. x ) = ( 1 x. y ) )
5 id 
 |-  ( x = y -> x = y )
6 4 5 eqeq12d 
 |-  ( x = y -> ( ( 1 x. x ) = x <-> ( 1 x. y ) = y ) )
7 oveq2 
 |-  ( x = ( y + 1 ) -> ( 1 x. x ) = ( 1 x. ( y + 1 ) ) )
8 id 
 |-  ( x = ( y + 1 ) -> x = ( y + 1 ) )
9 7 8 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( 1 x. x ) = x <-> ( 1 x. ( y + 1 ) ) = ( y + 1 ) ) )
10 oveq2 
 |-  ( x = A -> ( 1 x. x ) = ( 1 x. A ) )
11 id 
 |-  ( x = A -> x = A )
12 10 11 eqeq12d 
 |-  ( x = A -> ( ( 1 x. x ) = x <-> ( 1 x. A ) = A ) )
13 1t1e1ALT 
 |-  ( 1 x. 1 ) = 1
14 1cnd 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> 1 e. CC )
15 simpl 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> y e. NN )
16 15 nncnd 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> y e. CC )
17 14 16 14 adddid 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> ( 1 x. ( y + 1 ) ) = ( ( 1 x. y ) + ( 1 x. 1 ) ) )
18 simpr 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> ( 1 x. y ) = y )
19 13 a1i 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> ( 1 x. 1 ) = 1 )
20 18 19 oveq12d 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> ( ( 1 x. y ) + ( 1 x. 1 ) ) = ( y + 1 ) )
21 17 20 eqtrd 
 |-  ( ( y e. NN /\ ( 1 x. y ) = y ) -> ( 1 x. ( y + 1 ) ) = ( y + 1 ) )
22 21 ex 
 |-  ( y e. NN -> ( ( 1 x. y ) = y -> ( 1 x. ( y + 1 ) ) = ( y + 1 ) ) )
23 3 6 9 12 13 22 nnind 
 |-  ( A e. NN -> ( 1 x. A ) = A )
24 nnre 
 |-  ( A e. NN -> A e. RR )
25 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
26 24 25 syl 
 |-  ( A e. NN -> ( A x. 1 ) = A )
27 23 26 eqtr4d 
 |-  ( A e. NN -> ( 1 x. A ) = ( A x. 1 ) )