---

Step * 1 1 1 of Lemma posint_atom_imp_prime


1. a : {a:ℕ+| (¬(a | 1)) ∧ (¬(∃b,c:ℕ+. ((¬(b | 1)) ∧ (¬(c | 1)) ∧ (a = (b * c) ∈ ℕ+))))} 
2. ¬(a | 1)
3. b : ℕ+
4. c : ℕ+
5. a | (b * c)
6. ¬(∃b,c:ℕ+. ((¬(b | 1)) ∧ (¬(c | 1)) ∧ (a = (b * c) ∈ ℕ+)))
7. ∀x:ℕ+. (a | x ⇐⇒ a | x)
⊢ (a | b) ∨ (a | c)
BY
{ TACTIC:((RWO "-1" 0 THENA Auto) THEN (RWO "-1" 5 THENA Auto) THEN (RWO "-1" 2 THENA Auto)) }

1
1. a : {a:ℕ+| (¬(a | 1)) ∧ (¬(∃b,c:ℕ+. ((¬(b | 1)) ∧ (¬(c | 1)) ∧ (a = (b * c) ∈ ℕ+))))} 
2. ¬(a | 1)
3. b : ℕ+
4. c : ℕ+
5. a | (b * c)
6. ¬(∃b,c:ℕ+. ((¬(b | 1)) ∧ (¬(c | 1)) ∧ (a = (b * c) ∈ ℕ+)))
7. ∀x:ℕ+. (a | x ⇐⇒ a | x)
⊢ (a | b) ∨ (a | c)

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbN{}\msupplus{}|  (\mneg{}(a  |  1))  \mwedge{}  (\mneg{}(\mexists{}b,c:\mBbbN{}\msupplus{}.  ((\mneg{}(b  |  1))  \mwedge{}  (\mneg{}(c  |  1))  \mwedge{}  (a  =  (b  *  c)))))\} 
2.  \mneg{}(a  |  1)
3.  b  :  \mBbbN{}\msupplus{}
4.  c  :  \mBbbN{}\msupplus{}
5.  a  |  (b  *  c)
6.  \mneg{}(\mexists{}b,c:\mBbbN{}\msupplus{}.  ((\mneg{}(b  |  1))  \mwedge{}  (\mneg{}(c  |  1))  \mwedge{}  (a  =  (b  *  c))))
7.  \mforall{}x:\mBbbN{}\msupplus{}.  (a  |  x  \mLeftarrow{}{}\mRightarrow{}  a  |  x)
\mvdash{}  (a  |  b)  \mvee{}  (a  |  c)


By

---

Latex:
TACTIC:((RWO  "-1"  0  THENA  Auto)  THEN  (RWO  "-1"  5  THENA  Auto)  THEN  (RWO  "-1"  2  THENA  Auto))

---

Home Index