Nuprl Lemma : rdiv_functionality

[x1,x2,y1,y2:ℝ].  ((x1/y1) (x2/y2)) supposing ((y1 y2) and (x1 x2) and y1 ≠ r0)


Definitions occuring in Statement :  rdiv: (x/y) rneq: x ≠ y req: y int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T implies:  Q prop: rdiv: (x/y) all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)

\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