Metamath Proof Explorer

Theorem nnadddir

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

Ref Expression
Assertion nnadddir ⊢A∈ℕ∧B∈ℕ∧C∈ℕ→A+B⁢C=A⁢C+B⁢C

Proof

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