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

At: sqrt prime irrational 1 1 1 2 1 1 1 1 1

1. p:
2. p = 0
3. (p ~ 1)
4. b,c:. (p | (bc)) (p | b) (p | c)
5. 0 < p
6. m:
7. m1:. m1 < m (n:. m1m1 = pnn n = 0)
8. n:
9. ((m p)p+(m mod p))((m p)p+(m mod p)) = pnn
10. n = 0
11. m = (m p)p+(m mod p)
12. (m mod p) < p
13. n@0:. nn = pn@0n@0 n@0 = 0
14. p | ((m mod p)(m mod p))
15. (p | (m mod p)) (p | (m mod p))
p | (m mod p)

By:
Analyze -1
THEN
Trivial


Generated subgoals:

None

About:
intnatural_numberaddmultiplyless_thanequalimpliesorall

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