---

Step * of Lemma real-ring_wf

real-ring() ∈ CRng
BY
{ ((Assert λx,y. (x + y) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) BY
          (RepeatFor 2 (((MemCD THENA Auto) THEN D -1))
           THEN (EqTypeCD THEN Auto)
           THEN BLemma `radd_functionality`
           THEN Auto))
   THEN (Assert λx,y. (x * y) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) BY
               (RepeatFor 2 (((MemCD THENA Auto) THEN D -1))
                THEN (EqTypeCD THEN Auto)
                THEN BLemma `rmul_functionality`
                THEN Auto))
   THEN (Assert λx.-(x) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) BY
               (((MemCD THENA Auto) THEN D -1)
                THEN (EqTypeCD THEN Auto)
                THEN BLemma `rminus_functionality`
                THEN Auto))) }

1
1. λx,y. (x + y) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y))
2. λx,y. (x * y) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y))
3. λx.-(x) ∈ (x,y:ℝ//(x = y)) ⟶ (x,y:ℝ//(x = y))
⊢ real-ring() ∈ CRng

---

Latex:

---

Latex:
real-ring()  \mmember{}  CRng


By

---

Latex:
((Assert  \mlambda{}x,y.  (x  +  y)  \mmember{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  BY
                (RepeatFor  2  (((MemCD  THENA  Auto)  THEN  D  -1))
                  THEN  (EqTypeCD  THEN  Auto)
                  THEN  BLemma  `radd\_functionality`
                  THEN  Auto))
  THEN  (Assert  \mlambda{}x,y.  (x  *  y)  \mmember{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  BY
                          (RepeatFor  2  (((MemCD  THENA  Auto)  THEN  D  -1))
                            THEN  (EqTypeCD  THEN  Auto)
                            THEN  BLemma  `rmul\_functionality`
                            THEN  Auto))
  THEN  (Assert  \mlambda{}x.-(x)  \mmember{}  (x,y:\mBbbR{}//(x  =  y))  {}\mrightarrow{}  (x,y:\mBbbR{}//(x  =  y))  BY
                          (((MemCD  THENA  Auto)  THEN  D  -1)
                            THEN  (EqTypeCD  THEN  Auto)
                            THEN  BLemma  `rminus\_functionality`
                            THEN  Auto)))

---

Home Index