---

Step * of Lemma mk-rational_wf

∀[a:ℤ]. ∀[b:ℤ-o].  (mk-rational(a;b) ∈ ℚ)
BY
{ (Auto THEN MemTypeCDRational THEN Auto THEN RepUR ``mk-rational qeq`` 0) }

1
1. a : ℤ
2. b : ℤ-o
⊢ <a, b> ∈ ℤ ⋃ (ℤ × ℤ-o)

2
1. a : ℤ
2. b : ℤ-o
⊢ let r' ⟵ <a, b>
  in let s' ⟵ <a, b>
     in if isint(r')
     then if isint(s') then (r' =z s') else let i,j = s' in (r' * j =z i) fi 
     else let p,q = r' 
          in if isint(s') then (p =z s' * q) else let i,j = s' in (p * j =z i * q) fi 
     fi  
= tt

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (mk-rational(a;b)  \mmember{}  \mBbbQ{})


By

---

Latex:
(Auto  THEN  MemTypeCDRational  THEN  Auto  THEN  RepUR  ``mk-rational  qeq``  0)

---

Home Index