Nuprl Lemma : mul_preserves_le2

[a,c:ℕ]. ∀[b,d:ℤ].  ((a c) ≤ (b d)) supposing ((a ≤ b) and (c ≤ d))


Definitions occuring in Statement :  nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B multiply: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a nat: and: P ∧ Q le: A ≤ B cand: c∧ B implies:  Q all: x:A. B[x] sq_stable: SqStable(P) guard: {T} squash: T top: Top
Lemmas referenced :  mul_preserves_le sq_stable_from_decidable le_wf decidable__le le_transitivity istype-le le_witness_for_triv istype-int istype-nat istype-void mul-commutes
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality independent_isectElimination hypothesis Error :dependent_set_memberEquality_alt,  setElimination rename independent_pairFormation productElimination natural_numberEquality independent_functionElimination dependent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination equalityTransitivity equalitySymmetry Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :inhabitedIsType,  voidElimination

\mforall{}[a,c:\mBbbN{}].  \mforall{}[b,d:\mBbbZ{}].    ((a  *  c)  \mleq{}  (b  *  d))  supposing  ((a  \mleq{}  b)  and  (c  \mleq{}  d))

Date html generated: 2019_06_20-AM-11_23_20
Last ObjectModification: 2019_02_08-PM-01_26_03

Theory : arithmetic

Home Index