### Nuprl Lemma : div_bounds_2

`∀[a:{...-1}]. ∀[n:ℕ+].  ((a ÷ n) ≤ 0)`

Proof

Definitions occuring in Statement :  int_lower: `{...i}` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` le: `A ≤ B` divide: `n ÷ m` minus: `-n` natural_number: `\$n`
Definitions unfolded in proof :  true: `True` less_than': `less_than'(a;b)` top: `Top` subtract: `n - m` uiff: `uiff(P;Q)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)` and: `P ∧ Q` le: `A ≤ B` int_lower: `{...i}` guard: `{T}` false: `False` not: `¬A` nequal: `a ≠ b ∈ T ` implies: `P `` Q` all: `∀x:A. B[x]` prop: `ℙ` uimplies: `b supposing a` so_apply: `x[s]` so_lambda: `λ2x.t[x]` int_nzero: `ℤ-o` nat_plus: `ℕ+` subtype_rel: `A ⊆r B` member: `t ∈ T` uall: `∀[x:A]. B[x]` ge: `i ≥ j ` rev_uimplies: `rev_uimplies(P;Q)` gt: `i > j` squash: `↓T` sq_stable: `SqStable(P)` sq_type: `SQType(T)`
Rules used in proof :  equalitySymmetry equalityTransitivity axiomEquality divideEquality independent_pairEquality voidEquality isect_memberEquality addEquality independent_pairFormation unionElimination productElimination minusEquality baseClosed voidElimination independent_functionElimination dependent_functionElimination lambdaFormation setEquality rename setElimination independent_isectElimination hypothesis natural_numberEquality lambdaEquality intEquality sqequalRule applyEquality hypothesisEquality because_Cache thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution closedConclusion baseApply remainderEquality multiplyEquality imageElimination imageMemberEquality cumulativity instantiate

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

Date html generated: 2017_09_29-PM-05_47_11
Last ObjectModification: 2017_07_31-PM-04_18_52

Theory : arithmetic

Home Index