Step
*
1
1
1
2
1
2
1
of Lemma
qexp-difference-bound
1. a : ℚ
2. b : ℚ
3. n : ℕ+
4. 0 ≤ n
5. i : ℤ
6. 0 ≤ i
7. i < n
8. 0 ≤ |a ↑ i|
9. 0 ≤ |b ↑ n - i + 1|
10. 0 ≤ qmax(|a|;|b|)
11. 0 ≤ qmax(|a|;|b|) ↑ i
12. |a ↑ i| ≤ qmax(|a|;|b|) ↑ i
⊢ (|a ↑ i| * |b ↑ n - i + 1|) ≤ (|a ↑ i| * qmax(|a|;|b|) ↑ n - i + 1)
BY
{ (BLemma `qmul_preserves_qle2` THEN Auto) }
1
1. a : ℚ
2. b : ℚ
3. n : ℕ+
4. 0 ≤ n
5. i : ℤ
6. 0 ≤ i
7. i < n
8. 0 ≤ |a ↑ i|
9. 0 ≤ |b ↑ n - i + 1|
10. 0 ≤ qmax(|a|;|b|)
11. 0 ≤ qmax(|a|;|b|) ↑ i
12. |a ↑ i| ≤ qmax(|a|;|b|) ↑ i
⊢ |b ↑ n - i + 1| ≤ qmax(|a|;|b|) ↑ n - i + 1
Latex:
Latex:
1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  0  \mleq{}  n
5.  i  :  \mBbbZ{}
6.  0  \mleq{}  i
7.  i  <  n
8.  0  \mleq{}  |a  \muparrow{}  i|
9.  0  \mleq{}  |b  \muparrow{}  n  -  i  +  1|
10.  0  \mleq{}  qmax(|a|;|b|)
11.  0  \mleq{}  qmax(|a|;|b|)  \muparrow{}  i
12.  |a  \muparrow{}  i|  \mleq{}  qmax(|a|;|b|)  \muparrow{}  i
\mvdash{}  (|a  \muparrow{}  i|  *  |b  \muparrow{}  n  -  i  +  1|)  \mleq{}  (|a  \muparrow{}  i|  *  qmax(|a|;|b|)  \muparrow{}  n  -  i  +  1)
By
Latex:
(BLemma  `qmul\_preserves\_qle2`  THEN  Auto)
Home
Index