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 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
20 19 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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 20 19 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 20 19 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 syl5eq ( 𝑥 ∈ ( 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