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 ∈ 0 π ⟼ − cos ⁡ t
Assertion itgsin0pilem1 ⊢ ∫ 0 π sin ⁡ x dx = 2

Proof

Step Hyp Ref Expression
1 itgsin0pilem1.1 ⊢ C = t ∈ 0 π ⟼ − cos ⁡ t
2 fveq2 ⊢ t = x → cos ⁡ t = cos ⁡ x
3 2 negeqd ⊢ t = x → − cos ⁡ t = − cos ⁡ x
4 3 cbvmptv ⊢ t ∈ 0 π ⟼ − cos ⁡ t = x ∈ 0 π ⟼ − cos ⁡ x
5 1 4 eqtri ⊢ C = x ∈ 0 π ⟼ − cos ⁡ x
6 5 oveq2i ⊢ ℝ D C = dx ∈ 0 π − cos ⁡ x d ℝ x
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 ⊢ x ∈ 0 π → x ∈ ℂ
16 15 coscld ⊢ x ∈ 0 π → cos ⁡ x ∈ ℂ
17 16 adantl ⊢ ⊤ ∧ x ∈ 0 π → cos ⁡ x ∈ ℂ
18 17 negcld ⊢ ⊤ ∧ x ∈ 0 π → − cos ⁡ x ∈ ℂ
19 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
20 19 tgioo2 ⊢ topGen ⁡ ran ⁡ . = 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 20 19 23 dvmptntr ⊢ ⊤ → dx ∈ 0 π − cos ⁡ x d ℝ x = dx ∈ 0 π − cos ⁡ x d ℝ x
25 24 mptru ⊢ dx ∈ 0 π − cos ⁡ x d ℝ x = dx ∈ 0 π − cos ⁡ x d ℝ x
26 reelprrecn ⊢ ℝ ∈ ℝ ℂ
27 26 a1i ⊢ ⊤ → ℝ ∈ ℝ ℂ
28 recn ⊢ x ∈ ℝ → x ∈ ℂ
29 28 coscld ⊢ x ∈ ℝ → cos ⁡ x ∈ ℂ
30 29 adantl ⊢ ⊤ ∧ x ∈ ℝ → cos ⁡ x ∈ ℂ
31 30 negcld ⊢ ⊤ ∧ x ∈ ℝ → − cos ⁡ x ∈ ℂ
32 28 sincld ⊢ x ∈ ℝ → sin ⁡ x ∈ ℂ
33 32 adantl ⊢ ⊤ ∧ x ∈ ℝ → sin ⁡ x ∈ ℂ
34 32 negcld ⊢ x ∈ ℝ → − sin ⁡ x ∈ ℂ
35 34 adantl ⊢ ⊤ ∧ x ∈ ℝ → − sin ⁡ x ∈ ℂ
36 dvcosre ⊢ dx ∈ ℝ cos ⁡ x d ℝ x = x ∈ ℝ ⟼ − sin ⁡ x
37 36 a1i ⊢ ⊤ → dx ∈ ℝ cos ⁡ x d ℝ x = x ∈ ℝ ⟼ − sin ⁡ x
38 27 30 35 37 dvmptneg ⊢ ⊤ → dx ∈ ℝ − cos ⁡ x d ℝ x = x ∈ ℝ ⟼ − − sin ⁡ x
39 32 negnegd ⊢ x ∈ ℝ → − − sin ⁡ x = sin ⁡ x
40 39 mpteq2ia ⊢ x ∈ ℝ ⟼ − − sin ⁡ x = x ∈ ℝ ⟼ sin ⁡ x
41 38 40 eqtrdi ⊢ ⊤ → dx ∈ ℝ − cos ⁡ x d ℝ x = x ∈ ℝ ⟼ sin ⁡ x
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 ⊢ ⊤ → dx ∈ 0 π − cos ⁡ x d ℝ x = x ∈ 0 π ⟼ sin ⁡ x
47 46 mptru ⊢ dx ∈ 0 π − cos ⁡ x d ℝ x = x ∈ 0 π ⟼ sin ⁡ x
48 6 25 47 3eqtri ⊢ ℝ D C = x ∈ 0 π ⟼ sin ⁡ x
49 48 fveq1i ⊢ C ℝ ′ ⁡ x = x ∈ 0 π ⟼ sin ⁡ x ⁡ x
50 42 7 sstri ⊢ 0 π ⊆ ℂ
51 50 sseli ⊢ x ∈ 0 π → x ∈ ℂ
52 51 sincld ⊢ x ∈ 0 π → sin ⁡ x ∈ ℂ
53 eqid ⊢ x ∈ 0 π ⟼ sin ⁡ x = x ∈ 0 π ⟼ sin ⁡ x
54 53 fvmpt2 ⊢ x ∈ 0 π ∧ sin ⁡ x ∈ ℂ → x ∈ 0 π ⟼ sin ⁡ x ⁡ x = sin ⁡ x
55 52 54 mpdan ⊢ x ∈ 0 π → x ∈ 0 π ⟼ sin ⁡ x ⁡ x = sin ⁡ x
56 49 55 syl5eq ⊢ x ∈ 0 π → C ℝ ′ ⁡ x = sin ⁡ x
57 56 adantl ⊢ ⊤ ∧ x ∈ 0 π → C ℝ ′ ⁡ x = sin ⁡ x
58 57 itgeq2dv ⊢ ⊤ → ∫ 0 π C ℝ ′ ⁡ x dx = ∫ 0 π sin ⁡ x dx
59 58 mptru ⊢ ∫ 0 π C ℝ ′ ⁡ x dx = ∫ 0 π sin ⁡ x dx
60 9 a1i ⊢ ⊤ → 0 ∈ ℝ
61 10 a1i ⊢ ⊤ → π ∈ ℝ
62 pipos ⊢ 0 < π
63 9 10 62 ltleii ⊢ 0 ≤ π
64 63 a1i ⊢ ⊤ → 0 ≤ π
65 nfcv ⊢ Ⅎ _ x sin
66 sincn ⊢ sin : ℂ ⟶cn ℂ
67 66 a1i ⊢ ⊤ → sin : ℂ ⟶cn ℂ
68 50 a1i ⊢ ⊤ → 0 π ⊆ ℂ
69 65 67 68 cncfmptss ⊢ ⊤ → x ∈ 0 π ⟼ sin ⁡ x : 0 π ⟶cn ℂ
70 48 69 eqeltrid ⊢ ⊤ → C ℝ ′ : 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 ⊢ x ∈ 0 π → sin ⁡ x ∈ ℂ
76 75 adantl ⊢ ⊤ ∧ x ∈ 0 π → sin ⁡ x ∈ ℂ
77 14 a1i ⊢ ⊤ → 0 π ⊆ ℂ
78 65 67 77 cncfmptss ⊢ ⊤ → x ∈ 0 π ⟼ sin ⁡ x : 0 π ⟶cn ℂ
79 78 mptru ⊢ x ∈ 0 π ⟼ sin ⁡ x : 0 π ⟶cn ℂ
80 cniccibl ⊢ 0 ∈ ℝ ∧ π ∈ ℝ ∧ x ∈ 0 π ⟼ sin ⁡ x : 0 π ⟶cn ℂ → x ∈ 0 π ⟼ sin ⁡ x ∈ 𝐿 1
81 9 10 79 80 mp3an ⊢ x ∈ 0 π ⟼ sin ⁡ x ∈ 𝐿 1
82 81 a1i ⊢ ⊤ → x ∈ 0 π ⟼ sin ⁡ x ∈ 𝐿 1
83 72 74 76 82 iblss ⊢ ⊤ → x ∈ 0 π ⟼ sin ⁡ x ∈ 𝐿 1
84 48 83 eqeltrid ⊢ ⊤ → ℝ D C ∈ 𝐿 1
85 16 negcld ⊢ x ∈ 0 π → − cos ⁡ x ∈ ℂ
86 eqid ⊢ x ∈ ℂ ⟼ − cos ⁡ x = x ∈ ℂ ⟼ − cos ⁡ x
87 86 fvmpt2 ⊢ x ∈ ℂ ∧ − cos ⁡ x ∈ ℂ → x ∈ ℂ ⟼ − cos ⁡ x ⁡ x = − cos ⁡ x
88 15 85 87 syl2anc ⊢ x ∈ 0 π → x ∈ ℂ ⟼ − cos ⁡ x ⁡ x = − cos ⁡ x
89 88 eqcomd ⊢ x ∈ 0 π → − cos ⁡ x = x ∈ ℂ ⟼ − cos ⁡ x ⁡ x
90 89 mpteq2ia ⊢ x ∈ 0 π ⟼ − cos ⁡ x = x ∈ 0 π ⟼ x ∈ ℂ ⟼ − cos ⁡ x ⁡ x
91 nfmpt1 ⊢ Ⅎ _ x x ∈ ℂ ⟼ − cos ⁡ x
92 coscn ⊢ cos : ℂ ⟶cn ℂ
93 86 negfcncf ⊢ cos : ℂ ⟶cn ℂ → x ∈ ℂ ⟼ − cos ⁡ x : ℂ ⟶cn ℂ
94 92 93 ax-mp ⊢ x ∈ ℂ ⟼ − cos ⁡ x : ℂ ⟶cn ℂ
95 94 a1i ⊢ ⊤ → x ∈ ℂ ⟼ − cos ⁡ x : ℂ ⟶cn ℂ
96 91 95 77 cncfmptss ⊢ ⊤ → x ∈ 0 π ⟼ x ∈ ℂ ⟼ − cos ⁡ x ⁡ x : 0 π ⟶cn ℂ
97 96 mptru ⊢ x ∈ 0 π ⟼ x ∈ ℂ ⟼ − cos ⁡ x ⁡ x : 0 π ⟶cn ℂ
98 90 97 eqeltri ⊢ x ∈ 0 π ⟼ − cos ⁡ x : 0 π ⟶cn ℂ
99 5 98 eqeltri ⊢ C : 0 π ⟶cn ℂ
100 99 a1i ⊢ ⊤ → C : 0 π ⟶cn ℂ
101 60 61 64 70 84 100 ftc2 ⊢ ⊤ → ∫ 0 π C ℝ ′ ⁡ x dx = C ⁡ π − C ⁡ 0
102 101 mptru ⊢ ∫ 0 π C ℝ ′ ⁡ x dx = C ⁡ π − C ⁡ 0
103 59 102 eqtr3i ⊢ ∫ 0 π sin ⁡ x dx = C ⁡ π − C ⁡ 0
104 0xr ⊢ 0 ∈ ℝ *
105 10 rexri ⊢ π ∈ ℝ *
106 ubicc2 ⊢ 0 ∈ ℝ * ∧ π ∈ ℝ * ∧ 0 ≤ π → π ∈ 0 π
107 104 105 63 106 mp3an ⊢ π ∈ 0 π
108 fveq2 ⊢ t = π → cos ⁡ t = cos ⁡ π
109 cospi ⊢ cos ⁡ π = − 1
110 108 109 eqtrdi ⊢ t = π → cos ⁡ t = − 1
111 110 negeqd ⊢ t = π → − cos ⁡ t = − -1
112 ax-1cn ⊢ 1 ∈ ℂ
113 112 a1i ⊢ t = π → 1 ∈ ℂ
114 113 negnegd ⊢ t = π → − -1 = 1
115 111 114 eqtrd ⊢ t = π → − cos ⁡ t = 1
116 1ex ⊢ 1 ∈ V
117 115 1 116 fvmpt ⊢ π ∈ 0 π → C ⁡ π = 1
118 107 117 ax-mp ⊢ C ⁡ π = 1
119 lbicc2 ⊢ 0 ∈ ℝ * ∧ π ∈ ℝ * ∧ 0 ≤ π → 0 ∈ 0 π
120 104 105 63 119 mp3an ⊢ 0 ∈ 0 π
121 fveq2 ⊢ t = 0 → cos ⁡ t = cos ⁡ 0
122 121 negeqd ⊢ t = 0 → − cos ⁡ t = − cos ⁡ 0
123 negex ⊢ − cos ⁡ 0 ∈ V
124 122 1 123 fvmpt ⊢ 0 ∈ 0 π → C ⁡ 0 = − cos ⁡ 0
125 120 124 ax-mp ⊢ C ⁡ 0 = − cos ⁡ 0
126 cos0 ⊢ cos ⁡ 0 = 1
127 126 negeqi ⊢ − cos ⁡ 0 = − 1
128 125 127 eqtri ⊢ C ⁡ 0 = − 1
129 118 128 oveq12i ⊢ C ⁡ π − C ⁡ 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 ⁡ x dx = 2