Step * 1 1 1 of Lemma reciprocal-qle-proof


1. : ℚ
2. 0 < e
3. : ℤ
4. : ℤ
5. 0 < q
6. ¬(q 0 ∈ ℚ)
7. (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. 0 < (p/q)
⊢ 0 < p
BY
(QMul ⌜q⌝ (-1)⋅ THEN Auto) }

1
1. : ℚ
2. 0 < e
3. : ℤ
4. : ℤ
5. 0 < q
6. ¬(q 0 ∈ ℚ)
7. (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. 0 < p
⊢ 0 < p


Latex:


Latex:

1.  e  :  \mBbbQ{}
2.  0  <  e
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  e  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  0  <  (p/q)
\mvdash{}  0  <  p


By


Latex:
(QMul  \mkleeneopen{}q\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)




Home Index