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

At: sqrt prime irrational 1 1 1 1 1 2 1 1 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
9. m = (m p)p+(m mod p)
10. (m mod p) < p
11. mn
12. 0 < nn
13. nmnn
14. mmmn
15. mn = nm
16. p = 1
prime(1)

By:
Analyze 0
THEN
Analyze -1
THEN
Analyze -1
THEN
Analyze -2


Generated subgoal:

117. 1 = 0
18. b,c:. (1 | (bc)) (1 | b) (1 | c)
1 ~ 1
1 step

About:
intnatural_numberaddmultiplyless_thanequalimpliesall

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