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 1 A = A 1

Proof

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