---

Step * of Lemma qpositive_wf

∀[r:ℚ]. (qpositive(r) ∈ 𝔹)
BY
{ xxx(Auto
      THEN D -1
      THEN Auto
      THEN MoveToConcl (-1)
      THEN GenConclTerms Auto [⌜r⌝;⌜r1⌝]⋅
      THEN All Thin
      THEN (D 0 THENA Auto)
      THEN All D_rational_form
      THEN MoveToConcl (-1)
      THEN RepUR ``qeq qpositive`` 0
      THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
      THEN (Reduce 0 THENA Auto)
      THEN (D 0 THENA Auto)
      THEN ((RWO "eqtt_to_assert" (-1) THENM RW assert_pushdownC (-1)) THENA Auto)
      THEN Try ((EqCD THEN CompleteAuto))
      THEN (BLemma `iff_imp_equal_bool`⋅ THENA Auto)
      THEN RW assert_pushdownC 0
      THEN Auto)xxx }

1
1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
4. a3 = (a1 * a4) ∈ ℤ
5. (0 < a3 ∧ 0 < a4) ∨ (a3 < 0 ∧ a4 < 0)
⊢ 0 < a1

2
1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
4. a3 = (a1 * a4) ∈ ℤ
5. 0 < a1
⊢ (0 < a3 ∧ 0 < a4) ∨ (a3 < 0 ∧ a4 < 0)

3
1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
4. (a4 * a3) = a2 ∈ ℤ
5. 0 < a4
⊢ (0 < a2 ∧ 0 < a3) ∨ (a2 < 0 ∧ a3 < 0)

4
1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
4. (a4 * a3) = a2 ∈ ℤ
5. (0 < a2 ∧ 0 < a3) ∨ (a2 < 0 ∧ a3 < 0)
⊢ 0 < a4

5
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. (0 < a5 ∧ 0 < a6) ∨ (a5 < 0 ∧ a6 < 0)
⊢ (0 < a2 ∧ 0 < a3) ∨ (a2 < 0 ∧ a3 < 0)

6
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. (a5 * a3) = (a2 * a6) ∈ ℤ
6. (0 < a2 ∧ 0 < a3) ∨ (a2 < 0 ∧ a3 < 0)
⊢ (0 < a5 ∧ 0 < a6) ∨ (a5 < 0 ∧ a6 < 0)

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  (qpositive(r)  \mmember{}  \mBbbB{})


By

---

Latex:
xxx(Auto
        THEN  D  -1
        THEN  Auto
        THEN  MoveToConcl  (-1)
        THEN  GenConclTerms  Auto  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}
        THEN  All  Thin
        THEN  (D  0  THENA  Auto)
        THEN  All  D\_rational\_form
        THEN  MoveToConcl  (-1)
        THEN  RepUR  ``qeq  qpositive``  0
        THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
        THEN  (Reduce  0  THENA  Auto)
        THEN  (D  0  THENA  Auto)
        THEN  ((RWO  "eqtt\_to\_assert"  (-1)  THENM  RW  assert\_pushdownC  (-1))  THENA  Auto)
        THEN  Try  ((EqCD  THEN  CompleteAuto))
        THEN  (BLemma  `iff\_imp\_equal\_bool`\mcdot{}  THENA  Auto)
        THEN  RW  assert\_pushdownC  0
        THEN  Auto)xxx

---

Home Index