Metamath Proof Explorer

Theorem nadddi

Description: Natural multiplication distributes over natural addition. (Contributed by Scott Fenton, 27-Jul-2026)

Ref Expression
Assertion nadddi 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A .no ( B +no C ) ) = ( ( A .no B ) +no ( A .no C ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = d -> ( a .no ( b +no c ) ) = ( d .no ( b +no c ) ) )
2 oveq1 
 |-  ( a = d -> ( a .no b ) = ( d .no b ) )
3 oveq1 
 |-  ( a = d -> ( a .no c ) = ( d .no c ) )
4 2 3 oveq12d 
 |-  ( a = d -> ( ( a .no b ) +no ( a .no c ) ) = ( ( d .no b ) +no ( d .no c ) ) )
5 1 4 eqeq12d 
 |-  ( a = d -> ( ( a .no ( b +no c ) ) = ( ( a .no b ) +no ( a .no c ) ) <-> ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) ) )
6 oveq1 
 |-  ( b = e -> ( b +no c ) = ( e +no c ) )
7 6 oveq2d 
 |-  ( b = e -> ( d .no ( b +no c ) ) = ( d .no ( e +no c ) ) )
8 oveq2 
 |-  ( b = e -> ( d .no b ) = ( d .no e ) )
9 8 oveq1d 
 |-  ( b = e -> ( ( d .no b ) +no ( d .no c ) ) = ( ( d .no e ) +no ( d .no c ) ) )
10 7 9 eqeq12d 
 |-  ( b = e -> ( ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) <-> ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) ) )
11 oveq2 
 |-  ( c = f -> ( e +no c ) = ( e +no f ) )
12 11 oveq2d 
 |-  ( c = f -> ( d .no ( e +no c ) ) = ( d .no ( e +no f ) ) )
13 oveq2 
 |-  ( c = f -> ( d .no c ) = ( d .no f ) )
14 13 oveq2d 
 |-  ( c = f -> ( ( d .no e ) +no ( d .no c ) ) = ( ( d .no e ) +no ( d .no f ) ) )
15 12 14 eqeq12d 
 |-  ( c = f -> ( ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) <-> ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) ) )
16 oveq1 
 |-  ( a = d -> ( a .no ( e +no f ) ) = ( d .no ( e +no f ) ) )
17 oveq1 
 |-  ( a = d -> ( a .no e ) = ( d .no e ) )
18 oveq1 
 |-  ( a = d -> ( a .no f ) = ( d .no f ) )
19 17 18 oveq12d 
 |-  ( a = d -> ( ( a .no e ) +no ( a .no f ) ) = ( ( d .no e ) +no ( d .no f ) ) )
20 16 19 eqeq12d 
 |-  ( a = d -> ( ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) <-> ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) ) )
21 oveq1 
 |-  ( b = e -> ( b +no f ) = ( e +no f ) )
22 21 oveq2d 
 |-  ( b = e -> ( a .no ( b +no f ) ) = ( a .no ( e +no f ) ) )
23 oveq2 
 |-  ( b = e -> ( a .no b ) = ( a .no e ) )
24 23 oveq1d 
 |-  ( b = e -> ( ( a .no b ) +no ( a .no f ) ) = ( ( a .no e ) +no ( a .no f ) ) )
25 22 24 eqeq12d 
 |-  ( b = e -> ( ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) <-> ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) ) )
26 21 oveq2d 
 |-  ( b = e -> ( d .no ( b +no f ) ) = ( d .no ( e +no f ) ) )
27 8 oveq1d 
 |-  ( b = e -> ( ( d .no b ) +no ( d .no f ) ) = ( ( d .no e ) +no ( d .no f ) ) )
28 26 27 eqeq12d 
 |-  ( b = e -> ( ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) <-> ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) ) )
29 11 oveq2d 
 |-  ( c = f -> ( a .no ( e +no c ) ) = ( a .no ( e +no f ) ) )
30 oveq2 
 |-  ( c = f -> ( a .no c ) = ( a .no f ) )
31 30 oveq2d 
 |-  ( c = f -> ( ( a .no e ) +no ( a .no c ) ) = ( ( a .no e ) +no ( a .no f ) ) )
32 29 31 eqeq12d 
 |-  ( c = f -> ( ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) <-> ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) ) )
33 oveq1 
 |-  ( a = A -> ( a .no ( b +no c ) ) = ( A .no ( b +no c ) ) )
34 oveq1 
 |-  ( a = A -> ( a .no b ) = ( A .no b ) )
35 oveq1 
 |-  ( a = A -> ( a .no c ) = ( A .no c ) )
36 34 35 oveq12d 
 |-  ( a = A -> ( ( a .no b ) +no ( a .no c ) ) = ( ( A .no b ) +no ( A .no c ) ) )
37 33 36 eqeq12d 
 |-  ( a = A -> ( ( a .no ( b +no c ) ) = ( ( a .no b ) +no ( a .no c ) ) <-> ( A .no ( b +no c ) ) = ( ( A .no b ) +no ( A .no c ) ) ) )
38 oveq1 
 |-  ( b = B -> ( b +no c ) = ( B +no c ) )
39 38 oveq2d 
 |-  ( b = B -> ( A .no ( b +no c ) ) = ( A .no ( B +no c ) ) )
40 oveq2 
 |-  ( b = B -> ( A .no b ) = ( A .no B ) )
41 40 oveq1d 
 |-  ( b = B -> ( ( A .no b ) +no ( A .no c ) ) = ( ( A .no B ) +no ( A .no c ) ) )
42 39 41 eqeq12d 
 |-  ( b = B -> ( ( A .no ( b +no c ) ) = ( ( A .no b ) +no ( A .no c ) ) <-> ( A .no ( B +no c ) ) = ( ( A .no B ) +no ( A .no c ) ) ) )
43 oveq2 
 |-  ( c = C -> ( B +no c ) = ( B +no C ) )
44 43 oveq2d 
 |-  ( c = C -> ( A .no ( B +no c ) ) = ( A .no ( B +no C ) ) )
45 oveq2 
 |-  ( c = C -> ( A .no c ) = ( A .no C ) )
46 45 oveq2d 
 |-  ( c = C -> ( ( A .no B ) +no ( A .no c ) ) = ( ( A .no B ) +no ( A .no C ) ) )
47 44 46 eqeq12d 
 |-  ( c = C -> ( ( A .no ( B +no c ) ) = ( ( A .no B ) +no ( A .no c ) ) <-> ( A .no ( B +no C ) ) = ( ( A .no B ) +no ( A .no C ) ) ) )
48 simpl1 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> a e. On )
49 simpl2 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> b e. On )
50 simpl3 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> c e. On )
51 simpr21 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) )
52 simpr23 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) )
53 simpr3 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) )
54 simpr12 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) )
55 simpr13 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) )
56 48 49 50 51 52 53 54 55 nadddilem4 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> ( a .no ( b +no c ) ) C_ ( ( a .no b ) +no ( a .no c ) ) )
57 48 49 50 51 52 53 54 55 nadddilem2 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> ( ( a .no b ) +no ( a .no c ) ) C_ ( a .no ( b +no c ) ) )
58 56 57 eqssd 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) ) -> ( a .no ( b +no c ) ) = ( ( a .no b ) +no ( a .no c ) ) )
59 58 ex 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. d e. a A. e e. b A. f e. c ( d .no ( e +no f ) ) = ( ( d .no e ) +no ( d .no f ) ) /\ A. d e. a A. e e. b ( d .no ( e +no c ) ) = ( ( d .no e ) +no ( d .no c ) ) /\ A. d e. a A. f e. c ( d .no ( b +no f ) ) = ( ( d .no b ) +no ( d .no f ) ) ) /\ ( A. d e. a ( d .no ( b +no c ) ) = ( ( d .no b ) +no ( d .no c ) ) /\ A. e e. b A. f e. c ( a .no ( e +no f ) ) = ( ( a .no e ) +no ( a .no f ) ) /\ A. e e. b ( a .no ( e +no c ) ) = ( ( a .no e ) +no ( a .no c ) ) ) /\ A. f e. c ( a .no ( b +no f ) ) = ( ( a .no b ) +no ( a .no f ) ) ) -> ( a .no ( b +no c ) ) = ( ( a .no b ) +no ( a .no c ) ) ) )
60 5 10 15 20 25 28 32 37 42 47 59 on3ind 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A .no ( B +no C ) ) = ( ( A .no B ) +no ( A .no C ) ) )