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

At: sqrt prime irrational 1 1 1 2 1 1 1 2 1 1 2 1 3
1. p:
2. prime(p)
3. 0 < p
4. m:
5. m1:. m1 < m (n:. m1m1 = pnn n = 0)
6. n:
7. ((m p)p+(m mod p))((m p)p+(m mod p)) = pnn
8. n = 0
9. m = (m p)p+(m mod p)
10. (m mod p) < p
11. n@0:. nn = pn@0n@0 n@0 = 0
12. p | ((m mod p)(m mod p))
13. c:
14. (m mod p) = 0
15. c < 1
16. c < 0
17. (m p) = 0
n = 0
By:
HypSubst -1 7
THEN
HypSubst -4 7
THEN
ArithSimp 7
Generated subgoal:

17. 0 = nnp
8. n = 0
9. m = (m p)p+(m mod p)
10. (m mod p) < p
11. n@0:. nn = pn@0n@0 n@0 = 0
12. p | ((m mod p)(m mod p))
13. c:
14. (m mod p) = 0
15. c < 1
16. c < 0
17. (m p) = 0
n = 0		1 step

About:
intnatural_numberaddmultiplyless_thanequalimpliesall

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