nnadddir

Description: Right-distributivity for natural numbers without ax-mulcom . (Contributed by SN, 5-Feb-2024)

		Ref	Expression
	Assertion	nnadddir	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A + B) C = A C + B C$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 1 \to (A + B) x = (A + B) \cdot 1$
2		oveq2	$⊢ x = 1 \to A x = A \cdot 1$
3		oveq2	$⊢ x = 1 \to B x = B \cdot 1$
4	2 3	oveq12d	$⊢ x = 1 \to A x + B x = A \cdot 1 + B \cdot 1$
5	1 4	eqeq12d	$⊢ x = 1 \to ((A + B) x = A x + B x \leftrightarrow (A + B) \cdot 1 = A \cdot 1 + B \cdot 1)$
6	5	imbi2d	$⊢ x = 1 \to (((A \in ℕ \land B \in ℕ) \to (A + B) x = A x + B x) \leftrightarrow ((A \in ℕ \land B \in ℕ) \to (A + B) \cdot 1 = A \cdot 1 + B \cdot 1))$
7		oveq2	$⊢ x = y \to (A + B) x = (A + B) y$
8		oveq2	$⊢ x = y \to A x = A y$
9		oveq2	$⊢ x = y \to B x = B y$
10	8 9	oveq12d	$⊢ x = y \to A x + B x = A y + B y$
11	7 10	eqeq12d	$⊢ x = y \to ((A + B) x = A x + B x \leftrightarrow (A + B) y = A y + B y)$
12	11	imbi2d	$⊢ x = y \to (((A \in ℕ \land B \in ℕ) \to (A + B) x = A x + B x) \leftrightarrow ((A \in ℕ \land B \in ℕ) \to (A + B) y = A y + B y))$
13		oveq2	$⊢ x = y + 1 \to (A + B) x = (A + B) (y + 1)$
14		oveq2	$⊢ x = y + 1 \to A x = A (y + 1)$
15		oveq2	$⊢ x = y + 1 \to B x = B (y + 1)$
16	14 15	oveq12d	$⊢ x = y + 1 \to A x + B x = A (y + 1) + B (y + 1)$
17	13 16	eqeq12d	$⊢ x = y + 1 \to ((A + B) x = A x + B x \leftrightarrow (A + B) (y + 1) = A (y + 1) + B (y + 1))$
18	17	imbi2d	$⊢ x = y + 1 \to (((A \in ℕ \land B \in ℕ) \to (A + B) x = A x + B x) \leftrightarrow ((A \in ℕ \land B \in ℕ) \to (A + B) (y + 1) = A (y + 1) + B (y + 1)))$
19		oveq2	$⊢ x = C \to (A + B) x = (A + B) C$
20		oveq2	$⊢ x = C \to A x = A C$
21		oveq2	$⊢ x = C \to B x = B C$
22	20 21	oveq12d	$⊢ x = C \to A x + B x = A C + B C$
23	19 22	eqeq12d	$⊢ x = C \to ((A + B) x = A x + B x \leftrightarrow (A + B) C = A C + B C)$
24	23	imbi2d	$⊢ x = C \to (((A \in ℕ \land B \in ℕ) \to (A + B) x = A x + B x) \leftrightarrow ((A \in ℕ \land B \in ℕ) \to (A + B) C = A C + B C))$
25		nnaddcl	$⊢ (A \in ℕ \land B \in ℕ) \to A + B \in ℕ$
26	25	nnred	$⊢ (A \in ℕ \land B \in ℕ) \to A + B \in ℝ$
27		ax-1rid	$⊢ A + B \in ℝ \to (A + B) \cdot 1 = A + B$
28	26 27	syl	$⊢ (A \in ℕ \land B \in ℕ) \to (A + B) \cdot 1 = A + B$
29		nnre	$⊢ A \in ℕ \to A \in ℝ$
30		ax-1rid	$⊢ A \in ℝ \to A \cdot 1 = A$
31	29 30	syl	$⊢ A \in ℕ \to A \cdot 1 = A$
32		nnre	$⊢ B \in ℕ \to B \in ℝ$
33		ax-1rid	$⊢ B \in ℝ \to B \cdot 1 = B$
34	32 33	syl	$⊢ B \in ℕ \to B \cdot 1 = B$
35	31 34	oveqan12d	$⊢ (A \in ℕ \land B \in ℕ) \to A \cdot 1 + B \cdot 1 = A + B$
36	28 35	eqtr4d	$⊢ (A \in ℕ \land B \in ℕ) \to (A + B) \cdot 1 = A \cdot 1 + B \cdot 1$
37		simp2l	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A \in ℕ$
38		simp2r	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B \in ℕ$
39	37 38	nnaddcld	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A + B \in ℕ$
40	39	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A + B \in ℂ$
41		simp1	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to y \in ℕ$
42	41	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to y \in ℂ$
43		1cnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to 1 \in ℂ$
44	40 42 43	adddid	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to (A + B) (y + 1) = (A + B) y + (A + B) \cdot 1$
45	37	nnred	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A \in ℝ$
46	45 30	syl	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A \cdot 1 = A$
47	46	oveq2d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + A \cdot 1 = A y + A$
48	38	nnred	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B \in ℝ$
49	48 33	syl	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B \cdot 1 = B$
50	49	oveq2d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B y + B \cdot 1 = B y + B$
51	47 50	oveq12d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + A \cdot 1 + B y + B \cdot 1 = A y + A + B y + B$
52	37 41	nnmulcld	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y \in ℕ$
53	52	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y \in ℂ$
54	37	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A \in ℂ$
55	38 41	nnmulcld	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B y \in ℕ$
56	55 38	nnaddcld	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B y + B \in ℕ$
57	56	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B y + B \in ℂ$
58	53 54 57	addassd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + A + B y + B = A y + A + (B y + B)$
59	55	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B y \in ℂ$
60	38	nncnd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B \in ℂ$
61	54 59 60	addassd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A + B y + B = A + B y + B$
62	61	oveq2d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + (A + B y) + B = A y + A + (B y + B)$
63	59 54 60	addassd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B y + A + B = B y + A + B$
64	63	oveq2d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + (B y + A) + B = A y + B y + (A + B)$
65		nnaddcom	$⊢ (A \in ℕ \land B y \in ℕ) \to A + B y = B y + A$
66	37 55 65	syl2anc	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A + B y = B y + A$
67	66	oveq1d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A + B y + B = B y + A + B$
68	67	oveq2d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + (A + B y) + B = A y + (B y + A) + B$
69	53 59 40	addassd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + B y + A + B = A y + B y + (A + B)$
70	64 68 69	3eqtr4d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + (A + B y) + B = A y + B y + A + B$
71	58 62 70	3eqtr2d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + A + B y + B = A y + B y + A + B$
72	51 71	eqtrd	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A y + A \cdot 1 + B y + B \cdot 1 = A y + B y + A + B$
73	54 42 43	adddid	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A (y + 1) = A y + A \cdot 1$
74	60 42 43	adddid	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to B (y + 1) = B y + B \cdot 1$
75	73 74	oveq12d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A (y + 1) + B (y + 1) = A y + A \cdot 1 + B y + B \cdot 1$
76		simp3	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to (A + B) y = A y + B y$
77	39	nnred	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A + B \in ℝ$
78	77 27	syl	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to (A + B) \cdot 1 = A + B$
79	76 78	oveq12d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to (A + B) y + (A + B) \cdot 1 = A y + B y + A + B$
80	72 75 79	3eqtr4d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to A (y + 1) + B (y + 1) = (A + B) y + (A + B) \cdot 1$
81	44 80	eqtr4d	$⊢ (y \in ℕ \land (A \in ℕ \land B \in ℕ) \land (A + B) y = A y + B y) \to (A + B) (y + 1) = A (y + 1) + B (y + 1)$
82	81	3exp	$⊢ y \in ℕ \to ((A \in ℕ \land B \in ℕ) \to ((A + B) y = A y + B y \to (A + B) (y + 1) = A (y + 1) + B (y + 1)))$
83	82	a2d	$⊢ y \in ℕ \to (((A \in ℕ \land B \in ℕ) \to (A + B) y = A y + B y) \to ((A \in ℕ \land B \in ℕ) \to (A + B) (y + 1) = A (y + 1) + B (y + 1)))$
84	6 12 18 24 36 83	nnind	$⊢ C \in ℕ \to ((A \in ℕ \land B \in ℕ) \to (A + B) C = A C + B C)$
85	84	com12	$⊢ (A \in ℕ \land B \in ℕ) \to (C \in ℕ \to (A + B) C = A C + B C)$
86	85	3impia	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A + B) C = A C + B C$

Metamath Proof Explorer

Theorem nnadddir

Proof