Step * 1 4 1 1 1 of Lemma Legendre-differential-equation

.....assertion..... 
1. : ℕ
2. λx.r0 ∈ (-∞, ∞) ⟶ℝ
3. λx.r1 ∈ (-∞, ∞) ⟶ℝ
4. ¬(n 0 ∈ ℤ)
5. ¬(n 1 ∈ ℤ)
6. f1 (-∞, ∞) ⟶ℝ
7. g1 (-∞, ∞) ⟶ℝ
8. (-∞, ∞) ⟶ℝ
9. (-∞, ∞) ⟶ℝ
10. : ℝ
11. : ℝ
12. Legendre(n 1;x) v ∈ ℝ
13. v1 : ℝ
14. Legendre(n 2;x) v1 ∈ ℝ
15. v2 : ℝ
16. (f x) v2 ∈ ℝ
17. v3 : ℝ
18. (g x) v3 ∈ ℝ
19. v4 : ℝ
20. (f1 x) v4 ∈ ℝ
21. v5 : ℝ
22. (g1 x) v5 ∈ ℝ
23. {2...}
24. m ∈ {2...}
25. : ℝ
26. (r1 x) y ∈ ℝ
27. (((y v4) (r(2) x) v5) (r((m 2) (m 1)) v1)) r0
28. (((y v2) (r(2) x) v3) (r((m 1) m) v)) r0
29. (y v3) ((r(m 1) v1) (r(m 1) x) v)
⊢ (((y ((2 m) ((x v2) v3) v3 v4)) (r(2) x) ((2 m) (x v3) v5))
(r(m (m 1)) ((2 m) v1)))
r0
BY
((RWO "int-rmul-req" THENA Auto)
   THEN (RWW  "rmul-int< rsub-int<(-3) THENA Auto)
   THEN (RWW  "rmul-int< rsub-int<(-2) THENA Auto)
   THEN (RWW  "rmul-int< rsub-int<(-1) THENA Auto)
   THEN (RWW  "rmul-int< rsub-int< radd-int<THENA Auto)
   THEN RepeatFor (MoveToConcl (-1))
   THEN (GenConcl ⌜r(m) N ∈ ℝ⌝⋅ THENA Auto)
   THEN RepeatFor ((D THENA Auto))) }

1
1. : ℕ
2. λx.r0 ∈ (-∞, ∞) ⟶ℝ
3. λx.r1 ∈ (-∞, ∞) ⟶ℝ
4. ¬(n 0 ∈ ℤ)
5. ¬(n 1 ∈ ℤ)
6. f1 (-∞, ∞) ⟶ℝ
7. g1 (-∞, ∞) ⟶ℝ
8. (-∞, ∞) ⟶ℝ
9. (-∞, ∞) ⟶ℝ
10. : ℝ
11. : ℝ
12. Legendre(n 1;x) v ∈ ℝ
13. v1 : ℝ
14. Legendre(n 2;x) v1 ∈ ℝ
15. v2 : ℝ
16. (f x) v2 ∈ ℝ
17. v3 : ℝ
18. (g x) v3 ∈ ℝ
19. v4 : ℝ
20. (f1 x) v4 ∈ ℝ
21. v5 : ℝ
22. (g1 x) v5 ∈ ℝ
23. {2...}
24. m ∈ {2...}
25. : ℝ
26. (r1 x) y ∈ ℝ
27. : ℝ
28. r(m) N ∈ ℝ
29. (((y v4) (r(2) x) v5) (((N r(2)) (N r1)) v1)) r0
30. (((y v2) (r(2) x) v3) (((N r1) N) v)) r0
31. (y v3) (((N r1) v1) ((N r1) x) v)
⊢ (((y ((((r(2) N) r1) (((x v2) v3) v3)) (N r1) v4)) (r(2) x)
((((r(2) N) r1) ((x v3) v)) (N r1) v5))
((N (N r1)) ((((r(2) N) r1) v) (N r1) v1)))
r0


Latex:


Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  \mlambda{}x.r0  \mmember{}  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
3.  \mlambda{}x.r1  \mmember{}  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
4.  \mneg{}(n  =  0)
5.  \mneg{}(n  =  1)
6.  f1  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
7.  g1  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
8.  f  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
9.  g  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
10.  x  :  \mBbbR{}
11.  v  :  \mBbbR{}
12.  Legendre(n  -  1;x)  =  v
13.  v1  :  \mBbbR{}
14.  Legendre(n  -  2;x)  =  v1
15.  v2  :  \mBbbR{}
16.  (f  x)  =  v2
17.  v3  :  \mBbbR{}
18.  (g  x)  =  v3
19.  v4  :  \mBbbR{}
20.  (f1  x)  =  v4
21.  v5  :  \mBbbR{}
22.  (g1  x)  =  v5
23.  m  :  \{2...\}
24.  n  =  m
25.  y  :  \mBbbR{}
26.  (r1  -  x  *  x)  =  y
27.  (((y  *  v4)  -  (r(2)  *  x)  *  v5)  +  (r((m  -  2)  *  (m  -  1))  *  v1))  =  r0
28.  (((y  *  v2)  -  (r(2)  *  x)  *  v3)  +  (r((m  -  1)  *  m)  *  v))  =  r0
29.  (y  *  v3)  =  ((r(m  -  1)  *  v1)  -  (r(m  -  1)  *  x)  *  v)
\mvdash{}  (((y  *  ((2  *  m)  -  1  *  ((x  *  v2)  +  v3)  +  v3  -  m  -  1  *  v4))  -  (r(2)  *  x)
*  ((2  *  m)  -  1  *  (x  *  v3)  +  v  -  m  -  1  *  v5))
+  (r(m  *  (m  +  1))  *  ((2  *  m)  -  1  *  x  *  v  -  m  -  1  *  v1)))
=  r0


By


Latex:
((RWO  "int-rmul-req"  0  THENA  Auto)
  THEN  (RWW    "rmul-int<  rsub-int<"  (-3)  THENA  Auto)
  THEN  (RWW    "rmul-int<  rsub-int<"  (-2)  THENA  Auto)
  THEN  (RWW    "rmul-int<  rsub-int<"  (-1)  THENA  Auto)
  THEN  (RWW    "rmul-int<  rsub-int<  radd-int<"  0  THENA  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}r(m)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  ((D  0  THENA  Auto)))




Home Index