---

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


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

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

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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((D  (-2)  THEN  D  -1  THEN  InstHyp  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]  4\mcdot{})  THEN  Auto)\mcdot{}

---

Home Index