---

Step * of Lemma mod2-is-one

∀x:ℤ. ((x mod 2) = 1 ∈ ℤ ⇐⇒ ∃n:ℤ. (x = ((2 * n) + 1) ∈ ℤ))
BY
{ ((D 0 THENA Auto) THEN Assert ⌜(x mod 2) = 1 ∈ ℤ ⇐⇒ ((x - 1) mod 2) = 0 ∈ ℤ⌝⋅) }

1
.....assertion..... 
1. x : ℤ
⊢ (x mod 2) = 1 ∈ ℤ ⇐⇒ ((x - 1) mod 2) = 0 ∈ ℤ

2
1. x : ℤ
2. (x mod 2) = 1 ∈ ℤ ⇐⇒ ((x - 1) mod 2) = 0 ∈ ℤ
⊢ (x mod 2) = 1 ∈ ℤ ⇐⇒ ∃n:ℤ. (x = ((2 * n) + 1) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  ((x  mod  2)  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbZ{}.  (x  =  ((2  *  n)  +  1)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}(x  mod  2)  =  1  \mLeftarrow{}{}\mRightarrow{}  ((x  -  1)  mod  2)  =  0\mkleeneclose{}\mcdot{})

---

Home Index