---

Step * of Lemma posint_is_ufm

IsUFM(<ℤ+,*>)
BY
{ ((BLemma `ufm_char` THENM RepD) THENA Auto) }

1
Cancel(|<ℤ+,*>|;|<ℤ+,*>|;*)

2
WellFnd{i}(|<ℤ+,*>|;x,y.x p| y)

3
1. a : Atom{<ℤ+,*>}@i
⊢ IsPrime(a)

4
1. a : |<ℤ+,*>|@i
⊢ Dec(Reducible(a))

5
1. a : |<ℤ+,*>|@i
2. b : |<ℤ+,*>|@i
⊢ Dec(a | b)

---

Latex:

---

Latex:
IsUFM(<\mBbbZ{}\msupplus{},*>)


By

---

Latex:
((BLemma  `ufm\_char`  THENM  RepD)  THENA  Auto)

---

Home Index