---

Step * 1 of Lemma posint_well_fnd


WellFnd{i}(ℕ+;x,y.(∃c:ℕ+. (y = (x * c) ∈ ℕ+)) ∧ (¬(∃c:ℕ+. (x = (y * c) ∈ ℕ+))))
BY
{ ((RWH (RevLemmaC `divides_nchar`) 0) THENA Auto) 
THEN ((Try (BLemma `mul_bounds_1b`)) THENA Auto) }

1
WellFnd{i}(ℕ+;x,y.(x | y) ∧ (¬(y | x)))

---

Latex:

---

Latex:

WellFnd\{i\}(\mBbbN{}\msupplus{};x,y.(\mexists{}c:\mBbbN{}\msupplus{}.  (y  =  (x  *  c)))  \mwedge{}  (\mneg{}(\mexists{}c:\mBbbN{}\msupplus{}.  (x  =  (y  *  c)))))


By

---

Latex:
((RWH  (RevLemmaC  `divides\_nchar`)  0)  THENA  Auto) 
THEN  ((Try  (BLemma  `mul\_bounds\_1b`))  THENA  Auto)

---

Home Index