---

Step * 1 of Lemma int_pi_det_fun_wf


1. i : ℤ
2. i = 0 ∈ ℤ
⊢ ∀x@0:ℤ. (∃b:ℤ. (x@0 = (i * b) ∈ ℤ) ⇐⇒ ↑(x@0 =z 0))
BY
{ ((HypSubst' (-1) 0 THEN (D 0 THENA Auto)) THEN (RW assert_pushdownC 0 THENA Auto) THEN Auto THEN ExRepD THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  i  =  0
\mvdash{}  \mforall{}x@0:\mBbbZ{}.  (\mexists{}b:\mBbbZ{}.  (x@0  =  (i  *  b))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(x@0  =\msubz{}  0))


By

---

Latex:
((HypSubst'  (-1)  0  THEN  (D  0  THENA  Auto))
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Auto
  THEN  ExRepD
  THEN  Auto)

---

Home Index