---

Step * 1 1 of Lemma posint_reduc_dec


1. a : |<ℤ+,*>|
⊢ Dec(∃b:ℕ+. ((¬(<ℤ+,*>-unit(b))) ∧ (∃c:ℕ+. (a = (b * c) ∈ ℕ+)) ∧ (¬(∃c:ℕ+. (b = (a * c) ∈ ℕ+)))))
BY
{ ((RWH (LemmaC `posint_munit_elim` 
     ORELSEC RevLemmaC `divides_nchar`) 0) THENA Auto) 
THEN % Ugly% ((Try (BLemma `mul_bounds_1b`)) THEN Auto) }

1
.....decidable?..... 
1. a : |<ℤ+,*>|
⊢ Dec(∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ (b | a) ∧ (¬(a | b))))

---

Latex:

---

Latex:

1.  a  :  |<\mBbbZ{}\msupplus{},*>|
\mvdash{}  Dec(\mexists{}b:\mBbbN{}\msupplus{}.  ((\mneg{}(<\mBbbZ{}\msupplus{},*>-unit(b)))  \mwedge{}  (\mexists{}c:\mBbbN{}\msupplus{}.  (a  =  (b  *  c)))  \mwedge{}  (\mneg{}(\mexists{}c:\mBbbN{}\msupplus{}.  (b  =  (a  *  c))))))


By

---

Latex:
((RWH  (LemmaC  `posint\_munit\_elim` 
          ORELSEC  RevLemmaC  `divides\_nchar`)  0)  THENA  Auto) 
THEN  \%  Ugly\%  ((Try  (BLemma  `mul\_bounds\_1b`))  THEN  Auto)

---

Home Index