(42steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: sqrt prime irrational 1 1

1. p:
2. prime(p)
3. 0 < p
4. m:
5. m1:. m1 < m (n:. m1m1 = pnn n = 0)
6. n:
7. mm = pnn
8. n = 0
n = 0

By: Inst Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n [m;p]

Generated subgoal:

19. m = (m p)p+(m mod p)
10. (m mod p) < p
n = 0
33 steps

About:
intnatural_numberaddmultiplyless_thanequalimpliesandall

(42steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc