Nuprl Lemma : implies-equal-real

[x,y:ℝ].  y ∈ ℝ supposing ∀n:ℕ+((x n) (y n) ∈ ℤ)


Proof




Definitions occuring in Statement :  real: nat_plus: + uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] apply: a int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a real: squash: T prop: all: x:A. B[x] true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q nat_plus: + less_than: a < b less_than': less_than'(a;b) sq_stable: SqStable(P) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  equal_wf squash_wf true_wf iff_weakening_equal nat_plus_wf sq_stable__regular-int-seq less_than_wf regular-int-seq_wf all_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality functionExtensionality applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality intEquality dependent_functionElimination setElimination rename natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination because_Cache independent_pairFormation isect_memberEquality axiomEquality

Latex:
\mforall{}[x,y:\mBbbR{}].    x  =  y  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  =  (y  n))



Date html generated: 2017_10_02-PM-07_13_14
Last ObjectModification: 2017_07_28-AM-07_20_01

Theory : reals


Home Index