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

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

14. m:
5. n:
6. mm = pnn
7. n = 0
n = 0		5 steps

About:
intnatural_numbermultiplyless_thanequalimpliesall

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