Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sqwvfoura Structured version   Visualization version   GIF version

Theorem sqwvfoura 42398
Description: Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the 𝐴 coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
sqwvfoura.t 𝑇 = (2 · π)
sqwvfoura.f 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
sqwvfoura.n (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
sqwvfoura (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)
Distinct variable groups:   𝑥,𝑁   𝜑,𝑥
Allowed substitution hints:   𝑇(𝑥)   𝐹(𝑥)

Proof of Theorem sqwvfoura
StepHypRef Expression
1 pire 24978 . . . . . 6 π ∈ ℝ
21renegcli 10941 . . . . 5 -π ∈ ℝ
32a1i 11 . . . 4 (𝜑 → -π ∈ ℝ)
41a1i 11 . . . 4 (𝜑 → π ∈ ℝ)
5 0re 10637 . . . . . 6 0 ∈ ℝ
6 negpilt0 41430 . . . . . . 7 -π < 0
72, 5, 6ltleii 10757 . . . . . 6 -π ≤ 0
8 pipos 24980 . . . . . . 7 0 < π
95, 1, 8ltleii 10757 . . . . . 6 0 ≤ π
102, 1elicc2i 12797 . . . . . 6 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
115, 7, 9, 10mpbir3an 1335 . . . . 5 0 ∈ (-π[,]π)
1211a1i 11 . . . 4 (𝜑 → 0 ∈ (-π[,]π))
13 1red 10636 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 1 ∈ ℝ)
1413renegcld 11061 . . . . . . . . . . 11 (𝑥 ∈ ℝ → -1 ∈ ℝ)
1513, 14ifcld 4515 . . . . . . . . . 10 (𝑥 ∈ ℝ → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
1615adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
17 sqwvfoura.f . . . . . . . . 9 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
1816, 17fmptd 6876 . . . . . . . 8 (𝜑𝐹:ℝ⟶ℝ)
1918adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝐹:ℝ⟶ℝ)
20 elioore 12763 . . . . . . . 8 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
2120adantl 482 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℝ)
2219, 21ffvelrnd 6850 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (𝐹𝑥) ∈ ℝ)
23 sqwvfoura.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
2423nn0red 11950 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ)
2524adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑁 ∈ ℝ)
2625, 21remulcld 10665 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
2726recoscld 15492 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
2822, 27remulcld 10665 . . . . 5 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℝ)
2928recnd 10663 . . . 4 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℂ)
30 elioore 12763 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℝ)
3117fvmpt2 6777 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
3230, 15, 31syl2anc2 585 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
331a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π ∈ ℝ)
34 sqwvfoura.t . . . . . . . . . . . . . 14 𝑇 = (2 · π)
35 2rp 12389 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
36 pirp 24981 . . . . . . . . . . . . . . 15 π ∈ ℝ+
37 rpmulcl 12407 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
3835, 36, 37mp2an 688 . . . . . . . . . . . . . 14 (2 · π) ∈ ℝ+
3934, 38eqeltri 2914 . . . . . . . . . . . . 13 𝑇 ∈ ℝ+
4039a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ+)
4130, 40modcld 13238 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → (𝑥 mod 𝑇) ∈ ℝ)
42 picn 24979 . . . . . . . . . . . . . . . . 17 π ∈ ℂ
43422timesi 11769 . . . . . . . . . . . . . . . 16 (2 · π) = (π + π)
4434, 43eqtri 2849 . . . . . . . . . . . . . . 15 𝑇 = (π + π)
4544oveq2i 7161 . . . . . . . . . . . . . 14 (-π + 𝑇) = (-π + (π + π))
462recni 10649 . . . . . . . . . . . . . . 15 -π ∈ ℂ
4746, 42, 42addassi 10645 . . . . . . . . . . . . . 14 ((-π + π) + π) = (-π + (π + π))
4842negidi 10949 . . . . . . . . . . . . . . . . 17 (π + -π) = 0
4942, 46, 48addcomli 10826 . . . . . . . . . . . . . . . 16 (-π + π) = 0
5049oveq1i 7160 . . . . . . . . . . . . . . 15 ((-π + π) + π) = (0 + π)
5142addid2i 10822 . . . . . . . . . . . . . . 15 (0 + π) = π
5250, 51eqtri 2849 . . . . . . . . . . . . . 14 ((-π + π) + π) = π
5345, 47, 523eqtr2ri 2856 . . . . . . . . . . . . 13 π = (-π + 𝑇)
542a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ)
55 2re 11705 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
5655, 1remulcli 10651 . . . . . . . . . . . . . . . 16 (2 · π) ∈ ℝ
5734, 56eqeltri 2914 . . . . . . . . . . . . . . 15 𝑇 ∈ ℝ
5857a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ)
592rexri 10693 . . . . . . . . . . . . . . . 16 -π ∈ ℝ*
6059a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ*)
61 0red 10638 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ)
6261rexrd 10685 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ*)
63 id 22 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ (-π(,)0))
64 ioogtlb 41654 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → -π < 𝑥)
6560, 62, 63, 64syl3anc 1365 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π < 𝑥)
6654, 30, 58, 65ltadd1dd 11245 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → (-π + 𝑇) < (𝑥 + 𝑇))
6753, 66eqbrtrid 5098 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → π < (𝑥 + 𝑇))
6857recni 10649 . . . . . . . . . . . . . . . . 17 𝑇 ∈ ℂ
6968mulid2i 10640 . . . . . . . . . . . . . . . 16 (1 · 𝑇) = 𝑇
7069eqcomi 2835 . . . . . . . . . . . . . . 15 𝑇 = (1 · 𝑇)
7170oveq2i 7161 . . . . . . . . . . . . . 14 (𝑥 + 𝑇) = (𝑥 + (1 · 𝑇))
7271oveq1i 7160 . . . . . . . . . . . . 13 ((𝑥 + 𝑇) mod 𝑇) = ((𝑥 + (1 · 𝑇)) mod 𝑇)
7330, 58readdcld 10664 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) ∈ ℝ)
748a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 < π)
7561, 33, 73, 74, 67lttrd 10795 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 < (𝑥 + 𝑇))
7661, 73, 75ltled 10782 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 0 ≤ (𝑥 + 𝑇))
77 iooltub 41670 . . . . . . . . . . . . . . . . 17 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → 𝑥 < 0)
7860, 62, 63, 77syl3anc 1365 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑥 < 0)
7930, 61, 58, 78ltadd1dd 11245 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < (0 + 𝑇))
8068a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℂ)
8180addid2d 10835 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (0 + 𝑇) = 𝑇)
8279, 81breqtrd 5089 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < 𝑇)
83 modid 13259 . . . . . . . . . . . . . 14 ((((𝑥 + 𝑇) ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ (𝑥 + 𝑇) ∧ (𝑥 + 𝑇) < 𝑇)) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
8473, 40, 76, 82, 83syl22anc 836 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
85 1zzd 12007 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 1 ∈ ℤ)
86 modcyc 13269 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8730, 40, 85, 86syl3anc 1365 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8872, 84, 873eqtr3a 2885 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) = (𝑥 mod 𝑇))
8967, 88breqtrd 5089 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π < (𝑥 mod 𝑇))
9033, 41, 89ltnsymd 10783 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → ¬ (𝑥 mod 𝑇) < π)
9190iffalsed 4481 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) = -1)
9232, 91eqtrd 2861 . . . . . . . 8 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = -1)
9392oveq1d 7165 . . . . . . 7 (𝑥 ∈ (-π(,)0) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
9493adantl 482 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
9594mpteq2dva 5158 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))))
96 1cnd 10630 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
9796negcld 10978 . . . . . 6 (𝜑 → -1 ∈ ℂ)
9824adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑁 ∈ ℝ)
9930adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑥 ∈ ℝ)
10098, 99remulcld 10665 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) ∈ ℝ)
101100recoscld 15492 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
102 ioossicc 12817 . . . . . . . 8 (-π(,)0) ⊆ (-π[,]0)
103102a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ⊆ (-π[,]0))
104 ioombl 24100 . . . . . . . 8 (-π(,)0) ∈ dom vol
105104a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ∈ dom vol)
10624adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑁 ∈ ℝ)
107 iccssre 12813 . . . . . . . . . . . 12 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (-π[,]0) ⊆ ℝ)
1082, 5, 107mp2an 688 . . . . . . . . . . 11 (-π[,]0) ⊆ ℝ
109108sseli 3967 . . . . . . . . . 10 (𝑥 ∈ (-π[,]0) → 𝑥 ∈ ℝ)
110109adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑥 ∈ ℝ)
111106, 110remulcld 10665 . . . . . . . 8 ((𝜑𝑥 ∈ (-π[,]0)) → (𝑁 · 𝑥) ∈ ℝ)
112111recoscld 15492 . . . . . . 7 ((𝜑𝑥 ∈ (-π[,]0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
113 0red 10638 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
114 coscn 24967 . . . . . . . . . 10 cos ∈ (ℂ–cn→ℂ)
115114a1i 11 . . . . . . . . 9 (𝜑 → cos ∈ (ℂ–cn→ℂ))
116 ax-resscn 10588 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
117108, 116sstri 3980 . . . . . . . . . . . 12 (-π[,]0) ⊆ ℂ
118117a1i 11 . . . . . . . . . . 11 (𝜑 → (-π[,]0) ⊆ ℂ)
11924recnd 10663 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
120 ssid 3993 . . . . . . . . . . . 12 ℂ ⊆ ℂ
121120a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ⊆ ℂ)
122118, 119, 121constcncfg 42038 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑁) ∈ ((-π[,]0)–cn→ℂ))
123118, 121idcncfg 42039 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑥) ∈ ((-π[,]0)–cn→ℂ))
124122, 123mulcncf 23981 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (𝑁 · 𝑥)) ∈ ((-π[,]0)–cn→ℂ))
125115, 124cncfmpt1f 23455 . . . . . . . 8 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ))
126 cniccibl 24375 . . . . . . . 8 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ)) → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
1273, 113, 125, 126syl3anc 1365 . . . . . . 7 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
128103, 105, 112, 127iblss 24339 . . . . . 6 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
12997, 101, 128iblmulc2 24365 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
13095, 129eqeltrd 2918 . . . 4 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
131 elioore 12763 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℝ)
132131, 15, 31syl2anc2 585 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
13339a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ+)
134 0red 10638 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ)
135134rexrd 10685 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ*)
1361rexri 10693 . . . . . . . . . . . . . . 15 π ∈ ℝ*
137136a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → π ∈ ℝ*)
138 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 𝑥 ∈ (0(,)π))
139 ioogtlb 41654 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 0 < 𝑥)
140135, 137, 138, 139syl3anc 1365 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 < 𝑥)
141134, 131, 140ltled 10782 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 0 ≤ 𝑥)
1421a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → π ∈ ℝ)
14357a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ)
144 iooltub 41670 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 𝑥 < π)
145135, 137, 138, 144syl3anc 1365 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑥 < π)
146 2timesgt 41438 . . . . . . . . . . . . . . . 16 (π ∈ ℝ+ → π < (2 · π))
14736, 146ax-mp 5 . . . . . . . . . . . . . . 15 π < (2 · π)
148147, 34breqtrri 5090 . . . . . . . . . . . . . 14 π < 𝑇
149148a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → π < 𝑇)
150131, 142, 143, 145, 149lttrd 10795 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 𝑥 < 𝑇)
151 modid 13259 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ 𝑥𝑥 < 𝑇)) → (𝑥 mod 𝑇) = 𝑥)
152131, 133, 141, 150, 151syl22anc 836 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) = 𝑥)
153152, 145eqbrtrd 5085 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) < π)
154153iftrued 4478 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) = 1)
155132, 154eqtrd 2861 . . . . . . . 8 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = 1)
156155oveq1d 7165 . . . . . . 7 (𝑥 ∈ (0(,)π) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
157156adantl 482 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
158157mpteq2dva 5158 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))))
15924adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℝ)
160131adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℝ)
161159, 160remulcld 10665 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
162161recoscld 15492 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
163 ioossicc 12817 . . . . . . . 8 (0(,)π) ⊆ (0[,]π)
164163a1i 11 . . . . . . 7 (𝜑 → (0(,)π) ⊆ (0[,]π))
165 ioombl 24100 . . . . . . . 8 (0(,)π) ∈ dom vol
166165a1i 11 . . . . . . 7 (𝜑 → (0(,)π) ∈ dom vol)
16724adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℝ)
168 iccssre 12813 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
1695, 1, 168mp2an 688 . . . . . . . . . . 11 (0[,]π) ⊆ ℝ
170169sseli 3967 . . . . . . . . . 10 (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℝ)
171170adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℝ)
172167, 171remulcld 10665 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → (𝑁 · 𝑥) ∈ ℝ)
173172recoscld 15492 . . . . . . 7 ((𝜑𝑥 ∈ (0[,]π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
174169, 116sstri 3980 . . . . . . . . . . . 12 (0[,]π) ⊆ ℂ
175174a1i 11 . . . . . . . . . . 11 (𝜑 → (0[,]π) ⊆ ℂ)
176175, 119, 121constcncfg 42038 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑁) ∈ ((0[,]π)–cn→ℂ))
177175, 121idcncfg 42039 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑥) ∈ ((0[,]π)–cn→ℂ))
178176, 177mulcncf 23981 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑁 · 𝑥)) ∈ ((0[,]π)–cn→ℂ))
179115, 178cncfmpt1f 23455 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ))
180 cniccibl 24375 . . . . . . . 8 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
181113, 4, 179, 180syl3anc 1365 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
182164, 166, 173, 181iblss 24339 . . . . . 6 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
18396, 162, 182iblmulc2 24365 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
184158, 183eqeltrd 2918 . . . 4 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
1853, 4, 12, 29, 130, 184itgsplitioo 24372 . . 3 (𝜑 → ∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = (∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥))
186185oveq1d 7165 . 2 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = ((∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π))
18794itgeq2dv 24316 . . . . 5 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
18897, 101, 128itgmulc2 24368 . . . . 5 (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
189 oveq1 7157 . . . . . . . . . . . . . 14 (𝑁 = 0 → (𝑁 · 𝑥) = (0 · 𝑥))
190 ioosscn 41653 . . . . . . . . . . . . . . . 16 (-π(,)0) ⊆ ℂ
191190sseli 3967 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℂ)
192191mul02d 10832 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (0 · 𝑥) = 0)
193189, 192sylan9eq 2881 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) = 0)
194193fveq2d 6673 . . . . . . . . . . . 12 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
195 cos0 15498 . . . . . . . . . . . 12 (cos‘0) = 1
196194, 195syl6eq 2877 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
197196adantll 710 . . . . . . . . . 10 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
198197itgeq2dv 24316 . . . . . . . . 9 ((𝜑𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(-π(,)0)1 d𝑥)
199 ioovolcl 24105 . . . . . . . . . . . . 13 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (vol‘(-π(,)0)) ∈ ℝ)
2002, 5, 199mp2an 688 . . . . . . . . . . . 12 (vol‘(-π(,)0)) ∈ ℝ
201200a1i 11 . . . . . . . . . . 11 (𝜑 → (vol‘(-π(,)0)) ∈ ℝ)
202 itgconst 24353 . . . . . . . . . . 11 (((-π(,)0) ∈ dom vol ∧ (vol‘(-π(,)0)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
203105, 201, 96, 202syl3anc 1365 . . . . . . . . . 10 (𝜑 → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
204203adantr 481 . . . . . . . . 9 ((𝜑𝑁 = 0) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
205 volioo 24104 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ -π ≤ 0) → (vol‘(-π(,)0)) = (0 − -π))
2062, 5, 7, 205mp3an 1454 . . . . . . . . . . . . . 14 (vol‘(-π(,)0)) = (0 − -π)
207 0cn 10627 . . . . . . . . . . . . . . 15 0 ∈ ℂ
208207, 42subnegi 10959 . . . . . . . . . . . . . 14 (0 − -π) = (0 + π)
209206, 208, 513eqtri 2853 . . . . . . . . . . . . 13 (vol‘(-π(,)0)) = π
210209a1i 11 . . . . . . . . . . . 12 (𝜑 → (vol‘(-π(,)0)) = π)
211210oveq2d 7166 . . . . . . . . . . 11 (𝜑 → (1 · (vol‘(-π(,)0))) = (1 · π))
21242a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℂ)
213212mulid2d 10653 . . . . . . . . . . 11 (𝜑 → (1 · π) = π)
214211, 213eqtrd 2861 . . . . . . . . . 10 (𝜑 → (1 · (vol‘(-π(,)0))) = π)
215214adantr 481 . . . . . . . . 9 ((𝜑𝑁 = 0) → (1 · (vol‘(-π(,)0))) = π)
216198, 204, 2153eqtrd 2865 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = π)
217216oveq2d 7166 . . . . . . 7 ((𝜑𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · π))
21842mulm1i 11079 . . . . . . . 8 (-1 · π) = -π
219218a1i 11 . . . . . . 7 ((𝜑𝑁 = 0) → (-1 · π) = -π)
220 iftrue 4476 . . . . . . . . 9 (𝑁 = 0 → if(𝑁 = 0, -π, 0) = -π)
221220eqcomd 2832 . . . . . . . 8 (𝑁 = 0 → -π = if(𝑁 = 0, -π, 0))
222221adantl 482 . . . . . . 7 ((𝜑𝑁 = 0) → -π = if(𝑁 = 0, -π, 0))
223217, 219, 2223eqtrd 2865 . . . . . 6 ((𝜑𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
22424adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℝ)
22523nn0ge0d 11952 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑁)
226225adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 0 ≤ 𝑁)
227 neqne 3029 . . . . . . . . 9 𝑁 = 0 → 𝑁 ≠ 0)
228227adantl 482 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
229224, 226, 228ne0gt0d 10771 . . . . . . 7 ((𝜑 ∧ ¬ 𝑁 = 0) → 0 < 𝑁)
230 1cnd 10630 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → 1 ∈ ℂ)
231230negcld 10978 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → -1 ∈ ℂ)
232231mul01d 10833 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → (-1 · 0) = 0)
233119adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 𝑁 ∈ ℂ)
2342a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → -π ∈ ℝ)
235 0red 10638 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 0 ∈ ℝ)
2367a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → -π ≤ 0)
237 simpr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < 𝑁) → 0 < 𝑁)
238237gt0ne0d 11198 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 𝑁 ≠ 0)
239233, 234, 235, 236, 238itgcoscmulx 42138 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁))
240119mul01d 10833 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · 0) = 0)
241240fveq2d 6673 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘(𝑁 · 0)) = (sin‘0))
242 sin0 15497 . . . . . . . . . . . . . . 15 (sin‘0) = 0
243241, 242syl6eq 2877 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · 0)) = 0)
244119, 212mulneg2d 11088 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · -π) = -(𝑁 · π))
245244fveq2d 6673 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘(𝑁 · -π)) = (sin‘-(𝑁 · π)))
246119, 212mulcld 10655 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · π) ∈ ℂ)
247 sinneg 15494 . . . . . . . . . . . . . . . 16 ((𝑁 · π) ∈ ℂ → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
248246, 247syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
249245, 248eqtrd 2861 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · -π)) = -(sin‘(𝑁 · π)))
250243, 249oveq12d 7168 . . . . . . . . . . . . 13 (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (0 − -(sin‘(𝑁 · π))))
251 0cnd 10628 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ ℂ)
252246sincld 15478 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · π)) ∈ ℂ)
253251, 252subnegd 10998 . . . . . . . . . . . . 13 (𝜑 → (0 − -(sin‘(𝑁 · π))) = (0 + (sin‘(𝑁 · π))))
254252addid2d 10835 . . . . . . . . . . . . 13 (𝜑 → (0 + (sin‘(𝑁 · π))) = (sin‘(𝑁 · π)))
255250, 253, 2543eqtrd 2865 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
256255adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
257256oveq1d 7165 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁) = ((sin‘(𝑁 · π)) / 𝑁))
25823nn0zd 12079 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
259 sinkpi 25041 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (sin‘(𝑁 · π)) = 0)
260258, 259syl 17 . . . . . . . . . . . . 13 (𝜑 → (sin‘(𝑁 · π)) = 0)
261260oveq1d 7165 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
262261adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
263233, 238div0d 11409 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → (0 / 𝑁) = 0)
264262, 263eqtrd 2861 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = 0)
265239, 257, 2643eqtrd 2865 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = 0)
266265oveq2d 7166 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · 0))
267238neneqd 3026 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
268267iffalsed 4481 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, -π, 0) = 0)
269232, 266, 2683eqtr4d 2871 . . . . . . 7 ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
270229, 269syldan 591 . . . . . 6 ((𝜑 ∧ ¬ 𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
271223, 270pm2.61dan 809 . . . . 5 (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
272187, 188, 2713eqtr2d 2867 . . . 4 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, -π, 0))
273157itgeq2dv 24316 . . . . 5 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
27496, 162, 182itgmulc2 24368 . . . . 5 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
275162, 182itgcl 24318 . . . . . . 7 (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 ∈ ℂ)
276275mulid2d 10653 . . . . . 6 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥)
277 simpl 483 . . . . . . . . . . . . . 14 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 = 0)
278277oveq1d 7165 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = (0 · 𝑥))
279131recnd 10663 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℂ)
280279adantl 482 . . . . . . . . . . . . . 14 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℂ)
281280mul02d 10832 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (0 · 𝑥) = 0)
282278, 281eqtrd 2861 . . . . . . . . . . . 12 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = 0)
283282fveq2d 6673 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
284283, 195syl6eq 2877 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
285284adantll 710 . . . . . . . . 9 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
286285itgeq2dv 24316 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(0(,)π)1 d𝑥)
287 ioovolcl 24105 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ π ∈ ℝ) → (vol‘(0(,)π)) ∈ ℝ)
2885, 1, 287mp2an 688 . . . . . . . . . 10 (vol‘(0(,)π)) ∈ ℝ
289 ax-1cn 10589 . . . . . . . . . 10 1 ∈ ℂ
290 itgconst 24353 . . . . . . . . . 10 (((0(,)π) ∈ dom vol ∧ (vol‘(0(,)π)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
291165, 288, 289, 290mp3an 1454 . . . . . . . . 9 ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π)))
292291a1i 11 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
29342mulid2i 10640 . . . . . . . . . 10 (1 · π) = π
294 volioo 24104 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ 0 ≤ π) → (vol‘(0(,)π)) = (π − 0))
2955, 1, 9, 294mp3an 1454 . . . . . . . . . . . . 13 (vol‘(0(,)π)) = (π − 0)
29642subid1i 10952 . . . . . . . . . . . . 13 (π − 0) = π
297295, 296eqtri 2849 . . . . . . . . . . . 12 (vol‘(0(,)π)) = π
298297oveq2i 7161 . . . . . . . . . . 11 (1 · (vol‘(0(,)π))) = (1 · π)
299298a1i 11 . . . . . . . . . 10 (𝑁 = 0 → (1 · (vol‘(0(,)π))) = (1 · π))
300 iftrue 4476 . . . . . . . . . 10 (𝑁 = 0 → if(𝑁 = 0, π, 0) = π)
301293, 299, 3003eqtr4a 2887 . . . . . . . . 9 (𝑁 = 0 → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
302301adantl 482 . . . . . . . 8 ((𝜑𝑁 = 0) → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
303286, 292, 3023eqtrd 2865 . . . . . . 7 ((𝜑𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
304260, 243oveq12d 7168 . . . . . . . . . . . . 13 (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = (0 − 0))
305251subidd 10979 . . . . . . . . . . . . 13 (𝜑 → (0 − 0) = 0)
306304, 305eqtrd 2861 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = 0)
307306oveq1d 7165 . . . . . . . . . . 11 (𝜑 → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
308307adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
309308, 263eqtrd 2861 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = 0)
3101a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → π ∈ ℝ)
3119a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → 0 ≤ π)
312233, 235, 310, 311, 238itgcoscmulx 42138 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁))
313267iffalsed 4481 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, π, 0) = 0)
314309, 312, 3133eqtr4d 2871 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
315229, 314syldan 591 . . . . . . 7 ((𝜑 ∧ ¬ 𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
316303, 315pm2.61dan 809 . . . . . 6 (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
317276, 316eqtrd 2861 . . . . 5 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, π, 0))
318273, 274, 3173eqtr2d 2867 . . . 4 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, π, 0))
319272, 318oveq12d 7168 . . 3 (𝜑 → (∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) = (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)))
320319oveq1d 7165 . 2 (𝜑 → ((∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π) = ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π))
321220, 300oveq12d 7168 . . . . . . 7 (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (-π + π))
322321, 49syl6eq 2877 . . . . . 6 (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
323 iffalse 4479 . . . . . . . 8 𝑁 = 0 → if(𝑁 = 0, -π, 0) = 0)
324 iffalse 4479 . . . . . . . 8 𝑁 = 0 → if(𝑁 = 0, π, 0) = 0)
325323, 324oveq12d 7168 . . . . . . 7 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (0 + 0))
326 00id 10809 . . . . . . 7 (0 + 0) = 0
327325, 326syl6eq 2877 . . . . . 6 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
328322, 327pm2.61i 183 . . . . 5 (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0
329328oveq1i 7160 . . . 4 ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = (0 / π)
3305, 8gtneii 10746 . . . . 5 π ≠ 0
33142, 330div0i 11368 . . . 4 (0 / π) = 0
332329, 331eqtri 2849 . . 3 ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0
333332a1i 11 . 2 (𝜑 → ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0)
334186, 320, 3333eqtrd 2865 1 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1530  wcel 2107  wne 3021  wss 3940  ifcif 4470   class class class wbr 5063  cmpt 5143  dom cdm 5554  wf 6350  cfv 6354  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  *cxr 10668   < clt 10669  cle 10670  cmin 10864  -cneg 10865   / cdiv 11291  2c2 11686  0cn0 11891  cz 11975  +crp 12384  (,)cioo 12733  [,]cicc 12736   mod cmo 13232  sincsin 15412  cosccos 15413  πcpi 15415  cnccncf 23418  volcvol 23998  𝐿1cibl 24152  citg 24153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cc 9851  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-symdif 4223  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-disj 5029  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-ofr 7404  df-om 7574  df-1st 7685  df-2nd 7686  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8284  df-map 8403  df-pm 8404  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-fi 8869  df-sup 8900  df-inf 8901  df-oi 8968  df-dju 9324  df-card 9362  df-acn 9365  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-q 12343  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ioc 12738  df-ico 12739  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13425  df-fac 13629  df-bc 13658  df-hash 13686  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18170  df-cntz 18392  df-cmn 18844  df-psmet 20472  df-xmet 20473  df-met 20474  df-bl 20475  df-mopn 20476  df-fbas 20477  df-fg 20478  df-cnfld 20481  df-top 21437  df-topon 21454  df-topsp 21476  df-bases 21489  df-cld 21562  df-ntr 21563  df-cls 21564  df-nei 21641  df-lp 21679  df-perf 21680  df-cn 21770  df-cnp 21771  df-haus 21858  df-cmp 21930  df-tx 22105  df-hmeo 22298  df-fil 22389  df-fm 22481  df-flim 22482  df-flf 22483  df-xms 22864  df-ms 22865  df-tms 22866  df-cncf 23420  df-ovol 23999  df-vol 24000  df-mbf 24154  df-itg1 24155  df-itg2 24156  df-ibl 24157  df-itg 24158  df-0p 24205  df-limc 24398  df-dv 24399
This theorem is referenced by:  fouriersw  42401
  Copyright terms: Public domain W3C validator