Nuprl Lemma : omega-shadow-exact2

a:ℕ+. ∀c,d:ℤ.  (∃x:ℤ((c ≤ (a x)) ∧ (x ≤ d)) ⇐⇒ c ≤ (a d))


Proof




Definitions occuring in Statement :  nat_plus: + le: A ≤ B all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q multiply: m int:
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q exists: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat_plus: + decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top prop: less_than: a < b squash: T less_than': less_than'(a;b) true: True so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q
Lemmas referenced :  nat_plus_wf le_weakening le_wf and_wf exists_wf less_than_wf omega-shadow int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf itermMultiply_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_plus_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation sqequalHypSubstitution productElimination thin cut lemma_by_obid isectElimination hypothesisEquality hypothesis setElimination rename dependent_functionElimination multiplyEquality natural_numberEquality unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll dependent_set_memberEquality introduction imageMemberEquality baseClosed independent_functionElimination because_Cache

Latex:
\mforall{}a:\mBbbN{}\msupplus{}.  \mforall{}c,d:\mBbbZ{}.    (\mexists{}x:\mBbbZ{}.  ((c  \mleq{}  (a  *  x))  \mwedge{}  (x  \mleq{}  d))  \mLeftarrow{}{}\mRightarrow{}  c  \mleq{}  (a  *  d))



Date html generated: 2016_05_14-AM-07_23_25
Last ObjectModification: 2016_01_14-PM-10_02_33

Theory : int_2


Home Index