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 eqtrid 
 |-  ( 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