---

Step * of Lemma qmul_wf

No Annotations
∀[r,s:ℚ].  (r * s ∈ ℚ)
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (RationalD 1)
   THEN EqTypeCD
   THEN Auto
   THEN Try ((Unfold `member` 0
              THEN All Thin
              THEN All D_rational_form
              THEN Unfold `qmul` 0
              THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
              THEN Reduce 0
              THEN Auto))
   THEN Unfold `qmul` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (All D_rational_form THENW Auto)
   THEN (All (Unfolds ``qeq``))⋅
   THEN RepeatFor 2 (((All CallByValueReduce⋅ THENA Auto) THEN (All Reduce THENA Auto))⋅)
   THEN ((All (RW (SweepDnC isint_int_conv))) THENA Auto)
   THEN All Reduce
   THEN ((All (RWO "eqtt_to_assert")) THENA Auto)
   THEN ((All (RW assert_pushdownC)) THENA Auto)
   THEN (∀h:hyp. HypSubst' h 0  THENA Auto)
   THEN (RW IntNormC 0 THENA Auto)
   THEN (∀h:hyp. RevHypSubst' h 0  THENA Auto)
   THEN (RW IntNormC 0 THENA Auto)
   THEN Try ((Fold `member` 0 THEN Auto))
   THEN ∀h:hyp. ((RW IntNormC h THENA Auto) THEN HypSubst' h 0) 
   THEN (RW IntNormC 0 THENA Auto)
   THEN Try ((Fold `member` 0 THEN Auto))) }

1
1. a8 : ℤ
2. a7 : ℤ
3. a8 = a7 ∈ ℤ
4. a5 : ℤ
5. a6 : ℤ-o
6. a2 : ℤ
7. a3 : ℤ-o
8. (a3 * a5) = (a2 * a6) ∈ ℤ
⊢ (a3 * a5 * a7) = (a2 * a6 * a7) ∈ ℤ

2
1. a9 : ℤ
2. a10 : ℤ-o
3. a7 : ℤ
4. a9 = (a10 * a7) ∈ ℤ
5. a5 : ℤ
6. a6 : ℤ-o
7. a2 : ℤ
8. a3 : ℤ-o
9. (a3 * a5) = (a2 * a6) ∈ ℤ
⊢ (a10 * a3 * a5 * a7) = (a10 * a2 * a6 * a7) ∈ ℤ

3
1. a10 : ℤ
2. a8 : ℤ
3. a9 : ℤ-o
4. (a10 * a9) = a8 ∈ ℤ
5. a5 : ℤ
6. a6 : ℤ-o
7. a2 : ℤ
8. a3 : ℤ-o
9. (a3 * a5) = (a2 * a6) ∈ ℤ
⊢ (a10 * a3 * a5 * a9) = (a10 * a2 * a6 * a9) ∈ ℤ

4
1. a11 : ℤ
2. a12 : ℤ-o
3. a8 : ℤ
4. a9 : ℤ-o
5. (a11 * a9) = (a12 * a8) ∈ ℤ
6. a5 : ℤ
7. a6 : ℤ-o
8. a2 : ℤ
9. a3 : ℤ-o
10. (a3 * a5) = (a2 * a6) ∈ ℤ
⊢ (a11 * a3 * a5 * a9) = (a12 * a2 * a6 * a8) ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r,s:\mBbbQ{}].    (r  *  s  \mmember{}  \mBbbQ{})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (RationalD  1)
  THEN  EqTypeCD
  THEN  Auto
  THEN  Try  ((Unfold  `member`  0
                        THEN  All  Thin
                        THEN  All  D\_rational\_form
                        THEN  Unfold  `qmul`  0
                        THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
                        THEN  Reduce  0
                        THEN  Auto))
  THEN  Unfold  `qmul`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (All  D\_rational\_form  THENW  Auto)
  THEN  (All  (Unfolds  ``qeq``))\mcdot{}
  THEN  RepeatFor  2  (((All  CallByValueReduce\mcdot{}  THENA  Auto)  THEN  (All  Reduce  THENA  Auto))\mcdot{})
  THEN  ((All  (RW  (SweepDnC  isint\_int\_conv)))  THENA  Auto)
  THEN  All  Reduce
  THEN  ((All  (RWO  "eqtt\_to\_assert"))  THENA  Auto)
  THEN  ((All  (RW  assert\_pushdownC))  THENA  Auto)
  THEN  (\mforall{}h:hyp.  HypSubst'  h  0    THENA  Auto)
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  (\mforall{}h:hyp.  RevHypSubst'  h  0    THENA  Auto)
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  Try  ((Fold  `member`  0  THEN  Auto))
  THEN  \mforall{}h:hyp.  ((RW  IntNormC  h  THENA  Auto)  THEN  HypSubst'  h  0) 
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  Try  ((Fold  `member`  0  THEN  Auto)))

---

Home Index