Step
*
1
1
1
2
of Lemma
hyptrans_lemma
1. rv : InnerProductSpace
2. e : Point
3. h : Point
4. e^2 = r1
5. h ⋅ e = r0
6. tau : ℝ
7. t : ℝ
8. e ⋅ h = r0
9. h + sinh(tau) * rsqrt(r1 + h^2)*e^2 = (h^2 + (sinh(tau)^2 * (r1 + h^2)))
10. (r1 + h^2 + (sinh(tau)^2 * (r1 + h^2))) = (cosh(tau)^2 * (r1 + h^2))
11. r0 ≤ (r1 + h^2)
12. r0 ≤ (r1 + h + sinh(tau) * rsqrt(r1 + h^2)*e^2)
⊢ ((cosh(tau) * rsqrt(r1 + h^2)) * cosh(tau) * rsqrt(r1 + h^2)) = (r1 + h + sinh(tau) * rsqrt(r1 + h^2)*e^2)
BY
{ ((RWW "-4 -3" 0 THEN Auto) THEN nRNorm 0 THEN (RWO "rsqrt_squared" 0 THENA Auto) THEN RWO "rnexp2" 0 THEN Auto) }
Latex:
Latex:
1. rv : InnerProductSpace
2. e : Point
3. h : Point
4. e\^{}2 = r1
5. h \mcdot{} e = r0
6. tau : \mBbbR{}
7. t : \mBbbR{}
8. e \mcdot{} h = r0
9. h + sinh(tau) * rsqrt(r1 + h\^{}2)*e\^{}2 = (h\^{}2 + (sinh(tau)\^{}2 * (r1 + h\^{}2)))
10. (r1 + h\^{}2 + (sinh(tau)\^{}2 * (r1 + h\^{}2))) = (cosh(tau)\^{}2 * (r1 + h\^{}2))
11. r0 \mleq{} (r1 + h\^{}2)
12. r0 \mleq{} (r1 + h + sinh(tau) * rsqrt(r1 + h\^{}2)*e\^{}2)
\mvdash{} ((cosh(tau) * rsqrt(r1 + h\^{}2)) * cosh(tau) * rsqrt(r1 + h\^{}2))
= (r1 + h + sinh(tau) * rsqrt(r1 + h\^{}2)*e\^{}2)
By
Latex:
((RWW "-4 -3" 0 THEN Auto)
THEN nRNorm 0
THEN (RWO "rsqrt\_squared" 0 THENA Auto)
THEN RWO "rnexp2" 0
THEN Auto)
Home
Index