nnmulcom

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

		Ref	Expression
	Assertion	nnmulcom	$⊢ (A \in ℕ \land B \in ℕ) \to A B = B A$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = 1 \to x B = 1 B$
2		oveq2	$⊢ x = 1 \to B x = B \cdot 1$
3	1 2	eqeq12d	$⊢ x = 1 \to (x B = B x \leftrightarrow 1 B = B \cdot 1)$
4	3	imbi2d	$⊢ x = 1 \to ((B \in ℕ \to x B = B x) \leftrightarrow (B \in ℕ \to 1 B = B \cdot 1))$
5		oveq1	$⊢ x = y \to x B = y B$
6		oveq2	$⊢ x = y \to B x = B y$
7	5 6	eqeq12d	$⊢ x = y \to (x B = B x \leftrightarrow y B = B y)$
8	7	imbi2d	$⊢ x = y \to ((B \in ℕ \to x B = B x) \leftrightarrow (B \in ℕ \to y B = B y))$
9		oveq1	$⊢ x = y + 1 \to x B = (y + 1) B$
10		oveq2	$⊢ x = y + 1 \to B x = B (y + 1)$
11	9 10	eqeq12d	$⊢ x = y + 1 \to (x B = B x \leftrightarrow (y + 1) B = B (y + 1))$
12	11	imbi2d	$⊢ x = y + 1 \to ((B \in ℕ \to x B = B x) \leftrightarrow (B \in ℕ \to (y + 1) B = B (y + 1)))$
13		oveq1	$⊢ x = A \to x B = A B$
14		oveq2	$⊢ x = A \to B x = B A$
15	13 14	eqeq12d	$⊢ x = A \to (x B = B x \leftrightarrow A B = B A)$
16	15	imbi2d	$⊢ x = A \to ((B \in ℕ \to x B = B x) \leftrightarrow (B \in ℕ \to A B = B A))$
17		nnmul1com	$⊢ B \in ℕ \to 1 B = B \cdot 1$
18		simp3	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to y B = B y$
19	17	3ad2ant2	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to 1 B = B \cdot 1$
20	18 19	oveq12d	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to y B + 1 B = B y + B \cdot 1$
21		simp1	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to y \in ℕ$
22		1nn	$⊢ 1 \in ℕ$
23	22	a1i	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to 1 \in ℕ$
24		simp2	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to B \in ℕ$
25		nnadddir	$⊢ (y \in ℕ \land 1 \in ℕ \land B \in ℕ) \to (y + 1) B = y B + 1 B$
26	21 23 24 25	syl3anc	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to (y + 1) B = y B + 1 B$
27	24	nncnd	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to B \in ℂ$
28	21	nncnd	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to y \in ℂ$
29		1cnd	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to 1 \in ℂ$
30	27 28 29	adddid	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to B (y + 1) = B y + B \cdot 1$
31	20 26 30	3eqtr4d	$⊢ (y \in ℕ \land B \in ℕ \land y B = B y) \to (y + 1) B = B (y + 1)$
32	31	3exp	$⊢ y \in ℕ \to (B \in ℕ \to (y B = B y \to (y + 1) B = B (y + 1)))$
33	32	a2d	$⊢ y \in ℕ \to ((B \in ℕ \to y B = B y) \to (B \in ℕ \to (y + 1) B = B (y + 1)))$
34	4 8 12 16 17 33	nnind	$⊢ A \in ℕ \to (B \in ℕ \to A B = B A)$
35	34	imp	$⊢ (A \in ℕ \land B \in ℕ) \to A B = B A$

Metamath Proof Explorer

Theorem nnmulcom

Proof