---

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


1. p : {2...}
2. c : ℤ
3. c1 : ℤ
4. n : ℕ
5. ∀a:ℤ. ∀b:ℕ+.  (((a * a) = (n * b * b) ∈ ℤ) ⇒ (∀p:ℤ. (prime(p) ⇒ (p | b) ⇒ (p | a))))
6. x : ℕ
7. ∀x:ℕp * c. ((1 ≤ x) ⇒ (∀a:ℤ. (((a * a) = (n * x * x) ∈ ℤ) ⇒ (∃m:ℕn + 1. ((m * m) = n ∈ ℤ)))))
8. 1 ≤ (p * c)
9. a : ℤ
10. ((p * c1) * p * c1) = (n * (p * c) * p * c) ∈ ℤ
11. ¬((p * c) = 1 ∈ ℤ)
12. prime(p)
13. x = (p * c) ∈ ℤ
14. a = (p * c1) ∈ ℤ
⊢ (c1 * c1) = (n * c * c) ∈ ℤ
BY
{ (Mul ⌜p * p⌝ 0⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  c  :  \mBbbZ{}
3.  c1  :  \mBbbZ{}
4.  n  :  \mBbbN{}
5.  \mforall{}a:\mBbbZ{}.  \mforall{}b:\mBbbN{}\msupplus{}.    (((a  *  a)  =  (n  *  b  *  b))  {}\mRightarrow{}  (\mforall{}p:\mBbbZ{}.  (prime(p)  {}\mRightarrow{}  (p  |  b)  {}\mRightarrow{}  (p  |  a))))
6.  x  :  \mBbbN{}
7.  \mforall{}x:\mBbbN{}p  *  c.  ((1  \mleq{}  x)  {}\mRightarrow{}  (\mforall{}a:\mBbbZ{}.  (((a  *  a)  =  (n  *  x  *  x))  {}\mRightarrow{}  (\mexists{}m:\mBbbN{}n  +  1.  ((m  *  m)  =  n)))))
8.  1  \mleq{}  (p  *  c)
9.  a  :  \mBbbZ{}
10.  ((p  *  c1)  *  p  *  c1)  =  (n  *  (p  *  c)  *  p  *  c)
11.  \mneg{}((p  *  c)  =  1)
12.  prime(p)
13.  x  =  (p  *  c)
14.  a  =  (p  *  c1)
\mvdash{}  (c1  *  c1)  =  (n  *  c  *  c)


By

---

Latex:
(Mul  \mkleeneopen{}p  *  p\mkleeneclose{}  0\mcdot{}  THEN  Auto')

---

Home Index