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 e. NN /\ B e. NN /\ C e. NN ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )

Proof

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