---

Step * 1 2 1 1 1 of Lemma prime-factors2


1. n : {2...}
2. ∀n1:{2..n-}. (∃factors:{m:{2...}| prime(m)}  List [(n1 = Π(factors)  ∈ ℤ)])
3. x : ℤ
4. [%4] : x < n ∧ (2 ≤ x) ∧ (x | n)
5. y : ℤ
6. y = (n ÷ x) ∈ ℤ
7. ∃factors:{m:{2...}| prime(m)}  List [(x = Π(factors)  ∈ ℤ)]
⊢ ∃factors:{m:{2...}| prime(m)}  List [(n = Π(factors)  ∈ ℤ)]
BY
{ InstHyp [⌜y⌝] 2⋅ }

1
.....wf..... 
1. n : {2...}
2. ∀n1:{2..n-}. (∃factors:{m:{2...}| prime(m)}  List [(n1 = Π(factors)  ∈ ℤ)])
3. x : ℤ
4. x < n ∧ (2 ≤ x) ∧ (x | n)
5. y : ℤ
6. y = (n ÷ x) ∈ ℤ
7. ∃factors:{m:{2...}| prime(m)}  List [(x = Π(factors)  ∈ ℤ)]
⊢ y ∈ {2..n-}

2
1. n : {2...}
2. ∀n1:{2..n-}. (∃factors:{m:{2...}| prime(m)}  List [(n1 = Π(factors)  ∈ ℤ)])
3. x : ℤ
4. [%4] : x < n ∧ (2 ≤ x) ∧ (x | n)
5. y : ℤ
6. y = (n ÷ x) ∈ ℤ
7. ∃factors:{m:{2...}| prime(m)}  List [(x = Π(factors)  ∈ ℤ)]
8. ∃factors:{m:{2...}| prime(m)}  List [(y = Π(factors)  ∈ ℤ)]
⊢ ∃factors:{m:{2...}| prime(m)}  List [(n = Π(factors)  ∈ ℤ)]

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  \mforall{}n1:\{2..n\msupminus{}\}.  (\mexists{}factors:\{m:\{2...\}|  prime(m)\}    List  [(n1  =  \mPi{}(factors)  )])
3.  x  :  \mBbbZ{}
4.  [\%4]  :  x  <  n  \mwedge{}  (2  \mleq{}  x)  \mwedge{}  (x  |  n)
5.  y  :  \mBbbZ{}
6.  y  =  (n  \mdiv{}  x)
7.  \mexists{}factors:\{m:\{2...\}|  prime(m)\}    List  [(x  =  \mPi{}(factors)  )]
\mvdash{}  \mexists{}factors:\{m:\{2...\}|  prime(m)\}    List  [(n  =  \mPi{}(factors)  )]


By

---

Latex:
InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  2\mcdot{}

---

Home Index