Nuprl Lemma : qexp-convex3

a,b:ℚ.  ((((0 ≤ a) ∧ (0 ≤ b)) ∨ ((a ≤ 0) ∧ (b ≤ 0)))  (∀n:ℕ+(|a b| ↑ n ≤ |a ↑ b ↑ n|)))


Proof




Definitions occuring in Statement :  qexp: r ↑ n qabs: |r| qle: r ≤ s qsub: s rationals: nat_plus: + all: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q member: t ∈ T cand: c∧ B uall: [x:A]. B[x] subtype_rel: A ⊆B uimplies: supposing a qless: r < s grp_lt: a < b set_lt: a <b assert: b ifthenelse: if then else fi  set_blt: a <b b band: p ∧b q infix_ap: y set_le: b pi2: snd(t) oset_of_ocmon: g↓oset dset_of_mon: g↓set grp_le: b pi1: fst(t) qadd_grp: <ℚ+> q_le: q_le(r;s) callbyvalueall: callbyvalueall evalall: evalall(t) bor: p ∨bq qpositive: qpositive(r) qsub: s qadd: s qmul: s btrue: tt lt_int: i <j bnot: ¬bb bfalse: ff qeq: qeq(r;s) eq_int: (i =z j) true: True uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) prop: squash: T guard: {T} iff: ⇐⇒ Q rev_implies:  Q nat_plus: + bool: 𝔹 unit: Unit it: exists: x:A. B[x] sq_type: SQType(T) false: False
Lemmas referenced :  qexp-convex2 qmul_wf qmul_reverses_qle qle_wf nat_plus_wf or_wf int-subtype-rationals rationals_wf squash_wf true_wf qmul_zero_qrng qinv_inv_q iff_weakening_equal qexp_wf nat_wf equal_wf qabs-difference-symmetry qabs_wf qsub_wf nat_plus_subtype_nat qadd_wf qadd_comm_q isEven_wf bool_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot qabs-qminus qexp-qminus qmul_over_plus_qrng
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution unionElimination thin productElimination cut introduction extract_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis independent_pairFormation isectElimination minusEquality natural_numberEquality applyEquality because_Cache sqequalRule independent_isectElimination hyp_replacement equalitySymmetry lambdaEquality imageElimination imageMemberEquality baseClosed productEquality equalityTransitivity universeEquality setElimination rename equalityElimination dependent_pairFormation promote_hyp instantiate voidElimination

Latex:
\mforall{}a,b:\mBbbQ{}.    ((((0  \mleq{}  a)  \mwedge{}  (0  \mleq{}  b))  \mvee{}  ((a  \mleq{}  0)  \mwedge{}  (b  \mleq{}  0)))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  (|a  -  b|  \muparrow{}  n  \mleq{}  |a  \muparrow{}  n  -  b  \muparrow{}  n|)))



Date html generated: 2018_05_22-AM-00_01_45
Last ObjectModification: 2017_07_26-PM-06_50_23

Theory : rationals


Home Index