Step * 1 1 1 1 2 1 1 1 of Lemma sine-exists


1. : ℝ
2. : ℕ@i
3. : ℝ@i
4. v1 : ℝ@i
5. r0 < v1
6. r0 < v
7. (x x) ≤ (v1/v)
8. v ≠ r0
9. v1 ≠ r0
⊢ (x^2 (i 1)/v1) ≤ (x^2 i/v)
BY
(nRMul ⌜v⌝ (-3)⋅ THEN (nRMul ⌜v⌝ 0⋅ THEN nRMul ⌜v1⌝ 0⋅)⋅)⋅ }

1
1. : ℝ
2. : ℕ@i
3. : ℝ@i
4. v1 : ℝ@i
5. r0 < v1
6. r0 < v
7. (v x) ≤ v1
8. v ≠ r0
9. v1 ≠ r0
⊢ (x^2 (i 1) v) ≤ (x^2 v1)


Latex:


Latex:

1.  x  :  \mBbbR{}
2.  i  :  \mBbbN{}@i
3.  v  :  \mBbbR{}@i
4.  v1  :  \mBbbR{}@i
5.  r0  <  v1
6.  r0  <  v
7.  (x  *  x)  \mleq{}  (v1/v)
8.  v  \mneq{}  r0
9.  v1  \mneq{}  r0
\mvdash{}  (x\^{}2  *  (i  +  1)/v1)  \mleq{}  (x\^{}2  *  i/v)


By


Latex:
(nRMul  \mkleeneopen{}v\mkleeneclose{}  (-3)\mcdot{}  THEN  (nRMul  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{})\mcdot{})\mcdot{}




Home Index