Step | Hyp | Ref
| Expression |
1 | | nnuz 12811 |
. . . 4
β’ β =
(β€β₯β1) |
2 | | 1zzd 12539 |
. . . 4
β’ (β€
β 1 β β€) |
3 | | wallispi.1 |
. . . . . . . 8
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2
Β· π) / ((2 Β·
π) + 1)))) |
4 | | eqid 2733 |
. . . . . . . 8
β’ (π β β0
β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) = (π β β0 β¦
β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) |
5 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ (((π β β0
β¦ β«(0(,)Ο)((sinβπ₯)βπ) dπ₯)β(2 Β· π)) / ((π β β0 β¦
β«(0(,)Ο)((sinβπ₯)βπ) dπ₯)β((2 Β· π) + 1)))) = (π β β β¦ (((π β β0 β¦
β«(0(,)Ο)((sinβπ₯)βπ) dπ₯)β(2 Β· π)) / ((π β β0 β¦
β«(0(,)Ο)((sinβπ₯)βπ) dπ₯)β((2 Β· π) + 1)))) |
6 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ)))) = (π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ)))) |
7 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ (((2
Β· π) + 1) / (2
Β· π))) = (π β β β¦ (((2
Β· π) + 1) / (2
Β· π))) |
8 | 3, 4, 5, 6, 7 | wallispilem5 44396 |
. . . . . . 7
β’ (π β β β¦ ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ)))) β 1 |
9 | 8 | a1i 11 |
. . . . . 6
β’ (β€
β (π β β
β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ)))) β 1) |
10 | | 2cnd 12236 |
. . . . . . 7
β’ (β€
β 2 β β) |
11 | | picn 25832 |
. . . . . . . 8
β’ Ο
β β |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (β€
β Ο β β) |
13 | | pire 25831 |
. . . . . . . . 9
β’ Ο
β β |
14 | | pipos 25833 |
. . . . . . . . 9
β’ 0 <
Ο |
15 | 13, 14 | gt0ne0ii 11696 |
. . . . . . . 8
β’ Ο β
0 |
16 | 15 | a1i 11 |
. . . . . . 7
β’ (β€
β Ο β 0) |
17 | 10, 12, 16 | divcld 11936 |
. . . . . 6
β’ (β€
β (2 / Ο) β β) |
18 | | nnex 12164 |
. . . . . . . 8
β’ β
β V |
19 | 18 | mptex 7174 |
. . . . . . 7
β’ (π β β β¦ (1 /
(seq1( Β· , πΉ)βπ))) β V |
20 | 19 | a1i 11 |
. . . . . 6
β’ (β€
β (π β β
β¦ (1 / (seq1( Β· , πΉ)βπ))) β V) |
21 | 11 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β Ο
β β) |
22 | 21 | halfcld 12403 |
. . . . . . . . . 10
β’ (π β β β (Ο /
2) β β) |
23 | | elnnuz 12812 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
(β€β₯β1)) |
24 | 23 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β1)) |
25 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (2 Β· π) = (2 Β· π)) |
26 | 25 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((2 Β· π) β 1) = ((2 Β· π) β 1)) |
27 | 25, 26 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((2 Β· π) / ((2 Β· π) β 1)) = ((2 Β· π) / ((2 Β· π) β 1))) |
28 | 25 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
29 | 25, 28 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((2 Β· π) / ((2 Β· π) + 1)) = ((2 Β· π) / ((2 Β· π) + 1))) |
30 | 27, 29 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1))) = (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2
Β· π) / ((2 Β·
π) + 1)))) |
31 | | elfznn 13476 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β π β β) |
32 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β 2 β
β) |
33 | | nncn 12166 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β) |
34 | 32, 33 | mulcld 11180 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (2
Β· π) β
β) |
35 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β 1 β
β) |
36 | 34, 35 | subcld 11517 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((2
Β· π) β 1)
β β) |
37 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β 1 β
β) |
38 | | 1t1e1 12320 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1
Β· 1) = 1 |
39 | 37, 37 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (1
Β· 1) β β) |
40 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 2 β
β |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 2 β
β) |
42 | 41, 37 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (2
Β· 1) β β) |
43 | | nnre 12165 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β π β
β) |
44 | 41, 43 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (2
Β· π) β
β) |
45 | | 1rp 12924 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 β
β+ |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 1 β
β+) |
47 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 <
2 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 1 <
2) |
49 | 37, 41, 46, 48 | ltmul1dd 13017 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (1
Β· 1) < (2 Β· 1)) |
50 | | 0le2 12260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β€
2 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 0 β€
2) |
52 | | nnge1 12186 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 1 β€
π) |
53 | 37, 43, 41, 51, 52 | lemul2ad 12100 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (2
Β· 1) β€ (2 Β· π)) |
54 | 39, 42, 44, 49, 53 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β (1
Β· 1) < (2 Β· π)) |
55 | 38, 54 | eqbrtrrid 5142 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β 1 < (2
Β· π)) |
56 | 37, 55 | gtned 11295 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (2
Β· π) β
1) |
57 | 34, 35, 56 | subne0d 11526 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((2
Β· π) β 1) β
0) |
58 | 34, 36, 57 | divcld 11936 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((2
Β· π) / ((2 Β·
π) β 1)) β
β) |
59 | 34, 35 | addcld 11179 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((2
Β· π) + 1) β
β) |
60 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β 0 β
β) |
61 | 44, 37 | readdcld 11189 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β ((2
Β· π) + 1) β
β) |
62 | 46 | rpgt0d 12965 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β 0 <
1) |
63 | | 2rp 12925 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 β
β+ |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β 2 β
β+) |
65 | | nnrp 12931 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β π β
β+) |
66 | 64, 65 | rpmulcld 12978 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β (2
Β· π) β
β+) |
67 | 37, 66 | ltaddrp2d 12996 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β 1 <
((2 Β· π) +
1)) |
68 | 60, 37, 61, 62, 67 | lttrd 11321 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β 0 <
((2 Β· π) +
1)) |
69 | 60, 68 | gtned 11295 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((2
Β· π) + 1) β
0) |
70 | 34, 59, 69 | divcld 11936 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((2
Β· π) / ((2 Β·
π) + 1)) β
β) |
71 | 58, 70 | mulcld 11180 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (((2
Β· π) / ((2 Β·
π) β 1)) Β· ((2
Β· π) / ((2 Β·
π) + 1))) β
β) |
72 | 31, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1))) β
β) |
73 | 3, 30, 31, 72 | fvmptd3 6972 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β (πΉβπ) = (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1)))) |
74 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β 2 β
β+) |
75 | 31 | nnrpd 12960 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β π β β+) |
76 | 74, 75 | rpmulcld 12978 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β (2 Β· π) β
β+) |
77 | 44, 37 | resubcld 11588 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((2
Β· π) β 1)
β β) |
78 | | 1m1e0 12230 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1
β 1) = 0 |
79 | 37, 44, 37, 55 | ltsub1dd 11772 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (1
β 1) < ((2 Β· π) β 1)) |
80 | 78, 79 | eqbrtrrid 5142 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β 0 <
((2 Β· π) β
1)) |
81 | 77, 80 | elrpd 12959 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((2
Β· π) β 1)
β β+) |
82 | 31, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β ((2 Β· π) β 1) β
β+) |
83 | 76, 82 | rpdivcld 12979 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β ((2 Β· π) / ((2 Β· π) β 1)) β
β+) |
84 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β 2 β β) |
85 | 31 | nnred 12173 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β π β β) |
86 | 84, 85 | remulcld 11190 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (2 Β· π) β β) |
87 | 74 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β 0 β€ 2) |
88 | 75 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β 0 β€ π) |
89 | 84, 85, 87, 88 | mulge0d 11737 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β 0 β€ (2 Β· π)) |
90 | 86, 89 | ge0p1rpd 12992 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β ((2 Β· π) + 1) β
β+) |
91 | 76, 90 | rpdivcld 12979 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β ((2 Β· π) / ((2 Β· π) + 1)) β
β+) |
92 | 83, 91 | rpmulcld 12978 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1))) β
β+) |
93 | 73, 92 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (πΉβπ) β
β+) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β (πΉβπ) β
β+) |
95 | | rpmulcl 12943 |
. . . . . . . . . . . . . 14
β’ ((π β β+
β§ π€ β
β+) β (π Β· π€) β
β+) |
96 | 95 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β β+
β§ π€ β
β+)) β (π Β· π€) β
β+) |
97 | 24, 94, 96 | seqcl 13934 |
. . . . . . . . . . . 12
β’ (π β β β (seq1(
Β· , πΉ)βπ) β
β+) |
98 | 97 | rpcnd 12964 |
. . . . . . . . . . 11
β’ (π β β β (seq1(
Β· , πΉ)βπ) β
β) |
99 | 97 | rpne0d 12967 |
. . . . . . . . . . 11
β’ (π β β β (seq1(
Β· , πΉ)βπ) β 0) |
100 | 98, 99 | reccld 11929 |
. . . . . . . . . 10
β’ (π β β β (1 /
(seq1( Β· , πΉ)βπ)) β β) |
101 | 22, 100 | mulcld 11180 |
. . . . . . . . 9
β’ (π β β β ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ))) β β) |
102 | 6, 101 | fmpti 7061 |
. . . . . . . 8
β’ (π β β β¦ ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ)))):ββΆβ |
103 | 102 | a1i 11 |
. . . . . . 7
β’ (β€
β (π β β
β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ)))):ββΆβ) |
104 | 103 | ffvelcdmda 7036 |
. . . . . 6
β’
((β€ β§ π
β β) β ((π
β β β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ))))βπ) β β) |
105 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = π β (seq1( Β· , πΉ)βπ) = (seq1( Β· , πΉ)βπ)) |
106 | 105 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π β ((seq1( Β· , πΉ)βπ) β β+ β (seq1(
Β· , πΉ)βπ) β
β+)) |
107 | 106, 97 | vtoclga 3533 |
. . . . . . . . . . 11
β’ (π β β β (seq1(
Β· , πΉ)βπ) β
β+) |
108 | 107 | rpcnd 12964 |
. . . . . . . . . 10
β’ (π β β β (seq1(
Β· , πΉ)βπ) β
β) |
109 | 107 | rpne0d 12967 |
. . . . . . . . . 10
β’ (π β β β (seq1(
Β· , πΉ)βπ) β 0) |
110 | 35, 108, 109 | divrecd 11939 |
. . . . . . . . 9
β’ (π β β β (1 /
(seq1( Β· , πΉ)βπ)) = (1 Β· (1 / (seq1( Β· , πΉ)βπ)))) |
111 | 11 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β Ο
β β) |
112 | 64 | rpne0d 12967 |
. . . . . . . . . . . 12
β’ (π β β β 2 β
0) |
113 | 15 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β Ο β
0) |
114 | 32, 111, 112, 113 | divcan6d 11955 |
. . . . . . . . . . 11
β’ (π β β β ((2 /
Ο) Β· (Ο / 2)) = 1) |
115 | 114 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π β β β 1 = ((2 /
Ο) Β· (Ο / 2))) |
116 | 115 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β β β (1
Β· (1 / (seq1( Β· , πΉ)βπ))) = (((2 / Ο) Β· (Ο / 2))
Β· (1 / (seq1( Β· , πΉ)βπ)))) |
117 | 32, 111, 113 | divcld 11936 |
. . . . . . . . . 10
β’ (π β β β (2 /
Ο) β β) |
118 | 111 | halfcld 12403 |
. . . . . . . . . 10
β’ (π β β β (Ο /
2) β β) |
119 | 108, 109 | reccld 11929 |
. . . . . . . . . 10
β’ (π β β β (1 /
(seq1( Β· , πΉ)βπ)) β β) |
120 | 117, 118,
119 | mulassd 11183 |
. . . . . . . . 9
β’ (π β β β (((2 /
Ο) Β· (Ο / 2)) Β· (1 / (seq1( Β· , πΉ)βπ))) = ((2 / Ο) Β· ((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ))))) |
121 | 110, 116,
120 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β β β (1 /
(seq1( Β· , πΉ)βπ)) = ((2 / Ο) Β· ((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ))))) |
122 | | eqidd 2734 |
. . . . . . . . 9
β’ (π β β β (π β β β¦ (1 /
(seq1( Β· , πΉ)βπ))) = (π β β β¦ (1 / (seq1( Β·
, πΉ)βπ)))) |
123 | 105 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π = π β (1 / (seq1( Β· , πΉ)βπ)) = (1 / (seq1( Β· , πΉ)βπ))) |
124 | 123 | adantl 483 |
. . . . . . . . 9
β’ ((π β β β§ π = π) β (1 / (seq1( Β· , πΉ)βπ)) = (1 / (seq1( Β· , πΉ)βπ))) |
125 | | id 22 |
. . . . . . . . 9
β’ (π β β β π β
β) |
126 | 107 | rpreccld 12972 |
. . . . . . . . 9
β’ (π β β β (1 /
(seq1( Β· , πΉ)βπ)) β
β+) |
127 | 122, 124,
125, 126 | fvmptd 6956 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) = (1 / (seq1( Β· , πΉ)βπ))) |
128 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π β β β (π β β β¦ ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ)))) = (π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ))))) |
129 | 124 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π β β β§ π = π) β ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)βπ)))) |
130 | 118, 119 | mulcld 11180 |
. . . . . . . . . 10
β’ (π β β β ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ))) β β) |
131 | 128, 129,
125, 130 | fvmptd 6956 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ))))βπ) = ((Ο / 2) Β· (1 / (seq1( Β·
, πΉ)βπ)))) |
132 | 131 | oveq2d 7374 |
. . . . . . . 8
β’ (π β β β ((2 /
Ο) Β· ((π β
β β¦ ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ))))βπ)) = ((2 / Ο) Β· ((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ))))) |
133 | 121, 127,
132 | 3eqtr4d 2783 |
. . . . . . 7
β’ (π β β β ((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) = ((2 / Ο) Β· ((π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ))))βπ))) |
134 | 133 | adantl 483 |
. . . . . 6
β’
((β€ β§ π
β β) β ((π
β β β¦ (1 / (seq1( Β· , πΉ)βπ)))βπ) = ((2 / Ο) Β· ((π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ))))βπ))) |
135 | 1, 2, 9, 17, 20, 104, 134 | climmulc2 15525 |
. . . . 5
β’ (β€
β (π β β
β¦ (1 / (seq1( Β· , πΉ)βπ))) β ((2 / Ο) Β·
1)) |
136 | | 2cn 12233 |
. . . . . . 7
β’ 2 β
β |
137 | 136, 11, 15 | divcli 11902 |
. . . . . 6
β’ (2 /
Ο) β β |
138 | 137 | mulid1i 11164 |
. . . . 5
β’ ((2 /
Ο) Β· 1) = (2 / Ο) |
139 | 135, 138 | breqtrdi 5147 |
. . . 4
β’ (β€
β (π β β
β¦ (1 / (seq1( Β· , πΉ)βπ))) β (2 / Ο)) |
140 | | 2ne0 12262 |
. . . . . 6
β’ 2 β
0 |
141 | 136, 11, 140, 15 | divne0i 11908 |
. . . . 5
β’ (2 /
Ο) β 0 |
142 | 141 | a1i 11 |
. . . 4
β’ (β€
β (2 / Ο) β 0) |
143 | 127, 119 | eqeltrd 2834 |
. . . . . 6
β’ (π β β β ((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) β β) |
144 | 108, 109 | recne0d 11930 |
. . . . . . . 8
β’ (π β β β (1 /
(seq1( Β· , πΉ)βπ)) β 0) |
145 | 127, 144 | eqnetrd 3008 |
. . . . . . 7
β’ (π β β β ((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) β 0) |
146 | | nelsn 4627 |
. . . . . . 7
β’ (((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) β 0 β Β¬ ((π β β β¦ (1 / (seq1( Β·
, πΉ)βπ)))βπ) β {0}) |
147 | 145, 146 | syl 17 |
. . . . . 6
β’ (π β β β Β¬
((π β β β¦
(1 / (seq1( Β· , πΉ)βπ)))βπ) β {0}) |
148 | 143, 147 | eldifd 3922 |
. . . . 5
β’ (π β β β ((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) β (β β
{0})) |
149 | 148 | adantl 483 |
. . . 4
β’
((β€ β§ π
β β) β ((π
β β β¦ (1 / (seq1( Β· , πΉ)βπ)))βπ) β (β β
{0})) |
150 | 108, 109 | recrecd 11933 |
. . . . . 6
β’ (π β β β (1 / (1 /
(seq1( Β· , πΉ)βπ))) = (seq1( Β· , πΉ)βπ)) |
151 | 122, 124,
125, 119 | fvmptd 6956 |
. . . . . . 7
β’ (π β β β ((π β β β¦ (1 /
(seq1( Β· , πΉ)βπ)))βπ) = (1 / (seq1( Β· , πΉ)βπ))) |
152 | 151 | oveq2d 7374 |
. . . . . 6
β’ (π β β β (1 /
((π β β β¦
(1 / (seq1( Β· , πΉ)βπ)))βπ)) = (1 / (1 / (seq1( Β· , πΉ)βπ)))) |
153 | | wallispi.2 |
. . . . . . 7
β’ π = (π β β β¦ (seq1( Β· ,
πΉ)βπ)) |
154 | 105, 153,
97 | fvmpt3 6953 |
. . . . . 6
β’ (π β β β (πβπ) = (seq1( Β· , πΉ)βπ)) |
155 | 150, 152,
154 | 3eqtr4rd 2784 |
. . . . 5
β’ (π β β β (πβπ) = (1 / ((π β β β¦ (1 / (seq1( Β·
, πΉ)βπ)))βπ))) |
156 | 155 | adantl 483 |
. . . 4
β’
((β€ β§ π
β β) β (πβπ) = (1 / ((π β β β¦ (1 / (seq1( Β·
, πΉ)βπ)))βπ))) |
157 | 18 | mptex 7174 |
. . . . . 6
β’ (π β β β¦ (seq1(
Β· , πΉ)βπ)) β V |
158 | 153, 157 | eqeltri 2830 |
. . . . 5
β’ π β V |
159 | 158 | a1i 11 |
. . . 4
β’ (β€
β π β
V) |
160 | 1, 2, 139, 142, 149, 156, 159 | climrec 43930 |
. . 3
β’ (β€
β π β (1 / (2 /
Ο))) |
161 | 160 | mptru 1549 |
. 2
β’ π β (1 / (2 /
Ο)) |
162 | | recdiv 11866 |
. . 3
β’ (((2
β β β§ 2 β 0) β§ (Ο β β β§ Ο β 0))
β (1 / (2 / Ο)) = (Ο / 2)) |
163 | 136, 140,
11, 15, 162 | mp4an 692 |
. 2
β’ (1 / (2 /
Ο)) = (Ο / 2) |
164 | 161, 163 | breqtri 5131 |
1
β’ π β (Ο /
2) |