---

Step * of Lemma vexample_wf

∀n,a:ℕ. ∀b:{b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} .
  (vexample(n;a;b) ∈ a:ℕ × {b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} )
BY
{ (InductionOnNat THEN Intros THEN Unfold `vexample` 0 THEN Reduce 0) }

1
1. n : ℤ
2. a : ℕ
3. b : {b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} 
⊢ <a, b> ∈ a:ℕ × {b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} 

2
1. n : ℤ
2. 0 < n
3. ∀a:ℕ. ∀b:{b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} .
     (vexample(n - 1;a;b) ∈ a:ℕ × {b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} )
4. a : ℕ
5. b : {b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} 
⊢ if n=0 then <a, b> else eval b' = (3 * b) - a in eval m = n - 1 in   vexample(m;b;b') ∈ a:ℕ × {b:ℕ| 
                                                                                                 (((a * a) + (b * b))
                                                                                                 + 1)
                                                                                                 = ((a * b) * 3)
                                                                                                 ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}n,a:\mBbbN{}.  \mforall{}b:\{b:\mBbbN{}|  (((a  *  a)  +  (b  *  b))  +  1)  =  ((a  *  b)  *  3)\}  .
    (vexample(n;a;b)  \mmember{}  a:\mBbbN{}  \mtimes{}  \{b:\mBbbN{}|  (((a  *  a)  +  (b  *  b))  +  1)  =  ((a  *  b)  *  3)\}  )


By

---

Latex:
(InductionOnNat  THEN  Intros  THEN  Unfold  `vexample`  0  THEN  Reduce  0)

---

Home Index