Nuprl Lemma : div_mono1

[i,k:ℕ].  (i ÷ k < i) supposing (1 < and 0 < i)


Definitions occuring in Statement :  nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] divide: n ÷ m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] decidable: Dec(P) or: P ∨ Q nat: int_nzero: -o nequal: a ≠ b ∈  ge: i ≥  not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: subtype_rel: A ⊆B nat_plus: + uiff: uiff(P;Q) squash: T less_than: a < b
Lemmas referenced :  decidable__lt istype-less_than member-less_than divide_wfa nat_properties full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf int_subtype_base nequal_wf istype-nat div_base_case intformnot_wf int_formula_prop_not_lemma div_rem_sum rem_bounds_1 decidable__le intformle_wf int_formula_prop_le_lemma mul_preserves_le divide_wf satisfiable-full-omega-tt equal_wf add-is-int-iff multiply-is-int-iff itermMultiply_wf itermAdd_wf int_term_value_mul_lemma int_term_value_add_lemma false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache hypothesis unionElimination isectElimination natural_numberEquality setElimination rename hypothesisEquality sqequalRule Error :isect_memberEquality_alt,  Error :dependent_set_memberEquality_alt,  Error :lambdaFormation_alt,  independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality voidElimination independent_pairFormation Error :universeIsType,  Error :equalityIstype,  applyEquality baseClosed sqequalBase equalitySymmetry intEquality Error :isectIsTypeImplies,  Error :inhabitedIsType,  equalityTransitivity closedConclusion baseApply promote_hyp pointwiseFunctionality computeAll voidEquality isect_memberEquality lambdaEquality dependent_pairFormation imageElimination lambdaFormation divideEquality multiplyEquality lemma_by_obid productElimination

\mforall{}[i,k:\mBbbN{}].    (i  \mdiv{}  k  <  i)  supposing  (1  <  k  and  0  <  i)

Date html generated: 2019_06_20-PM-02_31_15
Last ObjectModification: 2019_03_06-AM-10_53_24

Theory : num_thy_1

Home Index