Nuprl Lemma : rng-pp-nontrivial-2

∀r:IntegDom{i}
  ((∀x,y:|r|.  Dec(x = y ∈ |r|))
  ⇒ (∀l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
        ∃a,b,c:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
         (((a . l) = 0 ∈ |r|)
         ∧ ((b . l) = 0 ∈ |r|)
         ∧ ((c . l) = 0 ∈ |r|)
         ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))
         ∧ (¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|)))
         ∧ (¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))))))


Proof



Definitions occuring in Statement :  int_seg: {i..j-},  decidable: Dec(P),  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  function: x:A ⟶ B[x],  natural_number: $n,  equal: s = t ∈ T,  integ_dom: IntegDom{i},  rng_zero: 0,  rng_car: |r|,  scalar-product: (a . b),  cross-product: (a x b),  zero-vector: 0
Definitions unfolded in proof :  rev_implies: P ⇐ Q,  iff: P ⇐⇒ Q,  guard: {T},  uimplies: b supposing a,  subtype_rel: A ⊆r B,  squash: ↓T,  true: True,  vector-add: (a + b),  zero-vector: 0,  infix_ap: x f y,  vector-mul: (c*a),  so_apply: x[s],  so_lambda: λ2x.t[x],  less_than': less_than'(a;b),  le: A ≤ B,  nat: ℕ,  rng: Rng,  crng: CRng,  integ_dom: IntegDom{i},  uall: ∀[x:A]. B[x],  prop: ℙ,  false: False,  not: ¬A,  cand: A c∧ B,  and: P ∧ Q,  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  member: t ∈ T,  all: ∀x:A. B[x]
Lemmas referenced :  zero-vector-add-left,  cross-product-distrib2,  zero-vector-add-right,  cross-product-distrib1,  cross-product-anti-comm,  scalar-product-add-left,  cross-product-same,  vector-mul_wf,  cross-product-mul1,  mul-zero-vector,  rng_sig_wf,  iff_weakening_equal,  rng_plus_zero,  rng_plus_inv,  rng_plus_comm,  rng_plus_assoc,  rng_times_one,  subtype_rel_self,  rng_times_over_minus,  true_wf,  squash_wf,  rng_one_wf,  rng_minus_wf,  rng_times_wf,  rng_plus_wf,  vector-add_wf,  integ_dom_wf,  decidable_wf,  all_wf,  rng_zero_wf,  exists_wf,  not_wf,  le_wf,  false_wf,  scalar-product_wf,  zero-vector_wf,  cross-product_wf,  rng_car_wf,  int_seg_wf,  equal_wf,  rng-pp-nontrivial-1-ext
Rules used in proof :  levelHypothesis,  equalityUniverse,  independent_isectElimination,  instantiate,  baseClosed,  imageMemberEquality,  universeEquality,  imageElimination,  applyLambdaEquality,  lambdaEquality,  applyEquality,  functionExtensionality,  setEquality,  sqequalRule,  dependent_set_memberEquality,  equalitySymmetry,  equalityTransitivity,  productEquality,  because_Cache,  natural_numberEquality,  functionEquality,  isectElimination,  voidElimination,  independent_pairFormation,  rename,  setElimination,  dependent_pairFormation,  productElimination,  independent_functionElimination,  hypothesisEquality,  thin,  dependent_functionElimination,  sqequalHypSubstitution,  hypothesis,  lambdaFormation,  sqequalReflexivity,  computationStep,  sqequalTransitivity,  sqequalSubstitution,  extract_by_obid,  introduction,  cut
Latex:
\mforall{}r:IntegDom\{i\}
    ((\mforall{}x,y:|r|.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
                \mexists{}a,b,c:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
                  (((a  .  l)  =  0)
                  \mwedge{}  ((b  .  l)  =  0)
                  \mwedge{}  ((c  .  l)  =  0)
                  \mwedge{}  (\mneg{}((a  x  b)  =  0))
                  \mwedge{}  (\mneg{}((b  x  c)  =  0))
                  \mwedge{}  (\mneg{}((c  x  a)  =  0)))))


Date html generated: 2018_05_22-PM-00_53_46
Last ObjectModification: 2018_05_21-AM-01_23_44

Theory : euclidean!plane!geometry


Home Index