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