Step | Hyp | Ref
| Expression |
1 | | nn0uz 12812 |
. . . 4
β’
β0 = (β€β₯β0) |
2 | | 0zd 12518 |
. . . 4
β’ (β€
β 0 β β€) |
3 | | 2cn 12235 |
. . . . . 6
β’ 2 β
β |
4 | | ax-icn 11117 |
. . . . . 6
β’ i β
β |
5 | | ine0 11597 |
. . . . . 6
β’ i β
0 |
6 | 3, 4, 5 | divcli 11904 |
. . . . 5
β’ (2 / i)
β β |
7 | 6 | a1i 11 |
. . . 4
β’ (β€
β (2 / i) β β) |
8 | | 3cn 12241 |
. . . . . . 7
β’ 3 β
β |
9 | | 3ne0 12266 |
. . . . . . 7
β’ 3 β
0 |
10 | 4, 8, 9 | divcli 11904 |
. . . . . 6
β’ (i / 3)
β β |
11 | | absdiv 15187 |
. . . . . . . . 9
β’ ((i
β β β§ 3 β β β§ 3 β 0) β (absβ(i /
3)) = ((absβi) / (absβ3))) |
12 | 4, 8, 9, 11 | mp3an 1462 |
. . . . . . . 8
β’
(absβ(i / 3)) = ((absβi) / (absβ3)) |
13 | | absi 15178 |
. . . . . . . . 9
β’
(absβi) = 1 |
14 | | 3re 12240 |
. . . . . . . . . 10
β’ 3 β
β |
15 | | 0re 11164 |
. . . . . . . . . . 11
β’ 0 β
β |
16 | | 3pos 12265 |
. . . . . . . . . . 11
β’ 0 <
3 |
17 | 15, 14, 16 | ltleii 11285 |
. . . . . . . . . 10
β’ 0 β€
3 |
18 | | absid 15188 |
. . . . . . . . . 10
β’ ((3
β β β§ 0 β€ 3) β (absβ3) = 3) |
19 | 14, 17, 18 | mp2an 691 |
. . . . . . . . 9
β’
(absβ3) = 3 |
20 | 13, 19 | oveq12i 7374 |
. . . . . . . 8
β’
((absβi) / (absβ3)) = (1 / 3) |
21 | 12, 20 | eqtri 2765 |
. . . . . . 7
β’
(absβ(i / 3)) = (1 / 3) |
22 | | 1lt3 12333 |
. . . . . . . 8
β’ 1 <
3 |
23 | | recgt1 12058 |
. . . . . . . . 9
β’ ((3
β β β§ 0 < 3) β (1 < 3 β (1 / 3) <
1)) |
24 | 14, 16, 23 | mp2an 691 |
. . . . . . . 8
β’ (1 < 3
β (1 / 3) < 1) |
25 | 22, 24 | mpbi 229 |
. . . . . . 7
β’ (1 / 3)
< 1 |
26 | 21, 25 | eqbrtri 5131 |
. . . . . 6
β’
(absβ(i / 3)) < 1 |
27 | | eqid 2737 |
. . . . . . 7
β’ (π β β0
β¦ ((-1βπ)
Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) = (π β β0 β¦
((-1βπ) Β· (((i
/ 3)β((2 Β· π) +
1)) / ((2 Β· π) +
1)))) |
28 | 27 | atantayl3 26305 |
. . . . . 6
β’ (((i / 3)
β β β§ (absβ(i / 3)) < 1) β seq0( + , (π β β0
β¦ ((-1βπ)
Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) β (arctanβ(i /
3))) |
29 | 10, 26, 28 | mp2an 691 |
. . . . 5
β’ seq0( + ,
(π β
β0 β¦ ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) β
(arctanβ(i / 3)) |
30 | 29 | a1i 11 |
. . . 4
β’ (β€
β seq0( + , (π β
β0 β¦ ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) β
(arctanβ(i / 3))) |
31 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = π β (-1βπ) = (-1βπ)) |
32 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (2 Β· π) = (2 Β· π)) |
33 | 32 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π = π β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
34 | 33 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π β ((i / 3)β((2 Β· π) + 1)) = ((i / 3)β((2
Β· π) +
1))) |
35 | 34, 33 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1)) = (((i / 3)β((2
Β· π) + 1)) / ((2
Β· π) +
1))) |
36 | 31, 35 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π β ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))) = ((-1βπ) Β· (((i / 3)β((2
Β· π) + 1)) / ((2
Β· π) +
1)))) |
37 | | ovex 7395 |
. . . . . . . 8
β’
((-1βπ)
Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))) β V |
38 | 36, 27, 37 | fvmpt 6953 |
. . . . . . 7
β’ (π β β0
β ((π β
β0 β¦ ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))βπ) = ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
39 | 4 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β0
β i β β) |
40 | 8 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β0
β 3 β β) |
41 | 9 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β0
β 3 β 0) |
42 | | 2nn0 12437 |
. . . . . . . . . . . . . 14
β’ 2 β
β0 |
43 | | nn0mulcl 12456 |
. . . . . . . . . . . . . 14
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
44 | 42, 43 | mpan 689 |
. . . . . . . . . . . . 13
β’ (π β β0
β (2 Β· π)
β β0) |
45 | | peano2nn0 12460 |
. . . . . . . . . . . . 13
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β
β0) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β0
β ((2 Β· π) + 1)
β β0) |
47 | 39, 40, 41, 46 | expdivd 14072 |
. . . . . . . . . . 11
β’ (π β β0
β ((i / 3)β((2 Β· π) + 1)) = ((iβ((2 Β· π) + 1)) / (3β((2 Β·
π) + 1)))) |
48 | 47 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β β0
β ((-1βπ)
Β· ((i / 3)β((2 Β· π) + 1))) = ((-1βπ) Β· ((iβ((2 Β· π) + 1)) / (3β((2 Β·
π) +
1))))) |
49 | | neg1cn 12274 |
. . . . . . . . . . . 12
β’ -1 β
β |
50 | | expcl 13992 |
. . . . . . . . . . . 12
β’ ((-1
β β β§ π
β β0) β (-1βπ) β β) |
51 | 49, 50 | mpan 689 |
. . . . . . . . . . 11
β’ (π β β0
β (-1βπ) β
β) |
52 | | expcl 13992 |
. . . . . . . . . . . 12
β’ ((i
β β β§ ((2 Β· π) + 1) β β0) β
(iβ((2 Β· π) +
1)) β β) |
53 | 4, 46, 52 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β β0
β (iβ((2 Β· π) + 1)) β β) |
54 | | 3nn 12239 |
. . . . . . . . . . . . 13
β’ 3 β
β |
55 | | nnexpcl 13987 |
. . . . . . . . . . . . 13
β’ ((3
β β β§ ((2 Β· π) + 1) β β0) β
(3β((2 Β· π) +
1)) β β) |
56 | 54, 46, 55 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β β0
β (3β((2 Β· π) + 1)) β β) |
57 | 56 | nncnd 12176 |
. . . . . . . . . . 11
β’ (π β β0
β (3β((2 Β· π) + 1)) β β) |
58 | 56 | nnne0d 12210 |
. . . . . . . . . . 11
β’ (π β β0
β (3β((2 Β· π) + 1)) β 0) |
59 | 51, 53, 57, 58 | divassd 11973 |
. . . . . . . . . 10
β’ (π β β0
β (((-1βπ)
Β· (iβ((2 Β· π) + 1))) / (3β((2 Β· π) + 1))) = ((-1βπ) Β· ((iβ((2 Β·
π) + 1)) / (3β((2
Β· π) +
1))))) |
60 | | expp1 13981 |
. . . . . . . . . . . . . . 15
β’ ((i
β β β§ (2 Β· π) β β0) β
(iβ((2 Β· π) +
1)) = ((iβ(2 Β· π)) Β· i)) |
61 | 4, 44, 60 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (iβ((2 Β· π) + 1)) = ((iβ(2 Β· π)) Β· i)) |
62 | | expmul 14020 |
. . . . . . . . . . . . . . . . 17
β’ ((i
β β β§ 2 β β0 β§ π β β0) β
(iβ(2 Β· π)) =
((iβ2)βπ)) |
63 | 4, 42, 62 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (iβ(2 Β· π)) = ((iβ2)βπ)) |
64 | | i2 14113 |
. . . . . . . . . . . . . . . . 17
β’
(iβ2) = -1 |
65 | 64 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’
((iβ2)βπ)
= (-1βπ) |
66 | 63, 65 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (iβ(2 Β· π)) = (-1βπ)) |
67 | 66 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ((iβ(2 Β· π)) Β· i) = ((-1βπ) Β· i)) |
68 | 61, 67 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β β0
β (iβ((2 Β· π) + 1)) = ((-1βπ) Β· i)) |
69 | 68 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π β β0
β ((-1βπ)
Β· (iβ((2 Β· π) + 1))) = ((-1βπ) Β· ((-1βπ) Β· i))) |
70 | 51, 51, 39 | mulassd 11185 |
. . . . . . . . . . . 12
β’ (π β β0
β (((-1βπ)
Β· (-1βπ))
Β· i) = ((-1βπ)
Β· ((-1βπ)
Β· i))) |
71 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β -1 β β) |
72 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β π β
β0) |
73 | 71, 72, 72 | expaddd 14060 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (-1β(π + π)) = ((-1βπ) Β· (-1βπ))) |
74 | | expmul 14020 |
. . . . . . . . . . . . . . . . . 18
β’ ((-1
β β β§ 2 β β0 β§ π β β0) β
(-1β(2 Β· π)) =
((-1β2)βπ)) |
75 | 49, 42, 74 | mp3an12 1452 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (-1β(2 Β· π)) = ((-1β2)βπ)) |
76 | | neg1sqe1 14107 |
. . . . . . . . . . . . . . . . . 18
β’
(-1β2) = 1 |
77 | 76 | oveq1i 7372 |
. . . . . . . . . . . . . . . . 17
β’
((-1β2)βπ)
= (1βπ) |
78 | 75, 77 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (-1β(2 Β· π)) = (1βπ)) |
79 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β π β
β) |
80 | 79 | 2timesd 12403 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (2 Β· π) =
(π + π)) |
81 | 80 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (-1β(2 Β· π)) = (-1β(π + π))) |
82 | | nn0z 12531 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β€) |
83 | | 1exp 14004 |
. . . . . . . . . . . . . . . . 17
β’ (π β β€ β
(1βπ) =
1) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (1βπ) =
1) |
85 | 78, 81, 84 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (-1β(π + π)) = 1) |
86 | 73, 85 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ((-1βπ)
Β· (-1βπ)) =
1) |
87 | 86 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π β β0
β (((-1βπ)
Β· (-1βπ))
Β· i) = (1 Β· i)) |
88 | 4 | mulid2i 11167 |
. . . . . . . . . . . . 13
β’ (1
Β· i) = i |
89 | 87, 88 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π β β0
β (((-1βπ)
Β· (-1βπ))
Β· i) = i) |
90 | 69, 70, 89 | 3eqtr2d 2783 |
. . . . . . . . . . 11
β’ (π β β0
β ((-1βπ)
Β· (iβ((2 Β· π) + 1))) = i) |
91 | 90 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β β0
β (((-1βπ)
Β· (iβ((2 Β· π) + 1))) / (3β((2 Β· π) + 1))) = (i / (3β((2
Β· π) +
1)))) |
92 | 48, 59, 91 | 3eqtr2d 2783 |
. . . . . . . . 9
β’ (π β β0
β ((-1βπ)
Β· ((i / 3)β((2 Β· π) + 1))) = (i / (3β((2 Β· π) + 1)))) |
93 | 92 | oveq1d 7377 |
. . . . . . . 8
β’ (π β β0
β (((-1βπ)
Β· ((i / 3)β((2 Β· π) + 1))) / ((2 Β· π) + 1)) = ((i / (3β((2 Β· π) + 1))) / ((2 Β· π) + 1))) |
94 | | expcl 13992 |
. . . . . . . . . 10
β’ (((i / 3)
β β β§ ((2 Β· π) + 1) β β0) β ((i
/ 3)β((2 Β· π) +
1)) β β) |
95 | 10, 46, 94 | sylancr 588 |
. . . . . . . . 9
β’ (π β β0
β ((i / 3)β((2 Β· π) + 1)) β β) |
96 | | nn0p1nn 12459 |
. . . . . . . . . . 11
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β β) |
97 | 44, 96 | syl 17 |
. . . . . . . . . 10
β’ (π β β0
β ((2 Β· π) + 1)
β β) |
98 | 97 | nncnd 12176 |
. . . . . . . . 9
β’ (π β β0
β ((2 Β· π) + 1)
β β) |
99 | 97 | nnne0d 12210 |
. . . . . . . . 9
β’ (π β β0
β ((2 Β· π) + 1)
β 0) |
100 | 51, 95, 98, 99 | divassd 11973 |
. . . . . . . 8
β’ (π β β0
β (((-1βπ)
Β· ((i / 3)β((2 Β· π) + 1))) / ((2 Β· π) + 1)) = ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
101 | 39, 57, 98, 58, 99 | divdiv1d 11969 |
. . . . . . . 8
β’ (π β β0
β ((i / (3β((2 Β· π) + 1))) / ((2 Β· π) + 1)) = (i / ((3β((2 Β· π) + 1)) Β· ((2 Β·
π) + 1)))) |
102 | 93, 100, 101 | 3eqtr3d 2785 |
. . . . . . 7
β’ (π β β0
β ((-1βπ)
Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))) = (i / ((3β((2 Β· π) + 1)) Β· ((2 Β·
π) + 1)))) |
103 | 57, 98 | mulcomd 11183 |
. . . . . . . 8
β’ (π β β0
β ((3β((2 Β· π) + 1)) Β· ((2 Β· π) + 1)) = (((2 Β· π) + 1) Β· (3β((2
Β· π) +
1)))) |
104 | 103 | oveq2d 7378 |
. . . . . . 7
β’ (π β β0
β (i / ((3β((2 Β· π) + 1)) Β· ((2 Β· π) + 1))) = (i / (((2 Β·
π) + 1) Β·
(3β((2 Β· π) +
1))))) |
105 | 38, 102, 104 | 3eqtrd 2781 |
. . . . . 6
β’ (π β β0
β ((π β
β0 β¦ ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))βπ) = (i / (((2 Β· π) + 1) Β· (3β((2
Β· π) +
1))))) |
106 | 97, 56 | nnmulcld 12213 |
. . . . . . . 8
β’ (π β β0
β (((2 Β· π) +
1) Β· (3β((2 Β· π) + 1))) β β) |
107 | 106 | nncnd 12176 |
. . . . . . 7
β’ (π β β0
β (((2 Β· π) +
1) Β· (3β((2 Β· π) + 1))) β β) |
108 | 106 | nnne0d 12210 |
. . . . . . 7
β’ (π β β0
β (((2 Β· π) +
1) Β· (3β((2 Β· π) + 1))) β 0) |
109 | 39, 107, 108 | divcld 11938 |
. . . . . 6
β’ (π β β0
β (i / (((2 Β· π) + 1) Β· (3β((2 Β· π) + 1)))) β
β) |
110 | 105, 109 | eqeltrd 2838 |
. . . . 5
β’ (π β β0
β ((π β
β0 β¦ ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))βπ) β
β) |
111 | 110 | adantl 483 |
. . . 4
β’
((β€ β§ π
β β0) β ((π β β0 β¦
((-1βπ) Β· (((i
/ 3)β((2 Β· π) +
1)) / ((2 Β· π) +
1))))βπ) β
β) |
112 | 33 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π β (3 Β· ((2 Β· π) + 1)) = (3 Β· ((2
Β· π) +
1))) |
113 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = π β (9βπ) = (9βπ)) |
114 | 112, 113 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π β ((3 Β· ((2 Β· π) + 1)) Β· (9βπ)) = ((3 Β· ((2 Β·
π) + 1)) Β·
(9βπ))) |
115 | 114 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (2 / ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) = (2 / ((3 Β· ((2
Β· π) + 1)) Β·
(9βπ)))) |
116 | | log2cnv.1 |
. . . . . . 7
β’ πΉ = (π β β0 β¦ (2 / ((3
Β· ((2 Β· π) +
1)) Β· (9βπ)))) |
117 | | ovex 7395 |
. . . . . . 7
β’ (2 / ((3
Β· ((2 Β· π) +
1)) Β· (9βπ)))
β V |
118 | 115, 116,
117 | fvmpt 6953 |
. . . . . 6
β’ (π β β0
β (πΉβπ) = (2 / ((3 Β· ((2
Β· π) + 1)) Β·
(9βπ)))) |
119 | | expp1 13981 |
. . . . . . . . . . . . . . 15
β’ ((3
β β β§ (2 Β· π) β β0) β
(3β((2 Β· π) +
1)) = ((3β(2 Β· π)) Β· 3)) |
120 | 8, 44, 119 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (3β((2 Β· π) + 1)) = ((3β(2 Β· π)) Β· 3)) |
121 | | expmul 14020 |
. . . . . . . . . . . . . . . . 17
β’ ((3
β β β§ 2 β β0 β§ π β β0) β
(3β(2 Β· π)) =
((3β2)βπ)) |
122 | 8, 42, 121 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (3β(2 Β· π)) = ((3β2)βπ)) |
123 | | sq3 14109 |
. . . . . . . . . . . . . . . . 17
β’
(3β2) = 9 |
124 | 123 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’
((3β2)βπ)
= (9βπ) |
125 | 122, 124 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (3β(2 Β· π)) = (9βπ)) |
126 | 125 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ((3β(2 Β· π)) Β· 3) = ((9βπ) Β· 3)) |
127 | | 9nn 12258 |
. . . . . . . . . . . . . . . . 17
β’ 9 β
β |
128 | | nnexpcl 13987 |
. . . . . . . . . . . . . . . . 17
β’ ((9
β β β§ π
β β0) β (9βπ) β β) |
129 | 127, 128 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (9βπ) β
β) |
130 | 129 | nncnd 12176 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (9βπ) β
β) |
131 | | mulcom 11144 |
. . . . . . . . . . . . . . 15
β’
(((9βπ) β
β β§ 3 β β) β ((9βπ) Β· 3) = (3 Β· (9βπ))) |
132 | 130, 8, 131 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ((9βπ) Β·
3) = (3 Β· (9βπ))) |
133 | 120, 126,
132 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
β’ (π β β0
β (3β((2 Β· π) + 1)) = (3 Β· (9βπ))) |
134 | 90, 133 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π β β0
β (((-1βπ)
Β· (iβ((2 Β· π) + 1))) / (3β((2 Β· π) + 1))) = (i / (3 Β·
(9βπ)))) |
135 | 48, 59, 134 | 3eqtr2d 2783 |
. . . . . . . . . . 11
β’ (π β β0
β ((-1βπ)
Β· ((i / 3)β((2 Β· π) + 1))) = (i / (3 Β· (9βπ)))) |
136 | 135 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β β0
β (((-1βπ)
Β· ((i / 3)β((2 Β· π) + 1))) / ((2 Β· π) + 1)) = ((i / (3 Β· (9βπ))) / ((2 Β· π) + 1))) |
137 | | nnmulcl 12184 |
. . . . . . . . . . . . 13
β’ ((3
β β β§ (9βπ) β β) β (3 Β·
(9βπ)) β
β) |
138 | 54, 129, 137 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β β0
β (3 Β· (9βπ)) β β) |
139 | 138 | nncnd 12176 |
. . . . . . . . . . 11
β’ (π β β0
β (3 Β· (9βπ)) β β) |
140 | 138 | nnne0d 12210 |
. . . . . . . . . . 11
β’ (π β β0
β (3 Β· (9βπ)) β 0) |
141 | 39, 139, 98, 140, 99 | divdiv1d 11969 |
. . . . . . . . . 10
β’ (π β β0
β ((i / (3 Β· (9βπ))) / ((2 Β· π) + 1)) = (i / ((3 Β· (9βπ)) Β· ((2 Β· π) + 1)))) |
142 | 136, 100,
141 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ (π β β0
β ((-1βπ)
Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))) = (i / ((3 Β· (9βπ)) Β· ((2 Β· π) + 1)))) |
143 | 40, 130, 98 | mul32d 11372 |
. . . . . . . . . 10
β’ (π β β0
β ((3 Β· (9βπ)) Β· ((2 Β· π) + 1)) = ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) |
144 | 143 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β β0
β (i / ((3 Β· (9βπ)) Β· ((2 Β· π) + 1))) = (i / ((3 Β· ((2 Β·
π) + 1)) Β·
(9βπ)))) |
145 | 38, 142, 144 | 3eqtrd 2781 |
. . . . . . . 8
β’ (π β β0
β ((π β
β0 β¦ ((-1βπ) Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))βπ) = (i / ((3 Β· ((2
Β· π) + 1)) Β·
(9βπ)))) |
146 | 145 | oveq2d 7378 |
. . . . . . 7
β’ (π β β0
β ((2 / i) Β· ((π β β0 β¦
((-1βπ) Β· (((i
/ 3)β((2 Β· π) +
1)) / ((2 Β· π) +
1))))βπ)) = ((2 / i)
Β· (i / ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))))) |
147 | | nnmulcl 12184 |
. . . . . . . . . . . 12
β’ ((3
β β β§ ((2 Β· π) + 1) β β) β (3 Β· ((2
Β· π) + 1)) β
β) |
148 | 54, 97, 147 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β β0
β (3 Β· ((2 Β· π) + 1)) β β) |
149 | 148, 129 | nnmulcld 12213 |
. . . . . . . . . 10
β’ (π β β0
β ((3 Β· ((2 Β· π) + 1)) Β· (9βπ)) β β) |
150 | 149 | nncnd 12176 |
. . . . . . . . 9
β’ (π β β0
β ((3 Β· ((2 Β· π) + 1)) Β· (9βπ)) β β) |
151 | 149 | nnne0d 12210 |
. . . . . . . . 9
β’ (π β β0
β ((3 Β· ((2 Β· π) + 1)) Β· (9βπ)) β 0) |
152 | 39, 150, 151 | divcld 11938 |
. . . . . . . 8
β’ (π β β0
β (i / ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) β β) |
153 | | mulcom 11144 |
. . . . . . . 8
β’ (((i /
((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) β β β§ (2 / i) β
β) β ((i / ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) Β· (2 / i)) = ((2 / i) Β· (i
/ ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))))) |
154 | 152, 6, 153 | sylancl 587 |
. . . . . . 7
β’ (π β β0
β ((i / ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) Β· (2 / i)) = ((2 / i) Β· (i
/ ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))))) |
155 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β β0
β 2 β β) |
156 | 5 | a1i 11 |
. . . . . . . 8
β’ (π β β0
β i β 0) |
157 | 155, 39, 150, 156, 151 | dmdcand 11967 |
. . . . . . 7
β’ (π β β0
β ((i / ((3 Β· ((2 Β· π) + 1)) Β· (9βπ))) Β· (2 / i)) = (2 / ((3 Β· ((2
Β· π) + 1)) Β·
(9βπ)))) |
158 | 146, 154,
157 | 3eqtr2d 2783 |
. . . . . 6
β’ (π β β0
β ((2 / i) Β· ((π β β0 β¦
((-1βπ) Β· (((i
/ 3)β((2 Β· π) +
1)) / ((2 Β· π) +
1))))βπ)) = (2 / ((3
Β· ((2 Β· π) +
1)) Β· (9βπ)))) |
159 | 118, 158 | eqtr4d 2780 |
. . . . 5
β’ (π β β0
β (πΉβπ) = ((2 / i) Β· ((π β β0
β¦ ((-1βπ)
Β· (((i / 3)β((2 Β· π) + 1)) / ((2 Β· π) + 1))))βπ))) |
160 | 159 | adantl 483 |
. . . 4
β’
((β€ β§ π
β β0) β (πΉβπ) = ((2 / i) Β· ((π β β0 β¦
((-1βπ) Β· (((i
/ 3)β((2 Β· π) +
1)) / ((2 Β· π) +
1))))βπ))) |
161 | 1, 2, 7, 30, 111, 160 | isermulc2 15549 |
. . 3
β’ (β€
β seq0( + , πΉ) β
((2 / i) Β· (arctanβ(i / 3)))) |
162 | 161 | mptru 1549 |
. 2
β’ seq0( + ,
πΉ) β ((2 / i)
Β· (arctanβ(i / 3))) |
163 | | bndatandm 26295 |
. . . . . . . 8
β’ (((i / 3)
β β β§ (absβ(i / 3)) < 1) β (i / 3) β dom
arctan) |
164 | 10, 26, 163 | mp2an 691 |
. . . . . . 7
β’ (i / 3)
β dom arctan |
165 | | atanval 26250 |
. . . . . . 7
β’ ((i / 3)
β dom arctan β (arctanβ(i / 3)) = ((i / 2) Β·
((logβ(1 β (i Β· (i / 3)))) β (logβ(1 + (i
Β· (i / 3))))))) |
166 | 164, 165 | ax-mp 5 |
. . . . . 6
β’
(arctanβ(i / 3)) = ((i / 2) Β· ((logβ(1 β (i
Β· (i / 3)))) β (logβ(1 + (i Β· (i /
3)))))) |
167 | | df-4 12225 |
. . . . . . . . . . . . 13
β’ 4 = (3 +
1) |
168 | 167 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ (4 / 3) =
((3 + 1) / 3) |
169 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
β’ 1 β
β |
170 | 8, 169, 8, 9 | divdiri 11919 |
. . . . . . . . . . . 12
β’ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) |
171 | 8, 9 | dividi 11895 |
. . . . . . . . . . . . 13
β’ (3 / 3) =
1 |
172 | 171 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) |
173 | 168, 170,
172 | 3eqtri 2769 |
. . . . . . . . . . 11
β’ (4 / 3) =
(1 + (1 / 3)) |
174 | 169, 8, 9 | divcli 11904 |
. . . . . . . . . . . 12
β’ (1 / 3)
β β |
175 | 169, 174 | subnegi 11487 |
. . . . . . . . . . 11
β’ (1
β -(1 / 3)) = (1 + (1 / 3)) |
176 | | divneg 11854 |
. . . . . . . . . . . . . 14
β’ ((1
β β β§ 3 β β β§ 3 β 0) β -(1 / 3) = (-1 /
3)) |
177 | 169, 8, 9, 176 | mp3an 1462 |
. . . . . . . . . . . . 13
β’ -(1 / 3)
= (-1 / 3) |
178 | | ixi 11791 |
. . . . . . . . . . . . . 14
β’ (i
Β· i) = -1 |
179 | 178 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ ((i
Β· i) / 3) = (-1 / 3) |
180 | 4, 4, 8, 9 | divassi 11918 |
. . . . . . . . . . . . 13
β’ ((i
Β· i) / 3) = (i Β· (i / 3)) |
181 | 177, 179,
180 | 3eqtr2i 2771 |
. . . . . . . . . . . 12
β’ -(1 / 3)
= (i Β· (i / 3)) |
182 | 181 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (1
β -(1 / 3)) = (1 β (i Β· (i / 3))) |
183 | 173, 175,
182 | 3eqtr2ri 2772 |
. . . . . . . . . 10
β’ (1
β (i Β· (i / 3))) = (4 / 3) |
184 | 183 | fveq2i 6850 |
. . . . . . . . 9
β’
(logβ(1 β (i Β· (i / 3)))) = (logβ(4 /
3)) |
185 | 8, 9 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (3 β
β β§ 3 β 0) |
186 | | divsubdir 11856 |
. . . . . . . . . . . . 13
β’ ((3
β β β§ 1 β β β§ (3 β β β§ 3 β 0))
β ((3 β 1) / 3) = ((3 / 3) β (1 / 3))) |
187 | 8, 169, 185, 186 | mp3an 1462 |
. . . . . . . . . . . 12
β’ ((3
β 1) / 3) = ((3 / 3) β (1 / 3)) |
188 | | 3m1e2 12288 |
. . . . . . . . . . . . 13
β’ (3
β 1) = 2 |
189 | 188 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ ((3
β 1) / 3) = (2 / 3) |
190 | 171 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ ((3 / 3)
β (1 / 3)) = (1 β (1 / 3)) |
191 | 187, 189,
190 | 3eqtr3i 2773 |
. . . . . . . . . . 11
β’ (2 / 3) =
(1 β (1 / 3)) |
192 | 169, 174 | negsubi 11486 |
. . . . . . . . . . 11
β’ (1 + -(1
/ 3)) = (1 β (1 / 3)) |
193 | 181 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (1 + -(1
/ 3)) = (1 + (i Β· (i / 3))) |
194 | 191, 192,
193 | 3eqtr2ri 2772 |
. . . . . . . . . 10
β’ (1 + (i
Β· (i / 3))) = (2 / 3) |
195 | 194 | fveq2i 6850 |
. . . . . . . . 9
β’
(logβ(1 + (i Β· (i / 3)))) = (logβ(2 /
3)) |
196 | 184, 195 | oveq12i 7374 |
. . . . . . . 8
β’
((logβ(1 β (i Β· (i / 3)))) β (logβ(1 + (i
Β· (i / 3))))) = ((logβ(4 / 3)) β (logβ(2 /
3))) |
197 | | 4re 12244 |
. . . . . . . . . . 11
β’ 4 β
β |
198 | | 4pos 12267 |
. . . . . . . . . . 11
β’ 0 <
4 |
199 | 197, 198 | elrpii 12925 |
. . . . . . . . . 10
β’ 4 β
β+ |
200 | | 3rp 12928 |
. . . . . . . . . 10
β’ 3 β
β+ |
201 | | rpdivcl 12947 |
. . . . . . . . . 10
β’ ((4
β β+ β§ 3 β β+) β (4 / 3)
β β+) |
202 | 199, 200,
201 | mp2an 691 |
. . . . . . . . 9
β’ (4 / 3)
β β+ |
203 | | 2rp 12927 |
. . . . . . . . . 10
β’ 2 β
β+ |
204 | | rpdivcl 12947 |
. . . . . . . . . 10
β’ ((2
β β+ β§ 3 β β+) β (2 / 3)
β β+) |
205 | 203, 200,
204 | mp2an 691 |
. . . . . . . . 9
β’ (2 / 3)
β β+ |
206 | | relogdiv 25964 |
. . . . . . . . 9
β’ (((4 / 3)
β β+ β§ (2 / 3) β β+) β
(logβ((4 / 3) / (2 / 3))) = ((logβ(4 / 3)) β (logβ(2 /
3)))) |
207 | 202, 205,
206 | mp2an 691 |
. . . . . . . 8
β’
(logβ((4 / 3) / (2 / 3))) = ((logβ(4 / 3)) β
(logβ(2 / 3))) |
208 | | 4cn 12245 |
. . . . . . . . . . 11
β’ 4 β
β |
209 | | 2cnne0 12370 |
. . . . . . . . . . 11
β’ (2 β
β β§ 2 β 0) |
210 | | divcan7 11871 |
. . . . . . . . . . 11
β’ ((4
β β β§ (2 β β β§ 2 β 0) β§ (3 β β
β§ 3 β 0)) β ((4 / 3) / (2 / 3)) = (4 / 2)) |
211 | 208, 209,
185, 210 | mp3an 1462 |
. . . . . . . . . 10
β’ ((4 / 3)
/ (2 / 3)) = (4 / 2) |
212 | | 4d2e2 12330 |
. . . . . . . . . 10
β’ (4 / 2) =
2 |
213 | 211, 212 | eqtri 2765 |
. . . . . . . . 9
β’ ((4 / 3)
/ (2 / 3)) = 2 |
214 | 213 | fveq2i 6850 |
. . . . . . . 8
β’
(logβ((4 / 3) / (2 / 3))) = (logβ2) |
215 | 196, 207,
214 | 3eqtr2i 2771 |
. . . . . . 7
β’
((logβ(1 β (i Β· (i / 3)))) β (logβ(1 + (i
Β· (i / 3))))) = (logβ2) |
216 | 215 | oveq2i 7373 |
. . . . . 6
β’ ((i / 2)
Β· ((logβ(1 β (i Β· (i / 3)))) β (logβ(1 +
(i Β· (i / 3)))))) = ((i / 2) Β· (logβ2)) |
217 | 166, 216 | eqtri 2765 |
. . . . 5
β’
(arctanβ(i / 3)) = ((i / 2) Β·
(logβ2)) |
218 | 217 | oveq2i 7373 |
. . . 4
β’ ((2 / i)
Β· (arctanβ(i / 3))) = ((2 / i) Β· ((i / 2) Β·
(logβ2))) |
219 | | 2ne0 12264 |
. . . . . 6
β’ 2 β
0 |
220 | 4, 3, 219 | divcli 11904 |
. . . . 5
β’ (i / 2)
β β |
221 | | logcl 25940 |
. . . . . 6
β’ ((2
β β β§ 2 β 0) β (logβ2) β
β) |
222 | 3, 219, 221 | mp2an 691 |
. . . . 5
β’
(logβ2) β β |
223 | 6, 220, 222 | mulassi 11173 |
. . . 4
β’ (((2 / i)
Β· (i / 2)) Β· (logβ2)) = ((2 / i) Β· ((i / 2) Β·
(logβ2))) |
224 | 218, 223 | eqtr4i 2768 |
. . 3
β’ ((2 / i)
Β· (arctanβ(i / 3))) = (((2 / i) Β· (i / 2)) Β·
(logβ2)) |
225 | | divcan6 11869 |
. . . . 5
β’ (((2
β β β§ 2 β 0) β§ (i β β β§ i β 0)) β
((2 / i) Β· (i / 2)) = 1) |
226 | 3, 219, 4, 5, 225 | mp4an 692 |
. . . 4
β’ ((2 / i)
Β· (i / 2)) = 1 |
227 | 226 | oveq1i 7372 |
. . 3
β’ (((2 / i)
Β· (i / 2)) Β· (logβ2)) = (1 Β·
(logβ2)) |
228 | 222 | mulid2i 11167 |
. . 3
β’ (1
Β· (logβ2)) = (logβ2) |
229 | 224, 227,
228 | 3eqtri 2769 |
. 2
β’ ((2 / i)
Β· (arctanβ(i / 3))) = (logβ2) |
230 | 162, 229 | breqtri 5135 |
1
β’ seq0( + ,
πΉ) β
(logβ2) |