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 ⊢ 𝐶 = ( 𝑡 ∈ ( 0 [,] π ) ↦ - ( cos ‘ 𝑡 ) )
Assertion itgsin0pilem1 ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 = 2

Proof

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