---

Step * 1 1 1 1 1 of Lemma posint_reduc_dec


1. a : ℕ+
2. ∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ b < a ∧ (b | a)) ⇐⇒ ∃b:{2..a-}. (b | a)
⊢ Dec(∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ b < a ∧ (b | a)))
BY
{ ((RWH (HypC 2) 0) THENA Auto) }

1
1. a : ℕ+
2. ∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ b < a ∧ (b | a)) ⇐⇒ ∃b:{2..a-}. (b | a)
⊢ Dec(∃b:{2..a-}. (b | a))

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}\msupplus{}
2.  \mexists{}b:\mBbbN{}\msupplus{}.  ((\mneg{}(b  =  1))  \mwedge{}  b  <  a  \mwedge{}  (b  |  a))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:\{2..a\msupminus{}\}.  (b  |  a)
\mvdash{}  Dec(\mexists{}b:\mBbbN{}\msupplus{}.  ((\mneg{}(b  =  1))  \mwedge{}  b  <  a  \mwedge{}  (b  |  a)))


By

---

Latex:
((RWH  (HypC  2)  0)  THENA  Auto)

---

Home Index