Theorem nndi

Description: Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Assertion	nndi	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = 𝐶 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝐶 ) )
2	1	oveq2d	⊢ ( 𝑥 = 𝐶 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) )
3		oveq2	⊢ ( 𝑥 = 𝐶 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐶 ) )
4	3	oveq2d	⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
5	2 4	eqeq12d	⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) )
6	5	imbi2d	⊢ ( 𝑥 = 𝐶 → ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) ↔ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) ) )
7		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o ∅ ) )
8	7	oveq2d	⊢ ( 𝑥 = ∅ → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o ∅ ) ) )
9		oveq2	⊢ ( 𝑥 = ∅ → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o ∅ ) )
10	9	oveq2d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) )
11	8 10	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) ) )
12		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝑦 ) )
13	12	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) )
14		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑦 ) )
15	14	oveq2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) )
16	13 15	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) ) )
17		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o suc 𝑦 ) )
18	17	oveq2d	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) )
19		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o suc 𝑦 ) )
20	19	oveq2d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) )
21	18 20	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ↔ ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) )
22		nna0	⊢ ( 𝐵 ∈ ω → ( 𝐵 +o ∅ ) = 𝐵 )
23	22	adantl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 +o ∅ ) = 𝐵 )
24	23	oveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( 𝐴 ·o 𝐵 ) )
25		nnmcl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) ∈ ω )
26		nna0	⊢ ( ( 𝐴 ·o 𝐵 ) ∈ ω → ( ( 𝐴 ·o 𝐵 ) +o ∅ ) = ( 𝐴 ·o 𝐵 ) )
27	25 26	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o ∅ ) = ( 𝐴 ·o 𝐵 ) )
28	24 27	eqtr4d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ∅ ) )
29		nnm0	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o ∅ ) = ∅ )
30	29	adantr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ∅ ) = ∅ )
31	30	oveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ∅ ) )
32	28 31	eqtr4d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o ∅ ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o ∅ ) ) )
33		oveq1	⊢ ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) = ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) )
34		nnasuc	⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
35	34	3adant1	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
36	35	oveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) )
37		nnacl	⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 +o 𝑦 ) ∈ ω )
38		nnmsuc	⊢ ( ( 𝐴 ∈ ω ∧ ( 𝐵 +o 𝑦 ) ∈ ω ) → ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
39	37 38	sylan2	⊢ ( ( 𝐴 ∈ ω ∧ ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
40	39	3impb	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o suc ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
41	36 40	eqtrd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) )
42		nnmsuc	⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
43	42	3adant2	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
44	43	oveq2d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
45		nnmcl	⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o 𝑦 ) ∈ ω )
46		nnaass	⊢ ( ( ( 𝐴 ·o 𝐵 ) ∈ ω ∧ ( 𝐴 ·o 𝑦 ) ∈ ω ∧ 𝐴 ∈ ω ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
47	25 46	syl3an1	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐴 ·o 𝑦 ) ∈ ω ∧ 𝐴 ∈ ω ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
48	45 47	syl3an2	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) ∧ 𝐴 ∈ ω ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
49	48	3exp	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ∈ ω → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) )
50	49	exp4b	⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) ) ) )
51	50	pm2.43a	⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) ) )
52	51	com4r	⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝑦 ∈ ω → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) ) )
53	52	pm2.43i	⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝑦 ∈ ω → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) ) ) )
54	53	3imp	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ) )
55	44 54	eqtr4d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) = ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) )
56	41 55	eqeq12d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ↔ ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) +o 𝐴 ) = ( ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) +o 𝐴 ) ) )
57	33 56	imbitrrid	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) )
58	57	3exp	⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝑦 ∈ ω → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) ) ) )
59	58	com3r	⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) ) ) )
60	59	impd	⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o ( 𝐵 +o 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑦 ) ) → ( 𝐴 ·o ( 𝐵 +o suc 𝑦 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o suc 𝑦 ) ) ) ) )
61	11 16 21 32 60	finds2	⊢ ( 𝑥 ∈ ω → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝑥 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝑥 ) ) ) )
62	6 61	vtoclga	⊢ ( 𝐶 ∈ ω → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) )
63	62	expdcom	⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝐶 ∈ ω → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) ) ) )
64	63	3imp	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )