---

Step * of Lemma pdivisor_bound

∀a:ℕ. ∀b:ℕ+.  ((a | b) ∧ (¬(b | a)) ⇐⇒ a < b ∧ (a | b))
BY
{ Auto }

1
1. a : ℕ
2. b : ℕ+
3. a | b
4. ¬(b | a)
⊢ a < b

2
1. a : ℕ
2. b : ℕ+
3. a < b
4. a | b
⊢ ¬(b | a)

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}.  \mforall{}b:\mBbbN{}\msupplus{}.    ((a  |  b)  \mwedge{}  (\mneg{}(b  |  a))  \mLeftarrow{}{}\mRightarrow{}  a  <  b  \mwedge{}  (a  |  b))


By

---

Latex:
Auto

---

Home Index