---

Step * 1 1 1 2 of Lemma qexp-difference-bound


1. a : ℚ
2. b : ℚ
3. n : ℕ+
4. 0 ≤ n
5. i : ℤ
6. 0 ≤ i
7. i < n
⊢ (|a ↑ i| * |b ↑ n - i + 1|) ≤ (qmax(|a|;|b|) ↑ i * qmax(|a|;|b|) ↑ n - i + 1)
BY
{ ((Assert (0 ≤ |a ↑ i|) ∧ (0 ≤ |b ↑ n - i + 1|) BY
          (Auto THEN BLemma `qabs-nonneg` THEN Auto))
   THEN (Assert 0 ≤ qmax(|a|;|b|) BY
               ((BLemma `qmax_ub` THEN Auto)⋅ THEN (OrLeft THENA Auto) THEN BLemma `qabs-nonneg` THEN Auto))
   THEN (Assert 0 ≤ qmax(|a|;|b|) ↑ i BY
               (BLemma `qexp-nonneg` THEN Auto))) }

1
1. a : ℚ
2. b : ℚ
3. n : ℕ+
4. 0 ≤ n
5. i : ℤ
6. 0 ≤ i
7. i < n
8. (0 ≤ |a ↑ i|) ∧ (0 ≤ |b ↑ n - i + 1|)
9. 0 ≤ qmax(|a|;|b|)
10. 0 ≤ qmax(|a|;|b|) ↑ i
⊢ (|a ↑ i| * |b ↑ n - i + 1|) ≤ (qmax(|a|;|b|) ↑ i * 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
\mvdash{}  (|a  \muparrow{}  i|  *  |b  \muparrow{}  n  -  i  +  1|)  \mleq{}  (qmax(|a|;|b|)  \muparrow{}  i  *  qmax(|a|;|b|)  \muparrow{}  n  -  i  +  1)


By

---

Latex:
((Assert  (0  \mleq{}  |a  \muparrow{}  i|)  \mwedge{}  (0  \mleq{}  |b  \muparrow{}  n  -  i  +  1|)  BY
                (Auto  THEN  BLemma  `qabs-nonneg`  THEN  Auto))
  THEN  (Assert  0  \mleq{}  qmax(|a|;|b|)  BY
                          ((BLemma  `qmax\_ub`  THEN  Auto)\mcdot{}
                            THEN  (OrLeft  THENA  Auto)
                            THEN  BLemma  `qabs-nonneg`
                            THEN  Auto))
  THEN  (Assert  0  \mleq{}  qmax(|a|;|b|)  \muparrow{}  i  BY
                          (BLemma  `qexp-nonneg`  THEN  Auto)))

---

Home Index