Nuprl Lemma : proper-divisor-aux

Nuprl Lemma : proper-divisor-aux_wf

∀[n:ℕ⁺]. ∀[m:ℕ].
  (proper-divisor-aux(n;m;m;1;m) ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])) supposing
     (m * m < n and
     n < (m * m) * m * m)

Proof

Error : references

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[m:\mBbbN{}]. (proper-divisor-aux(n;m;m;1;m) \mmember{} Dec(\mexists{}n1:\mBbbZ{} [(n1 < n \mwedge{} (2 \mleq{} n1) \mwedge{} (n1 | n))])) supposing (m * m < n and n < (m * m) * m * m) Date html generated: 2020_05_20-AM-08_41_38 Last ObjectModification: 2020_01_08-PM-01_47_14 Theory : general Home Index