---

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


1. n : {2...}
2. ∀n1:{2..n-}. (∃factors:{m:{2...}| prime(m)}  List [(n1 = Π(factors)  ∈ ℤ)])
3. x : ℤ
4. x < n
5. 2 ≤ x
6. x | n
7. y : ℤ
8. y = (n ÷ x) ∈ ℤ
9. factors : {m:{2...}| prime(m)}  List
10. x = Π(factors)  ∈ ℤ
11. ((n ÷ x) * x) = n ∈ ℤ
⊢ y < n
BY
{ (SupposeNot
   THEN (InstLemma `mul_preserves_le` [⌜n⌝;⌜n ÷ x⌝;⌜x⌝]⋅ THEN Auto)
   THEN InstLemma `mul_preserves_le` [⌜2⌝;⌜x⌝;⌜n⌝]⋅
   THEN Auto)⋅ }

---

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.  x  <  n
5.  2  \mleq{}  x
6.  x  |  n
7.  y  :  \mBbbZ{}
8.  y  =  (n  \mdiv{}  x)
9.  factors  :  \{m:\{2...\}|  prime(m)\}    List
10.  x  =  \mPi{}(factors) 
11.  ((n  \mdiv{}  x)  *  x)  =  n
\mvdash{}  y  <  n


By

---

Latex:
(SupposeNot
  THEN  (InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n  \mdiv{}  x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index