Step * 1 1 1 1 1 2 1 of Lemma rroot-regularity-lemma


1. {2...}
2. : ℕ+
3. : ℕ+
4. : ℤ
5. : ℤ
6. : ℤ
7. : ℤ
8. 0 ≤ b
9. 0 ∈ ℤ
10. 0 ∈ ℤ
11. (n ≤ b) ∨ ((b 0 ∈ ℤ) ∧ (d 0 ∈ ℤ))
12. 0^k ≤ 0
13. 0 < m^k
14. b^k ≤ d
15. d < n^k
16. |0 d| ≤ (2^k (n^k m^k))
17. ((2 n) m) m < b
⊢ False
BY
((Assert 0 ≤ b^k BY Auto) THEN (Assert 0 ≤ BY Auto)) }

1
1. {2...}
2. : ℕ+
3. : ℕ+
4. : ℤ
5. : ℤ
6. : ℤ
7. : ℤ
8. 0 ≤ b
9. 0 ∈ ℤ
10. 0 ∈ ℤ
11. (n ≤ b) ∨ ((b 0 ∈ ℤ) ∧ (d 0 ∈ ℤ))
12. 0^k ≤ 0
13. 0 < m^k
14. b^k ≤ d
15. d < n^k
16. |0 d| ≤ (2^k (n^k m^k))
17. ((2 n) m) m < b
18. 0 ≤ b^k
19. 0 ≤ d
⊢ False


Latex:


Latex:

1.  k  :  \{2...\}
2.  n  :  \mBbbN{}\msupplus{}
3.  m  :  \mBbbN{}\msupplus{}
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  c  :  \mBbbZ{}
7.  d  :  \mBbbZ{}
8.  0  \mleq{}  b
9.  a  =  0
10.  c  =  0
11.  (n  \mleq{}  b)  \mvee{}  ((b  =  0)  \mwedge{}  (d  =  0))
12.  0\^{}k  \mleq{}  0
13.  0  <  0  +  m\^{}k
14.  b\^{}k  \mleq{}  d
15.  d  <  b  +  n\^{}k
16.  |0  -  d|  \mleq{}  (2\^{}k  *  (n\^{}k  +  m\^{}k))
17.  ((2  *  n)  +  m)  +  0  +  m  <  b
\mvdash{}  False


By


Latex:
((Assert  0  \mleq{}  b\^{}k  BY  Auto)  THEN  (Assert  0  \mleq{}  d  BY  Auto))




Home Index