Metamath Proof Explorer


Theorem itgsin0pilem1

Description: Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis itgsin0pilem1.1
|- C = ( t e. ( 0 [,] _pi ) |-> -u ( cos ` t ) )
Assertion itgsin0pilem1
|- S. ( 0 (,) _pi ) ( sin ` x ) _d x = 2

Proof

Step Hyp Ref Expression
1 itgsin0pilem1.1
 |-  C = ( t e. ( 0 [,] _pi ) |-> -u ( cos ` t ) )
2 fveq2
 |-  ( t = x -> ( cos ` t ) = ( cos ` x ) )
3 2 negeqd
 |-  ( t = x -> -u ( cos ` t ) = -u ( cos ` x ) )
4 3 cbvmptv
 |-  ( t e. ( 0 [,] _pi ) |-> -u ( cos ` t ) ) = ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) )
5 1 4 eqtri
 |-  C = ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) )
6 5 oveq2i
 |-  ( RR _D C ) = ( RR _D ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) ) )
7 ax-resscn
 |-  RR C_ CC
8 7 a1i
 |-  ( T. -> RR C_ CC )
9 0re
 |-  0 e. RR
10 pire
 |-  _pi e. RR
11 iccssre
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( 0 [,] _pi ) C_ RR )
12 9 10 11 mp2an
 |-  ( 0 [,] _pi ) C_ RR
13 12 a1i
 |-  ( T. -> ( 0 [,] _pi ) C_ RR )
14 12 7 sstri
 |-  ( 0 [,] _pi ) C_ CC
15 14 sseli
 |-  ( x e. ( 0 [,] _pi ) -> x e. CC )
16 15 coscld
 |-  ( x e. ( 0 [,] _pi ) -> ( cos ` x ) e. CC )
17 16 adantl
 |-  ( ( T. /\ x e. ( 0 [,] _pi ) ) -> ( cos ` x ) e. CC )
18 17 negcld
 |-  ( ( T. /\ x e. ( 0 [,] _pi ) ) -> -u ( cos ` x ) e. CC )
19 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
20 19 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
21 iccntr
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] _pi ) ) = ( 0 (,) _pi ) )
22 9 10 21 mp2an
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] _pi ) ) = ( 0 (,) _pi )
23 22 a1i
 |-  ( T. -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] _pi ) ) = ( 0 (,) _pi ) )
24 8 13 18 20 19 23 dvmptntr
 |-  ( T. -> ( RR _D ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) ) ) = ( RR _D ( x e. ( 0 (,) _pi ) |-> -u ( cos ` x ) ) ) )
25 24 mptru
 |-  ( RR _D ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) ) ) = ( RR _D ( x e. ( 0 (,) _pi ) |-> -u ( cos ` x ) ) )
26 reelprrecn
 |-  RR e. { RR , CC }
27 26 a1i
 |-  ( T. -> RR e. { RR , CC } )
28 recn
 |-  ( x e. RR -> x e. CC )
29 28 coscld
 |-  ( x e. RR -> ( cos ` x ) e. CC )
30 29 adantl
 |-  ( ( T. /\ x e. RR ) -> ( cos ` x ) e. CC )
31 30 negcld
 |-  ( ( T. /\ x e. RR ) -> -u ( cos ` x ) e. CC )
32 28 sincld
 |-  ( x e. RR -> ( sin ` x ) e. CC )
33 32 adantl
 |-  ( ( T. /\ x e. RR ) -> ( sin ` x ) e. CC )
34 32 negcld
 |-  ( x e. RR -> -u ( sin ` x ) e. CC )
35 34 adantl
 |-  ( ( T. /\ x e. RR ) -> -u ( sin ` x ) e. CC )
36 dvcosre
 |-  ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) )
37 36 a1i
 |-  ( T. -> ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) ) )
38 27 30 35 37 dvmptneg
 |-  ( T. -> ( RR _D ( x e. RR |-> -u ( cos ` x ) ) ) = ( x e. RR |-> -u -u ( sin ` x ) ) )
39 32 negnegd
 |-  ( x e. RR -> -u -u ( sin ` x ) = ( sin ` x ) )
40 39 mpteq2ia
 |-  ( x e. RR |-> -u -u ( sin ` x ) ) = ( x e. RR |-> ( sin ` x ) )
41 38 40 eqtrdi
 |-  ( T. -> ( RR _D ( x e. RR |-> -u ( cos ` x ) ) ) = ( x e. RR |-> ( sin ` x ) ) )
42 ioossre
 |-  ( 0 (,) _pi ) C_ RR
43 42 a1i
 |-  ( T. -> ( 0 (,) _pi ) C_ RR )
44 iooretop
 |-  ( 0 (,) _pi ) e. ( topGen ` ran (,) )
45 44 a1i
 |-  ( T. -> ( 0 (,) _pi ) e. ( topGen ` ran (,) ) )
46 27 31 33 41 43 20 19 45 dvmptres
 |-  ( T. -> ( RR _D ( x e. ( 0 (,) _pi ) |-> -u ( cos ` x ) ) ) = ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) )
47 46 mptru
 |-  ( RR _D ( x e. ( 0 (,) _pi ) |-> -u ( cos ` x ) ) ) = ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) )
48 6 25 47 3eqtri
 |-  ( RR _D C ) = ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) )
49 48 fveq1i
 |-  ( ( RR _D C ) ` x ) = ( ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) ` x )
50 42 7 sstri
 |-  ( 0 (,) _pi ) C_ CC
51 50 sseli
 |-  ( x e. ( 0 (,) _pi ) -> x e. CC )
52 51 sincld
 |-  ( x e. ( 0 (,) _pi ) -> ( sin ` x ) e. CC )
53 eqid
 |-  ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) = ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) )
54 53 fvmpt2
 |-  ( ( x e. ( 0 (,) _pi ) /\ ( sin ` x ) e. CC ) -> ( ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) ` x ) = ( sin ` x ) )
55 52 54 mpdan
 |-  ( x e. ( 0 (,) _pi ) -> ( ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) ` x ) = ( sin ` x ) )
56 49 55 syl5eq
 |-  ( x e. ( 0 (,) _pi ) -> ( ( RR _D C ) ` x ) = ( sin ` x ) )
57 56 adantl
 |-  ( ( T. /\ x e. ( 0 (,) _pi ) ) -> ( ( RR _D C ) ` x ) = ( sin ` x ) )
58 57 itgeq2dv
 |-  ( T. -> S. ( 0 (,) _pi ) ( ( RR _D C ) ` x ) _d x = S. ( 0 (,) _pi ) ( sin ` x ) _d x )
59 58 mptru
 |-  S. ( 0 (,) _pi ) ( ( RR _D C ) ` x ) _d x = S. ( 0 (,) _pi ) ( sin ` x ) _d x
60 9 a1i
 |-  ( T. -> 0 e. RR )
61 10 a1i
 |-  ( T. -> _pi e. RR )
62 pipos
 |-  0 < _pi
63 9 10 62 ltleii
 |-  0 <_ _pi
64 63 a1i
 |-  ( T. -> 0 <_ _pi )
65 nfcv
 |-  F/_ x sin
66 sincn
 |-  sin e. ( CC -cn-> CC )
67 66 a1i
 |-  ( T. -> sin e. ( CC -cn-> CC ) )
68 50 a1i
 |-  ( T. -> ( 0 (,) _pi ) C_ CC )
69 65 67 68 cncfmptss
 |-  ( T. -> ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) e. ( ( 0 (,) _pi ) -cn-> CC ) )
70 48 69 eqeltrid
 |-  ( T. -> ( RR _D C ) e. ( ( 0 (,) _pi ) -cn-> CC ) )
71 ioossicc
 |-  ( 0 (,) _pi ) C_ ( 0 [,] _pi )
72 71 a1i
 |-  ( T. -> ( 0 (,) _pi ) C_ ( 0 [,] _pi ) )
73 ioombl
 |-  ( 0 (,) _pi ) e. dom vol
74 73 a1i
 |-  ( T. -> ( 0 (,) _pi ) e. dom vol )
75 15 sincld
 |-  ( x e. ( 0 [,] _pi ) -> ( sin ` x ) e. CC )
76 75 adantl
 |-  ( ( T. /\ x e. ( 0 [,] _pi ) ) -> ( sin ` x ) e. CC )
77 14 a1i
 |-  ( T. -> ( 0 [,] _pi ) C_ CC )
78 65 67 77 cncfmptss
 |-  ( T. -> ( x e. ( 0 [,] _pi ) |-> ( sin ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
79 78 mptru
 |-  ( x e. ( 0 [,] _pi ) |-> ( sin ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC )
80 cniccibl
 |-  ( ( 0 e. RR /\ _pi e. RR /\ ( x e. ( 0 [,] _pi ) |-> ( sin ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] _pi ) |-> ( sin ` x ) ) e. L^1 )
81 9 10 79 80 mp3an
 |-  ( x e. ( 0 [,] _pi ) |-> ( sin ` x ) ) e. L^1
82 81 a1i
 |-  ( T. -> ( x e. ( 0 [,] _pi ) |-> ( sin ` x ) ) e. L^1 )
83 72 74 76 82 iblss
 |-  ( T. -> ( x e. ( 0 (,) _pi ) |-> ( sin ` x ) ) e. L^1 )
84 48 83 eqeltrid
 |-  ( T. -> ( RR _D C ) e. L^1 )
85 16 negcld
 |-  ( x e. ( 0 [,] _pi ) -> -u ( cos ` x ) e. CC )
86 eqid
 |-  ( x e. CC |-> -u ( cos ` x ) ) = ( x e. CC |-> -u ( cos ` x ) )
87 86 fvmpt2
 |-  ( ( x e. CC /\ -u ( cos ` x ) e. CC ) -> ( ( x e. CC |-> -u ( cos ` x ) ) ` x ) = -u ( cos ` x ) )
88 15 85 87 syl2anc
 |-  ( x e. ( 0 [,] _pi ) -> ( ( x e. CC |-> -u ( cos ` x ) ) ` x ) = -u ( cos ` x ) )
89 88 eqcomd
 |-  ( x e. ( 0 [,] _pi ) -> -u ( cos ` x ) = ( ( x e. CC |-> -u ( cos ` x ) ) ` x ) )
90 89 mpteq2ia
 |-  ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) ) = ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> -u ( cos ` x ) ) ` x ) )
91 nfmpt1
 |-  F/_ x ( x e. CC |-> -u ( cos ` x ) )
92 coscn
 |-  cos e. ( CC -cn-> CC )
93 86 negfcncf
 |-  ( cos e. ( CC -cn-> CC ) -> ( x e. CC |-> -u ( cos ` x ) ) e. ( CC -cn-> CC ) )
94 92 93 ax-mp
 |-  ( x e. CC |-> -u ( cos ` x ) ) e. ( CC -cn-> CC )
95 94 a1i
 |-  ( T. -> ( x e. CC |-> -u ( cos ` x ) ) e. ( CC -cn-> CC ) )
96 91 95 77 cncfmptss
 |-  ( T. -> ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> -u ( cos ` x ) ) ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
97 96 mptru
 |-  ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> -u ( cos ` x ) ) ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC )
98 90 97 eqeltri
 |-  ( x e. ( 0 [,] _pi ) |-> -u ( cos ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC )
99 5 98 eqeltri
 |-  C e. ( ( 0 [,] _pi ) -cn-> CC )
100 99 a1i
 |-  ( T. -> C e. ( ( 0 [,] _pi ) -cn-> CC ) )
101 60 61 64 70 84 100 ftc2
 |-  ( T. -> S. ( 0 (,) _pi ) ( ( RR _D C ) ` x ) _d x = ( ( C ` _pi ) - ( C ` 0 ) ) )
102 101 mptru
 |-  S. ( 0 (,) _pi ) ( ( RR _D C ) ` x ) _d x = ( ( C ` _pi ) - ( C ` 0 ) )
103 59 102 eqtr3i
 |-  S. ( 0 (,) _pi ) ( sin ` x ) _d x = ( ( C ` _pi ) - ( C ` 0 ) )
104 0xr
 |-  0 e. RR*
105 10 rexri
 |-  _pi e. RR*
106 ubicc2
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ 0 <_ _pi ) -> _pi e. ( 0 [,] _pi ) )
107 104 105 63 106 mp3an
 |-  _pi e. ( 0 [,] _pi )
108 fveq2
 |-  ( t = _pi -> ( cos ` t ) = ( cos ` _pi ) )
109 cospi
 |-  ( cos ` _pi ) = -u 1
110 108 109 eqtrdi
 |-  ( t = _pi -> ( cos ` t ) = -u 1 )
111 110 negeqd
 |-  ( t = _pi -> -u ( cos ` t ) = -u -u 1 )
112 ax-1cn
 |-  1 e. CC
113 112 a1i
 |-  ( t = _pi -> 1 e. CC )
114 113 negnegd
 |-  ( t = _pi -> -u -u 1 = 1 )
115 111 114 eqtrd
 |-  ( t = _pi -> -u ( cos ` t ) = 1 )
116 1ex
 |-  1 e. _V
117 115 1 116 fvmpt
 |-  ( _pi e. ( 0 [,] _pi ) -> ( C ` _pi ) = 1 )
118 107 117 ax-mp
 |-  ( C ` _pi ) = 1
119 lbicc2
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ 0 <_ _pi ) -> 0 e. ( 0 [,] _pi ) )
120 104 105 63 119 mp3an
 |-  0 e. ( 0 [,] _pi )
121 fveq2
 |-  ( t = 0 -> ( cos ` t ) = ( cos ` 0 ) )
122 121 negeqd
 |-  ( t = 0 -> -u ( cos ` t ) = -u ( cos ` 0 ) )
123 negex
 |-  -u ( cos ` 0 ) e. _V
124 122 1 123 fvmpt
 |-  ( 0 e. ( 0 [,] _pi ) -> ( C ` 0 ) = -u ( cos ` 0 ) )
125 120 124 ax-mp
 |-  ( C ` 0 ) = -u ( cos ` 0 )
126 cos0
 |-  ( cos ` 0 ) = 1
127 126 negeqi
 |-  -u ( cos ` 0 ) = -u 1
128 125 127 eqtri
 |-  ( C ` 0 ) = -u 1
129 118 128 oveq12i
 |-  ( ( C ` _pi ) - ( C ` 0 ) ) = ( 1 - -u 1 )
130 112 112 subnegi
 |-  ( 1 - -u 1 ) = ( 1 + 1 )
131 1p1e2
 |-  ( 1 + 1 ) = 2
132 130 131 eqtri
 |-  ( 1 - -u 1 ) = 2
133 103 129 132 3eqtri
 |-  S. ( 0 (,) _pi ) ( sin ` x ) _d x = 2