Step * 2 1 of Lemma qabs-difference-qmax


1. ∀a,b,c,d:ℚ.  ((b ≤ a)  (c ≤ a)  (d ≤ a)  (|qmax(a;b) qmax(c;d)| ≤ qmax(|a c|;|b d|)))
2. : ℚ
3. : ℚ
4. : ℚ
5. : ℚ
6. qmax(c;d) ≤ qmax(a;b)
⊢ |qmax(a;b) qmax(c;d)| ≤ qmax(|a c|;|b d|)
BY
xxx(Decide b ≤ THENA Auto)xxx }

1
1. ∀a,b,c,d:ℚ.  ((b ≤ a)  (c ≤ a)  (d ≤ a)  (|qmax(a;b) qmax(c;d)| ≤ qmax(|a c|;|b d|)))
2. : ℚ
3. : ℚ
4. : ℚ
5. : ℚ
6. qmax(c;d) ≤ qmax(a;b)
7. b ≤ a
⊢ |qmax(a;b) qmax(c;d)| ≤ qmax(|a c|;|b d|)

2
1. ∀a,b,c,d:ℚ.  ((b ≤ a)  (c ≤ a)  (d ≤ a)  (|qmax(a;b) qmax(c;d)| ≤ qmax(|a c|;|b d|)))
2. : ℚ
3. : ℚ
4. : ℚ
5. : ℚ
6. qmax(c;d) ≤ qmax(a;b)
7. ¬(b ≤ a)
⊢ |qmax(a;b) qmax(c;d)| ≤ qmax(|a c|;|b d|)


Latex:


Latex:

1.  \mforall{}a,b,c,d:\mBbbQ{}.    ((b  \mleq{}  a)  {}\mRightarrow{}  (c  \mleq{}  a)  {}\mRightarrow{}  (d  \mleq{}  a)  {}\mRightarrow{}  (|qmax(a;b)  -  qmax(c;d)|  \mleq{}  qmax(|a  -  c|;|b  -  d|)))
2.  a  :  \mBbbQ{}
3.  b  :  \mBbbQ{}
4.  c  :  \mBbbQ{}
5.  d  :  \mBbbQ{}
6.  qmax(c;d)  \mleq{}  qmax(a;b)
\mvdash{}  |qmax(a;b)  -  qmax(c;d)|  \mleq{}  qmax(|a  -  c|;|b  -  d|)


By


Latex:
xxx(Decide  b  \mleq{}  a  THENA  Auto)xxx




Home Index