### Nuprl Lemma : prime_ideals_in_int_ring

`∀i:ℕ+. (ℤ-rng-Prime(i) `⇐⇒` prime(i))`

Proof

Definitions occuring in Statement :  int_ring: `ℤ-rng` rprime: `r-Prime(u)` prime: `prime(a)` nat_plus: `ℕ+` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q`
Definitions unfolded in proof :  int_ring: `ℤ-rng` rprime: `r-Prime(u)` rng_one: `1` pi2: `snd(t)` pi1: `fst(t)` rng_car: `|r|` rng_times: `*` infix_ap: `x f y` ring_divs: `a | b in r` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` nat_plus: `ℕ+` so_apply: `x[s]` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` or: `P ∨ Q` rev_implies: `P `` Q` not: `¬A` false: `False` prime: `prime(a)` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` cand: `A c∧ B` assoced: `a ~ b` divides: `b | a` decidable: `Dec(P)` guard: `{T}`
Lemmas referenced :  one_divs_any assoced_wf int_term_value_mul_lemma int_formula_prop_not_lemma itermMultiply_wf intformnot_wf decidable__equal_int divides_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt nat_plus_properties nat_plus_wf prime_wf equal_wf or_wf int_subtype_base all_wf equal-wf-T-base exists_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule lambdaFormation independent_pairFormation sqequalHypSubstitution productElimination thin productEquality cut lemma_by_obid isectElimination intEquality lambdaEquality multiplyEquality hypothesisEquality setElimination rename baseClosed hypothesis because_Cache functionEquality baseApply closedConclusion applyEquality independent_functionElimination voidElimination natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality dependent_functionElimination isect_memberEquality voidEquality computeAll introduction unionElimination inlFormation inrFormation

Latex:
\mforall{}i:\mBbbN{}\msupplus{}.  (\mBbbZ{}-rng-Prime(i)  \mLeftarrow{}{}\mRightarrow{}  prime(i))

Date html generated: 2016_05_15-PM-00_26_25
Last ObjectModification: 2016_01_15-AM-08_52_21

Theory : rings_1

Home Index