Metamath Proof Explorer

Theorem nnadddir

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

Ref Expression
Assertion nnadddir ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐴 + 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) )

Proof

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