Metamath Proof Explorer

Theorem nadddi

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

Ref Expression
Assertion nadddi Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A .no ( B +no C ) ) = ( ( A .no B ) +no ( A .no C ) ) ) with typecode |-

Proof

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