Nuprl Lemma : div_nat_induction

b:{b:ℤ1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0]  (∀i:ℕ+(P[i ÷ b]  P[i]))  (∀i:ℕP[i]))


Proof




Definitions occuring in Statement :  nat_plus: + nat: less_than: a < b uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] divide: n ÷ m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] implies:  Q member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uimplies: supposing a sq_type: SQType(T) guard: {T} nequal: a ≠ b ∈  not: ¬A false: False ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q prop: so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] nat_plus: + iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) true: True subtract: m int_seg: {i..j-} lelt: i ≤ j < k squash: T sq_stable: SqStable(P)
Lemmas referenced :  lelt_wf int_formula_prop_le_lemma int_formula_prop_not_lemma intformle_wf intformnot_wf decidable__le sq_stable__less_than subtype_rel_sets div_mono1 div_bounds_1 minus-zero minus-add condition-implies-le add-zero not-equal-2 set_wf le_wf less_than_wf le-add-cancel zero-add add-associates add-commutes add-swap add_functionality_wrt_le less-iff-le not-lt-2 decidable__lt nat_plus_subtype_nat divide_wf nat_plus_wf natrec_wf nat_wf false_wf int_seg_subtype_nat int_seg_wf all_wf int-value-type set-value-type equal_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt nat_properties int_subtype_base subtype_base_sq decidable__equal_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut thin lemma_by_obid sqequalHypSubstitution dependent_functionElimination setElimination rename hypothesisEquality because_Cache hypothesis unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination independent_functionElimination divideEquality natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll cutEval introduction dependent_set_memberEquality equalityTransitivity equalitySymmetry equalityEquality applyEquality functionEquality productElimination addEquality universeEquality minusEquality setEquality imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}b:\{b:\mBbbZ{}|  1  <  b\}  .  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  \mdiv{}  b]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))



Date html generated: 2016_05_15-PM-05_12_35
Last ObjectModification: 2016_01_16-AM-11_36_23

Theory : general


Home Index