`∀[n,m:ℕ].  n < m supposing n < ((n + m) + 1) ÷ 2`

Proof

Definitions occuring in Statement :  nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` divide: `n ÷ m` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat: `ℕ` ge: `i ≥ j ` all: `∀x:A. B[x]` true: `True` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` sq_type: `SQType(T)` guard: `{T}` false: `False` prop: `ℙ` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` and: `P ∧ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` int_nzero: `ℤ-o` uiff: `uiff(P;Q)` nat_plus: `ℕ+` less_than': `less_than'(a;b)` subtype_rel: `A ⊆r B` le: `A ≤ B` iff: `P `⇐⇒` Q` subtract: `n - m` isOdd: `isOdd(n)` rev_uimplies: `rev_uimplies(P;Q)` ifthenelse: `if b then t else f fi ` btrue: `tt` rev_implies: `P `` Q` bfalse: `ff`
Lemmas referenced :  nat_properties decidable__lt subtype_base_sq int_subtype_base equal-wf-base true_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermMultiply_wf itermVar_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_mul_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf div_rem_sum nequal_wf decidable__equal_int add-is-int-iff intformeq_wf itermSubtract_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_subtract_lemma int_term_value_add_lemma false_wf less_than_wf subtract_wf subtract-is-int-iff rem_bounds_1 decidable__le intformle_wf int_formula_prop_le_lemma le_wf decidable__or intformor_wf int_formula_prop_or_lemma rem_add1 iff_weakening_equal member-less_than nat_wf eq_int_wf add-zero assert_of_eq_int modulus_wf_int_mod int-subtype-int_mod modulus-is-rem assert_wf bnot_wf not_wf equal-wf-T-base bool_cases bool_wf bool_subtype_base eqtt_to_assert eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot isOdd-add not-same-parity-implies-even-odd even-iff-not-odd not_assert_elim isOdd_wf and_wf equal_wf assert_elim btrue_neq_bfalse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename dependent_functionElimination multiplyEquality natural_numberEquality divideEquality addEquality addLevel lambdaFormation instantiate cumulativity intEquality independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination baseClosed because_Cache unionElimination imageElimination productElimination dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidEquality sqequalRule independent_pairFormation computeAll dependent_set_memberEquality pointwiseFunctionality promote_hyp baseApply closedConclusion hyp_replacement Error :applyLambdaEquality,  remainderEquality imageMemberEquality applyEquality equalityEquality impliesFunctionality setEquality

Latex:
\mforall{}[n,m:\mBbbN{}].    n  <  m  supposing  n  <  ((n  +  m)  +  1)  \mdiv{}  2

Date html generated: 2016_10_25-AM-10_59_26
Last ObjectModification: 2016_07_12-AM-07_07_09

Theory : general

Home Index