equal
deleted
inserted
replaced
133 |
133 |
134 lemma "100094 mod 144 = (14::int)" |
134 lemma "100094 mod 144 = (14::int)" |
135 by simp |
135 by simp |
136 |
136 |
137 |
137 |
|
138 text {* \medskip Powers *} |
|
139 |
|
140 lemma "2 ^ 10 = (1024::int)" |
|
141 by simp |
|
142 |
|
143 lemma "-3 ^ 7 = (-2187::int)" |
|
144 by simp |
|
145 |
|
146 lemma "13 ^ 7 = (62748517::int)" |
|
147 by simp |
|
148 |
|
149 lemma "3 ^ 15 = (14348907::int)" |
|
150 by simp |
|
151 |
|
152 lemma "-5 ^ 11 = (-48828125::int)" |
|
153 by simp |
|
154 |
|
155 |
138 subsection {* The Natural Numbers *} |
156 subsection {* The Natural Numbers *} |
139 |
157 |
140 text {* Successor *} |
158 text {* Successor *} |
141 |
159 |
142 lemma "Suc 99999 = 100000" |
160 lemma "Suc 99999 = 100000" |
196 |
214 |
197 lemma "(10000::nat) div 16 = 625" |
215 lemma "(10000::nat) div 16 = 625" |
198 by simp |
216 by simp |
199 |
217 |
200 lemma "(10000::nat) mod 16 = 0" |
218 lemma "(10000::nat) mod 16 = 0" |
|
219 by simp |
|
220 |
|
221 |
|
222 text {* \medskip Powers *} |
|
223 |
|
224 lemma "2 ^ 12 = (4096::nat)" |
|
225 by simp |
|
226 |
|
227 lemma "3 ^ 10 = (59049::nat)" |
|
228 by simp |
|
229 |
|
230 lemma "12 ^ 7 = (35831808::nat)" |
|
231 by simp |
|
232 |
|
233 lemma "3 ^ 14 = (4782969::nat)" |
|
234 by simp |
|
235 |
|
236 lemma "5 ^ 11 = (48828125::nat)" |
201 by simp |
237 by simp |
202 |
238 |
203 |
239 |
204 text {* \medskip Testing the cancellation of complementary terms *} |
240 text {* \medskip Testing the cancellation of complementary terms *} |
205 |
241 |