### Nuprl Lemma : rmul-int-fractions

`∀[a,b:ℤ]. ∀[c,d:ℕ+].  (((r(a)/r(c)) * (r(b)/r(d))) = (r(a * b)/r(c * d)))`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` req: `x = y` rmul: `a * b` int-to-real: `r(n)` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` multiply: `n * m` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat_plus: `ℕ+` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` decidable: `Dec(P)` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` prop: `ℙ` nequal: `a ≠ b ∈ T ` subtype_rel: `A ⊆r B` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[c,d:\mBbbN{}\msupplus{}].    (((r(a)/r(c))  *  (r(b)/r(d)))  =  (r(a  *  b)/r(c  *  d)))

Date html generated: 2020_05_20-AM-11_00_54
Last ObjectModification: 2020_01_02-PM-02_12_40

Theory : reals

Home Index