Step
*
1
of Lemma
rdiv_functionality
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. y1 ≠ r0
6. x1 = x2
7. y1 = y2
⊢ (x1/y1) = (x2/y2)
BY
{ TACTIC:((Assert y2 ≠ r0 BY
(∀h:hyp. (RWOL [RevHypC h] 0) THEN Auto))
THEN Unfold `rdiv` 0
THEN ∀h:hyp. SubstReal h 0
THEN Auto) }
Latex:
Latex:
1. x1 : \mBbbR{}
2. x2 : \mBbbR{}
3. y1 : \mBbbR{}
4. y2 : \mBbbR{}
5. y1 \mneq{} r0
6. x1 = x2
7. y1 = y2
\mvdash{} (x1/y1) = (x2/y2)
By
Latex:
TACTIC:((Assert y2 \mneq{} r0 BY
(\mforall{}h:hyp. (RWOL [RevHypC h] 0) THEN Auto))
THEN Unfold `rdiv` 0
THEN \mforall{}h:hyp. SubstReal h 0
THEN Auto)
Home
Index