Step | Hyp | Ref
| Expression |
1 | | atantayl3.1 |
. . . 4
β’ πΉ = (π β β0 β¦
((-1βπ) Β·
((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
2 | | 2nn0 12489 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
3 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β π β β0) |
4 | | nn0mulcl 12508 |
. . . . . . . . . . . 12
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β (2 Β· π) β
β0) |
6 | 5 | nn0cnd 12534 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β (2 Β· π) β β) |
7 | | ax-1cn 11168 |
. . . . . . . . . 10
β’ 1 β
β |
8 | | pncan 11466 |
. . . . . . . . . 10
β’ (((2
Β· π) β β
β§ 1 β β) β (((2 Β· π) + 1) β 1) = (2 Β· π)) |
9 | 6, 7, 8 | sylancl 587 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β (((2 Β· π) + 1) β 1) = (2 Β· π)) |
10 | 9 | oveq1d 7424 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((((2 Β· π) + 1) β 1) / 2) = ((2 Β· π) / 2)) |
11 | | nn0cn 12482 |
. . . . . . . . . 10
β’ (π β β0
β π β
β) |
12 | 11 | adantl 483 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β π β β) |
13 | | 2cnd 12290 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β 2 β β) |
14 | | 2ne0 12316 |
. . . . . . . . . 10
β’ 2 β
0 |
15 | 14 | a1i 11 |
. . . . . . . . 9
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β 2 β 0) |
16 | 12, 13, 15 | divcan3d 11995 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((2 Β· π) / 2) = π) |
17 | 10, 16 | eqtr2d 2774 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β π = ((((2 Β· π) + 1) β 1) / 2)) |
18 | 17 | oveq2d 7425 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β (-1βπ) = (-1β((((2 Β· π) + 1) β 1) /
2))) |
19 | 18 | oveq1d 7424 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((-1βπ) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))) = ((-1β((((2 Β· π) + 1) β 1) / 2)) Β·
((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
20 | 19 | mpteq2dva 5249 |
. . . 4
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (π β
β0 β¦ ((-1βπ) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) = (π β β0 β¦
((-1β((((2 Β· π)
+ 1) β 1) / 2)) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) |
21 | 1, 20 | eqtrid 2785 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β πΉ = (π β β0
β¦ ((-1β((((2 Β· π) + 1) β 1) / 2)) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) |
22 | 21 | seqeq3d 13974 |
. 2
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq0( + , πΉ) = seq0(
+ , (π β
β0 β¦ ((-1β((((2 Β· π) + 1) β 1) / 2)) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1)))))) |
23 | | eqid 2733 |
. . . 4
β’ (π β β β¦ if(2
β₯ π, 0,
((-1β((π β 1) /
2)) Β· ((π΄βπ) / π)))) = (π β β β¦ if(2 β₯ π, 0, ((-1β((π β 1) / 2)) Β·
((π΄βπ) / π)))) |
24 | 23 | atantayl2 26443 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq1( + , (π β
β β¦ if(2 β₯ π, 0, ((-1β((π β 1) / 2)) Β· ((π΄βπ) / π))))) β (arctanβπ΄)) |
25 | | neg1cn 12326 |
. . . . . . 7
β’ -1 β
β |
26 | | expcl 14045 |
. . . . . . 7
β’ ((-1
β β β§ π
β β0) β (-1βπ) β β) |
27 | 25, 3, 26 | sylancr 588 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β (-1βπ) β β) |
28 | | simpll 766 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β π΄ β β) |
29 | | peano2nn0 12512 |
. . . . . . . . 9
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β
β0) |
30 | 5, 29 | syl 17 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((2 Β· π) + 1) β
β0) |
31 | 28, 30 | expcld 14111 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β (π΄β((2 Β· π) + 1)) β β) |
32 | | nn0p1nn 12511 |
. . . . . . . . 9
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β β) |
33 | 5, 32 | syl 17 |
. . . . . . . 8
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((2 Β· π) + 1) β β) |
34 | 33 | nncnd 12228 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((2 Β· π) + 1) β β) |
35 | 33 | nnne0d 12262 |
. . . . . . 7
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((2 Β· π) + 1) β 0) |
36 | 31, 34, 35 | divcld 11990 |
. . . . . 6
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1)) β β) |
37 | 27, 36 | mulcld 11234 |
. . . . 5
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((-1βπ) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))) β β) |
38 | 19, 37 | eqeltrrd 2835 |
. . . 4
β’ (((π΄ β β β§
(absβπ΄) < 1) β§
π β
β0) β ((-1β((((2 Β· π) + 1) β 1) / 2)) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))) β
β) |
39 | | oveq1 7416 |
. . . . . . 7
β’ (π = ((2 Β· π) + 1) β (π β 1) = (((2 Β·
π) + 1) β
1)) |
40 | 39 | oveq1d 7424 |
. . . . . 6
β’ (π = ((2 Β· π) + 1) β ((π β 1) / 2) = ((((2
Β· π) + 1) β 1)
/ 2)) |
41 | 40 | oveq2d 7425 |
. . . . 5
β’ (π = ((2 Β· π) + 1) β (-1β((π β 1) / 2)) =
(-1β((((2 Β· π)
+ 1) β 1) / 2))) |
42 | | oveq2 7417 |
. . . . . 6
β’ (π = ((2 Β· π) + 1) β (π΄βπ) = (π΄β((2 Β· π) + 1))) |
43 | | id 22 |
. . . . . 6
β’ (π = ((2 Β· π) + 1) β π = ((2 Β· π) + 1)) |
44 | 42, 43 | oveq12d 7427 |
. . . . 5
β’ (π = ((2 Β· π) + 1) β ((π΄βπ) / π) = ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))) |
45 | 41, 44 | oveq12d 7427 |
. . . 4
β’ (π = ((2 Β· π) + 1) β ((-1β((π β 1) / 2)) Β·
((π΄βπ) / π)) = ((-1β((((2 Β· π) + 1) β 1) / 2)) Β·
((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1)))) |
46 | 38, 45 | iserodd 16768 |
. . 3
β’ ((π΄ β β β§
(absβπ΄) < 1)
β (seq0( + , (π β
β0 β¦ ((-1β((((2 Β· π) + 1) β 1) / 2)) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) β
(arctanβπ΄) β
seq1( + , (π β β
β¦ if(2 β₯ π, 0,
((-1β((π β 1) /
2)) Β· ((π΄βπ) / π))))) β (arctanβπ΄))) |
47 | 24, 46 | mpbird 257 |
. 2
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq0( + , (π β
β0 β¦ ((-1β((((2 Β· π) + 1) β 1) / 2)) Β· ((π΄β((2 Β· π) + 1)) / ((2 Β· π) + 1))))) β
(arctanβπ΄)) |
48 | 22, 47 | eqbrtrd 5171 |
1
β’ ((π΄ β β β§
(absβπ΄) < 1)
β seq0( + , πΉ) β
(arctanβπ΄)) |