Proof of Theorem itgsin0pilem1
| Step | Hyp | Ref
| Expression |
| 1 | | itgsin0pilem1.1 |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑡 ∈ (0[,]π) ↦ -(cos‘𝑡)) |
| 2 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑥 → (cos‘𝑡) = (cos‘𝑥)) |
| 3 | 2 | negeqd 11502 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → -(cos‘𝑡) = -(cos‘𝑥)) |
| 4 | 3 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (0[,]π) ↦
-(cos‘𝑡)) = (𝑥 ∈ (0[,]π) ↦
-(cos‘𝑥)) |
| 5 | 1, 4 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐶 = (𝑥 ∈ (0[,]π) ↦ -(cos‘𝑥)) |
| 6 | 5 | oveq2i 7442 |
. . . . . . . . 9
⊢ (ℝ
D 𝐶) = (ℝ D (𝑥 ∈ (0[,]π) ↦
-(cos‘𝑥))) |
| 7 | | ax-resscn 11212 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
| 8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ ℝ ⊆ ℂ) |
| 9 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 10 | | pire 26500 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
| 11 | | iccssre 13469 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
| 12 | 9, 10, 11 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(0[,]π) ⊆ ℝ |
| 13 | 12 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (0[,]π) ⊆ ℝ) |
| 14 | 12, 7 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢
(0[,]π) ⊆ ℂ |
| 15 | 14 | sseli 3979 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈
ℂ) |
| 16 | 15 | coscld 16167 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,]π) →
(cos‘𝑥) ∈
ℂ) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (0[,]π)) → (cos‘𝑥) ∈ ℂ) |
| 18 | 17 | negcld 11607 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (0[,]π)) → -(cos‘𝑥) ∈ ℂ) |
| 19 | | tgioo4 24826 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 20 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 21 | | iccntr 24843 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → ((int‘(topGen‘ran
(,)))‘(0[,]π)) = (0(,)π)) |
| 22 | 9, 10, 21 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((int‘(topGen‘ran (,)))‘(0[,]π)) =
(0(,)π) |
| 23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ ((int‘(topGen‘ran (,)))‘(0[,]π)) =
(0(,)π)) |
| 24 | 8, 13, 18, 19, 20, 23 | dvmptntr 26009 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑥 ∈
(0[,]π) ↦ -(cos‘𝑥))) = (ℝ D (𝑥 ∈ (0(,)π) ↦ -(cos‘𝑥)))) |
| 25 | 24 | mptru 1547 |
. . . . . . . . 9
⊢ (ℝ
D (𝑥 ∈ (0[,]π)
↦ -(cos‘𝑥))) =
(ℝ D (𝑥 ∈
(0(,)π) ↦ -(cos‘𝑥))) |
| 26 | | reelprrecn 11247 |
. . . . . . . . . . . 12
⊢ ℝ
∈ {ℝ, ℂ} |
| 27 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ ℝ ∈ {ℝ, ℂ}) |
| 28 | | recn 11245 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 29 | 28 | coscld 16167 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(cos‘𝑥) ∈
ℂ) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (cos‘𝑥) ∈ ℂ) |
| 31 | 30 | negcld 11607 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ) → -(cos‘𝑥) ∈ ℂ) |
| 32 | 28 | sincld 16166 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(sin‘𝑥) ∈
ℂ) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (sin‘𝑥) ∈ ℂ) |
| 34 | 32 | negcld 11607 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
-(sin‘𝑥) ∈
ℂ) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ) → -(sin‘𝑥) ∈ ℂ) |
| 36 | | dvcosre 45927 |
. . . . . . . . . . . . . 14
⊢ (ℝ
D (𝑥 ∈ ℝ ↦
(cos‘𝑥))) = (𝑥 ∈ ℝ ↦
-(sin‘𝑥)) |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ (cos‘𝑥))) = (𝑥 ∈ ℝ ↦ -(sin‘𝑥))) |
| 38 | 27, 30, 35, 37 | dvmptneg 26004 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ -(cos‘𝑥))) = (𝑥 ∈ ℝ ↦ --(sin‘𝑥))) |
| 39 | 32 | negnegd 11611 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
--(sin‘𝑥) =
(sin‘𝑥)) |
| 40 | 39 | mpteq2ia 5245 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦
--(sin‘𝑥)) = (𝑥 ∈ ℝ ↦
(sin‘𝑥)) |
| 41 | 38, 40 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℝ D (𝑥 ∈
ℝ ↦ -(cos‘𝑥))) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))) |
| 42 | | ioossre 13448 |
. . . . . . . . . . . 12
⊢
(0(,)π) ⊆ ℝ |
| 43 | 42 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (0(,)π) ⊆ ℝ) |
| 44 | | iooretop 24786 |
. . . . . . . . . . . 12
⊢
(0(,)π) ∈ (topGen‘ran (,)) |
| 45 | 44 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (0(,)π) ∈ (topGen‘ran (,))) |
| 46 | 27, 31, 33, 41, 43, 19, 20, 45 | dvmptres 26001 |
. . . . . . . . . 10
⊢ (⊤
→ (ℝ D (𝑥 ∈
(0(,)π) ↦ -(cos‘𝑥))) = (𝑥 ∈ (0(,)π) ↦ (sin‘𝑥))) |
| 47 | 46 | mptru 1547 |
. . . . . . . . 9
⊢ (ℝ
D (𝑥 ∈ (0(,)π)
↦ -(cos‘𝑥))) =
(𝑥 ∈ (0(,)π)
↦ (sin‘𝑥)) |
| 48 | 6, 25, 47 | 3eqtri 2769 |
. . . . . . . 8
⊢ (ℝ
D 𝐶) = (𝑥 ∈ (0(,)π) ↦ (sin‘𝑥)) |
| 49 | 48 | fveq1i 6907 |
. . . . . . 7
⊢ ((ℝ
D 𝐶)‘𝑥) = ((𝑥 ∈ (0(,)π) ↦ (sin‘𝑥))‘𝑥) |
| 50 | 42, 7 | sstri 3993 |
. . . . . . . . . 10
⊢
(0(,)π) ⊆ ℂ |
| 51 | 50 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
ℂ) |
| 52 | 51 | sincld 16166 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)π) →
(sin‘𝑥) ∈
ℂ) |
| 53 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)π) ↦
(sin‘𝑥)) = (𝑥 ∈ (0(,)π) ↦
(sin‘𝑥)) |
| 54 | 53 | fvmpt2 7027 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0(,)π) ∧
(sin‘𝑥) ∈
ℂ) → ((𝑥 ∈
(0(,)π) ↦ (sin‘𝑥))‘𝑥) = (sin‘𝑥)) |
| 55 | 52, 54 | mpdan 687 |
. . . . . . 7
⊢ (𝑥 ∈ (0(,)π) →
((𝑥 ∈ (0(,)π)
↦ (sin‘𝑥))‘𝑥) = (sin‘𝑥)) |
| 56 | 49, 55 | eqtrid 2789 |
. . . . . 6
⊢ (𝑥 ∈ (0(,)π) →
((ℝ D 𝐶)‘𝑥) = (sin‘𝑥)) |
| 57 | 56 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (0(,)π)) → ((ℝ D 𝐶)‘𝑥) = (sin‘𝑥)) |
| 58 | 57 | itgeq2dv 25817 |
. . . 4
⊢ (⊤
→ ∫(0(,)π)((ℝ D 𝐶)‘𝑥) d𝑥 = ∫(0(,)π)(sin‘𝑥) d𝑥) |
| 59 | 58 | mptru 1547 |
. . 3
⊢
∫(0(,)π)((ℝ D 𝐶)‘𝑥) d𝑥 = ∫(0(,)π)(sin‘𝑥) d𝑥 |
| 60 | 9 | a1i 11 |
. . . . 5
⊢ (⊤
→ 0 ∈ ℝ) |
| 61 | 10 | a1i 11 |
. . . . 5
⊢ (⊤
→ π ∈ ℝ) |
| 62 | | pipos 26502 |
. . . . . . 7
⊢ 0 <
π |
| 63 | 9, 10, 62 | ltleii 11384 |
. . . . . 6
⊢ 0 ≤
π |
| 64 | 63 | a1i 11 |
. . . . 5
⊢ (⊤
→ 0 ≤ π) |
| 65 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥sin |
| 66 | | sincn 26488 |
. . . . . . . 8
⊢ sin
∈ (ℂ–cn→ℂ) |
| 67 | 66 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ sin ∈ (ℂ–cn→ℂ)) |
| 68 | 50 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (0(,)π) ⊆ ℂ) |
| 69 | 65, 67, 68 | cncfmptss 45602 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ (0(,)π)
↦ (sin‘𝑥))
∈ ((0(,)π)–cn→ℂ)) |
| 70 | 48, 69 | eqeltrid 2845 |
. . . . 5
⊢ (⊤
→ (ℝ D 𝐶) ∈
((0(,)π)–cn→ℂ)) |
| 71 | | ioossicc 13473 |
. . . . . . . 8
⊢
(0(,)π) ⊆ (0[,]π) |
| 72 | 71 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (0(,)π) ⊆ (0[,]π)) |
| 73 | | ioombl 25600 |
. . . . . . . 8
⊢
(0(,)π) ∈ dom vol |
| 74 | 73 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (0(,)π) ∈ dom vol) |
| 75 | 15 | sincld 16166 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]π) →
(sin‘𝑥) ∈
ℂ) |
| 76 | 75 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (0[,]π)) → (sin‘𝑥) ∈ ℂ) |
| 77 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (0[,]π) ⊆ ℂ) |
| 78 | 65, 67, 77 | cncfmptss 45602 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈ (0[,]π)
↦ (sin‘𝑥))
∈ ((0[,]π)–cn→ℂ)) |
| 79 | 78 | mptru 1547 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]π) ↦
(sin‘𝑥)) ∈
((0[,]π)–cn→ℂ) |
| 80 | | cniccibl 25876 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (sin‘𝑥)) ∈
((0[,]π)–cn→ℂ)) →
(𝑥 ∈ (0[,]π)
↦ (sin‘𝑥))
∈ 𝐿1) |
| 81 | 9, 10, 79, 80 | mp3an 1463 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]π) ↦
(sin‘𝑥)) ∈
𝐿1 |
| 82 | 81 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ (0[,]π)
↦ (sin‘𝑥))
∈ 𝐿1) |
| 83 | 72, 74, 76, 82 | iblss 25840 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈ (0(,)π)
↦ (sin‘𝑥))
∈ 𝐿1) |
| 84 | 48, 83 | eqeltrid 2845 |
. . . . 5
⊢ (⊤
→ (ℝ D 𝐶) ∈
𝐿1) |
| 85 | 16 | negcld 11607 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]π) →
-(cos‘𝑥) ∈
ℂ) |
| 86 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) = (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) |
| 87 | 86 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
-(cos‘𝑥) ∈
ℂ) → ((𝑥 ∈
ℂ ↦ -(cos‘𝑥))‘𝑥) = -(cos‘𝑥)) |
| 88 | 15, 85, 87 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0[,]π) →
((𝑥 ∈ ℂ ↦
-(cos‘𝑥))‘𝑥) = -(cos‘𝑥)) |
| 89 | 88 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0[,]π) →
-(cos‘𝑥) = ((𝑥 ∈ ℂ ↦
-(cos‘𝑥))‘𝑥)) |
| 90 | 89 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]π) ↦
-(cos‘𝑥)) = (𝑥 ∈ (0[,]π) ↦
((𝑥 ∈ ℂ ↦
-(cos‘𝑥))‘𝑥)) |
| 91 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ ℂ ↦ -(cos‘𝑥)) |
| 92 | | coscn 26489 |
. . . . . . . . . . . 12
⊢ cos
∈ (ℂ–cn→ℂ) |
| 93 | 86 | negfcncf 24950 |
. . . . . . . . . . . 12
⊢ (cos
∈ (ℂ–cn→ℂ)
→ (𝑥 ∈ ℂ
↦ -(cos‘𝑥))
∈ (ℂ–cn→ℂ)) |
| 94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ ↦
-(cos‘𝑥)) ∈
(ℂ–cn→ℂ) |
| 95 | 94 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈ ℂ
↦ -(cos‘𝑥))
∈ (ℂ–cn→ℂ)) |
| 96 | 91, 95, 77 | cncfmptss 45602 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈ (0[,]π)
↦ ((𝑥 ∈ ℂ
↦ -(cos‘𝑥))‘𝑥)) ∈ ((0[,]π)–cn→ℂ)) |
| 97 | 96 | mptru 1547 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,]π) ↦
((𝑥 ∈ ℂ ↦
-(cos‘𝑥))‘𝑥)) ∈
((0[,]π)–cn→ℂ) |
| 98 | 90, 97 | eqeltri 2837 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,]π) ↦
-(cos‘𝑥)) ∈
((0[,]π)–cn→ℂ) |
| 99 | 5, 98 | eqeltri 2837 |
. . . . . 6
⊢ 𝐶 ∈ ((0[,]π)–cn→ℂ) |
| 100 | 99 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐶 ∈
((0[,]π)–cn→ℂ)) |
| 101 | 60, 61, 64, 70, 84, 100 | ftc2 26085 |
. . . 4
⊢ (⊤
→ ∫(0(,)π)((ℝ D 𝐶)‘𝑥) d𝑥 = ((𝐶‘π) − (𝐶‘0))) |
| 102 | 101 | mptru 1547 |
. . 3
⊢
∫(0(,)π)((ℝ D 𝐶)‘𝑥) d𝑥 = ((𝐶‘π) − (𝐶‘0)) |
| 103 | 59, 102 | eqtr3i 2767 |
. 2
⊢
∫(0(,)π)(sin‘𝑥) d𝑥 = ((𝐶‘π) − (𝐶‘0)) |
| 104 | | 0xr 11308 |
. . . . 5
⊢ 0 ∈
ℝ* |
| 105 | 10 | rexri 11319 |
. . . . 5
⊢ π
∈ ℝ* |
| 106 | | ubicc2 13505 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ 0 ≤
π) → π ∈ (0[,]π)) |
| 107 | 104, 105,
63, 106 | mp3an 1463 |
. . . 4
⊢ π
∈ (0[,]π) |
| 108 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑡 = π → (cos‘𝑡) =
(cos‘π)) |
| 109 | | cospi 26514 |
. . . . . . . 8
⊢
(cos‘π) = -1 |
| 110 | 108, 109 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑡 = π → (cos‘𝑡) = -1) |
| 111 | 110 | negeqd 11502 |
. . . . . 6
⊢ (𝑡 = π → -(cos‘𝑡) = --1) |
| 112 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 113 | 112 | a1i 11 |
. . . . . . 7
⊢ (𝑡 = π → 1 ∈
ℂ) |
| 114 | 113 | negnegd 11611 |
. . . . . 6
⊢ (𝑡 = π → --1 =
1) |
| 115 | 111, 114 | eqtrd 2777 |
. . . . 5
⊢ (𝑡 = π → -(cos‘𝑡) = 1) |
| 116 | | 1ex 11257 |
. . . . 5
⊢ 1 ∈
V |
| 117 | 115, 1, 116 | fvmpt 7016 |
. . . 4
⊢ (π
∈ (0[,]π) → (𝐶‘π) = 1) |
| 118 | 107, 117 | ax-mp 5 |
. . 3
⊢ (𝐶‘π) =
1 |
| 119 | | lbicc2 13504 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ 0 ≤
π) → 0 ∈ (0[,]π)) |
| 120 | 104, 105,
63, 119 | mp3an 1463 |
. . . . 5
⊢ 0 ∈
(0[,]π) |
| 121 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑡 = 0 → (cos‘𝑡) =
(cos‘0)) |
| 122 | 121 | negeqd 11502 |
. . . . . 6
⊢ (𝑡 = 0 → -(cos‘𝑡) =
-(cos‘0)) |
| 123 | | negex 11506 |
. . . . . 6
⊢
-(cos‘0) ∈ V |
| 124 | 122, 1, 123 | fvmpt 7016 |
. . . . 5
⊢ (0 ∈
(0[,]π) → (𝐶‘0) = -(cos‘0)) |
| 125 | 120, 124 | ax-mp 5 |
. . . 4
⊢ (𝐶‘0) =
-(cos‘0) |
| 126 | | cos0 16186 |
. . . . 5
⊢
(cos‘0) = 1 |
| 127 | 126 | negeqi 11501 |
. . . 4
⊢
-(cos‘0) = -1 |
| 128 | 125, 127 | eqtri 2765 |
. . 3
⊢ (𝐶‘0) = -1 |
| 129 | 118, 128 | oveq12i 7443 |
. 2
⊢ ((𝐶‘π) − (𝐶‘0)) = (1 −
-1) |
| 130 | 112, 112 | subnegi 11588 |
. . 3
⊢ (1
− -1) = (1 + 1) |
| 131 | | 1p1e2 12391 |
. . 3
⊢ (1 + 1) =
2 |
| 132 | 130, 131 | eqtri 2765 |
. 2
⊢ (1
− -1) = 2 |
| 133 | 103, 129,
132 | 3eqtri 2769 |
1
⊢
∫(0(,)π)(sin‘𝑥) d𝑥 = 2 |