---

Step * 1 1 1 1 of Lemma posint_reduc_dec


1. a : ℕ+
⊢ Dec(∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ b < a ∧ (b | a)))
BY
{ Assert ∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ b < a ∧ (b | a)) ⇐⇒ ∃b:{2..a-}. (b | a) 
THENA (GenExRepD THENM With b (D 0) THEN Auto)  }

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mexists{}b:\mBbbN{}\msupplus{}.  ((\mneg{}(b  =  1))  \mwedge{}  b  <  a  \mwedge{}  (b  |  a))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:\{2..a\msupminus{}\}.  (b  |  a) 
THENA  (GenExRepD  THENM  With  b  (D  0)  THEN  Auto) 

---

Home Index