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

.....wf..... 
1. : ℕ
2. ∀a:ℤ. ∀b:ℕ+.  (((a a) (n b) ∈ ℤ (∀p:ℤ(prime(p)  (p b)  (p a))))
3. : ℕ
4. ∀x:ℕx. ((1 ≤ x)  (∀a:ℤ(((a a) (n x) ∈ ℤ (∃m:ℕ1. ((m m) n ∈ ℤ)))))
5. 1 ≤ x
6. : ℤ
7. (a a) n ∈ ℤ
8. 1 ∈ ℤ
⊢ |a| ∈ ℕ1
BY
((MemTypeCD THEN Auto) THEN SupposeNot THEN (Assert (n 1) ≤ |a| BY Auto)) }

1
1. : ℕ
2. ∀a:ℤ. ∀b:ℕ+.  (((a a) (n b) ∈ ℤ (∀p:ℤ(prime(p)  (p b)  (p a))))
3. : ℕ
4. ∀x:ℕx. ((1 ≤ x)  (∀a:ℤ(((a a) (n x) ∈ ℤ (∃m:ℕ1. ((m m) n ∈ ℤ)))))
5. 1 ≤ x
6. : ℤ
7. (a a) n ∈ ℤ
8. 1 ∈ ℤ
9. ¬|a| < 1
10. (n 1) ≤ |a|
⊢ |a| < 1


Latex:


Latex:
.....wf..... 
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
8.  x  =  1
\mvdash{}  |a|  \mmember{}  \mBbbN{}n  +  1


By


Latex:
((MemTypeCD  THEN  Auto)  THEN  SupposeNot  THEN  (Assert  (n  +  1)  \mleq{}  |a|  BY  Auto))




Home Index