Nuprl Lemma : sqrt-int-aa-real-fast-complete-ext
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 :
nat: ,
exists: x:A. B[x],
and: P Q,
le: A B,
member: t 
T,
sqrt-int-aa-real-fast-complete,
rem_bounds_1,
decidable__lt,
natInd4BootFast,
not: 
A,
decidable__equal_int,
completeInductionFast,
implies: P 
Q,
false: False,
so_apply: x[s1;s2],
genrec-ap: Error :genrec-ap
Lemmas :
sqrt-int-aa-real-fast-complete
\mforall{}n:\mBbbN{}. \mexists{}r:\mBbbN{}. (((r * r) \mleq{} n) \mwedge{} (n < ((r + 1) * (r + 1))))
Date html generated:
2013_03_20-AM-09_47_37
Last ObjectModification:
2012_11_27-AM-10_31_59
Home
Index