Metamath Proof Explorer

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 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⋅ 𝑜 B + 𝑜 C = A ⋅ 𝑜 B + 𝑜 A ⋅ 𝑜 C

Proof

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