### Nuprl Lemma : int-eq-in-rationals

`∀[x,y:ℤ].  uiff(x = y ∈ ℚ;x = y ∈ ℤ)`

Proof

Definitions occuring in Statement :  rationals: `ℚ` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}` implies: `P `` Q` qeq: `qeq(r;s)` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` ifthenelse: `if b then t else f fi ` btrue: `tt`
Lemmas referenced :  equal_wf rationals_wf int-subtype-rationals equal_functionality_wrt_subtype_rel2 assert-qeq valueall-type-has-valueall int-valueall-type evalall-reduce assert_of_eq_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality sqequalRule because_Cache intEquality independent_isectElimination independent_functionElimination productElimination independent_pairEquality isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry callbyvalueReduce isintReduceTrue

Latex:
\mforall{}[x,y:\mBbbZ{}].    uiff(x  =  y;x  =  y)

Date html generated: 2016_05_15-PM-10_39_14
Last ObjectModification: 2015_12_27-PM-07_59_21

Theory : rationals

Home Index