(6steps total)
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
2 has no rational square root.
At:
two
sqr
roots
(
p
:
,
q
:
.
p
p
= 2
q
q
)
By:
BackThru:
Thm*
P
:(
Prop). (
x
:
.
P
(
x
)
(
x'
:
.
x'
<
x
&
P
(
x'
)))
(
x
:
.
P
(
x
))
Generated subgoal:
1
1.
p
:
2.
q
:
.
p
p
= 2
q
q
p'
:
.
p'
<
p
& (
q'
:
.
p'
p'
= 2
q'
q'
)
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc
(
p:
, q:
. p
p = 2qq) (p:, q:. pp = 2qq)
P:(
Prop). (x:. P(x) 
(x':. x'<x & P(x'))) (x:. P(x))
q:. pp = 2qq
p':. p'<p & (q':. p'p' = 2q'q')
