### Nuprl Lemma : divisor-in-range

`∀n:{2...}`
`  ∀[k:ℕ]`
`    ∀i:{1...}. ∀j:{i..i + k-}.`
`      (∃m:ℤ [(m < n ∧ (2 ≤ m) ∧ (m | n))]) ∨ (¬(∃m:ℤ [((2 ≤ m) ∧ (i ≤ m) ∧ (m ≤ j) ∧ (m | n))])) supposing j < n`

Proof

Definitions occuring in Statement :  divides: `b | a` int_upper: `{i...}` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` not: `¬A` or: `P ∨ Q` and: `P ∧ Q` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` member: `t ∈ T` int_upper: `{i...}` nat: `ℕ` uimplies: `b supposing a` int_seg: `{i..j-}` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` implies: `P `` Q` nat_plus: `ℕ+` le: `A ≤ B` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` true: `True` sq_stable: `SqStable(P)` squash: `↓T` subtract: `n - m` lelt: `i ≤ j < k` guard: `{T}` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` sq_type: `SQType(T)` sq_exists: `∃x:A [B[x]]` gcd: `gcd(a;b)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` nequal: `a ≠ b ∈ T ` cand: `A c∧ B` gcd_p: `GCD(a;b;y)` iseg_product: `iseg_product(i;j)` int_nzero: `ℤ-o` less_than: `a < b`
Lemmas referenced :  uniform-comp-nat-induction all_wf int_upper_wf int_seg_wf isect_wf less_than_wf or_wf sq_exists_wf le_wf divides_wf istype-int not_wf nat_wf member-less_than iseg_product_rem_wf decidable__lt istype-false not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel int_seg_subtype_nat decidable__le not-le-2 sq_stable__le condition-implies-le minus-add minus-one-mul minus-one-mul-top add-associates int_seg_properties nat_properties int_upper_properties full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma set-value-type equal_wf int-value-type better-gcd_wf subtype_base_sq int_subtype_base better-gcd-gcd upper_subtype_nat iseg_product_wf eq_int_wf eqtt_to_assert assert_of_eq_int intformeq_wf int_formula_prop_eq_lemma eqff_to_assert set_subtype_base bool_cases_sqequal bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int gcd_wf istype-universe iseg_product_rem_property iff_weakening_equal rem_rem_to_rem not-equal-2 gcd_com gcd_sat_pred combinations-step subtract_wf itermSubtract_wf int_term_value_subtract_lemma lelt_wf decidable__equal_int itermMultiply_wf int_term_value_mul_lemma divisors_bound gcd-non-neg gcd_is_divisor_2 squash_wf true_wf subtype_rel_self div_rem_sum nequal_wf rem_bounds_1 add-is-int-iff multiply-is-int-iff false_wf gcd-positive divides-combinations pdivisor_bound one_divs_any
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality_alt natural_numberEquality hypothesis setElimination rename because_Cache addEquality intEquality productEquality hypothesisEquality universeIsType independent_functionElimination isect_memberFormation_alt independent_isectElimination dependent_set_memberEquality_alt productElimination dependent_functionElimination unionElimination independent_pairFormation voidElimination applyEquality imageMemberEquality baseClosed imageElimination minusEquality approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt productIsType cutEval equalityTransitivity equalitySymmetry equalityIsType1 inhabitedIsType instantiate cumulativity isectIsType functionIsType unionIsType equalityElimination equalityIsType2 baseApply closedConclusion promote_hyp universeEquality remainderEquality inlFormation_alt dependent_set_memberFormation_alt equalityIsType4 divideEquality pointwiseFunctionality inrFormation_alt applyLambdaEquality

Latex:
\mforall{}n:\{2...\}
\mforall{}[k:\mBbbN{}]
\mforall{}i:\{1...\}.  \mforall{}j:\{i..i  +  k\msupminus{}\}.
(\mexists{}m:\mBbbZ{}  [(m  <  n  \mwedge{}  (2  \mleq{}  m)  \mwedge{}  (m  |  n))])  \mvee{}  (\mneg{}(\mexists{}m:\mBbbZ{}  [((2  \mleq{}  m)  \mwedge{}  (i  \mleq{}  m)  \mwedge{}  (m  \mleq{}  j)  \mwedge{}  (m  |  n))]))
supposing  j  <  n

Date html generated: 2019_10_15-AM-11_17_39
Last ObjectModification: 2018_10_09-PM-02_12_13

Theory : general

Home Index