:: Elementary Number Theory Problems. {P}art {XI}
:: by Adam Naumowicz
::
:: Received December 12, 2023
:: Copyright (c) 2023-2024 Association of Mizar Users


registration
let n be Nat;
cluster <%n%> -> NAT -valued ;
correctness
coherence
<%n%> is NAT -valued ;
;
end;

registration
let n1, n2 be Nat;
cluster <%n1,n2%> -> NAT -valued ;
correctness
coherence
<%n1,n2%> is NAT -valued ;
;
end;

registration
let n1, n2, n3 be Nat;
cluster <%n1,n2,n3%> -> NAT -valued ;
correctness
coherence
<%n1,n2,n3%> is NAT -valued ;
;
end;

registration
let n1, n2, n3, n4 be Nat;
cluster <%n1,n2,n3,n4%> -> NAT -valued ;
correctness
coherence
<%n1,n2,n3,n4%> is NAT -valued ;
;
end;

theorem Th1: :: NUMBER11:1
for b being Nat
for E being XFinSequence of NAT st E = {} holds
value (E,b) = 0
proof end;

theorem Th2: :: NUMBER11:2
for n, b being Nat holds value (<%n%>,b) = n
proof end;

theorem Th3: :: NUMBER11:3
for n, b being Nat st n < b & b > 1 holds
digits (n,b) = <%n%>
proof end;

theorem :: NUMBER11:4
for b being Nat st b > 1 holds
digits ((value (<%0%>,b)),b) = <%0%>
proof end;

theorem Th5: :: NUMBER11:5
for b being Nat st b > 1 holds
for s being NAT -valued XFinSequence st len s > 0 & s . ((len s) - 1) <> 0 & ( for i being Nat st i in dom s holds
s . i < b ) holds
digits ((value (s,b)),b) = s
proof end;

theorem Th6: :: NUMBER11:6
for n, b being Nat st n < b & b > 1 holds
Sum (digits (n,b)) = n
proof end;

theorem Th7: :: NUMBER11:7
for n, b being Nat st b > 1 holds
value ((n --> (b -' 1)),b) = (b |^ n) - 1
proof end;

theorem Th8: :: NUMBER11:8
for b being Nat st b > 1 holds
for s being NAT -valued XFinSequence st len s > 0 & ( for i being Nat st i in dom s holds
s . i < b ) holds
( (s . ((len s) - 1)) * (b |^ ((len s) -' 1)) <= value (s,b) & value (s,b) < b |^ (len s) )
proof end;

theorem Th9: :: NUMBER11:9
for n, b being Nat st b > 1 holds
n < b |^ (len (digits (n,b)))
proof end;

theorem Th10: :: NUMBER11:10
for n, m, b being Nat st n <> 0 & b > 1 & m < len (digits (n,b)) holds
n >= b |^ m
proof end;

theorem :: NUMBER11:11
for d1, d2 being XFinSequence of NAT
for b being Nat st b > 1 & dom d1 = dom d2 & ( for n being Nat st n in dom d1 holds
d1 . n <= d2 . n ) holds
value (d1,b) <= value (d2,b)
proof end;

theorem Th12: :: NUMBER11:12
for m, n, b being Nat st b > 1 holds
( ( len (digits (m,b)) < len (digits (n,b)) or ( len (digits (m,b)) = len (digits (n,b)) & ex i being Nat st
( i < len (digits (m,b)) & (digits (m,b)) . i < (digits (n,b)) . i & ( for j being Nat st j < len (digits (m,b)) & (digits (m,b)) . j <> (digits (n,b)) . j holds
i >= j ) ) ) ) iff m < n )
proof end;

theorem Th13: :: NUMBER11:13
for n being Nat holds
( 100 divides n iff ( (digits (n,10)) . 0 = 0 & (digits (n,10)) . 1 = 0 ) )
proof end;

theorem Th14: :: NUMBER11:14
for f being XFinSequence st len f >= 2 holds
f | 2 = <%(f . 0),(f . 1)%>
proof end;

definition
let n, s be Nat;
pred Sierp36 n,s means :: NUMBER11:def 1
( Sum (digits (n,10)) = s & s divides n & ( for m being Nat st Sum (digits (m,10)) = s & s divides m holds
n <= m ) );
end;

:: deftheorem defines Sierp36 NUMBER11:def 1 :
for n, s being Nat holds
( Sierp36 n,s iff ( Sum (digits (n,10)) = s & s divides n & ( for m being Nat st Sum (digits (m,10)) = s & s divides m holds
n <= m ) ) );

theorem :: NUMBER11:15
for n being Nat st n < 10 holds
Sierp36 n,n
proof end;

theorem Th16: :: NUMBER11:16
digits (10,10) = <%0,1%>
proof end;

theorem Th17: :: NUMBER11:17
Sum (digits (10,10)) = 1
proof end;

theorem Th18: :: NUMBER11:18
digits (20,10) = <%0,2%>
proof end;

theorem Th19: :: NUMBER11:19
Sum (digits (20,10)) = 2
proof end;

theorem Th20: :: NUMBER11:20
digits (30,10) = <%0,3%>
proof end;

theorem Th21: :: NUMBER11:21
Sum (digits (30,10)) = 3
proof end;

theorem Th22: :: NUMBER11:22
digits (40,10) = <%0,4%>
proof end;

theorem Th23: :: NUMBER11:23
Sum (digits (40,10)) = 4
proof end;

theorem Th24: :: NUMBER11:24
digits (50,10) = <%0,5%>
proof end;

theorem Th25: :: NUMBER11:25
Sum (digits (50,10)) = 5
proof end;

theorem Th26: :: NUMBER11:26
digits (60,10) = <%0,6%>
proof end;

theorem Th27: :: NUMBER11:27
Sum (digits (60,10)) = 6
proof end;

theorem Th28: :: NUMBER11:28
digits (70,10) = <%0,7%>
proof end;

theorem Th29: :: NUMBER11:29
Sum (digits (70,10)) = 7
proof end;

theorem Th30: :: NUMBER11:30
digits (80,10) = <%0,8%>
proof end;

theorem Th31: :: NUMBER11:31
Sum (digits (80,10)) = 8
proof end;

theorem Th32: :: NUMBER11:32
digits (90,10) = <%0,9%>
proof end;

theorem Th33: :: NUMBER11:33
Sum (digits (90,10)) = 9
proof end;

theorem Th34: :: NUMBER11:34
digits (100,10) = <%0,0,1%>
proof end;

theorem Th35: :: NUMBER11:35
Sum (digits (100,10)) = 1
proof end;

theorem Th36: :: NUMBER11:36
digits (110,10) = <%0,1,1%>
proof end;

theorem Th37: :: NUMBER11:37
Sum (digits (110,10)) = 2
proof end;

theorem Th38: :: NUMBER11:38
digits (120,10) = <%0,2,1%>
proof end;

theorem Th39: :: NUMBER11:39
Sum (digits (120,10)) = 3
proof end;

theorem Th40: :: NUMBER11:40
digits (130,10) = <%0,3,1%>
proof end;

theorem Th41: :: NUMBER11:41
Sum (digits (130,10)) = 4
proof end;

theorem Th42: :: NUMBER11:42
digits (140,10) = <%0,4,1%>
proof end;

theorem Th43: :: NUMBER11:43
Sum (digits (140,10)) = 5
proof end;

theorem Th44: :: NUMBER11:44
digits (150,10) = <%0,5,1%>
proof end;

theorem Th45: :: NUMBER11:45
Sum (digits (150,10)) = 6
proof end;

theorem Th46: :: NUMBER11:46
digits (160,10) = <%0,6,1%>
proof end;

theorem Th47: :: NUMBER11:47
Sum (digits (160,10)) = 7
proof end;

theorem Th48: :: NUMBER11:48
digits (170,10) = <%0,7,1%>
proof end;

theorem Th49: :: NUMBER11:49
Sum (digits (170,10)) = 8
proof end;

theorem Th50: :: NUMBER11:50
digits (180,10) = <%0,8,1%>
proof end;

theorem Th51: :: NUMBER11:51
Sum (digits (180,10)) = 9
proof end;

theorem Th52: :: NUMBER11:52
digits (190,10) = <%0,9,1%>
proof end;

theorem Th53: :: NUMBER11:53
Sum (digits (190,10)) = 10
proof end;

theorem :: NUMBER11:54
Sierp36 190,10
proof end;

theorem Th55: :: NUMBER11:55
digits (11,10) = <%1,1%>
proof end;

theorem Th56: :: NUMBER11:56
Sum (digits (11,10)) = 2
proof end;

theorem Th57: :: NUMBER11:57
digits (22,10) = <%2,2%>
proof end;

theorem Th58: :: NUMBER11:58
Sum (digits (22,10)) = 4
proof end;

theorem Th59: :: NUMBER11:59
digits (33,10) = <%3,3%>
proof end;

theorem Th60: :: NUMBER11:60
Sum (digits (33,10)) = 6
proof end;

theorem Th61: :: NUMBER11:61
digits (44,10) = <%4,4%>
proof end;

theorem Th62: :: NUMBER11:62
Sum (digits (44,10)) = 8
proof end;

theorem Th63: :: NUMBER11:63
digits (55,10) = <%5,5%>
proof end;

theorem Th64: :: NUMBER11:64
Sum (digits (55,10)) = 10
proof end;

theorem Th65: :: NUMBER11:65
digits (66,10) = <%6,6%>
proof end;

theorem Th66: :: NUMBER11:66
Sum (digits (66,10)) = 12
proof end;

theorem Th67: :: NUMBER11:67
digits (77,10) = <%7,7%>
proof end;

theorem Th68: :: NUMBER11:68
Sum (digits (77,10)) = 14
proof end;

theorem Th69: :: NUMBER11:69
digits (88,10) = <%8,8%>
proof end;

theorem Th70: :: NUMBER11:70
Sum (digits (88,10)) = 16
proof end;

theorem Th71: :: NUMBER11:71
digits (99,10) = <%9,9%>
proof end;

theorem Th72: :: NUMBER11:72
Sum (digits (99,10)) = 18
proof end;

theorem Th73: :: NUMBER11:73
digits (121,10) = <%1,2,1%>
proof end;

theorem Th74: :: NUMBER11:74
Sum (digits (121,10)) = 4
proof end;

theorem Th75: :: NUMBER11:75
digits (132,10) = <%2,3,1%>
proof end;

theorem Th76: :: NUMBER11:76
Sum (digits (132,10)) = 6
proof end;

theorem Th77: :: NUMBER11:77
digits (143,10) = <%3,4,1%>
proof end;

theorem Th78: :: NUMBER11:78
Sum (digits (143,10)) = 8
proof end;

theorem Th79: :: NUMBER11:79
digits (154,10) = <%4,5,1%>
proof end;

theorem Th80: :: NUMBER11:80
Sum (digits (154,10)) = 10
proof end;

theorem Th81: :: NUMBER11:81
digits (165,10) = <%5,6,1%>
proof end;

theorem Th82: :: NUMBER11:82
Sum (digits (165,10)) = 12
proof end;

theorem Th83: :: NUMBER11:83
digits (176,10) = <%6,7,1%>
proof end;

theorem Th84: :: NUMBER11:84
Sum (digits (176,10)) = 14
proof end;

theorem Th85: :: NUMBER11:85
digits (187,10) = <%7,8,1%>
proof end;

theorem Th86: :: NUMBER11:86
Sum (digits (187,10)) = 16
proof end;

theorem Th87: :: NUMBER11:87
digits (198,10) = <%8,9,1%>
proof end;

theorem Th88: :: NUMBER11:88
Sum (digits (198,10)) = 18
proof end;

theorem Th89: :: NUMBER11:89
digits (209,10) = <%9,0,2%>
proof end;

theorem Th90: :: NUMBER11:90
Sum (digits (209,10)) = 11
proof end;

theorem :: NUMBER11:91
Sierp36 209,11
proof end;

theorem Th92: :: NUMBER11:92
digits (12,10) = <%2,1%>
proof end;

theorem Th93: :: NUMBER11:93
Sum (digits (12,10)) = 3
proof end;

theorem Th94: :: NUMBER11:94
digits (24,10) = <%4,2%>
proof end;

theorem Th95: :: NUMBER11:95
Sum (digits (24,10)) = 6
proof end;

theorem Th96: :: NUMBER11:96
digits (36,10) = <%6,3%>
proof end;

theorem Th97: :: NUMBER11:97
Sum (digits (36,10)) = 9
proof end;

theorem Th98: :: NUMBER11:98
digits (48,10) = <%8,4%>
proof end;

theorem Th99: :: NUMBER11:99
Sum (digits (48,10)) = 12
proof end;

theorem :: NUMBER11:100
Sierp36 48,12
proof end;

theorem Th101: :: NUMBER11:101
digits (13,10) = <%3,1%>
proof end;

theorem Th102: :: NUMBER11:102
Sum (digits (13,10)) = 4
proof end;

theorem Th103: :: NUMBER11:103
digits (26,10) = <%6,2%>
proof end;

theorem Th104: :: NUMBER11:104
Sum (digits (26,10)) = 8
proof end;

theorem Th105: :: NUMBER11:105
digits (39,10) = <%9,3%>
proof end;

theorem Th106: :: NUMBER11:106
Sum (digits (39,10)) = 12
proof end;

theorem Th107: :: NUMBER11:107
digits (52,10) = <%2,5%>
proof end;

theorem Th108: :: NUMBER11:108
Sum (digits (52,10)) = 7
proof end;

theorem Th109: :: NUMBER11:109
digits (65,10) = <%5,6%>
proof end;

theorem Th110: :: NUMBER11:110
Sum (digits (65,10)) = 11
proof end;

theorem Th111: :: NUMBER11:111
digits (78,10) = <%8,7%>
proof end;

theorem Th112: :: NUMBER11:112
Sum (digits (78,10)) = 15
proof end;

theorem Th113: :: NUMBER11:113
digits (91,10) = <%1,9%>
proof end;

theorem Th114: :: NUMBER11:114
Sum (digits (91,10)) = 10
proof end;

theorem Th115: :: NUMBER11:115
digits (104,10) = <%4,0,1%>
proof end;

theorem Th116: :: NUMBER11:116
Sum (digits (104,10)) = 5
proof end;

theorem Th117: :: NUMBER11:117
digits (117,10) = <%7,1,1%>
proof end;

theorem Th118: :: NUMBER11:118
Sum (digits (117,10)) = 9
proof end;

theorem Th119: :: NUMBER11:119
digits (156,10) = <%6,5,1%>
proof end;

theorem Th120: :: NUMBER11:120
Sum (digits (156,10)) = 12
proof end;

theorem Th121: :: NUMBER11:121
digits (169,10) = <%9,6,1%>
proof end;

theorem Th122: :: NUMBER11:122
Sum (digits (169,10)) = 16
proof end;

theorem Th123: :: NUMBER11:123
digits (182,10) = <%2,8,1%>
proof end;

theorem Th124: :: NUMBER11:124
Sum (digits (182,10)) = 11
proof end;

theorem Th125: :: NUMBER11:125
digits (195,10) = <%5,9,1%>
proof end;

theorem Th126: :: NUMBER11:126
Sum (digits (195,10)) = 15
proof end;

theorem Th127: :: NUMBER11:127
digits (208,10) = <%8,0,2%>
proof end;

theorem Th128: :: NUMBER11:128
Sum (digits (208,10)) = 10
proof end;

theorem Th129: :: NUMBER11:129
digits (221,10) = <%1,2,2%>
proof end;

theorem Th130: :: NUMBER11:130
Sum (digits (221,10)) = 5
proof end;

theorem Th131: :: NUMBER11:131
digits (234,10) = <%4,3,2%>
proof end;

theorem Th132: :: NUMBER11:132
Sum (digits (234,10)) = 9
proof end;

theorem Th133: :: NUMBER11:133
digits (247,10) = <%7,4,2%>
proof end;

theorem Th134: :: NUMBER11:134
Sum (digits (247,10)) = 13
proof end;

theorem :: NUMBER11:135
Sierp36 247,13
proof end;

theorem Th136: :: NUMBER11:136
digits (14,10) = <%4,1%>
proof end;

theorem Th137: :: NUMBER11:137
Sum (digits (14,10)) = 5
proof end;

theorem Th138: :: NUMBER11:138
digits (28,10) = <%8,2%>
proof end;

theorem Th139: :: NUMBER11:139
Sum (digits (28,10)) = 10
proof end;

theorem Th140: :: NUMBER11:140
digits (42,10) = <%2,4%>
proof end;

theorem Th141: :: NUMBER11:141
Sum (digits (42,10)) = 6
proof end;

theorem Th142: :: NUMBER11:142
digits (56,10) = <%6,5%>
proof end;

theorem Th143: :: NUMBER11:143
Sum (digits (56,10)) = 11
proof end;

theorem Th144: :: NUMBER11:144
digits (84,10) = <%4,8%>
proof end;

theorem Th145: :: NUMBER11:145
Sum (digits (84,10)) = 12
proof end;

theorem Th146: :: NUMBER11:146
digits (98,10) = <%8,9%>
proof end;

theorem Th147: :: NUMBER11:147
Sum (digits (98,10)) = 17
proof end;

theorem Th148: :: NUMBER11:148
digits (112,10) = <%2,1,1%>
proof end;

theorem Th149: :: NUMBER11:149
Sum (digits (112,10)) = 4
proof end;

theorem Th150: :: NUMBER11:150
digits (126,10) = <%6,2,1%>
proof end;

theorem Th151: :: NUMBER11:151
Sum (digits (126,10)) = 9
proof end;

theorem Th152: :: NUMBER11:152
digits (168,10) = <%8,6,1%>
proof end;

theorem Th153: :: NUMBER11:153
Sum (digits (168,10)) = 15
proof end;

theorem Th154: :: NUMBER11:154
digits (196,10) = <%6,9,1%>
proof end;

theorem Th155: :: NUMBER11:155
Sum (digits (196,10)) = 16
proof end;

theorem Th156: :: NUMBER11:156
digits (210,10) = <%0,1,2%>
proof end;

theorem Th157: :: NUMBER11:157
Sum (digits (210,10)) = 3
proof end;

theorem Th158: :: NUMBER11:158
digits (224,10) = <%4,2,2%>
proof end;

theorem Th159: :: NUMBER11:159
Sum (digits (224,10)) = 8
proof end;

theorem Th160: :: NUMBER11:160
digits (238,10) = <%8,3,2%>
proof end;

theorem Th161: :: NUMBER11:161
Sum (digits (238,10)) = 13
proof end;

theorem Th162: :: NUMBER11:162
digits (252,10) = <%2,5,2%>
proof end;

theorem Th163: :: NUMBER11:163
Sum (digits (252,10)) = 9
proof end;

theorem Th164: :: NUMBER11:164
digits (266,10) = <%6,6,2%>
proof end;

theorem Th165: :: NUMBER11:165
Sum (digits (266,10)) = 14
proof end;

theorem :: NUMBER11:166
Sierp36 266,14
proof end;

theorem Th167: :: NUMBER11:167
digits (15,10) = <%5,1%>
proof end;

theorem Th168: :: NUMBER11:168
Sum (digits (15,10)) = 6
proof end;

theorem Th169: :: NUMBER11:169
digits (45,10) = <%5,4%>
proof end;

theorem Th170: :: NUMBER11:170
Sum (digits (45,10)) = 9
proof end;

theorem Th171: :: NUMBER11:171
digits (75,10) = <%5,7%>
proof end;

theorem Th172: :: NUMBER11:172
Sum (digits (75,10)) = 12
proof end;

theorem Th173: :: NUMBER11:173
digits (105,10) = <%5,0,1%>
proof end;

theorem Th174: :: NUMBER11:174
Sum (digits (105,10)) = 6
proof end;

theorem Th175: :: NUMBER11:175
digits (135,10) = <%5,3,1%>
proof end;

theorem Th176: :: NUMBER11:176
Sum (digits (135,10)) = 9
proof end;

theorem :: NUMBER11:177
Sierp36 195,15
proof end;

theorem Th178: :: NUMBER11:178
digits (16,10) = <%6,1%>
proof end;

theorem Th179: :: NUMBER11:179
Sum (digits (16,10)) = 7
proof end;

theorem Th180: :: NUMBER11:180
digits (32,10) = <%2,3%>
proof end;

theorem Th181: :: NUMBER11:181
Sum (digits (32,10)) = 5
proof end;

theorem Th182: :: NUMBER11:182
digits (64,10) = <%4,6%>
proof end;

theorem Th183: :: NUMBER11:183
Sum (digits (64,10)) = 10
proof end;

theorem Th184: :: NUMBER11:184
digits (96,10) = <%6,9%>
proof end;

theorem Th185: :: NUMBER11:185
Sum (digits (96,10)) = 15
proof end;

theorem Th186: :: NUMBER11:186
digits (128,10) = <%8,2,1%>
proof end;

theorem Th187: :: NUMBER11:187
Sum (digits (128,10)) = 11
proof end;

theorem Th188: :: NUMBER11:188
digits (144,10) = <%4,4,1%>
proof end;

theorem Th189: :: NUMBER11:189
Sum (digits (144,10)) = 9
proof end;

theorem Th190: :: NUMBER11:190
digits (192,10) = <%2,9,1%>
proof end;

theorem Th191: :: NUMBER11:191
Sum (digits (192,10)) = 12
proof end;

theorem Th192: :: NUMBER11:192
digits (240,10) = <%0,4,2%>
proof end;

theorem Th193: :: NUMBER11:193
Sum (digits (240,10)) = 6
proof end;

theorem Th194: :: NUMBER11:194
digits (256,10) = <%6,5,2%>
proof end;

theorem Th195: :: NUMBER11:195
Sum (digits (256,10)) = 13
proof end;

theorem Th196: :: NUMBER11:196
digits (272,10) = <%2,7,2%>
proof end;

theorem Th197: :: NUMBER11:197
Sum (digits (272,10)) = 11
proof end;

theorem Th198: :: NUMBER11:198
digits (288,10) = <%8,8,2%>
proof end;

theorem Th199: :: NUMBER11:199
Sum (digits (288,10)) = 18
proof end;

theorem Th200: :: NUMBER11:200
digits (304,10) = <%4,0,3%>
proof end;

theorem Th201: :: NUMBER11:201
Sum (digits (304,10)) = 7
proof end;

theorem Th202: :: NUMBER11:202
digits (320,10) = <%0,2,3%>
proof end;

theorem Th203: :: NUMBER11:203
Sum (digits (320,10)) = 5
proof end;

theorem Th204: :: NUMBER11:204
digits (336,10) = <%6,3,3%>
proof end;

theorem Th205: :: NUMBER11:205
Sum (digits (336,10)) = 12
proof end;

theorem Th206: :: NUMBER11:206
digits (352,10) = <%2,5,3%>
proof end;

theorem Th207: :: NUMBER11:207
Sum (digits (352,10)) = 10
proof end;

theorem Th208: :: NUMBER11:208
digits (368,10) = <%8,6,3%>
proof end;

theorem Th209: :: NUMBER11:209
Sum (digits (368,10)) = 17
proof end;

theorem Th210: :: NUMBER11:210
digits (384,10) = <%4,8,3%>
proof end;

theorem Th211: :: NUMBER11:211
Sum (digits (384,10)) = 15
proof end;

theorem Th212: :: NUMBER11:212
digits (400,10) = <%0,0,4%>
proof end;

theorem Th213: :: NUMBER11:213
Sum (digits (400,10)) = 4
proof end;

theorem Th214: :: NUMBER11:214
digits (416,10) = <%6,1,4%>
proof end;

theorem Th215: :: NUMBER11:215
Sum (digits (416,10)) = 11
proof end;

theorem Th216: :: NUMBER11:216
digits (432,10) = <%2,3,4%>
proof end;

theorem Th217: :: NUMBER11:217
Sum (digits (432,10)) = 9
proof end;

theorem Th218: :: NUMBER11:218
digits (448,10) = <%8,4,4%>
proof end;

theorem Th219: :: NUMBER11:219
Sum (digits (448,10)) = 16
proof end;

theorem :: NUMBER11:220
Sierp36 448,16
proof end;

theorem Th221: :: NUMBER11:221
digits (17,10) = <%7,1%>
proof end;

theorem Th222: :: NUMBER11:222
Sum (digits (17,10)) = 8
proof end;

theorem Th223: :: NUMBER11:223
digits (34,10) = <%4,3%>
proof end;

theorem Th224: :: NUMBER11:224
Sum (digits (34,10)) = 7
proof end;

theorem Th225: :: NUMBER11:225
digits (51,10) = <%1,5%>
proof end;

theorem Th226: :: NUMBER11:226
Sum (digits (51,10)) = 6
proof end;

theorem Th227: :: NUMBER11:227
digits (68,10) = <%8,6%>
proof end;

theorem Th228: :: NUMBER11:228
Sum (digits (68,10)) = 14
proof end;

theorem Th229: :: NUMBER11:229
digits (85,10) = <%5,8%>
proof end;

theorem Th230: :: NUMBER11:230
Sum (digits (85,10)) = 13
proof end;

theorem Th231: :: NUMBER11:231
digits (102,10) = <%2,0,1%>
proof end;

theorem Th232: :: NUMBER11:232
Sum (digits (102,10)) = 3
proof end;

theorem Th233: :: NUMBER11:233
digits (119,10) = <%9,1,1%>
proof end;

theorem Th234: :: NUMBER11:234
Sum (digits (119,10)) = 11
proof end;

theorem Th235: :: NUMBER11:235
digits (136,10) = <%6,3,1%>
proof end;

theorem Th236: :: NUMBER11:236
Sum (digits (136,10)) = 10
proof end;

theorem Th237: :: NUMBER11:237
digits (153,10) = <%3,5,1%>
proof end;

theorem Th238: :: NUMBER11:238
Sum (digits (153,10)) = 9
proof end;

theorem Th239: :: NUMBER11:239
digits (204,10) = <%4,0,2%>
proof end;

theorem Th240: :: NUMBER11:240
Sum (digits (204,10)) = 6
proof end;

theorem Th241: :: NUMBER11:241
digits (255,10) = <%5,5,2%>
proof end;

theorem Th242: :: NUMBER11:242
Sum (digits (255,10)) = 12
proof end;

theorem Th243: :: NUMBER11:243
digits (289,10) = <%9,8,2%>
proof end;

theorem Th244: :: NUMBER11:244
Sum (digits (289,10)) = 19
proof end;

theorem Th245: :: NUMBER11:245
digits (306,10) = <%6,0,3%>
proof end;

theorem Th246: :: NUMBER11:246
Sum (digits (306,10)) = 9
proof end;

theorem Th247: :: NUMBER11:247
digits (323,10) = <%3,2,3%>
proof end;

theorem Th248: :: NUMBER11:248
Sum (digits (323,10)) = 8
proof end;

theorem Th249: :: NUMBER11:249
digits (340,10) = <%0,4,3%>
proof end;

theorem Th250: :: NUMBER11:250
Sum (digits (340,10)) = 7
proof end;

theorem Th251: :: NUMBER11:251
digits (357,10) = <%7,5,3%>
proof end;

theorem Th252: :: NUMBER11:252
Sum (digits (357,10)) = 15
proof end;

theorem Th253: :: NUMBER11:253
digits (374,10) = <%4,7,3%>
proof end;

theorem Th254: :: NUMBER11:254
Sum (digits (374,10)) = 14
proof end;

theorem Th255: :: NUMBER11:255
digits (391,10) = <%1,9,3%>
proof end;

theorem Th256: :: NUMBER11:256
Sum (digits (391,10)) = 13
proof end;

theorem Th257: :: NUMBER11:257
digits (408,10) = <%8,0,4%>
proof end;

theorem Th258: :: NUMBER11:258
Sum (digits (408,10)) = 12
proof end;

theorem Th259: :: NUMBER11:259
digits (425,10) = <%5,2,4%>
proof end;

theorem Th260: :: NUMBER11:260
Sum (digits (425,10)) = 11
proof end;

theorem Th261: :: NUMBER11:261
digits (442,10) = <%2,4,4%>
proof end;

theorem Th262: :: NUMBER11:262
Sum (digits (442,10)) = 10
proof end;

theorem Th263: :: NUMBER11:263
digits (459,10) = <%9,5,4%>
proof end;

theorem Th264: :: NUMBER11:264
Sum (digits (459,10)) = 18
proof end;

theorem Th265: :: NUMBER11:265
digits (476,10) = <%6,7,4%>
proof end;

theorem Th266: :: NUMBER11:266
Sum (digits (476,10)) = 17
proof end;

theorem :: NUMBER11:267
Sierp36 476,17
proof end;

theorem Th268: :: NUMBER11:268
digits (18,10) = <%8,1%>
proof end;

theorem Th269: :: NUMBER11:269
Sum (digits (18,10)) = 9
proof end;

theorem Th270: :: NUMBER11:270
digits (54,10) = <%4,5%>
proof end;

theorem Th271: :: NUMBER11:271
Sum (digits (54,10)) = 9
proof end;

theorem Th272: :: NUMBER11:272
digits (72,10) = <%2,7%>
proof end;

theorem Th273: :: NUMBER11:273
Sum (digits (72,10)) = 9
proof end;

theorem Th274: :: NUMBER11:274
digits (108,10) = <%8,0,1%>
proof end;

theorem Th275: :: NUMBER11:275
Sum (digits (108,10)) = 9
proof end;

theorem Th276: :: NUMBER11:276
digits (162,10) = <%2,6,1%>
proof end;

theorem Th277: :: NUMBER11:277
Sum (digits (162,10)) = 9
proof end;

theorem :: NUMBER11:278
Sierp36 198,18
proof end;

theorem Th279: :: NUMBER11:279
digits (19,10) = <%9,1%>
proof end;

theorem Th280: :: NUMBER11:280
Sum (digits (19,10)) = 10
proof end;

theorem Th281: :: NUMBER11:281
digits (38,10) = <%8,3%>
proof end;

theorem Th282: :: NUMBER11:282
Sum (digits (38,10)) = 11
proof end;

theorem Th283: :: NUMBER11:283
digits (57,10) = <%7,5%>
proof end;

theorem Th284: :: NUMBER11:284
Sum (digits (57,10)) = 12
proof end;

theorem Th285: :: NUMBER11:285
digits (76,10) = <%6,7%>
proof end;

theorem Th286: :: NUMBER11:286
Sum (digits (76,10)) = 13
proof end;

theorem Th287: :: NUMBER11:287
digits (95,10) = <%5,9%>
proof end;

theorem Th288: :: NUMBER11:288
Sum (digits (95,10)) = 14
proof end;

theorem Th289: :: NUMBER11:289
digits (114,10) = <%4,1,1%>
proof end;

theorem Th290: :: NUMBER11:290
Sum (digits (114,10)) = 6
proof end;

theorem Th291: :: NUMBER11:291
digits (133,10) = <%3,3,1%>
proof end;

theorem Th292: :: NUMBER11:292
Sum (digits (133,10)) = 7
proof end;

theorem Th293: :: NUMBER11:293
digits (152,10) = <%2,5,1%>
proof end;

theorem Th294: :: NUMBER11:294
Sum (digits (152,10)) = 8
proof end;

theorem Th295: :: NUMBER11:295
digits (171,10) = <%1,7,1%>
proof end;

theorem Th296: :: NUMBER11:296
Sum (digits (171,10)) = 9
proof end;

theorem Th297: :: NUMBER11:297
digits (228,10) = <%8,2,2%>
proof end;

theorem Th298: :: NUMBER11:298
Sum (digits (228,10)) = 12
proof end;

theorem Th299: :: NUMBER11:299
digits (285,10) = <%5,8,2%>
proof end;

theorem Th300: :: NUMBER11:300
Sum (digits (285,10)) = 15
proof end;

theorem Th301: :: NUMBER11:301
digits (342,10) = <%2,4,3%>
proof end;

theorem Th302: :: NUMBER11:302
Sum (digits (342,10)) = 9
proof end;

theorem Th303: :: NUMBER11:303
digits (361,10) = <%1,6,3%>
proof end;

theorem Th304: :: NUMBER11:304
Sum (digits (361,10)) = 10
proof end;

theorem Th305: :: NUMBER11:305
digits (380,10) = <%0,8,3%>
proof end;

theorem Th306: :: NUMBER11:306
Sum (digits (380,10)) = 11
proof end;

theorem Th307: :: NUMBER11:307
digits (399,10) = <%9,9,3%>
proof end;

theorem Th308: :: NUMBER11:308
Sum (digits (399,10)) = 21
proof end;

theorem Th309: :: NUMBER11:309
digits (418,10) = <%8,1,4%>
proof end;

theorem Th310: :: NUMBER11:310
Sum (digits (418,10)) = 13
proof end;

theorem Th311: :: NUMBER11:311
digits (437,10) = <%7,3,4%>
proof end;

theorem Th312: :: NUMBER11:312
Sum (digits (437,10)) = 14
proof end;

theorem Th313: :: NUMBER11:313
digits (456,10) = <%6,5,4%>
proof end;

theorem Th314: :: NUMBER11:314
Sum (digits (456,10)) = 15
proof end;

theorem Th315: :: NUMBER11:315
digits (475,10) = <%5,7,4%>
proof end;

theorem Th316: :: NUMBER11:316
Sum (digits (475,10)) = 16
proof end;

theorem Th317: :: NUMBER11:317
digits (494,10) = <%4,9,4%>
proof end;

theorem Th318: :: NUMBER11:318
Sum (digits (494,10)) = 17
proof end;

theorem Th319: :: NUMBER11:319
digits (513,10) = <%3,1,5%>
proof end;

theorem Th320: :: NUMBER11:320
Sum (digits (513,10)) = 9
proof end;

theorem Th321: :: NUMBER11:321
digits (532,10) = <%2,3,5%>
proof end;

theorem Th322: :: NUMBER11:322
Sum (digits (532,10)) = 10
proof end;

theorem Th323: :: NUMBER11:323
digits (551,10) = <%1,5,5%>
proof end;

theorem Th324: :: NUMBER11:324
Sum (digits (551,10)) = 11
proof end;

theorem Th325: :: NUMBER11:325
digits (570,10) = <%0,7,5%>
proof end;

theorem Th326: :: NUMBER11:326
Sum (digits (570,10)) = 12
proof end;

theorem Th327: :: NUMBER11:327
digits (589,10) = <%9,8,5%>
proof end;

theorem Th328: :: NUMBER11:328
Sum (digits (589,10)) = 22
proof end;

theorem Th329: :: NUMBER11:329
digits (608,10) = <%8,0,6%>
proof end;

theorem Th330: :: NUMBER11:330
Sum (digits (608,10)) = 14
proof end;

theorem Th331: :: NUMBER11:331
digits (627,10) = <%7,2,6%>
proof end;

theorem Th332: :: NUMBER11:332
Sum (digits (627,10)) = 15
proof end;

theorem Th333: :: NUMBER11:333
digits (646,10) = <%6,4,6%>
proof end;

theorem Th334: :: NUMBER11:334
Sum (digits (646,10)) = 16
proof end;

theorem Th335: :: NUMBER11:335
digits (665,10) = <%5,6,6%>
proof end;

theorem Th336: :: NUMBER11:336
Sum (digits (665,10)) = 17
proof end;

theorem Th337: :: NUMBER11:337
digits (684,10) = <%4,8,6%>
proof end;

theorem Th338: :: NUMBER11:338
Sum (digits (684,10)) = 18
proof end;

theorem Th339: :: NUMBER11:339
digits (703,10) = <%3,0,7%>
proof end;

theorem Th340: :: NUMBER11:340
Sum (digits (703,10)) = 10
proof end;

theorem Th341: :: NUMBER11:341
digits (722,10) = <%2,2,7%>
proof end;

theorem Th342: :: NUMBER11:342
Sum (digits (722,10)) = 11
proof end;

theorem Th343: :: NUMBER11:343
digits (741,10) = <%1,4,7%>
proof end;

theorem Th344: :: NUMBER11:344
Sum (digits (741,10)) = 12
proof end;

theorem Th345: :: NUMBER11:345
digits (760,10) = <%0,6,7%>
proof end;

theorem Th346: :: NUMBER11:346
Sum (digits (760,10)) = 13
proof end;

theorem Th347: :: NUMBER11:347
digits (779,10) = <%9,7,7%>
proof end;

theorem Th348: :: NUMBER11:348
Sum (digits (779,10)) = 23
proof end;

theorem Th349: :: NUMBER11:349
digits (798,10) = <%8,9,7%>
proof end;

theorem Th350: :: NUMBER11:350
Sum (digits (798,10)) = 24
proof end;

theorem Th351: :: NUMBER11:351
digits (817,10) = <%7,1,8%>
proof end;

theorem Th352: :: NUMBER11:352
Sum (digits (817,10)) = 16
proof end;

theorem Th353: :: NUMBER11:353
digits (836,10) = <%6,3,8%>
proof end;

theorem Th354: :: NUMBER11:354
Sum (digits (836,10)) = 17
proof end;

theorem Th355: :: NUMBER11:355
digits (855,10) = <%5,5,8%>
proof end;

theorem Th356: :: NUMBER11:356
Sum (digits (855,10)) = 18
proof end;

theorem Th357: :: NUMBER11:357
digits (874,10) = <%4,7,8%>
proof end;

theorem Th358: :: NUMBER11:358
Sum (digits (874,10)) = 19
proof end;

theorem :: NUMBER11:359
Sierp36 874,19
proof end;

theorem Th360: :: NUMBER11:360
digits (200,10) = <%0,0,2%>
proof end;

theorem Th361: :: NUMBER11:361
Sum (digits (200,10)) = 2
proof end;

theorem Th362: :: NUMBER11:362
digits (220,10) = <%0,2,2%>
proof end;

theorem Th363: :: NUMBER11:363
Sum (digits (220,10)) = 4
proof end;

theorem Th364: :: NUMBER11:364
digits (260,10) = <%0,6,2%>
proof end;

theorem Th365: :: NUMBER11:365
Sum (digits (260,10)) = 8
proof end;

theorem Th366: :: NUMBER11:366
digits (280,10) = <%0,8,2%>
proof end;

theorem Th367: :: NUMBER11:367
Sum (digits (280,10)) = 10
proof end;

theorem Th368: :: NUMBER11:368
digits (300,10) = <%0,0,3%>
proof end;

theorem Th369: :: NUMBER11:369
Sum (digits (300,10)) = 3
proof end;

theorem Th370: :: NUMBER11:370
digits (360,10) = <%0,6,3%>
proof end;

theorem Th371: :: NUMBER11:371
Sum (digits (360,10)) = 9
proof end;

theorem Th372: :: NUMBER11:372
digits (420,10) = <%0,2,4%>
proof end;

theorem Th373: :: NUMBER11:373
Sum (digits (420,10)) = 6
proof end;

theorem Th374: :: NUMBER11:374
digits (440,10) = <%0,4,4%>
proof end;

theorem Th375: :: NUMBER11:375
Sum (digits (440,10)) = 8
proof end;

theorem Th376: :: NUMBER11:376
digits (460,10) = <%0,6,4%>
proof end;

theorem Th377: :: NUMBER11:377
Sum (digits (460,10)) = 10
proof end;

theorem Th378: :: NUMBER11:378
digits (480,10) = <%0,8,4%>
proof end;

theorem Th379: :: NUMBER11:379
Sum (digits (480,10)) = 12
proof end;

theorem Th380: :: NUMBER11:380
digits (500,10) = <%0,0,5%>
proof end;

theorem Th381: :: NUMBER11:381
Sum (digits (500,10)) = 5
proof end;

theorem Th382: :: NUMBER11:382
digits (520,10) = <%0,2,5%>
proof end;

theorem Th383: :: NUMBER11:383
Sum (digits (520,10)) = 7
proof end;

theorem Th384: :: NUMBER11:384
digits (540,10) = <%0,4,5%>
proof end;

theorem Th385: :: NUMBER11:385
Sum (digits (540,10)) = 9
proof end;

theorem Th386: :: NUMBER11:386
digits (560,10) = <%0,6,5%>
proof end;

theorem Th387: :: NUMBER11:387
Sum (digits (560,10)) = 11
proof end;

theorem Th388: :: NUMBER11:388
digits (580,10) = <%0,8,5%>
proof end;

theorem Th389: :: NUMBER11:389
Sum (digits (580,10)) = 13
proof end;

theorem Th390: :: NUMBER11:390
digits (600,10) = <%0,0,6%>
proof end;

theorem Th391: :: NUMBER11:391
Sum (digits (600,10)) = 6
proof end;

theorem Th392: :: NUMBER11:392
digits (620,10) = <%0,2,6%>
proof end;

theorem Th393: :: NUMBER11:393
Sum (digits (620,10)) = 8
proof end;

theorem Th394: :: NUMBER11:394
digits (640,10) = <%0,4,6%>
proof end;

theorem Th395: :: NUMBER11:395
Sum (digits (640,10)) = 10
proof end;

theorem Th396: :: NUMBER11:396
digits (660,10) = <%0,6,6%>
proof end;

theorem Th397: :: NUMBER11:397
Sum (digits (660,10)) = 12
proof end;

theorem Th398: :: NUMBER11:398
digits (680,10) = <%0,8,6%>
proof end;

theorem Th399: :: NUMBER11:399
Sum (digits (680,10)) = 14
proof end;

theorem Th400: :: NUMBER11:400
digits (700,10) = <%0,0,7%>
proof end;

theorem Th401: :: NUMBER11:401
Sum (digits (700,10)) = 7
proof end;

theorem Th402: :: NUMBER11:402
digits (720,10) = <%0,2,7%>
proof end;

theorem Th403: :: NUMBER11:403
Sum (digits (720,10)) = 9
proof end;

theorem Th404: :: NUMBER11:404
digits (740,10) = <%0,4,7%>
proof end;

theorem Th405: :: NUMBER11:405
Sum (digits (740,10)) = 11
proof end;

theorem Th406: :: NUMBER11:406
digits (780,10) = <%0,8,7%>
proof end;

theorem Th407: :: NUMBER11:407
Sum (digits (780,10)) = 15
proof end;

theorem Th408: :: NUMBER11:408
digits (800,10) = <%0,0,8%>
proof end;

theorem Th409: :: NUMBER11:409
Sum (digits (800,10)) = 8
proof end;

theorem Th410: :: NUMBER11:410
digits (820,10) = <%0,2,8%>
proof end;

theorem Th411: :: NUMBER11:411
Sum (digits (820,10)) = 10
proof end;

theorem Th412: :: NUMBER11:412
digits (840,10) = <%0,4,8%>
proof end;

theorem Th413: :: NUMBER11:413
Sum (digits (840,10)) = 12
proof end;

theorem Th414: :: NUMBER11:414
digits (860,10) = <%0,6,8%>
proof end;

theorem Th415: :: NUMBER11:415
Sum (digits (860,10)) = 14
proof end;

theorem Th416: :: NUMBER11:416
digits (880,10) = <%0,8,8%>
proof end;

theorem Th417: :: NUMBER11:417
Sum (digits (880,10)) = 16
proof end;

theorem Th418: :: NUMBER11:418
digits (900,10) = <%0,0,9%>
proof end;

theorem Th419: :: NUMBER11:419
Sum (digits (900,10)) = 9
proof end;

theorem Th420: :: NUMBER11:420
digits (920,10) = <%0,2,9%>
proof end;

theorem Th421: :: NUMBER11:421
Sum (digits (920,10)) = 11
proof end;

theorem Th422: :: NUMBER11:422
digits (940,10) = <%0,4,9%>
proof end;

theorem Th423: :: NUMBER11:423
Sum (digits (940,10)) = 13
proof end;

theorem Th424: :: NUMBER11:424
digits (960,10) = <%0,6,9%>
proof end;

theorem Th425: :: NUMBER11:425
Sum (digits (960,10)) = 15
proof end;

theorem Th426: :: NUMBER11:426
digits (980,10) = <%0,8,9%>
proof end;

theorem Th427: :: NUMBER11:427
Sum (digits (980,10)) = 17
proof end;

theorem Th428: :: NUMBER11:428
digits (1000,10) = <%0,0,0,1%>
proof end;

theorem Th429: :: NUMBER11:429
Sum (digits (1000,10)) = 1
proof end;

theorem Th430: :: NUMBER11:430
digits (1020,10) = <%0,2,0,1%>
proof end;

theorem Th431: :: NUMBER11:431
Sum (digits (1020,10)) = 3
proof end;

theorem Th432: :: NUMBER11:432
digits (1040,10) = <%0,4,0,1%>
proof end;

theorem Th433: :: NUMBER11:433
Sum (digits (1040,10)) = 5
proof end;

theorem Th434: :: NUMBER11:434
digits (1060,10) = <%0,6,0,1%>
proof end;

theorem Th435: :: NUMBER11:435
Sum (digits (1060,10)) = 7
proof end;

theorem Th436: :: NUMBER11:436
digits (1080,10) = <%0,8,0,1%>
proof end;

theorem Th437: :: NUMBER11:437
Sum (digits (1080,10)) = 9
proof end;

theorem Th438: :: NUMBER11:438
digits (1100,10) = <%0,0,1,1%>
proof end;

theorem Th439: :: NUMBER11:439
Sum (digits (1100,10)) = 2
proof end;

theorem Th440: :: NUMBER11:440
digits (1120,10) = <%0,2,1,1%>
proof end;

theorem Th441: :: NUMBER11:441
Sum (digits (1120,10)) = 4
proof end;

theorem Th442: :: NUMBER11:442
digits (1140,10) = <%0,4,1,1%>
proof end;

theorem Th443: :: NUMBER11:443
Sum (digits (1140,10)) = 6
proof end;

theorem Th444: :: NUMBER11:444
digits (1160,10) = <%0,6,1,1%>
proof end;

theorem Th445: :: NUMBER11:445
Sum (digits (1160,10)) = 8
proof end;

theorem Th446: :: NUMBER11:446
digits (1180,10) = <%0,8,1,1%>
proof end;

theorem Th447: :: NUMBER11:447
Sum (digits (1180,10)) = 10
proof end;

theorem Th448: :: NUMBER11:448
digits (1200,10) = <%0,0,2,1%>
proof end;

theorem Th449: :: NUMBER11:449
Sum (digits (1200,10)) = 3
proof end;

theorem Th450: :: NUMBER11:450
digits (1220,10) = <%0,2,2,1%>
proof end;

theorem Th451: :: NUMBER11:451
Sum (digits (1220,10)) = 5
proof end;

theorem Th452: :: NUMBER11:452
digits (1240,10) = <%0,4,2,1%>
proof end;

theorem Th453: :: NUMBER11:453
Sum (digits (1240,10)) = 7
proof end;

theorem Th454: :: NUMBER11:454
digits (1260,10) = <%0,6,2,1%>
proof end;

theorem Th455: :: NUMBER11:455
Sum (digits (1260,10)) = 9
proof end;

theorem Th456: :: NUMBER11:456
digits (1280,10) = <%0,8,2,1%>
proof end;

theorem Th457: :: NUMBER11:457
Sum (digits (1280,10)) = 11
proof end;

theorem Th458: :: NUMBER11:458
digits (1300,10) = <%0,0,3,1%>
proof end;

theorem Th459: :: NUMBER11:459
Sum (digits (1300,10)) = 4
proof end;

theorem Th460: :: NUMBER11:460
digits (1320,10) = <%0,2,3,1%>
proof end;

theorem Th461: :: NUMBER11:461
Sum (digits (1320,10)) = 6
proof end;

theorem Th462: :: NUMBER11:462
digits (1340,10) = <%0,4,3,1%>
proof end;

theorem Th463: :: NUMBER11:463
Sum (digits (1340,10)) = 8
proof end;

theorem Th464: :: NUMBER11:464
digits (1360,10) = <%0,6,3,1%>
proof end;

theorem Th465: :: NUMBER11:465
Sum (digits (1360,10)) = 10
proof end;

theorem Th466: :: NUMBER11:466
digits (1380,10) = <%0,8,3,1%>
proof end;

theorem Th467: :: NUMBER11:467
Sum (digits (1380,10)) = 12
proof end;

theorem Th468: :: NUMBER11:468
digits (1400,10) = <%0,0,4,1%>
proof end;

theorem Th469: :: NUMBER11:469
Sum (digits (1400,10)) = 5
proof end;

theorem Th470: :: NUMBER11:470
digits (1420,10) = <%0,2,4,1%>
proof end;

theorem Th471: :: NUMBER11:471
Sum (digits (1420,10)) = 7
proof end;

theorem Th472: :: NUMBER11:472
digits (1440,10) = <%0,4,4,1%>
proof end;

theorem Th473: :: NUMBER11:473
Sum (digits (1440,10)) = 9
proof end;

theorem Th474: :: NUMBER11:474
digits (1460,10) = <%0,6,4,1%>
proof end;

theorem Th475: :: NUMBER11:475
Sum (digits (1460,10)) = 11
proof end;

theorem Th476: :: NUMBER11:476
digits (1480,10) = <%0,8,4,1%>
proof end;

theorem Th477: :: NUMBER11:477
Sum (digits (1480,10)) = 13
proof end;

theorem Th478: :: NUMBER11:478
digits (1500,10) = <%0,0,5,1%>
proof end;

theorem Th479: :: NUMBER11:479
Sum (digits (1500,10)) = 6
proof end;

theorem Th480: :: NUMBER11:480
digits (1520,10) = <%0,2,5,1%>
proof end;

theorem Th481: :: NUMBER11:481
Sum (digits (1520,10)) = 8
proof end;

theorem Th482: :: NUMBER11:482
digits (1540,10) = <%0,4,5,1%>
proof end;

theorem Th483: :: NUMBER11:483
Sum (digits (1540,10)) = 10
proof end;

theorem Th484: :: NUMBER11:484
digits (1560,10) = <%0,6,5,1%>
proof end;

theorem Th485: :: NUMBER11:485
Sum (digits (1560,10)) = 12
proof end;

theorem Th486: :: NUMBER11:486
digits (1580,10) = <%0,8,5,1%>
proof end;

theorem Th487: :: NUMBER11:487
Sum (digits (1580,10)) = 14
proof end;

theorem Th488: :: NUMBER11:488
digits (1600,10) = <%0,0,6,1%>
proof end;

theorem Th489: :: NUMBER11:489
Sum (digits (1600,10)) = 7
proof end;

theorem Th490: :: NUMBER11:490
digits (1620,10) = <%0,2,6,1%>
proof end;

theorem Th491: :: NUMBER11:491
Sum (digits (1620,10)) = 9
proof end;

theorem Th492: :: NUMBER11:492
digits (1640,10) = <%0,4,6,1%>
proof end;

theorem Th493: :: NUMBER11:493
Sum (digits (1640,10)) = 11
proof end;

theorem Th494: :: NUMBER11:494
digits (1660,10) = <%0,6,6,1%>
proof end;

theorem Th495: :: NUMBER11:495
Sum (digits (1660,10)) = 13
proof end;

theorem Th496: :: NUMBER11:496
digits (1680,10) = <%0,8,6,1%>
proof end;

theorem Th497: :: NUMBER11:497
Sum (digits (1680,10)) = 15
proof end;

theorem Th498: :: NUMBER11:498
digits (1700,10) = <%0,0,7,1%>
proof end;

theorem Th499: :: NUMBER11:499
Sum (digits (1700,10)) = 8
proof end;

theorem Th500: :: NUMBER11:500
digits (1720,10) = <%0,2,7,1%>
proof end;

theorem Th501: :: NUMBER11:501
Sum (digits (1720,10)) = 10
proof end;

theorem Th502: :: NUMBER11:502
digits (1740,10) = <%0,4,7,1%>
proof end;

theorem Th503: :: NUMBER11:503
Sum (digits (1740,10)) = 12
proof end;

theorem Th504: :: NUMBER11:504
digits (1760,10) = <%0,6,7,1%>
proof end;

theorem Th505: :: NUMBER11:505
Sum (digits (1760,10)) = 14
proof end;

theorem Th506: :: NUMBER11:506
digits (1780,10) = <%0,8,7,1%>
proof end;

theorem Th507: :: NUMBER11:507
Sum (digits (1780,10)) = 16
proof end;

theorem Th508: :: NUMBER11:508
digits (1800,10) = <%0,0,8,1%>
proof end;

theorem Th509: :: NUMBER11:509
Sum (digits (1800,10)) = 9
proof end;

theorem Th510: :: NUMBER11:510
digits (1820,10) = <%0,2,8,1%>
proof end;

theorem Th511: :: NUMBER11:511
Sum (digits (1820,10)) = 11
proof end;

theorem Th512: :: NUMBER11:512
digits (1840,10) = <%0,4,8,1%>
proof end;

theorem Th513: :: NUMBER11:513
Sum (digits (1840,10)) = 13
proof end;

theorem Th514: :: NUMBER11:514
digits (1860,10) = <%0,6,8,1%>
proof end;

theorem Th515: :: NUMBER11:515
Sum (digits (1860,10)) = 15
proof end;

theorem Th516: :: NUMBER11:516
digits (1880,10) = <%0,8,8,1%>
proof end;

theorem Th517: :: NUMBER11:517
Sum (digits (1880,10)) = 17
proof end;

theorem Th518: :: NUMBER11:518
digits (1900,10) = <%0,0,9,1%>
proof end;

theorem Th519: :: NUMBER11:519
Sum (digits (1900,10)) = 10
proof end;

theorem Th520: :: NUMBER11:520
digits (1920,10) = <%0,2,9,1%>
proof end;

theorem Th521: :: NUMBER11:521
Sum (digits (1920,10)) = 12
proof end;

theorem Th522: :: NUMBER11:522
digits (1940,10) = <%0,4,9,1%>
proof end;

theorem Th523: :: NUMBER11:523
Sum (digits (1940,10)) = 14
proof end;

theorem Th524: :: NUMBER11:524
digits (1960,10) = <%0,6,9,1%>
proof end;

theorem Th525: :: NUMBER11:525
Sum (digits (1960,10)) = 16
proof end;

theorem Th526: :: NUMBER11:526
digits (1980,10) = <%0,8,9,1%>
proof end;

theorem Th527: :: NUMBER11:527
Sum (digits (1980,10)) = 18
proof end;

theorem Th528: :: NUMBER11:528
digits (2000,10) = <%0,0,0,2%>
proof end;

theorem Th529: :: NUMBER11:529
Sum (digits (2000,10)) = 2
proof end;

theorem Th530: :: NUMBER11:530
digits (2020,10) = <%0,2,0,2%>
proof end;

theorem Th531: :: NUMBER11:531
Sum (digits (2020,10)) = 4
proof end;

theorem Th532: :: NUMBER11:532
digits (2040,10) = <%0,4,0,2%>
proof end;

theorem Th533: :: NUMBER11:533
Sum (digits (2040,10)) = 6
proof end;

theorem Th534: :: NUMBER11:534
digits (2060,10) = <%0,6,0,2%>
proof end;

theorem Th535: :: NUMBER11:535
Sum (digits (2060,10)) = 8
proof end;

theorem Th536: :: NUMBER11:536
digits (2080,10) = <%0,8,0,2%>
proof end;

theorem Th537: :: NUMBER11:537
Sum (digits (2080,10)) = 10
proof end;

theorem Th538: :: NUMBER11:538
digits (2100,10) = <%0,0,1,2%>
proof end;

theorem Th539: :: NUMBER11:539
Sum (digits (2100,10)) = 3
proof end;

theorem Th540: :: NUMBER11:540
digits (2120,10) = <%0,2,1,2%>
proof end;

theorem Th541: :: NUMBER11:541
Sum (digits (2120,10)) = 5
proof end;

theorem Th542: :: NUMBER11:542
digits (2140,10) = <%0,4,1,2%>
proof end;

theorem Th543: :: NUMBER11:543
Sum (digits (2140,10)) = 7
proof end;

theorem Th544: :: NUMBER11:544
digits (2160,10) = <%0,6,1,2%>
proof end;

theorem Th545: :: NUMBER11:545
Sum (digits (2160,10)) = 9
proof end;

theorem Th546: :: NUMBER11:546
digits (2180,10) = <%0,8,1,2%>
proof end;

theorem Th547: :: NUMBER11:547
Sum (digits (2180,10)) = 11
proof end;

theorem Th548: :: NUMBER11:548
digits (2200,10) = <%0,0,2,2%>
proof end;

theorem Th549: :: NUMBER11:549
Sum (digits (2200,10)) = 4
proof end;

theorem Th550: :: NUMBER11:550
digits (2220,10) = <%0,2,2,2%>
proof end;

theorem Th551: :: NUMBER11:551
Sum (digits (2220,10)) = 6
proof end;

theorem Th552: :: NUMBER11:552
digits (2240,10) = <%0,4,2,2%>
proof end;

theorem Th553: :: NUMBER11:553
Sum (digits (2240,10)) = 8
proof end;

theorem Th554: :: NUMBER11:554
digits (2260,10) = <%0,6,2,2%>
proof end;

theorem Th555: :: NUMBER11:555
Sum (digits (2260,10)) = 10
proof end;

theorem Th556: :: NUMBER11:556
digits (2280,10) = <%0,8,2,2%>
proof end;

theorem Th557: :: NUMBER11:557
Sum (digits (2280,10)) = 12
proof end;

theorem Th558: :: NUMBER11:558
digits (2300,10) = <%0,0,3,2%>
proof end;

theorem Th559: :: NUMBER11:559
Sum (digits (2300,10)) = 5
proof end;

theorem Th560: :: NUMBER11:560
digits (2320,10) = <%0,2,3,2%>
proof end;

theorem Th561: :: NUMBER11:561
Sum (digits (2320,10)) = 7
proof end;

theorem Th562: :: NUMBER11:562
digits (2340,10) = <%0,4,3,2%>
proof end;

theorem Th563: :: NUMBER11:563
Sum (digits (2340,10)) = 9
proof end;

theorem Th564: :: NUMBER11:564
digits (2360,10) = <%0,6,3,2%>
proof end;

theorem Th565: :: NUMBER11:565
Sum (digits (2360,10)) = 11
proof end;

theorem Th566: :: NUMBER11:566
digits (2380,10) = <%0,8,3,2%>
proof end;

theorem Th567: :: NUMBER11:567
Sum (digits (2380,10)) = 13
proof end;

theorem Th568: :: NUMBER11:568
digits (2400,10) = <%0,0,4,2%>
proof end;

theorem Th569: :: NUMBER11:569
Sum (digits (2400,10)) = 6
proof end;

theorem Th570: :: NUMBER11:570
digits (2420,10) = <%0,2,4,2%>
proof end;

theorem Th571: :: NUMBER11:571
Sum (digits (2420,10)) = 8
proof end;

theorem Th572: :: NUMBER11:572
digits (2440,10) = <%0,4,4,2%>
proof end;

theorem Th573: :: NUMBER11:573
Sum (digits (2440,10)) = 10
proof end;

theorem Th574: :: NUMBER11:574
digits (2460,10) = <%0,6,4,2%>
proof end;

theorem Th575: :: NUMBER11:575
Sum (digits (2460,10)) = 12
proof end;

theorem Th576: :: NUMBER11:576
digits (2480,10) = <%0,8,4,2%>
proof end;

theorem Th577: :: NUMBER11:577
Sum (digits (2480,10)) = 14
proof end;

theorem Th578: :: NUMBER11:578
digits (2500,10) = <%0,0,5,2%>
proof end;

theorem Th579: :: NUMBER11:579
Sum (digits (2500,10)) = 7
proof end;

theorem Th580: :: NUMBER11:580
digits (2520,10) = <%0,2,5,2%>
proof end;

theorem Th581: :: NUMBER11:581
Sum (digits (2520,10)) = 9
proof end;

theorem Th582: :: NUMBER11:582
digits (2540,10) = <%0,4,5,2%>
proof end;

theorem Th583: :: NUMBER11:583
Sum (digits (2540,10)) = 11
proof end;

theorem Th584: :: NUMBER11:584
digits (2560,10) = <%0,6,5,2%>
proof end;

theorem Th585: :: NUMBER11:585
Sum (digits (2560,10)) = 13
proof end;

theorem Th586: :: NUMBER11:586
digits (2580,10) = <%0,8,5,2%>
proof end;

theorem Th587: :: NUMBER11:587
Sum (digits (2580,10)) = 15
proof end;

theorem Th588: :: NUMBER11:588
digits (2600,10) = <%0,0,6,2%>
proof end;

theorem Th589: :: NUMBER11:589
Sum (digits (2600,10)) = 8
proof end;

theorem Th590: :: NUMBER11:590
digits (2620,10) = <%0,2,6,2%>
proof end;

theorem Th591: :: NUMBER11:591
Sum (digits (2620,10)) = 10
proof end;

theorem Th592: :: NUMBER11:592
digits (2640,10) = <%0,4,6,2%>
proof end;

theorem Th593: :: NUMBER11:593
Sum (digits (2640,10)) = 12
proof end;

theorem Th594: :: NUMBER11:594
digits (2660,10) = <%0,6,6,2%>
proof end;

theorem Th595: :: NUMBER11:595
Sum (digits (2660,10)) = 14
proof end;

theorem Th596: :: NUMBER11:596
digits (2680,10) = <%0,8,6,2%>
proof end;

theorem Th597: :: NUMBER11:597
Sum (digits (2680,10)) = 16
proof end;

theorem Th598: :: NUMBER11:598
digits (2700,10) = <%0,0,7,2%>
proof end;

theorem Th599: :: NUMBER11:599
Sum (digits (2700,10)) = 9
proof end;

theorem Th600: :: NUMBER11:600
digits (2720,10) = <%0,2,7,2%>
proof end;

theorem Th601: :: NUMBER11:601
Sum (digits (2720,10)) = 11
proof end;

theorem Th602: :: NUMBER11:602
digits (2740,10) = <%0,4,7,2%>
proof end;

theorem Th603: :: NUMBER11:603
Sum (digits (2740,10)) = 13
proof end;

theorem Th604: :: NUMBER11:604
digits (2760,10) = <%0,6,7,2%>
proof end;

theorem Th605: :: NUMBER11:605
Sum (digits (2760,10)) = 15
proof end;

theorem Th606: :: NUMBER11:606
digits (2780,10) = <%0,8,7,2%>
proof end;

theorem Th607: :: NUMBER11:607
Sum (digits (2780,10)) = 17
proof end;

theorem Th608: :: NUMBER11:608
digits (2800,10) = <%0,0,8,2%>
proof end;

theorem Th609: :: NUMBER11:609
Sum (digits (2800,10)) = 10
proof end;

theorem Th610: :: NUMBER11:610
digits (2820,10) = <%0,2,8,2%>
proof end;

theorem Th611: :: NUMBER11:611
Sum (digits (2820,10)) = 12
proof end;

theorem Th612: :: NUMBER11:612
digits (2840,10) = <%0,4,8,2%>
proof end;

theorem Th613: :: NUMBER11:613
Sum (digits (2840,10)) = 14
proof end;

theorem Th614: :: NUMBER11:614
digits (2860,10) = <%0,6,8,2%>
proof end;

theorem Th615: :: NUMBER11:615
Sum (digits (2860,10)) = 16
proof end;

theorem Th616: :: NUMBER11:616
digits (2880,10) = <%0,8,8,2%>
proof end;

theorem Th617: :: NUMBER11:617
Sum (digits (2880,10)) = 18
proof end;

theorem Th618: :: NUMBER11:618
digits (2900,10) = <%0,0,9,2%>
proof end;

theorem Th619: :: NUMBER11:619
Sum (digits (2900,10)) = 11
proof end;

theorem Th620: :: NUMBER11:620
digits (2920,10) = <%0,2,9,2%>
proof end;

theorem Th621: :: NUMBER11:621
Sum (digits (2920,10)) = 13
proof end;

theorem Th622: :: NUMBER11:622
digits (2940,10) = <%0,4,9,2%>
proof end;

theorem Th623: :: NUMBER11:623
Sum (digits (2940,10)) = 15
proof end;

theorem Th624: :: NUMBER11:624
digits (2960,10) = <%0,6,9,2%>
proof end;

theorem Th625: :: NUMBER11:625
Sum (digits (2960,10)) = 17
proof end;

theorem Th626: :: NUMBER11:626
digits (2980,10) = <%0,8,9,2%>
proof end;

theorem Th627: :: NUMBER11:627
Sum (digits (2980,10)) = 19
proof end;

theorem Th628: :: NUMBER11:628
digits (3000,10) = <%0,0,0,3%>
proof end;

theorem Th629: :: NUMBER11:629
Sum (digits (3000,10)) = 3
proof end;

theorem Th630: :: NUMBER11:630
digits (3020,10) = <%0,2,0,3%>
proof end;

theorem Th631: :: NUMBER11:631
Sum (digits (3020,10)) = 5
proof end;

theorem Th632: :: NUMBER11:632
digits (3040,10) = <%0,4,0,3%>
proof end;

theorem Th633: :: NUMBER11:633
Sum (digits (3040,10)) = 7
proof end;

theorem Th634: :: NUMBER11:634
digits (3060,10) = <%0,6,0,3%>
proof end;

theorem Th635: :: NUMBER11:635
Sum (digits (3060,10)) = 9
proof end;

theorem Th636: :: NUMBER11:636
digits (3080,10) = <%0,8,0,3%>
proof end;

theorem Th637: :: NUMBER11:637
Sum (digits (3080,10)) = 11
proof end;

theorem Th638: :: NUMBER11:638
digits (3100,10) = <%0,0,1,3%>
proof end;

theorem Th639: :: NUMBER11:639
Sum (digits (3100,10)) = 4
proof end;

theorem Th640: :: NUMBER11:640
digits (3120,10) = <%0,2,1,3%>
proof end;

theorem Th641: :: NUMBER11:641
Sum (digits (3120,10)) = 6
proof end;

theorem Th642: :: NUMBER11:642
digits (3140,10) = <%0,4,1,3%>
proof end;

theorem Th643: :: NUMBER11:643
Sum (digits (3140,10)) = 8
proof end;

theorem Th644: :: NUMBER11:644
digits (3160,10) = <%0,6,1,3%>
proof end;

theorem Th645: :: NUMBER11:645
Sum (digits (3160,10)) = 10
proof end;

theorem Th646: :: NUMBER11:646
digits (3180,10) = <%0,8,1,3%>
proof end;

theorem Th647: :: NUMBER11:647
Sum (digits (3180,10)) = 12
proof end;

theorem Th648: :: NUMBER11:648
digits (3200,10) = <%0,0,2,3%>
proof end;

theorem Th649: :: NUMBER11:649
Sum (digits (3200,10)) = 5
proof end;

theorem Th650: :: NUMBER11:650
digits (3220,10) = <%0,2,2,3%>
proof end;

theorem Th651: :: NUMBER11:651
Sum (digits (3220,10)) = 7
proof end;

theorem Th652: :: NUMBER11:652
digits (3240,10) = <%0,4,2,3%>
proof end;

theorem Th653: :: NUMBER11:653
Sum (digits (3240,10)) = 9
proof end;

theorem Th654: :: NUMBER11:654
digits (3260,10) = <%0,6,2,3%>
proof end;

theorem Th655: :: NUMBER11:655
Sum (digits (3260,10)) = 11
proof end;

theorem Th656: :: NUMBER11:656
digits (3280,10) = <%0,8,2,3%>
proof end;

theorem Th657: :: NUMBER11:657
Sum (digits (3280,10)) = 13
proof end;

theorem Th658: :: NUMBER11:658
digits (3300,10) = <%0,0,3,3%>
proof end;

theorem Th659: :: NUMBER11:659
Sum (digits (3300,10)) = 6
proof end;

theorem Th660: :: NUMBER11:660
digits (3320,10) = <%0,2,3,3%>
proof end;

theorem Th661: :: NUMBER11:661
Sum (digits (3320,10)) = 8
proof end;

theorem Th662: :: NUMBER11:662
digits (3340,10) = <%0,4,3,3%>
proof end;

theorem Th663: :: NUMBER11:663
Sum (digits (3340,10)) = 10
proof end;

theorem Th664: :: NUMBER11:664
digits (3360,10) = <%0,6,3,3%>
proof end;

theorem Th665: :: NUMBER11:665
Sum (digits (3360,10)) = 12
proof end;

theorem Th666: :: NUMBER11:666
digits (3380,10) = <%0,8,3,3%>
proof end;

theorem Th667: :: NUMBER11:667
Sum (digits (3380,10)) = 14
proof end;

theorem Th668: :: NUMBER11:668
digits (3400,10) = <%0,0,4,3%>
proof end;

theorem Th669: :: NUMBER11:669
Sum (digits (3400,10)) = 7
proof end;

theorem Th670: :: NUMBER11:670
digits (3420,10) = <%0,2,4,3%>
proof end;

theorem Th671: :: NUMBER11:671
Sum (digits (3420,10)) = 9
proof end;

theorem Th672: :: NUMBER11:672
digits (3440,10) = <%0,4,4,3%>
proof end;

theorem Th673: :: NUMBER11:673
Sum (digits (3440,10)) = 11
proof end;

theorem Th674: :: NUMBER11:674
digits (3460,10) = <%0,6,4,3%>
proof end;

theorem Th675: :: NUMBER11:675
Sum (digits (3460,10)) = 13
proof end;

theorem Th676: :: NUMBER11:676
digits (3480,10) = <%0,8,4,3%>
proof end;

theorem Th677: :: NUMBER11:677
Sum (digits (3480,10)) = 15
proof end;

theorem Th678: :: NUMBER11:678
digits (3500,10) = <%0,0,5,3%>
proof end;

theorem Th679: :: NUMBER11:679
Sum (digits (3500,10)) = 8
proof end;

theorem Th680: :: NUMBER11:680
digits (3520,10) = <%0,2,5,3%>
proof end;

theorem Th681: :: NUMBER11:681
Sum (digits (3520,10)) = 10
proof end;

theorem Th682: :: NUMBER11:682
digits (3540,10) = <%0,4,5,3%>
proof end;

theorem Th683: :: NUMBER11:683
Sum (digits (3540,10)) = 12
proof end;

theorem Th684: :: NUMBER11:684
digits (3560,10) = <%0,6,5,3%>
proof end;

theorem Th685: :: NUMBER11:685
Sum (digits (3560,10)) = 14
proof end;

theorem Th686: :: NUMBER11:686
digits (3580,10) = <%0,8,5,3%>
proof end;

theorem Th687: :: NUMBER11:687
Sum (digits (3580,10)) = 16
proof end;

theorem Th688: :: NUMBER11:688
digits (3600,10) = <%0,0,6,3%>
proof end;

theorem Th689: :: NUMBER11:689
Sum (digits (3600,10)) = 9
proof end;

theorem Th690: :: NUMBER11:690
digits (3620,10) = <%0,2,6,3%>
proof end;

theorem Th691: :: NUMBER11:691
Sum (digits (3620,10)) = 11
proof end;

theorem Th692: :: NUMBER11:692
digits (3640,10) = <%0,4,6,3%>
proof end;

theorem Th693: :: NUMBER11:693
Sum (digits (3640,10)) = 13
proof end;

theorem Th694: :: NUMBER11:694
digits (3660,10) = <%0,6,6,3%>
proof end;

theorem Th695: :: NUMBER11:695
Sum (digits (3660,10)) = 15
proof end;

theorem Th696: :: NUMBER11:696
digits (3680,10) = <%0,8,6,3%>
proof end;

theorem Th697: :: NUMBER11:697
Sum (digits (3680,10)) = 17
proof end;

theorem Th698: :: NUMBER11:698
digits (3700,10) = <%0,0,7,3%>
proof end;

theorem Th699: :: NUMBER11:699
Sum (digits (3700,10)) = 10
proof end;

theorem Th700: :: NUMBER11:700
digits (3720,10) = <%0,2,7,3%>
proof end;

theorem Th701: :: NUMBER11:701
Sum (digits (3720,10)) = 12
proof end;

theorem Th702: :: NUMBER11:702
digits (3740,10) = <%0,4,7,3%>
proof end;

theorem Th703: :: NUMBER11:703
Sum (digits (3740,10)) = 14
proof end;

theorem Th704: :: NUMBER11:704
digits (3760,10) = <%0,6,7,3%>
proof end;

theorem Th705: :: NUMBER11:705
Sum (digits (3760,10)) = 16
proof end;

theorem Th706: :: NUMBER11:706
digits (3780,10) = <%0,8,7,3%>
proof end;

theorem Th707: :: NUMBER11:707
Sum (digits (3780,10)) = 18
proof end;

theorem Th708: :: NUMBER11:708
digits (3800,10) = <%0,0,8,3%>
proof end;

theorem Th709: :: NUMBER11:709
Sum (digits (3800,10)) = 11
proof end;

theorem Th710: :: NUMBER11:710
digits (3820,10) = <%0,2,8,3%>
proof end;

theorem Th711: :: NUMBER11:711
Sum (digits (3820,10)) = 13
proof end;

theorem Th712: :: NUMBER11:712
digits (3840,10) = <%0,4,8,3%>
proof end;

theorem Th713: :: NUMBER11:713
Sum (digits (3840,10)) = 15
proof end;

theorem Th714: :: NUMBER11:714
digits (3860,10) = <%0,6,8,3%>
proof end;

theorem Th715: :: NUMBER11:715
Sum (digits (3860,10)) = 17
proof end;

theorem Th716: :: NUMBER11:716
digits (3880,10) = <%0,8,8,3%>
proof end;

theorem Th717: :: NUMBER11:717
Sum (digits (3880,10)) = 19
proof end;

theorem Th718: :: NUMBER11:718
digits (3900,10) = <%0,0,9,3%>
proof end;

theorem Th719: :: NUMBER11:719
Sum (digits (3900,10)) = 12
proof end;

theorem Th720: :: NUMBER11:720
digits (3920,10) = <%0,2,9,3%>
proof end;

theorem Th721: :: NUMBER11:721
Sum (digits (3920,10)) = 14
proof end;

theorem Th722: :: NUMBER11:722
digits (3940,10) = <%0,4,9,3%>
proof end;

theorem Th723: :: NUMBER11:723
Sum (digits (3940,10)) = 16
proof end;

theorem Th724: :: NUMBER11:724
digits (3960,10) = <%0,6,9,3%>
proof end;

theorem Th725: :: NUMBER11:725
Sum (digits (3960,10)) = 18
proof end;

theorem Th726: :: NUMBER11:726
digits (3980,10) = <%0,8,9,3%>
proof end;

theorem Th727: :: NUMBER11:727
Sum (digits (3980,10)) = 20
proof end;

theorem :: NUMBER11:728
Sierp36 3980,20
proof end;

theorem Th729: :: NUMBER11:729
digits (21,10) = <%1,2%>
proof end;

theorem Th730: :: NUMBER11:730
Sum (digits (21,10)) = 3
proof end;

theorem Th731: :: NUMBER11:731
digits (63,10) = <%3,6%>
proof end;

theorem Th732: :: NUMBER11:732
Sum (digits (63,10)) = 9
proof end;

theorem Th733: :: NUMBER11:733
digits (147,10) = <%7,4,1%>
proof end;

theorem Th734: :: NUMBER11:734
Sum (digits (147,10)) = 12
proof end;

theorem Th735: :: NUMBER11:735
digits (189,10) = <%9,8,1%>
proof end;

theorem Th736: :: NUMBER11:736
Sum (digits (189,10)) = 18
proof end;

theorem Th737: :: NUMBER11:737
digits (231,10) = <%1,3,2%>
proof end;

theorem Th738: :: NUMBER11:738
Sum (digits (231,10)) = 6
proof end;

theorem Th739: :: NUMBER11:739
digits (273,10) = <%3,7,2%>
proof end;

theorem Th740: :: NUMBER11:740
Sum (digits (273,10)) = 12
proof end;

theorem Th741: :: NUMBER11:741
digits (294,10) = <%4,9,2%>
proof end;

theorem Th742: :: NUMBER11:742
Sum (digits (294,10)) = 15
proof end;

theorem Th743: :: NUMBER11:743
digits (315,10) = <%5,1,3%>
proof end;

theorem Th744: :: NUMBER11:744
Sum (digits (315,10)) = 9
proof end;

theorem Th745: :: NUMBER11:745
digits (378,10) = <%8,7,3%>
proof end;

theorem Th746: :: NUMBER11:746
Sum (digits (378,10)) = 18
proof end;

theorem :: NUMBER11:747
Sierp36 399,21
proof end;

theorem Th748: :: NUMBER11:748
digits (242,10) = <%2,4,2%>
proof end;

theorem Th749: :: NUMBER11:749
Sum (digits (242,10)) = 8
proof end;

theorem Th750: :: NUMBER11:750
digits (264,10) = <%4,6,2%>
proof end;

theorem Th751: :: NUMBER11:751
Sum (digits (264,10)) = 12
proof end;

theorem Th752: :: NUMBER11:752
digits (286,10) = <%6,8,2%>
proof end;

theorem Th753: :: NUMBER11:753
Sum (digits (286,10)) = 16
proof end;

theorem Th754: :: NUMBER11:754
digits (308,10) = <%8,0,3%>
proof end;

theorem Th755: :: NUMBER11:755
Sum (digits (308,10)) = 11
proof end;

theorem Th756: :: NUMBER11:756
digits (330,10) = <%0,3,3%>
proof end;

theorem Th757: :: NUMBER11:757
Sum (digits (330,10)) = 6
proof end;

theorem Th758: :: NUMBER11:758
digits (396,10) = <%6,9,3%>
proof end;

theorem Th759: :: NUMBER11:759
Sum (digits (396,10)) = 18
proof end;

theorem Th760: :: NUMBER11:760
digits (462,10) = <%2,6,4%>
proof end;

theorem Th761: :: NUMBER11:761
Sum (digits (462,10)) = 12
proof end;

theorem Th762: :: NUMBER11:762
digits (484,10) = <%4,8,4%>
proof end;

theorem Th763: :: NUMBER11:763
Sum (digits (484,10)) = 16
proof end;

theorem Th764: :: NUMBER11:764
digits (506,10) = <%6,0,5%>
proof end;

theorem Th765: :: NUMBER11:765
Sum (digits (506,10)) = 11
proof end;

theorem Th766: :: NUMBER11:766
digits (528,10) = <%8,2,5%>
proof end;

theorem Th767: :: NUMBER11:767
Sum (digits (528,10)) = 15
proof end;

theorem Th768: :: NUMBER11:768
digits (550,10) = <%0,5,5%>
proof end;

theorem Th769: :: NUMBER11:769
Sum (digits (550,10)) = 10
proof end;

theorem Th770: :: NUMBER11:770
digits (572,10) = <%2,7,5%>
proof end;

theorem Th771: :: NUMBER11:771
Sum (digits (572,10)) = 14
proof end;

theorem Th772: :: NUMBER11:772
digits (594,10) = <%4,9,5%>
proof end;

theorem Th773: :: NUMBER11:773
Sum (digits (594,10)) = 18
proof end;

theorem Th774: :: NUMBER11:774
digits (616,10) = <%6,1,6%>
proof end;

theorem Th775: :: NUMBER11:775
Sum (digits (616,10)) = 13
proof end;

theorem Th776: :: NUMBER11:776
digits (638,10) = <%8,3,6%>
proof end;

theorem Th777: :: NUMBER11:777
Sum (digits (638,10)) = 17
proof end;

theorem Th778: :: NUMBER11:778
digits (682,10) = <%2,8,6%>
proof end;

theorem Th779: :: NUMBER11:779
Sum (digits (682,10)) = 16
proof end;

theorem Th780: :: NUMBER11:780
digits (704,10) = <%4,0,7%>
proof end;

theorem Th781: :: NUMBER11:781
Sum (digits (704,10)) = 11
proof end;

theorem Th782: :: NUMBER11:782
digits (726,10) = <%6,2,7%>
proof end;

theorem Th783: :: NUMBER11:783
Sum (digits (726,10)) = 15
proof end;

theorem Th784: :: NUMBER11:784
digits (748,10) = <%8,4,7%>
proof end;

theorem Th785: :: NUMBER11:785
Sum (digits (748,10)) = 19
proof end;

theorem Th786: :: NUMBER11:786
digits (770,10) = <%0,7,7%>
proof end;

theorem Th787: :: NUMBER11:787
Sum (digits (770,10)) = 14
proof end;

theorem Th788: :: NUMBER11:788
digits (792,10) = <%2,9,7%>
proof end;

theorem Th789: :: NUMBER11:789
Sum (digits (792,10)) = 18
proof end;

theorem Th790: :: NUMBER11:790
digits (814,10) = <%4,1,8%>
proof end;

theorem Th791: :: NUMBER11:791
Sum (digits (814,10)) = 13
proof end;

theorem Th792: :: NUMBER11:792
digits (858,10) = <%8,5,8%>
proof end;

theorem Th793: :: NUMBER11:793
Sum (digits (858,10)) = 21
proof end;

theorem Th794: :: NUMBER11:794
digits (902,10) = <%2,0,9%>
proof end;

theorem Th795: :: NUMBER11:795
Sum (digits (902,10)) = 11
proof end;

theorem Th796: :: NUMBER11:796
digits (924,10) = <%4,2,9%>
proof end;

theorem Th797: :: NUMBER11:797
Sum (digits (924,10)) = 15
proof end;

theorem Th798: :: NUMBER11:798
digits (946,10) = <%6,4,9%>
proof end;

theorem Th799: :: NUMBER11:799
Sum (digits (946,10)) = 19
proof end;

theorem Th800: :: NUMBER11:800
digits (968,10) = <%8,6,9%>
proof end;

theorem Th801: :: NUMBER11:801
Sum (digits (968,10)) = 23
proof end;

theorem Th802: :: NUMBER11:802
digits (990,10) = <%0,9,9%>
proof end;

theorem Th803: :: NUMBER11:803
Sum (digits (990,10)) = 18
proof end;

theorem Th804: :: NUMBER11:804
digits (1012,10) = <%2,1,0,1%>
proof end;

theorem Th805: :: NUMBER11:805
Sum (digits (1012,10)) = 4
proof end;

theorem Th806: :: NUMBER11:806
digits (1034,10) = <%4,3,0,1%>
proof end;

theorem Th807: :: NUMBER11:807
Sum (digits (1034,10)) = 8
proof end;

theorem Th808: :: NUMBER11:808
digits (1056,10) = <%6,5,0,1%>
proof end;

theorem Th809: :: NUMBER11:809
Sum (digits (1056,10)) = 12
proof end;

theorem Th810: :: NUMBER11:810
digits (1078,10) = <%8,7,0,1%>
proof end;

theorem Th811: :: NUMBER11:811
Sum (digits (1078,10)) = 16
proof end;

theorem Th812: :: NUMBER11:812
digits (1122,10) = <%2,2,1,1%>
proof end;

theorem Th813: :: NUMBER11:813
Sum (digits (1122,10)) = 6
proof end;

theorem Th814: :: NUMBER11:814
digits (1144,10) = <%4,4,1,1%>
proof end;

theorem Th815: :: NUMBER11:815
Sum (digits (1144,10)) = 10
proof end;

theorem Th816: :: NUMBER11:816
digits (1166,10) = <%6,6,1,1%>
proof end;

theorem Th817: :: NUMBER11:817
Sum (digits (1166,10)) = 14
proof end;

theorem Th818: :: NUMBER11:818
digits (1188,10) = <%8,8,1,1%>
proof end;

theorem Th819: :: NUMBER11:819
Sum (digits (1188,10)) = 18
proof end;

theorem Th820: :: NUMBER11:820
digits (1210,10) = <%0,1,2,1%>
proof end;

theorem Th821: :: NUMBER11:821
Sum (digits (1210,10)) = 4
proof end;

theorem Th822: :: NUMBER11:822
digits (1232,10) = <%2,3,2,1%>
proof end;

theorem Th823: :: NUMBER11:823
Sum (digits (1232,10)) = 8
proof end;

theorem Th824: :: NUMBER11:824
digits (1254,10) = <%4,5,2,1%>
proof end;

theorem Th825: :: NUMBER11:825
Sum (digits (1254,10)) = 12
proof end;

theorem Th826: :: NUMBER11:826
digits (1276,10) = <%6,7,2,1%>
proof end;

theorem Th827: :: NUMBER11:827
Sum (digits (1276,10)) = 16
proof end;

theorem Th828: :: NUMBER11:828
digits (1298,10) = <%8,9,2,1%>
proof end;

theorem Th829: :: NUMBER11:829
Sum (digits (1298,10)) = 20
proof end;

theorem Th830: :: NUMBER11:830
digits (1342,10) = <%2,4,3,1%>
proof end;

theorem Th831: :: NUMBER11:831
Sum (digits (1342,10)) = 10
proof end;

theorem Th832: :: NUMBER11:832
digits (1364,10) = <%4,6,3,1%>
proof end;

theorem Th833: :: NUMBER11:833
Sum (digits (1364,10)) = 14
proof end;

theorem Th834: :: NUMBER11:834
digits (1386,10) = <%6,8,3,1%>
proof end;

theorem Th835: :: NUMBER11:835
Sum (digits (1386,10)) = 18
proof end;

theorem Th836: :: NUMBER11:836
digits (1408,10) = <%8,0,4,1%>
proof end;

theorem Th837: :: NUMBER11:837
Sum (digits (1408,10)) = 13
proof end;

theorem Th838: :: NUMBER11:838
digits (1430,10) = <%0,3,4,1%>
proof end;

theorem Th839: :: NUMBER11:839
Sum (digits (1430,10)) = 8
proof end;

theorem Th840: :: NUMBER11:840
digits (1452,10) = <%2,5,4,1%>
proof end;

theorem Th841: :: NUMBER11:841
Sum (digits (1452,10)) = 12
proof end;

theorem Th842: :: NUMBER11:842
digits (1474,10) = <%4,7,4,1%>
proof end;

theorem Th843: :: NUMBER11:843
Sum (digits (1474,10)) = 16
proof end;

theorem Th844: :: NUMBER11:844
digits (1496,10) = <%6,9,4,1%>
proof end;

theorem Th845: :: NUMBER11:845
Sum (digits (1496,10)) = 20
proof end;

theorem Th846: :: NUMBER11:846
digits (1518,10) = <%8,1,5,1%>
proof end;

theorem Th847: :: NUMBER11:847
Sum (digits (1518,10)) = 15
proof end;

theorem Th848: :: NUMBER11:848
digits (1562,10) = <%2,6,5,1%>
proof end;

theorem Th849: :: NUMBER11:849
Sum (digits (1562,10)) = 14
proof end;

theorem Th850: :: NUMBER11:850
digits (1584,10) = <%4,8,5,1%>
proof end;

theorem Th851: :: NUMBER11:851
Sum (digits (1584,10)) = 18
proof end;

theorem Th852: :: NUMBER11:852
digits (1606,10) = <%6,0,6,1%>
proof end;

theorem Th853: :: NUMBER11:853
Sum (digits (1606,10)) = 13
proof end;

theorem Th854: :: NUMBER11:854
digits (1628,10) = <%8,2,6,1%>
proof end;

theorem Th855: :: NUMBER11:855
Sum (digits (1628,10)) = 17
proof end;

theorem Th856: :: NUMBER11:856
digits (1650,10) = <%0,5,6,1%>
proof end;

theorem Th857: :: NUMBER11:857
Sum (digits (1650,10)) = 12
proof end;

theorem Th858: :: NUMBER11:858
digits (1672,10) = <%2,7,6,1%>
proof end;

theorem Th859: :: NUMBER11:859
Sum (digits (1672,10)) = 16
proof end;

theorem Th860: :: NUMBER11:860
digits (1694,10) = <%4,9,6,1%>
proof end;

theorem Th861: :: NUMBER11:861
Sum (digits (1694,10)) = 20
proof end;

theorem Th862: :: NUMBER11:862
digits (1716,10) = <%6,1,7,1%>
proof end;

theorem Th863: :: NUMBER11:863
Sum (digits (1716,10)) = 15
proof end;

theorem Th864: :: NUMBER11:864
digits (1738,10) = <%8,3,7,1%>
proof end;

theorem Th865: :: NUMBER11:865
Sum (digits (1738,10)) = 19
proof end;

theorem Th866: :: NUMBER11:866
digits (1782,10) = <%2,8,7,1%>
proof end;

theorem Th867: :: NUMBER11:867
Sum (digits (1782,10)) = 18
proof end;

theorem Th868: :: NUMBER11:868
digits (1804,10) = <%4,0,8,1%>
proof end;

theorem Th869: :: NUMBER11:869
Sum (digits (1804,10)) = 13
proof end;

theorem Th870: :: NUMBER11:870
digits (1826,10) = <%6,2,8,1%>
proof end;

theorem Th871: :: NUMBER11:871
Sum (digits (1826,10)) = 17
proof end;

theorem Th872: :: NUMBER11:872
digits (1848,10) = <%8,4,8,1%>
proof end;

theorem Th873: :: NUMBER11:873
Sum (digits (1848,10)) = 21
proof end;

theorem Th874: :: NUMBER11:874
digits (1870,10) = <%0,7,8,1%>
proof end;

theorem Th875: :: NUMBER11:875
Sum (digits (1870,10)) = 16
proof end;

theorem Th876: :: NUMBER11:876
digits (1892,10) = <%2,9,8,1%>
proof end;

theorem Th877: :: NUMBER11:877
Sum (digits (1892,10)) = 20
proof end;

theorem Th878: :: NUMBER11:878
digits (1914,10) = <%4,1,9,1%>
proof end;

theorem Th879: :: NUMBER11:879
Sum (digits (1914,10)) = 15
proof end;

theorem Th880: :: NUMBER11:880
digits (1936,10) = <%6,3,9,1%>
proof end;

theorem Th881: :: NUMBER11:881
Sum (digits (1936,10)) = 19
proof end;

theorem Th882: :: NUMBER11:882
digits (1958,10) = <%8,5,9,1%>
proof end;

theorem Th883: :: NUMBER11:883
Sum (digits (1958,10)) = 23
proof end;

theorem Th884: :: NUMBER11:884
digits (2002,10) = <%2,0,0,2%>
proof end;

theorem Th885: :: NUMBER11:885
Sum (digits (2002,10)) = 4
proof end;

theorem Th886: :: NUMBER11:886
digits (2024,10) = <%4,2,0,2%>
proof end;

theorem Th887: :: NUMBER11:887
Sum (digits (2024,10)) = 8
proof end;

theorem Th888: :: NUMBER11:888
digits (2046,10) = <%6,4,0,2%>
proof end;

theorem Th889: :: NUMBER11:889
Sum (digits (2046,10)) = 12
proof end;

theorem Th890: :: NUMBER11:890
digits (2068,10) = <%8,6,0,2%>
proof end;

theorem Th891: :: NUMBER11:891
Sum (digits (2068,10)) = 16
proof end;

theorem Th892: :: NUMBER11:892
digits (2090,10) = <%0,9,0,2%>
proof end;

theorem Th893: :: NUMBER11:893
Sum (digits (2090,10)) = 11
proof end;

theorem Th894: :: NUMBER11:894
digits (2112,10) = <%2,1,1,2%>
proof end;

theorem Th895: :: NUMBER11:895
Sum (digits (2112,10)) = 6
proof end;

theorem Th896: :: NUMBER11:896
digits (2134,10) = <%4,3,1,2%>
proof end;

theorem Th897: :: NUMBER11:897
Sum (digits (2134,10)) = 10
proof end;

theorem Th898: :: NUMBER11:898
digits (2156,10) = <%6,5,1,2%>
proof end;

theorem Th899: :: NUMBER11:899
Sum (digits (2156,10)) = 14
proof end;

theorem Th900: :: NUMBER11:900
digits (2178,10) = <%8,7,1,2%>
proof end;

theorem Th901: :: NUMBER11:901
Sum (digits (2178,10)) = 18
proof end;

theorem Th902: :: NUMBER11:902
digits (2222,10) = <%2,2,2,2%>
proof end;

theorem Th903: :: NUMBER11:903
Sum (digits (2222,10)) = 8
proof end;

theorem Th904: :: NUMBER11:904
digits (2244,10) = <%4,4,2,2%>
proof end;

theorem Th905: :: NUMBER11:905
Sum (digits (2244,10)) = 12
proof end;

theorem Th906: :: NUMBER11:906
digits (2266,10) = <%6,6,2,2%>
proof end;

theorem Th907: :: NUMBER11:907
Sum (digits (2266,10)) = 16
proof end;

theorem Th908: :: NUMBER11:908
digits (2288,10) = <%8,8,2,2%>
proof end;

theorem Th909: :: NUMBER11:909
Sum (digits (2288,10)) = 20
proof end;

theorem Th910: :: NUMBER11:910
digits (2310,10) = <%0,1,3,2%>
proof end;

theorem Th911: :: NUMBER11:911
Sum (digits (2310,10)) = 6
proof end;

theorem Th912: :: NUMBER11:912
digits (2332,10) = <%2,3,3,2%>
proof end;

theorem Th913: :: NUMBER11:913
Sum (digits (2332,10)) = 10
proof end;

theorem Th914: :: NUMBER11:914
digits (2354,10) = <%4,5,3,2%>
proof end;

theorem Th915: :: NUMBER11:915
Sum (digits (2354,10)) = 14
proof end;

theorem Th916: :: NUMBER11:916
digits (2376,10) = <%6,7,3,2%>
proof end;

theorem Th917: :: NUMBER11:917
Sum (digits (2376,10)) = 18
proof end;

theorem Th918: :: NUMBER11:918
digits (2398,10) = <%8,9,3,2%>
proof end;

theorem Th919: :: NUMBER11:919
Sum (digits (2398,10)) = 22
proof end;

theorem :: NUMBER11:920
Sierp36 2398,22
proof end;

theorem Th921: :: NUMBER11:921
digits (23,10) = <%3,2%>
proof end;

theorem Th922: :: NUMBER11:922
Sum (digits (23,10)) = 5
proof end;

theorem Th923: :: NUMBER11:923
digits (46,10) = <%6,4%>
proof end;

theorem Th924: :: NUMBER11:924
Sum (digits (46,10)) = 10
proof end;

theorem Th925: :: NUMBER11:925
digits (69,10) = <%9,6%>
proof end;

theorem Th926: :: NUMBER11:926
Sum (digits (69,10)) = 15
proof end;

theorem Th927: :: NUMBER11:927
digits (92,10) = <%2,9%>
proof end;

theorem Th928: :: NUMBER11:928
Sum (digits (92,10)) = 11
proof end;

theorem Th929: :: NUMBER11:929
digits (115,10) = <%5,1,1%>
proof end;

theorem Th930: :: NUMBER11:930
Sum (digits (115,10)) = 7
proof end;

theorem Th931: :: NUMBER11:931
digits (138,10) = <%8,3,1%>
proof end;

theorem Th932: :: NUMBER11:932
Sum (digits (138,10)) = 12
proof end;

theorem Th933: :: NUMBER11:933
digits (161,10) = <%1,6,1%>
proof end;

theorem Th934: :: NUMBER11:934
Sum (digits (161,10)) = 8
proof end;

theorem Th935: :: NUMBER11:935
digits (184,10) = <%4,8,1%>
proof end;

theorem Th936: :: NUMBER11:936
Sum (digits (184,10)) = 13
proof end;

theorem Th937: :: NUMBER11:937
digits (207,10) = <%7,0,2%>
proof end;

theorem Th938: :: NUMBER11:938
Sum (digits (207,10)) = 9
proof end;

theorem Th939: :: NUMBER11:939
digits (230,10) = <%0,3,2%>
proof end;

theorem Th940: :: NUMBER11:940
Sum (digits (230,10)) = 5
proof end;

theorem Th941: :: NUMBER11:941
digits (253,10) = <%3,5,2%>
proof end;

theorem Th942: :: NUMBER11:942
Sum (digits (253,10)) = 10
proof end;

theorem Th943: :: NUMBER11:943
digits (276,10) = <%6,7,2%>
proof end;

theorem Th944: :: NUMBER11:944
Sum (digits (276,10)) = 15
proof end;

theorem Th945: :: NUMBER11:945
digits (299,10) = <%9,9,2%>
proof end;

theorem Th946: :: NUMBER11:946
Sum (digits (299,10)) = 20
proof end;

theorem Th947: :: NUMBER11:947
digits (322,10) = <%2,2,3%>
proof end;

theorem Th948: :: NUMBER11:948
Sum (digits (322,10)) = 7
proof end;

theorem Th949: :: NUMBER11:949
digits (345,10) = <%5,4,3%>
proof end;

theorem Th950: :: NUMBER11:950
Sum (digits (345,10)) = 12
proof end;

theorem Th951: :: NUMBER11:951
digits (414,10) = <%4,1,4%>
proof end;

theorem Th952: :: NUMBER11:952
Sum (digits (414,10)) = 9
proof end;

theorem Th953: :: NUMBER11:953
digits (483,10) = <%3,8,4%>
proof end;

theorem Th954: :: NUMBER11:954
Sum (digits (483,10)) = 15
proof end;

theorem Th955: :: NUMBER11:955
digits (529,10) = <%9,2,5%>
proof end;

theorem Th956: :: NUMBER11:956
Sum (digits (529,10)) = 16
proof end;

theorem Th957: :: NUMBER11:957
digits (552,10) = <%2,5,5%>
proof end;

theorem Th958: :: NUMBER11:958
Sum (digits (552,10)) = 12
proof end;

theorem Th959: :: NUMBER11:959
digits (575,10) = <%5,7,5%>
proof end;

theorem Th960: :: NUMBER11:960
Sum (digits (575,10)) = 17
proof end;

theorem Th961: :: NUMBER11:961
digits (598,10) = <%8,9,5%>
proof end;

theorem Th962: :: NUMBER11:962
Sum (digits (598,10)) = 22
proof end;

theorem Th963: :: NUMBER11:963
digits (621,10) = <%1,2,6%>
proof end;

theorem Th964: :: NUMBER11:964
Sum (digits (621,10)) = 9
proof end;

theorem Th965: :: NUMBER11:965
digits (644,10) = <%4,4,6%>
proof end;

theorem Th966: :: NUMBER11:966
Sum (digits (644,10)) = 14
proof end;

theorem Th967: :: NUMBER11:967
digits (667,10) = <%7,6,6%>
proof end;

theorem Th968: :: NUMBER11:968
Sum (digits (667,10)) = 19
proof end;

theorem Th969: :: NUMBER11:969
digits (690,10) = <%0,9,6%>
proof end;

theorem Th970: :: NUMBER11:970
Sum (digits (690,10)) = 15
proof end;

theorem Th971: :: NUMBER11:971
digits (713,10) = <%3,1,7%>
proof end;

theorem Th972: :: NUMBER11:972
Sum (digits (713,10)) = 11
proof end;

theorem Th973: :: NUMBER11:973
digits (736,10) = <%6,3,7%>
proof end;

theorem Th974: :: NUMBER11:974
Sum (digits (736,10)) = 16
proof end;

theorem Th975: :: NUMBER11:975
digits (759,10) = <%9,5,7%>
proof end;

theorem Th976: :: NUMBER11:976
Sum (digits (759,10)) = 21
proof end;

theorem Th977: :: NUMBER11:977
digits (782,10) = <%2,8,7%>
proof end;

theorem Th978: :: NUMBER11:978
Sum (digits (782,10)) = 17
proof end;

theorem Th979: :: NUMBER11:979
digits (805,10) = <%5,0,8%>
proof end;

theorem Th980: :: NUMBER11:980
Sum (digits (805,10)) = 13
proof end;

theorem Th981: :: NUMBER11:981
digits (828,10) = <%8,2,8%>
proof end;

theorem Th982: :: NUMBER11:982
Sum (digits (828,10)) = 18
proof end;

theorem Th983: :: NUMBER11:983
digits (851,10) = <%1,5,8%>
proof end;

theorem Th984: :: NUMBER11:984
Sum (digits (851,10)) = 14
proof end;

theorem Th985: :: NUMBER11:985
digits (897,10) = <%7,9,8%>
proof end;

theorem Th986: :: NUMBER11:986
Sum (digits (897,10)) = 24
proof end;

theorem Th987: :: NUMBER11:987
digits (943,10) = <%3,4,9%>
proof end;

theorem Th988: :: NUMBER11:988
Sum (digits (943,10)) = 16
proof end;

theorem Th989: :: NUMBER11:989
digits (966,10) = <%6,6,9%>
proof end;

theorem Th990: :: NUMBER11:990
Sum (digits (966,10)) = 21
proof end;

theorem Th991: :: NUMBER11:991
digits (989,10) = <%9,8,9%>
proof end;

theorem Th992: :: NUMBER11:992
Sum (digits (989,10)) = 26
proof end;

theorem Th993: :: NUMBER11:993
digits (1035,10) = <%5,3,0,1%>
proof end;

theorem Th994: :: NUMBER11:994
Sum (digits (1035,10)) = 9
proof end;

theorem Th995: :: NUMBER11:995
digits (1058,10) = <%8,5,0,1%>
proof end;

theorem Th996: :: NUMBER11:996
Sum (digits (1058,10)) = 14
proof end;

theorem Th997: :: NUMBER11:997
digits (1081,10) = <%1,8,0,1%>
proof end;

theorem Th998: :: NUMBER11:998
Sum (digits (1081,10)) = 10
proof end;

theorem Th999: :: NUMBER11:999
digits (1104,10) = <%4,0,1,1%>
proof end;

theorem Th1000: :: NUMBER11:1000
Sum (digits (1104,10)) = 6
proof end;

theorem Th1001: :: NUMBER11:1001
digits (1127,10) = <%7,2,1,1%>
proof end;

theorem Th1002: :: NUMBER11:1002
Sum (digits (1127,10)) = 11
proof end;

theorem Th1003: :: NUMBER11:1003
digits (1150,10) = <%0,5,1,1%>
proof end;

theorem Th1004: :: NUMBER11:1004
Sum (digits (1150,10)) = 7
proof end;

theorem Th1005: :: NUMBER11:1005
digits (1173,10) = <%3,7,1,1%>
proof end;

theorem Th1006: :: NUMBER11:1006
Sum (digits (1173,10)) = 12
proof end;

theorem Th1007: :: NUMBER11:1007
digits (1196,10) = <%6,9,1,1%>
proof end;

theorem Th1008: :: NUMBER11:1008
Sum (digits (1196,10)) = 17
proof end;

theorem Th1009: :: NUMBER11:1009
digits (1219,10) = <%9,1,2,1%>
proof end;

theorem Th1010: :: NUMBER11:1010
Sum (digits (1219,10)) = 13
proof end;

theorem Th1011: :: NUMBER11:1011
digits (1242,10) = <%2,4,2,1%>
proof end;

theorem Th1012: :: NUMBER11:1012
Sum (digits (1242,10)) = 9
proof end;

theorem Th1013: :: NUMBER11:1013
digits (1265,10) = <%5,6,2,1%>
proof end;

theorem Th1014: :: NUMBER11:1014
Sum (digits (1265,10)) = 14
proof end;

theorem Th1015: :: NUMBER11:1015
digits (1288,10) = <%8,8,2,1%>
proof end;

theorem Th1016: :: NUMBER11:1016
Sum (digits (1288,10)) = 19
proof end;

theorem Th1017: :: NUMBER11:1017
digits (1311,10) = <%1,1,3,1%>
proof end;

theorem Th1018: :: NUMBER11:1018
Sum (digits (1311,10)) = 6
proof end;

theorem Th1019: :: NUMBER11:1019
digits (1334,10) = <%4,3,3,1%>
proof end;

theorem Th1020: :: NUMBER11:1020
Sum (digits (1334,10)) = 11
proof end;

theorem Th1021: :: NUMBER11:1021
digits (1357,10) = <%7,5,3,1%>
proof end;

theorem Th1022: :: NUMBER11:1022
Sum (digits (1357,10)) = 16
proof end;

theorem Th1023: :: NUMBER11:1023
digits (1403,10) = <%3,0,4,1%>
proof end;

theorem Th1024: :: NUMBER11:1024
Sum (digits (1403,10)) = 8
proof end;

theorem Th1025: :: NUMBER11:1025
digits (1426,10) = <%6,2,4,1%>
proof end;

theorem Th1026: :: NUMBER11:1026
Sum (digits (1426,10)) = 13
proof end;

theorem Th1027: :: NUMBER11:1027
digits (1449,10) = <%9,4,4,1%>
proof end;

theorem Th1028: :: NUMBER11:1028
Sum (digits (1449,10)) = 18
proof end;

theorem Th1029: :: NUMBER11:1029
digits (1472,10) = <%2,7,4,1%>
proof end;

theorem Th1030: :: NUMBER11:1030
Sum (digits (1472,10)) = 14
proof end;

theorem Th1031: :: NUMBER11:1031
digits (1495,10) = <%5,9,4,1%>
proof end;

theorem Th1032: :: NUMBER11:1032
Sum (digits (1495,10)) = 19
proof end;

theorem Th1033: :: NUMBER11:1033
digits (1541,10) = <%1,4,5,1%>
proof end;

theorem Th1034: :: NUMBER11:1034
Sum (digits (1541,10)) = 11
proof end;

theorem Th1035: :: NUMBER11:1035
digits (1564,10) = <%4,6,5,1%>
proof end;

theorem Th1036: :: NUMBER11:1036
Sum (digits (1564,10)) = 16
proof end;

theorem Th1037: :: NUMBER11:1037
digits (1587,10) = <%7,8,5,1%>
proof end;

theorem Th1038: :: NUMBER11:1038
Sum (digits (1587,10)) = 21
proof end;

theorem Th1039: :: NUMBER11:1039
digits (1610,10) = <%0,1,6,1%>
proof end;

theorem Th1040: :: NUMBER11:1040
Sum (digits (1610,10)) = 8
proof end;

theorem Th1041: :: NUMBER11:1041
digits (1633,10) = <%3,3,6,1%>
proof end;

theorem Th1042: :: NUMBER11:1042
Sum (digits (1633,10)) = 13
proof end;

theorem Th1043: :: NUMBER11:1043
digits (1656,10) = <%6,5,6,1%>
proof end;

theorem Th1044: :: NUMBER11:1044
Sum (digits (1656,10)) = 18
proof end;

theorem Th1045: :: NUMBER11:1045
digits (1679,10) = <%9,7,6,1%>
proof end;

theorem Th1046: :: NUMBER11:1046
Sum (digits (1679,10)) = 23
proof end;

theorem :: NUMBER11:1047
Sierp36 1679,23
proof end;

theorem Th1048: :: NUMBER11:1048
digits (216,10) = <%6,1,2%>
proof end;

theorem Th1049: :: NUMBER11:1049
Sum (digits (216,10)) = 9
proof end;

theorem Th1050: :: NUMBER11:1050
digits (312,10) = <%2,1,3%>
proof end;

theorem Th1051: :: NUMBER11:1051
Sum (digits (312,10)) = 6
proof end;

theorem Th1052: :: NUMBER11:1052
digits (504,10) = <%4,0,5%>
proof end;

theorem Th1053: :: NUMBER11:1053
Sum (digits (504,10)) = 9
proof end;

theorem Th1054: :: NUMBER11:1054
digits (576,10) = <%6,7,5%>
proof end;

theorem Th1055: :: NUMBER11:1055
Sum (digits (576,10)) = 18
proof end;

theorem Th1056: :: NUMBER11:1056
digits (624,10) = <%4,2,6%>
proof end;

theorem Th1057: :: NUMBER11:1057
Sum (digits (624,10)) = 12
proof end;

theorem Th1058: :: NUMBER11:1058
digits (648,10) = <%8,4,6%>
proof end;

theorem Th1059: :: NUMBER11:1059
Sum (digits (648,10)) = 18
proof end;

theorem Th1060: :: NUMBER11:1060
digits (672,10) = <%2,7,6%>
proof end;

theorem Th1061: :: NUMBER11:1061
Sum (digits (672,10)) = 15
proof end;

theorem Th1062: :: NUMBER11:1062
digits (696,10) = <%6,9,6%>
proof end;

theorem Th1063: :: NUMBER11:1063
Sum (digits (696,10)) = 21
proof end;

theorem Th1064: :: NUMBER11:1064
digits (744,10) = <%4,4,7%>
proof end;

theorem Th1065: :: NUMBER11:1065
Sum (digits (744,10)) = 15
proof end;

theorem Th1066: :: NUMBER11:1066
digits (768,10) = <%8,6,7%>
proof end;

theorem Th1067: :: NUMBER11:1067
Sum (digits (768,10)) = 21
proof end;

theorem Th1068: :: NUMBER11:1068
digits (816,10) = <%6,1,8%>
proof end;

theorem Th1069: :: NUMBER11:1069
Sum (digits (816,10)) = 15
proof end;

theorem Th1070: :: NUMBER11:1070
digits (864,10) = <%4,6,8%>
proof end;

theorem Th1071: :: NUMBER11:1071
Sum (digits (864,10)) = 18
proof end;

theorem Th1072: :: NUMBER11:1072
digits (888,10) = <%8,8,8%>
proof end;

theorem Th1073: :: NUMBER11:1073
Sum (digits (888,10)) = 24
proof end;

theorem :: NUMBER11:1074
Sierp36 888,24
proof end;

theorem Th1075: :: NUMBER11:1075
digits (25,10) = <%5,2%>
proof end;

theorem Th1076: :: NUMBER11:1076
Sum (digits (25,10)) = 7
proof end;

theorem Th1077: :: NUMBER11:1077
digits (125,10) = <%5,2,1%>
proof end;

theorem Th1078: :: NUMBER11:1078
Sum (digits (125,10)) = 8
proof end;

theorem Th1079: :: NUMBER11:1079
digits (175,10) = <%5,7,1%>
proof end;

theorem Th1080: :: NUMBER11:1080
Sum (digits (175,10)) = 13
proof end;

theorem Th1081: :: NUMBER11:1081
digits (225,10) = <%5,2,2%>
proof end;

theorem Th1082: :: NUMBER11:1082
Sum (digits (225,10)) = 9
proof end;

theorem Th1083: :: NUMBER11:1083
digits (250,10) = <%0,5,2%>
proof end;

theorem Th1084: :: NUMBER11:1084
Sum (digits (250,10)) = 7
proof end;

theorem Th1085: :: NUMBER11:1085
digits (275,10) = <%5,7,2%>
proof end;

theorem Th1086: :: NUMBER11:1086
Sum (digits (275,10)) = 14
proof end;

theorem Th1087: :: NUMBER11:1087
digits (325,10) = <%5,2,3%>
proof end;

theorem Th1088: :: NUMBER11:1088
Sum (digits (325,10)) = 10
proof end;

theorem Th1089: :: NUMBER11:1089
digits (350,10) = <%0,5,3%>
proof end;

theorem Th1090: :: NUMBER11:1090
Sum (digits (350,10)) = 8
proof end;

theorem Th1091: :: NUMBER11:1091
digits (375,10) = <%5,7,3%>
proof end;

theorem Th1092: :: NUMBER11:1092
Sum (digits (375,10)) = 15
proof end;

theorem Th1093: :: NUMBER11:1093
digits (450,10) = <%0,5,4%>
proof end;

theorem Th1094: :: NUMBER11:1094
Sum (digits (450,10)) = 9
proof end;

theorem Th1095: :: NUMBER11:1095
digits (525,10) = <%5,2,5%>
proof end;

theorem Th1096: :: NUMBER11:1096
Sum (digits (525,10)) = 12
proof end;

theorem Th1097: :: NUMBER11:1097
digits (625,10) = <%5,2,6%>
proof end;

theorem Th1098: :: NUMBER11:1098
Sum (digits (625,10)) = 13
proof end;

theorem Th1099: :: NUMBER11:1099
digits (650,10) = <%0,5,6%>
proof end;

theorem Th1100: :: NUMBER11:1100
Sum (digits (650,10)) = 11
proof end;

theorem Th1101: :: NUMBER11:1101
digits (675,10) = <%5,7,6%>
proof end;

theorem Th1102: :: NUMBER11:1102
Sum (digits (675,10)) = 18
proof end;

theorem Th1103: :: NUMBER11:1103
digits (725,10) = <%5,2,7%>
proof end;

theorem Th1104: :: NUMBER11:1104
Sum (digits (725,10)) = 14
proof end;

theorem Th1105: :: NUMBER11:1105
digits (750,10) = <%0,5,7%>
proof end;

theorem Th1106: :: NUMBER11:1106
Sum (digits (750,10)) = 12
proof end;

theorem Th1107: :: NUMBER11:1107
digits (775,10) = <%5,7,7%>
proof end;

theorem Th1108: :: NUMBER11:1108
Sum (digits (775,10)) = 19
proof end;

theorem Th1109: :: NUMBER11:1109
digits (825,10) = <%5,2,8%>
proof end;

theorem Th1110: :: NUMBER11:1110
Sum (digits (825,10)) = 15
proof end;

theorem Th1111: :: NUMBER11:1111
digits (850,10) = <%0,5,8%>
proof end;

theorem Th1112: :: NUMBER11:1112
Sum (digits (850,10)) = 13
proof end;

theorem Th1113: :: NUMBER11:1113
digits (875,10) = <%5,7,8%>
proof end;

theorem Th1114: :: NUMBER11:1114
Sum (digits (875,10)) = 20
proof end;

theorem Th1115: :: NUMBER11:1115
digits (925,10) = <%5,2,9%>
proof end;

theorem Th1116: :: NUMBER11:1116
Sum (digits (925,10)) = 16
proof end;

theorem Th1117: :: NUMBER11:1117
digits (950,10) = <%0,5,9%>
proof end;

theorem Th1118: :: NUMBER11:1118
Sum (digits (950,10)) = 14
proof end;

theorem Th1119: :: NUMBER11:1119
digits (975,10) = <%5,7,9%>
proof end;

theorem Th1120: :: NUMBER11:1120
Sum (digits (975,10)) = 21
proof end;

theorem Th1121: :: NUMBER11:1121
digits (1025,10) = <%5,2,0,1%>
proof end;

theorem Th1122: :: NUMBER11:1122
Sum (digits (1025,10)) = 8
proof end;

theorem Th1123: :: NUMBER11:1123
digits (1050,10) = <%0,5,0,1%>
proof end;

theorem Th1124: :: NUMBER11:1124
Sum (digits (1050,10)) = 6
proof end;

theorem Th1125: :: NUMBER11:1125
digits (1075,10) = <%5,7,0,1%>
proof end;

theorem Th1126: :: NUMBER11:1126
Sum (digits (1075,10)) = 13
proof end;

theorem Th1127: :: NUMBER11:1127
digits (1125,10) = <%5,2,1,1%>
proof end;

theorem Th1128: :: NUMBER11:1128
Sum (digits (1125,10)) = 9
proof end;

theorem Th1129: :: NUMBER11:1129
digits (1175,10) = <%5,7,1,1%>
proof end;

theorem Th1130: :: NUMBER11:1130
Sum (digits (1175,10)) = 14
proof end;

theorem Th1131: :: NUMBER11:1131
digits (1225,10) = <%5,2,2,1%>
proof end;

theorem Th1132: :: NUMBER11:1132
Sum (digits (1225,10)) = 10
proof end;

theorem Th1133: :: NUMBER11:1133
digits (1250,10) = <%0,5,2,1%>
proof end;

theorem Th1134: :: NUMBER11:1134
Sum (digits (1250,10)) = 8
proof end;

theorem Th1135: :: NUMBER11:1135
digits (1275,10) = <%5,7,2,1%>
proof end;

theorem Th1136: :: NUMBER11:1136
Sum (digits (1275,10)) = 15
proof end;

theorem Th1137: :: NUMBER11:1137
digits (1325,10) = <%5,2,3,1%>
proof end;

theorem Th1138: :: NUMBER11:1138
Sum (digits (1325,10)) = 11
proof end;

theorem Th1139: :: NUMBER11:1139
digits (1350,10) = <%0,5,3,1%>
proof end;

theorem Th1140: :: NUMBER11:1140
Sum (digits (1350,10)) = 9
proof end;

theorem Th1141: :: NUMBER11:1141
digits (1375,10) = <%5,7,3,1%>
proof end;

theorem Th1142: :: NUMBER11:1142
Sum (digits (1375,10)) = 16
proof end;

theorem Th1143: :: NUMBER11:1143
digits (1425,10) = <%5,2,4,1%>
proof end;

theorem Th1144: :: NUMBER11:1144
Sum (digits (1425,10)) = 12
proof end;

theorem Th1145: :: NUMBER11:1145
digits (1450,10) = <%0,5,4,1%>
proof end;

theorem Th1146: :: NUMBER11:1146
Sum (digits (1450,10)) = 10
proof end;

theorem Th1147: :: NUMBER11:1147
digits (1475,10) = <%5,7,4,1%>
proof end;

theorem Th1148: :: NUMBER11:1148
Sum (digits (1475,10)) = 17
proof end;

theorem Th1149: :: NUMBER11:1149
digits (1525,10) = <%5,2,5,1%>
proof end;

theorem Th1150: :: NUMBER11:1150
Sum (digits (1525,10)) = 13
proof end;

theorem Th1151: :: NUMBER11:1151
digits (1550,10) = <%0,5,5,1%>
proof end;

theorem Th1152: :: NUMBER11:1152
Sum (digits (1550,10)) = 11
proof end;

theorem Th1153: :: NUMBER11:1153
digits (1575,10) = <%5,7,5,1%>
proof end;

theorem Th1154: :: NUMBER11:1154
Sum (digits (1575,10)) = 18
proof end;

theorem Th1155: :: NUMBER11:1155
digits (1625,10) = <%5,2,6,1%>
proof end;

theorem Th1156: :: NUMBER11:1156
Sum (digits (1625,10)) = 14
proof end;

theorem Th1157: :: NUMBER11:1157
digits (1675,10) = <%5,7,6,1%>
proof end;

theorem Th1158: :: NUMBER11:1158
Sum (digits (1675,10)) = 19
proof end;

theorem Th1159: :: NUMBER11:1159
digits (1725,10) = <%5,2,7,1%>
proof end;

theorem Th1160: :: NUMBER11:1160
Sum (digits (1725,10)) = 15
proof end;

theorem Th1161: :: NUMBER11:1161
digits (1750,10) = <%0,5,7,1%>
proof end;

theorem Th1162: :: NUMBER11:1162
Sum (digits (1750,10)) = 13
proof end;

theorem Th1163: :: NUMBER11:1163
digits (1775,10) = <%5,7,7,1%>
proof end;

theorem Th1164: :: NUMBER11:1164
Sum (digits (1775,10)) = 20
proof end;

theorem Th1165: :: NUMBER11:1165
digits (1825,10) = <%5,2,8,1%>
proof end;

theorem Th1166: :: NUMBER11:1166
Sum (digits (1825,10)) = 16
proof end;

theorem Th1167: :: NUMBER11:1167
digits (1850,10) = <%0,5,8,1%>
proof end;

theorem Th1168: :: NUMBER11:1168
Sum (digits (1850,10)) = 14
proof end;

theorem Th1169: :: NUMBER11:1169
digits (1875,10) = <%5,7,8,1%>
proof end;

theorem Th1170: :: NUMBER11:1170
Sum (digits (1875,10)) = 21
proof end;

theorem Th1171: :: NUMBER11:1171
digits (1925,10) = <%5,2,9,1%>
proof end;

theorem Th1172: :: NUMBER11:1172
Sum (digits (1925,10)) = 17
proof end;

theorem Th1173: :: NUMBER11:1173
digits (1950,10) = <%0,5,9,1%>
proof end;

theorem Th1174: :: NUMBER11:1174
Sum (digits (1950,10)) = 15
proof end;

theorem Th1175: :: NUMBER11:1175
digits (1975,10) = <%5,7,9,1%>
proof end;

theorem Th1176: :: NUMBER11:1176
Sum (digits (1975,10)) = 22
proof end;

theorem Th1177: :: NUMBER11:1177
digits (2025,10) = <%5,2,0,2%>
proof end;

theorem Th1178: :: NUMBER11:1178
Sum (digits (2025,10)) = 9
proof end;

theorem Th1179: :: NUMBER11:1179
digits (2050,10) = <%0,5,0,2%>
proof end;

theorem Th1180: :: NUMBER11:1180
Sum (digits (2050,10)) = 7
proof end;

theorem Th1181: :: NUMBER11:1181
digits (2075,10) = <%5,7,0,2%>
proof end;

theorem Th1182: :: NUMBER11:1182
Sum (digits (2075,10)) = 14
proof end;

theorem Th1183: :: NUMBER11:1183
digits (2125,10) = <%5,2,1,2%>
proof end;

theorem Th1184: :: NUMBER11:1184
Sum (digits (2125,10)) = 10
proof end;

theorem Th1185: :: NUMBER11:1185
digits (2150,10) = <%0,5,1,2%>
proof end;

theorem Th1186: :: NUMBER11:1186
Sum (digits (2150,10)) = 8
proof end;

theorem Th1187: :: NUMBER11:1187
digits (2175,10) = <%5,7,1,2%>
proof end;

theorem Th1188: :: NUMBER11:1188
Sum (digits (2175,10)) = 15
proof end;

theorem Th1189: :: NUMBER11:1189
digits (2225,10) = <%5,2,2,2%>
proof end;

theorem Th1190: :: NUMBER11:1190
Sum (digits (2225,10)) = 11
proof end;

theorem Th1191: :: NUMBER11:1191
digits (2250,10) = <%0,5,2,2%>
proof end;

theorem Th1192: :: NUMBER11:1192
Sum (digits (2250,10)) = 9
proof end;

theorem Th1193: :: NUMBER11:1193
digits (2275,10) = <%5,7,2,2%>
proof end;

theorem Th1194: :: NUMBER11:1194
Sum (digits (2275,10)) = 16
proof end;

theorem Th1195: :: NUMBER11:1195
digits (2325,10) = <%5,2,3,2%>
proof end;

theorem Th1196: :: NUMBER11:1196
Sum (digits (2325,10)) = 12
proof end;

theorem Th1197: :: NUMBER11:1197
digits (2350,10) = <%0,5,3,2%>
proof end;

theorem Th1198: :: NUMBER11:1198
Sum (digits (2350,10)) = 10
proof end;

theorem Th1199: :: NUMBER11:1199
digits (2375,10) = <%5,7,3,2%>
proof end;

theorem Th1200: :: NUMBER11:1200
Sum (digits (2375,10)) = 17
proof end;

theorem Th1201: :: NUMBER11:1201
digits (2425,10) = <%5,2,4,2%>
proof end;

theorem Th1202: :: NUMBER11:1202
Sum (digits (2425,10)) = 13
proof end;

theorem Th1203: :: NUMBER11:1203
digits (2450,10) = <%0,5,4,2%>
proof end;

theorem Th1204: :: NUMBER11:1204
Sum (digits (2450,10)) = 11
proof end;

theorem Th1205: :: NUMBER11:1205
digits (2475,10) = <%5,7,4,2%>
proof end;

theorem Th1206: :: NUMBER11:1206
Sum (digits (2475,10)) = 18
proof end;

theorem Th1207: :: NUMBER11:1207
digits (2525,10) = <%5,2,5,2%>
proof end;

theorem Th1208: :: NUMBER11:1208
Sum (digits (2525,10)) = 14
proof end;

theorem Th1209: :: NUMBER11:1209
digits (2550,10) = <%0,5,5,2%>
proof end;

theorem Th1210: :: NUMBER11:1210
Sum (digits (2550,10)) = 12
proof end;

theorem Th1211: :: NUMBER11:1211
digits (2575,10) = <%5,7,5,2%>
proof end;

theorem Th1212: :: NUMBER11:1212
Sum (digits (2575,10)) = 19
proof end;

theorem Th1213: :: NUMBER11:1213
digits (2625,10) = <%5,2,6,2%>
proof end;

theorem Th1214: :: NUMBER11:1214
Sum (digits (2625,10)) = 15
proof end;

theorem Th1215: :: NUMBER11:1215
digits (2650,10) = <%0,5,6,2%>
proof end;

theorem Th1216: :: NUMBER11:1216
Sum (digits (2650,10)) = 13
proof end;

theorem Th1217: :: NUMBER11:1217
digits (2675,10) = <%5,7,6,2%>
proof end;

theorem Th1218: :: NUMBER11:1218
Sum (digits (2675,10)) = 20
proof end;

theorem Th1219: :: NUMBER11:1219
digits (2725,10) = <%5,2,7,2%>
proof end;

theorem Th1220: :: NUMBER11:1220
Sum (digits (2725,10)) = 16
proof end;

theorem Th1221: :: NUMBER11:1221
digits (2750,10) = <%0,5,7,2%>
proof end;

theorem Th1222: :: NUMBER11:1222
Sum (digits (2750,10)) = 14
proof end;

theorem Th1223: :: NUMBER11:1223
digits (2775,10) = <%5,7,7,2%>
proof end;

theorem Th1224: :: NUMBER11:1224
Sum (digits (2775,10)) = 21
proof end;

theorem Th1225: :: NUMBER11:1225
digits (2825,10) = <%5,2,8,2%>
proof end;

theorem Th1226: :: NUMBER11:1226
Sum (digits (2825,10)) = 17
proof end;

theorem Th1227: :: NUMBER11:1227
digits (2850,10) = <%0,5,8,2%>
proof end;

theorem Th1228: :: NUMBER11:1228
Sum (digits (2850,10)) = 15
proof end;

theorem Th1229: :: NUMBER11:1229
digits (2875,10) = <%5,7,8,2%>
proof end;

theorem Th1230: :: NUMBER11:1230
Sum (digits (2875,10)) = 22
proof end;

theorem Th1231: :: NUMBER11:1231
digits (2925,10) = <%5,2,9,2%>
proof end;

theorem Th1232: :: NUMBER11:1232
Sum (digits (2925,10)) = 18
proof end;

theorem Th1233: :: NUMBER11:1233
digits (2950,10) = <%0,5,9,2%>
proof end;

theorem Th1234: :: NUMBER11:1234
Sum (digits (2950,10)) = 16
proof end;

theorem Th1235: :: NUMBER11:1235
digits (2975,10) = <%5,7,9,2%>
proof end;

theorem Th1236: :: NUMBER11:1236
Sum (digits (2975,10)) = 23
proof end;

theorem Th1237: :: NUMBER11:1237
digits (3025,10) = <%5,2,0,3%>
proof end;

theorem Th1238: :: NUMBER11:1238
Sum (digits (3025,10)) = 10
proof end;

theorem Th1239: :: NUMBER11:1239
digits (3050,10) = <%0,5,0,3%>
proof end;

theorem Th1240: :: NUMBER11:1240
Sum (digits (3050,10)) = 8
proof end;

theorem Th1241: :: NUMBER11:1241
digits (3075,10) = <%5,7,0,3%>
proof end;

theorem Th1242: :: NUMBER11:1242
Sum (digits (3075,10)) = 15
proof end;

theorem Th1243: :: NUMBER11:1243
digits (3125,10) = <%5,2,1,3%>
proof end;

theorem Th1244: :: NUMBER11:1244
Sum (digits (3125,10)) = 11
proof end;

theorem Th1245: :: NUMBER11:1245
digits (3150,10) = <%0,5,1,3%>
proof end;

theorem Th1246: :: NUMBER11:1246
Sum (digits (3150,10)) = 9
proof end;

theorem Th1247: :: NUMBER11:1247
digits (3175,10) = <%5,7,1,3%>
proof end;

theorem Th1248: :: NUMBER11:1248
Sum (digits (3175,10)) = 16
proof end;

theorem Th1249: :: NUMBER11:1249
digits (3225,10) = <%5,2,2,3%>
proof end;

theorem Th1250: :: NUMBER11:1250
Sum (digits (3225,10)) = 12
proof end;

theorem Th1251: :: NUMBER11:1251
digits (3250,10) = <%0,5,2,3%>
proof end;

theorem Th1252: :: NUMBER11:1252
Sum (digits (3250,10)) = 10
proof end;

theorem Th1253: :: NUMBER11:1253
digits (3275,10) = <%5,7,2,3%>
proof end;

theorem Th1254: :: NUMBER11:1254
Sum (digits (3275,10)) = 17
proof end;

theorem Th1255: :: NUMBER11:1255
digits (3325,10) = <%5,2,3,3%>
proof end;

theorem Th1256: :: NUMBER11:1256
Sum (digits (3325,10)) = 13
proof end;

theorem Th1257: :: NUMBER11:1257
digits (3350,10) = <%0,5,3,3%>
proof end;

theorem Th1258: :: NUMBER11:1258
Sum (digits (3350,10)) = 11
proof end;

theorem Th1259: :: NUMBER11:1259
digits (3375,10) = <%5,7,3,3%>
proof end;

theorem Th1260: :: NUMBER11:1260
Sum (digits (3375,10)) = 18
proof end;

theorem Th1261: :: NUMBER11:1261
digits (3425,10) = <%5,2,4,3%>
proof end;

theorem Th1262: :: NUMBER11:1262
Sum (digits (3425,10)) = 14
proof end;

theorem Th1263: :: NUMBER11:1263
digits (3450,10) = <%0,5,4,3%>
proof end;

theorem Th1264: :: NUMBER11:1264
Sum (digits (3450,10)) = 12
proof end;

theorem Th1265: :: NUMBER11:1265
digits (3475,10) = <%5,7,4,3%>
proof end;

theorem Th1266: :: NUMBER11:1266
Sum (digits (3475,10)) = 19
proof end;

theorem Th1267: :: NUMBER11:1267
digits (3525,10) = <%5,2,5,3%>
proof end;

theorem Th1268: :: NUMBER11:1268
Sum (digits (3525,10)) = 15
proof end;

theorem Th1269: :: NUMBER11:1269
digits (3550,10) = <%0,5,5,3%>
proof end;

theorem Th1270: :: NUMBER11:1270
Sum (digits (3550,10)) = 13
proof end;

theorem Th1271: :: NUMBER11:1271
digits (3575,10) = <%5,7,5,3%>
proof end;

theorem Th1272: :: NUMBER11:1272
Sum (digits (3575,10)) = 20
proof end;

theorem Th1273: :: NUMBER11:1273
digits (3625,10) = <%5,2,6,3%>
proof end;

theorem Th1274: :: NUMBER11:1274
Sum (digits (3625,10)) = 16
proof end;

theorem Th1275: :: NUMBER11:1275
digits (3650,10) = <%0,5,6,3%>
proof end;

theorem Th1276: :: NUMBER11:1276
Sum (digits (3650,10)) = 14
proof end;

theorem Th1277: :: NUMBER11:1277
digits (3675,10) = <%5,7,6,3%>
proof end;

theorem Th1278: :: NUMBER11:1278
Sum (digits (3675,10)) = 21
proof end;

theorem Th1279: :: NUMBER11:1279
digits (3725,10) = <%5,2,7,3%>
proof end;

theorem Th1280: :: NUMBER11:1280
Sum (digits (3725,10)) = 17
proof end;

theorem Th1281: :: NUMBER11:1281
digits (3750,10) = <%0,5,7,3%>
proof end;

theorem Th1282: :: NUMBER11:1282
Sum (digits (3750,10)) = 15
proof end;

theorem Th1283: :: NUMBER11:1283
digits (3775,10) = <%5,7,7,3%>
proof end;

theorem Th1284: :: NUMBER11:1284
Sum (digits (3775,10)) = 22
proof end;

theorem Th1285: :: NUMBER11:1285
digits (3825,10) = <%5,2,8,3%>
proof end;

theorem Th1286: :: NUMBER11:1286
Sum (digits (3825,10)) = 18
proof end;

theorem Th1287: :: NUMBER11:1287
digits (3850,10) = <%0,5,8,3%>
proof end;

theorem Th1288: :: NUMBER11:1288
Sum (digits (3850,10)) = 16
proof end;

theorem Th1289: :: NUMBER11:1289
digits (3875,10) = <%5,7,8,3%>
proof end;

theorem Th1290: :: NUMBER11:1290
Sum (digits (3875,10)) = 23
proof end;

theorem Th1291: :: NUMBER11:1291
digits (3925,10) = <%5,2,9,3%>
proof end;

theorem Th1292: :: NUMBER11:1292
Sum (digits (3925,10)) = 19
proof end;

theorem Th1293: :: NUMBER11:1293
digits (3950,10) = <%0,5,9,3%>
proof end;

theorem Th1294: :: NUMBER11:1294
Sum (digits (3950,10)) = 17
proof end;

theorem Th1295: :: NUMBER11:1295
digits (3975,10) = <%5,7,9,3%>
proof end;

theorem Th1296: :: NUMBER11:1296
Sum (digits (3975,10)) = 24
proof end;

theorem Th1297: :: NUMBER11:1297
digits (4000,10) = <%0,0,0,4%>
proof end;

theorem Th1298: :: NUMBER11:1298
Sum (digits (4000,10)) = 4
proof end;

theorem Th1299: :: NUMBER11:1299
digits (4025,10) = <%5,2,0,4%>
proof end;

theorem Th1300: :: NUMBER11:1300
Sum (digits (4025,10)) = 11
proof end;

theorem Th1301: :: NUMBER11:1301
digits (4050,10) = <%0,5,0,4%>
proof end;

theorem Th1302: :: NUMBER11:1302
Sum (digits (4050,10)) = 9
proof end;

theorem Th1303: :: NUMBER11:1303
digits (4075,10) = <%5,7,0,4%>
proof end;

theorem Th1304: :: NUMBER11:1304
Sum (digits (4075,10)) = 16
proof end;

theorem Th1305: :: NUMBER11:1305
digits (4100,10) = <%0,0,1,4%>
proof end;

theorem Th1306: :: NUMBER11:1306
Sum (digits (4100,10)) = 5
proof end;

theorem Th1307: :: NUMBER11:1307
digits (4125,10) = <%5,2,1,4%>
proof end;

theorem Th1308: :: NUMBER11:1308
Sum (digits (4125,10)) = 12
proof end;

theorem Th1309: :: NUMBER11:1309
digits (4150,10) = <%0,5,1,4%>
proof end;

theorem Th1310: :: NUMBER11:1310
Sum (digits (4150,10)) = 10
proof end;

theorem Th1311: :: NUMBER11:1311
digits (4175,10) = <%5,7,1,4%>
proof end;

theorem Th1312: :: NUMBER11:1312
Sum (digits (4175,10)) = 17
proof end;

theorem Th1313: :: NUMBER11:1313
digits (4200,10) = <%0,0,2,4%>
proof end;

theorem Th1314: :: NUMBER11:1314
Sum (digits (4200,10)) = 6
proof end;

theorem Th1315: :: NUMBER11:1315
digits (4225,10) = <%5,2,2,4%>
proof end;

theorem Th1316: :: NUMBER11:1316
Sum (digits (4225,10)) = 13
proof end;

theorem Th1317: :: NUMBER11:1317
digits (4250,10) = <%0,5,2,4%>
proof end;

theorem Th1318: :: NUMBER11:1318
Sum (digits (4250,10)) = 11
proof end;

theorem Th1319: :: NUMBER11:1319
digits (4275,10) = <%5,7,2,4%>
proof end;

theorem Th1320: :: NUMBER11:1320
Sum (digits (4275,10)) = 18
proof end;

theorem Th1321: :: NUMBER11:1321
digits (4300,10) = <%0,0,3,4%>
proof end;

theorem Th1322: :: NUMBER11:1322
Sum (digits (4300,10)) = 7
proof end;

theorem Th1323: :: NUMBER11:1323
digits (4325,10) = <%5,2,3,4%>
proof end;

theorem Th1324: :: NUMBER11:1324
Sum (digits (4325,10)) = 14
proof end;

theorem Th1325: :: NUMBER11:1325
digits (4350,10) = <%0,5,3,4%>
proof end;

theorem Th1326: :: NUMBER11:1326
Sum (digits (4350,10)) = 12
proof end;

theorem Th1327: :: NUMBER11:1327
digits (4375,10) = <%5,7,3,4%>
proof end;

theorem Th1328: :: NUMBER11:1328
Sum (digits (4375,10)) = 19
proof end;

theorem Th1329: :: NUMBER11:1329
digits (4400,10) = <%0,0,4,4%>
proof end;

theorem Th1330: :: NUMBER11:1330
Sum (digits (4400,10)) = 8
proof end;

theorem Th1331: :: NUMBER11:1331
digits (4425,10) = <%5,2,4,4%>
proof end;

theorem Th1332: :: NUMBER11:1332
Sum (digits (4425,10)) = 15
proof end;

theorem Th1333: :: NUMBER11:1333
digits (4450,10) = <%0,5,4,4%>
proof end;

theorem Th1334: :: NUMBER11:1334
Sum (digits (4450,10)) = 13
proof end;

theorem Th1335: :: NUMBER11:1335
digits (4475,10) = <%5,7,4,4%>
proof end;

theorem Th1336: :: NUMBER11:1336
Sum (digits (4475,10)) = 20
proof end;

theorem Th1337: :: NUMBER11:1337
digits (4500,10) = <%0,0,5,4%>
proof end;

theorem Th1338: :: NUMBER11:1338
Sum (digits (4500,10)) = 9
proof end;

theorem Th1339: :: NUMBER11:1339
digits (4525,10) = <%5,2,5,4%>
proof end;

theorem Th1340: :: NUMBER11:1340
Sum (digits (4525,10)) = 16
proof end;

theorem Th1341: :: NUMBER11:1341
digits (4550,10) = <%0,5,5,4%>
proof end;

theorem Th1342: :: NUMBER11:1342
Sum (digits (4550,10)) = 14
proof end;

theorem Th1343: :: NUMBER11:1343
digits (4575,10) = <%5,7,5,4%>
proof end;

theorem Th1344: :: NUMBER11:1344
Sum (digits (4575,10)) = 21
proof end;

theorem Th1345: :: NUMBER11:1345
digits (4600,10) = <%0,0,6,4%>
proof end;

theorem Th1346: :: NUMBER11:1346
Sum (digits (4600,10)) = 10
proof end;

theorem Th1347: :: NUMBER11:1347
digits (4625,10) = <%5,2,6,4%>
proof end;

theorem Th1348: :: NUMBER11:1348
Sum (digits (4625,10)) = 17
proof end;

theorem Th1349: :: NUMBER11:1349
digits (4650,10) = <%0,5,6,4%>
proof end;

theorem Th1350: :: NUMBER11:1350
Sum (digits (4650,10)) = 15
proof end;

theorem Th1351: :: NUMBER11:1351
digits (4675,10) = <%5,7,6,4%>
proof end;

theorem Th1352: :: NUMBER11:1352
Sum (digits (4675,10)) = 22
proof end;

theorem Th1353: :: NUMBER11:1353
digits (4700,10) = <%0,0,7,4%>
proof end;

theorem Th1354: :: NUMBER11:1354
Sum (digits (4700,10)) = 11
proof end;

theorem Th1355: :: NUMBER11:1355
digits (4725,10) = <%5,2,7,4%>
proof end;

theorem Th1356: :: NUMBER11:1356
Sum (digits (4725,10)) = 18
proof end;

theorem Th1357: :: NUMBER11:1357
digits (4750,10) = <%0,5,7,4%>
proof end;

theorem Th1358: :: NUMBER11:1358
Sum (digits (4750,10)) = 16
proof end;

theorem Th1359: :: NUMBER11:1359
digits (4775,10) = <%5,7,7,4%>
proof end;

theorem Th1360: :: NUMBER11:1360
Sum (digits (4775,10)) = 23
proof end;

theorem Th1361: :: NUMBER11:1361
digits (4800,10) = <%0,0,8,4%>
proof end;

theorem Th1362: :: NUMBER11:1362
Sum (digits (4800,10)) = 12
proof end;

theorem Th1363: :: NUMBER11:1363
digits (4825,10) = <%5,2,8,4%>
proof end;

theorem Th1364: :: NUMBER11:1364
Sum (digits (4825,10)) = 19
proof end;

theorem Th1365: :: NUMBER11:1365
digits (4850,10) = <%0,5,8,4%>
proof end;

theorem Th1366: :: NUMBER11:1366
Sum (digits (4850,10)) = 17
proof end;

theorem Th1367: :: NUMBER11:1367
digits (4875,10) = <%5,7,8,4%>
proof end;

theorem Th1368: :: NUMBER11:1368
Sum (digits (4875,10)) = 24
proof end;

theorem Th1369: :: NUMBER11:1369
digits (4900,10) = <%0,0,9,4%>
proof end;

theorem Th1370: :: NUMBER11:1370
Sum (digits (4900,10)) = 13
proof end;

theorem Th1371: :: NUMBER11:1371
digits (4925,10) = <%5,2,9,4%>
proof end;

theorem Th1372: :: NUMBER11:1372
Sum (digits (4925,10)) = 20
proof end;

theorem Th1373: :: NUMBER11:1373
digits (4950,10) = <%0,5,9,4%>
proof end;

theorem Th1374: :: NUMBER11:1374
Sum (digits (4950,10)) = 18
proof end;

theorem Th1375: :: NUMBER11:1375
digits (4975,10) = <%5,7,9,4%>
proof end;

theorem Th1376: :: NUMBER11:1376
Sum (digits (4975,10)) = 25
proof end;

theorem :: NUMBER11:1377
Sierp36 4975,25
proof end;

theorem :: NUMBER11:1378
Sierp36 value (((<%0,0%> ^ (11 --> 9)) ^ <%1%>),10),100
proof end;