---

Step * of Lemma rdiv_functionality

No Annotations
∀[x1,x2,y1,y2:ℝ].  ((x1/y1) = (x2/y2)) supposing ((y1 = y2) and (x1 = x2) and y1 ≠ r0)
BY
{ UniformUnivCD Auto }

1
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. y1 ≠ r0
6. x1 = x2
7. y1 = y2
⊢ (x1/y1) = (x2/y2)

2
.....wf..... 
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. y1 ≠ r0
6. x1 = x2
7. y1 = y2
8. (x1/y1) = (x2/y2)
⊢ (x1/y1) ∈ ℝ

3
.....wf..... 
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. y1 ≠ r0
6. x1 = x2
7. y1 = y2
8. (x1/y1) = (x2/y2)
⊢ (x2/y2) ∈ ℝ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x1,x2,y1,y2:\mBbbR{}].    ((x1/y1)  =  (x2/y2))  supposing  ((y1  =  y2)  and  (x1  =  x2)  and  y1  \mneq{}  r0)


By

---

Latex:
UniformUnivCD  Auto

---

Home Index