Nuprl - Proof: sqrt prime irrational 1 1 1 2 1 1 1 1

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

At: sqrt prime irrational 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. ((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))

p | (m mod p)

By: Unfold `prime` 2 THEN RepD THEN InstHyp [m mod p;m mod p] 4

Generated subgoal:

1 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) 1 step

About:

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