Nuprl Lemma : rdiv_functionality
∀[x1,x2,y1,y2:ℝ]. ((x1/y1) = (x2/y2)) supposing ((y1 = y2) and (x1 = x2) and y1 ≠ r0)
Proof
Definitions occuring in Statement :
rdiv: (x/y),
rneq: x ≠ y,
req: x = y,
int-to-real: r(n),
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
implies: P ⇒ Q,
prop: ℙ,
rdiv: (x/y),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q)
Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}]. ((x1/y1) = (x2/y2)) supposing ((y1 = y2) and (x1 = x2) and y1 \mneq{} r0)
Date html generated:
2020_05_20-AM-10_59_34
Last ObjectModification:
2020_01_06-PM-00_26_51
Theory : reals
Home
Index