### Nuprl Lemma : stamps35_wf

`∀n:ℕ. (stamps35(n) ∈ ∃i:ℕ. (∃j:ℕ [((n + 8) = ((3 * i) + (5 * j)) ∈ ℤ)]))`

Proof

Definitions occuring in Statement :  stamps35: `stamps35(n)` nat: `ℕ` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` member: `t ∈ T` multiply: `n * m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` stamps35: `stamps35(n)` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` nat: `ℕ` so_apply: `x[s]` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` prop: `ℙ`
Lemmas referenced :  stamps-example-ext subtype_rel_self nat_wf exists_wf sq_exists_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule applyEquality thin instantiate extract_by_obid hypothesis introduction sqequalHypSubstitution isectElimination functionEquality lambdaEquality intEquality addEquality setElimination rename hypothesisEquality natural_numberEquality multiplyEquality

Latex:
\mforall{}n:\mBbbN{}.  (stamps35(n)  \mmember{}  \mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((n  +  8)  =  ((3  *  i)  +  (5  *  j)))]))

Date html generated: 2018_05_21-PM-00_04_07
Last ObjectModification: 2018_05_19-AM-07_10_48

Theory : int_1

Home Index