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