Nuprl Lemma : rat2real-qdiv2
∀a:ℤ. ∀b:ℤ-o. (rat2real((a/b)) = (r(a)/r(b)))
Proof
Definitions occuring in Statement :
rat2real: rat2real(q),
rdiv: (x/y),
req: x = y,
int-to-real: r(n),
int_nzero: ℤ-o,
all: ∀x:A. B[x],
int: ℤ,
qdiv: (r/s)
Definitions unfolded in proof :
all: ∀x:A. B[x],
rat2real: rat2real(q),
ifthenelse: if b then t else f fi ,
btrue: tt,
member: t ∈ T,
subtype_rel: A ⊆r B
Latex:
\mforall{}a:\mBbbZ{}. \mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}. (rat2real((a/b)) = (r(a)/r(b)))
Date html generated:
2020_05_20-AM-11_01_27
Last ObjectModification:
2019_12_09-AM-00_44_03
Theory : reals
Home
Index