Nuprl Lemma : sqrt-int-aa2
n:
. 
r:. (((r * r) 
n) 
(n < ((r + 1) * (r + 1))))
Proof
Definitions occuring in Statement :
nat: ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
and: P Q,
less_than: a < b,
multiply: n * m,
add: n + m,
natural_number: $n
Definitions :
all: x:A. B[x],
and: P Q,
prop: 
,
implies: P 
Q,
member: t 
T,
so_lambda: 
x.t[x],
exists: x:A. B[x],
nat: ,
le: A B,
not: 
A,
false: False,
uall: [x:A]. B[x],
so_apply: x[s],
decidable: Dec(P),
or: P 
Q
Lemmas :
nat-ind-boot-direct,
exists_wf,
nat_wf,
le_wf,
decidable__lt
\mforall{}n:\mBbbN{}. \mexists{}r:\mBbbN{}. (((r * r) \mleq{} n) \mwedge{} (n < ((r + 1) * (r + 1))))
Date html generated:
2013_03_20-AM-09_46_34
Last ObjectModification:
2012_11_27-AM-10_31_57
Home
Index