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

At: sqrt prime irrational 1
1. p:
2. prime(p)
3. 0 < p
m,n:. mm = pnn n = 0
By:
CompleteInductionOnNat
THEN
SupposeNot
Generated subgoal:

14. m:
5. m1:. m1 < m (n:. m1m1 = pnn n = 0)
6. n:
7. mm = pnn
8. n = 0
n = 0		34 steps

About:
intnatural_numbermultiplyless_thanequalimpliesall

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