Step * 2 2 of Lemma iroot-lemma


1. : ℕ
2. : ℕ+
3. : ℕ+
4. : ℕ+
5. k ∈ ℕ+
6. : ℕ+
7. k < M^n
8. ∃y:ℕ+((n M^(n 1)) ≤ (k y))
⊢ ∃x:ℕ. ∃y:ℕ+(a y^n < (x b)^n ∧ ((x b)^n ≤ ((a k) y^n)))
BY
TACTIC:(ExRepD THEN Assert ⌜(a k) y^n ∈ ℕ+⌝⋅}

1
.....assertion..... 
1. : ℕ
2. : ℕ+
3. : ℕ+
4. : ℕ+
5. k ∈ ℕ+
6. : ℕ+
7. k < M^n
8. : ℕ+
9. (n M^(n 1)) ≤ (k y)
⊢ (a k) y^n ∈ ℕ+

2
1. : ℕ
2. : ℕ+
3. : ℕ+
4. : ℕ+
5. k ∈ ℕ+
6. : ℕ+
7. k < M^n
8. : ℕ+
9. (n M^(n 1)) ≤ (k y)
10. (a k) y^n ∈ ℕ+
⊢ ∃x:ℕ. ∃y:ℕ+(a y^n < (x b)^n ∧ ((x b)^n ≤ ((a k) y^n)))


Latex:


Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  b  :  \mBbbN{}\msupplus{}
4.  k  :  \mBbbN{}\msupplus{}
5.  a  +  k  \mmember{}  \mBbbN{}\msupplus{}
6.  M  :  \mBbbN{}\msupplus{}
7.  a  +  k  <  M\^{}n
8.  \mexists{}y:\mBbbN{}\msupplus{}.  ((n  *  b  *  M\^{}(n  -  1))  \mleq{}  (k  *  y))
\mvdash{}  \mexists{}x:\mBbbN{}.  \mexists{}y:\mBbbN{}\msupplus{}.  (a  *  y\^{}n  <  (x  *  b)\^{}n  \mwedge{}  ((x  *  b)\^{}n  \mleq{}  ((a  +  k)  *  y\^{}n)))


By


Latex:
TACTIC:(ExRepD  THEN  Assert  \mkleeneopen{}(a  +  k)  *  y\^{}n  \mmember{}  \mBbbN{}\msupplus{}\mkleeneclose{}\mcdot{})




Home Index