---

Step * 1 of Lemma irrational-sqrt-number-lemma


1. a : ℤ
2. b : ℕ+
3. n : ℕ
4. (a * a) = (n * b * b) ∈ ℤ
⊢ ∃m:ℕn + 1. ((m * m) = n ∈ ℤ)
BY
{ Assert ⌜∀a:ℤ. ∀b:ℕ+.  (((a * a) = (n * b * b) ∈ ℤ) ⇒ (∀p:ℤ. (prime(p) ⇒ (p | b) ⇒ (p | a))))⌝⋅ }

1
.....assertion..... 
1. a : ℤ
2. b : ℕ+
3. n : ℕ
4. (a * a) = (n * b * b) ∈ ℤ
⊢ ∀a:ℤ. ∀b:ℕ+.  (((a * a) = (n * b * b) ∈ ℤ) ⇒ (∀p:ℤ. (prime(p) ⇒ (p | b) ⇒ (p | a))))

2
1. a : ℤ
2. b : ℕ+
3. n : ℕ
4. (a * a) = (n * b * b) ∈ ℤ
5. ∀a:ℤ. ∀b:ℕ+.  (((a * a) = (n * b * b) ∈ ℤ) ⇒ (∀p:ℤ. (prime(p) ⇒ (p | b) ⇒ (p | a))))
⊢ ∃m:ℕn + 1. ((m * m) = n ∈ ℤ)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbN{}\msupplus{}
3.  n  :  \mBbbN{}
4.  (a  *  a)  =  (n  *  b  *  b)
\mvdash{}  \mexists{}m:\mBbbN{}n  +  1.  ((m  *  m)  =  n)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}a:\mBbbZ{}.  \mforall{}b:\mBbbN{}\msupplus{}.    (((a  *  a)  =  (n  *  b  *  b))  {}\mRightarrow{}  (\mforall{}p:\mBbbZ{}.  (prime(p)  {}\mRightarrow{}  (p  |  b)  {}\mRightarrow{}  (p  |  a))))\mkleeneclose{}\mcdot{}

---

Home Index