---

Step * of Lemma positive-prime-divides-product

∀p:{p:ℕ| prime(p)} . ∀qs:{p:ℕ| prime(p)}  List.  ((p | reduce(λx,y. (x * y);1;qs)) ⇒ (p ∈ qs))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN (D 1 THEN Unhide) THEN Auto THEN DupHyp 2 THEN D -1 THEN Auto) }

1
1. p : ℕ@i
2. prime(p)@i
3. p | 1@i
4. ¬(p = 0 ∈ ℤ)@i
5. ¬(p ~ 1)@i
6. ∀b,c:ℤ.  ((p | (b * c)) ⇒ ((p | b) ∨ (p | c)))@i
⊢ (p ∈ [])

2
1. p : ℕ@i
2. prime(p)@i
3. u : {p:ℕ| prime(p)} @i
4. v : {p:ℕ| prime(p)}  List@i
5. (p | reduce(λx,y. (x * y);1;v)) ⇒ (p ∈ v)@i
6. p | (u * reduce(λx,y. (x * y);1;v))@i
7. ¬(p = 0 ∈ ℤ)@i
8. ¬(p ~ 1)@i
9. ∀b,c:ℤ.  ((p | (b * c)) ⇒ ((p | b) ∨ (p | c)))@i
⊢ (p ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}p:\{p:\mBbbN{}|  prime(p)\}  .  \mforall{}qs:\{p:\mBbbN{}|  prime(p)\}    List.    ((p  |  reduce(\mlambda{}x,y.  (x  *  y);1;qs))  {}\mRightarrow{}  (p  \mmember{}  qs))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (D  1  THEN  Unhide)
  THEN  Auto
  THEN  DupHyp  2
  THEN  D  -1
  THEN  Auto)

---

Home Index