Nuprl Lemma : div_bounds_1

`∀[a:ℕ]. ∀[n:ℕ+].  (0 ≤ (a ÷ n))`

Proof

Definitions occuring in Statement :  nat_plus: `ℕ+` nat: `ℕ` uall: `∀[x:A]. B[x]` le: `A ≤ B` divide: `n ÷ m` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat_plus: `ℕ+` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` nequal: `a ≠ b ∈ T ` guard: `{T}` uimplies: `b supposing a` all: `∀x:A. B[x]` prop: `ℙ` int_nzero: `ℤ-o` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` subtype_rel: `A ⊆r B` top: `Top` less_than': `less_than'(a;b)` true: `True` cand: `A c∧ B` sq_type: `SQType(T)`
Lemmas referenced :  zero-mul add-mul-special le_transitivity subtype_base_sq le_reflexive multiply-is-int-iff mul-commutes le-add-cancel add_functionality_wrt_le minus-one-mul-top minus-one-mul int_subtype_base add-is-int-iff zero-add add-associates add-commutes add-swap minus-minus minus-add add-zero minus-zero condition-implies-le not-le-2 false_wf le_weakening2 mul_preserves_le decidable__le less_than_wf le_wf rem_bounds_1 nequal_wf div_rem_sum nat_wf nat_plus_wf equal_wf less_than_irreflexivity le_weakening less_than_transitivity1 less_than'_wf nat_properties nat_plus_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename sqequalRule productElimination independent_pairEquality lambdaEquality dependent_functionElimination because_Cache divideEquality lambdaFormation natural_numberEquality independent_isectElimination independent_functionElimination voidElimination intEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality dependent_set_memberEquality unionElimination minusEquality independent_pairFormation addEquality applyEquality voidEquality baseApply closedConclusion baseClosed multiplyEquality instantiate cumulativity

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (0  \mleq{}  (a  \mdiv{}  n))

Date html generated: 2016_05_13-PM-03_35_04
Last ObjectModification: 2016_01_14-PM-06_40_02

Theory : arithmetic

Home Index