Step
*
1
1
2
1
of Lemma
rsin-positive-near-11/7
1. x : {x:ℝ| x ∈ ((r(41)/r(70)), (r(179)/r(70)))}
2. |rsin(x) - rsin((r(110)/r(70)))| ≤ (r(69)/r(70))
⊢ r0 < rsin(x)
BY
{ ((RWO "rabs-difference-bound-rleq" (-1) THENA Auto) THEN D -1) }
1
1. x : {x:ℝ| x ∈ ((r(41)/r(70)), (r(179)/r(70)))}
2. (rsin((r(110)/r(70))) - (r(69)/r(70))) ≤ rsin(x)
3. rsin(x) ≤ (rsin((r(110)/r(70))) + (r(69)/r(70)))
⊢ r0 < rsin(x)
Latex:
Latex:
1. x : \{x:\mBbbR{}| x \mmember{} ((r(41)/r(70)), (r(179)/r(70)))\}
2. |rsin(x) - rsin((r(110)/r(70)))| \mleq{} (r(69)/r(70))
\mvdash{} r0 < rsin(x)
By
Latex:
((RWO "rabs-difference-bound-rleq" (-1) THENA Auto) THEN D -1)
Home
Index