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

Theorem sqwvfoura 39121
 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 24014 . . . . . 6 π ∈ ℝ
21renegcli 10221 . . . . 5 -π ∈ ℝ
32a1i 11 . . . 4 (𝜑 → -π ∈ ℝ)
41a1i 11 . . . 4 (𝜑 → π ∈ ℝ)
5 0re 9919 . . . . . 6 0 ∈ ℝ
6 negpilt0 38433 . . . . . . 7 -π < 0
72, 5, 6ltleii 10039 . . . . . 6 -π ≤ 0
8 pipos 24016 . . . . . . 7 0 < π
95, 1, 8ltleii 10039 . . . . . 6 0 ≤ π
102, 1elicc2i 12110 . . . . . 6 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
115, 7, 9, 10mpbir3an 1237 . . . . 5 0 ∈ (-π[,]π)
1211a1i 11 . . . 4 (𝜑 → 0 ∈ (-π[,]π))
13 1red 9934 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 1 ∈ ℝ)
1413renegcld 10336 . . . . . . . . . . 11 (𝑥 ∈ ℝ → -1 ∈ ℝ)
1513, 14ifcld 4081 . . . . . . . . . 10 (𝑥 ∈ ℝ → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
1615adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
17 sqwvfoura.f . . . . . . . . 9 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
1816, 17fmptd 6292 . . . . . . . 8 (𝜑𝐹:ℝ⟶ℝ)
1918adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝐹:ℝ⟶ℝ)
20 elioore 12076 . . . . . . . 8 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
2120adantl 481 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℝ)
2219, 21ffvelrnd 6268 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (𝐹𝑥) ∈ ℝ)
23 sqwvfoura.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
2423nn0red 11229 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ)
2524adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑁 ∈ ℝ)
2625, 21remulcld 9949 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
2726recoscld 14713 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
2822, 27remulcld 9949 . . . . 5 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℝ)
2928recnd 9947 . . . 4 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℂ)
30 elioore 12076 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℝ)
3130, 15syl 17 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
3217fvmpt2 6200 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
3330, 31, 32syl2anc 691 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
341a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π ∈ ℝ)
35 sqwvfoura.t . . . . . . . . . . . . . 14 𝑇 = (2 · π)
36 2rp 11713 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
37 pirp 24017 . . . . . . . . . . . . . . 15 π ∈ ℝ+
38 rpmulcl 11731 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
3936, 37, 38mp2an 704 . . . . . . . . . . . . . 14 (2 · π) ∈ ℝ+
4035, 39eqeltri 2684 . . . . . . . . . . . . 13 𝑇 ∈ ℝ+
4140a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ+)
4230, 41modcld 12536 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → (𝑥 mod 𝑇) ∈ ℝ)
43 picn 24015 . . . . . . . . . . . . . . . . 17 π ∈ ℂ
44432timesi 11024 . . . . . . . . . . . . . . . 16 (2 · π) = (π + π)
4535, 44eqtri 2632 . . . . . . . . . . . . . . 15 𝑇 = (π + π)
4645oveq2i 6560 . . . . . . . . . . . . . 14 (-π + 𝑇) = (-π + (π + π))
472recni 9931 . . . . . . . . . . . . . . 15 -π ∈ ℂ
4847, 43, 43addassi 9927 . . . . . . . . . . . . . 14 ((-π + π) + π) = (-π + (π + π))
4943negidi 10229 . . . . . . . . . . . . . . . . 17 (π + -π) = 0
5043, 47, 49addcomli 10107 . . . . . . . . . . . . . . . 16 (-π + π) = 0
5150oveq1i 6559 . . . . . . . . . . . . . . 15 ((-π + π) + π) = (0 + π)
5243addid2i 10103 . . . . . . . . . . . . . . 15 (0 + π) = π
5351, 52eqtri 2632 . . . . . . . . . . . . . 14 ((-π + π) + π) = π
5446, 48, 533eqtr2ri 2639 . . . . . . . . . . . . 13 π = (-π + 𝑇)
552a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ)
56 2re 10967 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
5756, 1remulcli 9933 . . . . . . . . . . . . . . . 16 (2 · π) ∈ ℝ
5835, 57eqeltri 2684 . . . . . . . . . . . . . . 15 𝑇 ∈ ℝ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ)
602rexri 9976 . . . . . . . . . . . . . . . 16 -π ∈ ℝ*
6160a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ*)
62 0red 9920 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ)
6362rexrd 9968 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ*)
64 id 22 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ (-π(,)0))
65 ioogtlb 38564 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → -π < 𝑥)
6661, 63, 64, 65syl3anc 1318 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π < 𝑥)
6755, 30, 59, 66ltadd1dd 10517 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → (-π + 𝑇) < (𝑥 + 𝑇))
6854, 67syl5eqbr 4618 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → π < (𝑥 + 𝑇))
6958recni 9931 . . . . . . . . . . . . . . . . 17 𝑇 ∈ ℂ
7069mulid2i 9922 . . . . . . . . . . . . . . . 16 (1 · 𝑇) = 𝑇
7170eqcomi 2619 . . . . . . . . . . . . . . 15 𝑇 = (1 · 𝑇)
7271oveq2i 6560 . . . . . . . . . . . . . 14 (𝑥 + 𝑇) = (𝑥 + (1 · 𝑇))
7372oveq1i 6559 . . . . . . . . . . . . 13 ((𝑥 + 𝑇) mod 𝑇) = ((𝑥 + (1 · 𝑇)) mod 𝑇)
7430, 59readdcld 9948 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) ∈ ℝ)
758a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 < π)
7662, 34, 74, 75, 68lttrd 10077 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 < (𝑥 + 𝑇))
7762, 74, 76ltled 10064 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 0 ≤ (𝑥 + 𝑇))
78 iooltub 38582 . . . . . . . . . . . . . . . . 17 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → 𝑥 < 0)
7961, 63, 64, 78syl3anc 1318 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑥 < 0)
8030, 62, 59, 79ltadd1dd 10517 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < (0 + 𝑇))
8169a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℂ)
8281addid2d 10116 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (0 + 𝑇) = 𝑇)
8380, 82breqtrd 4609 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < 𝑇)
84 modid 12557 . . . . . . . . . . . . . 14 ((((𝑥 + 𝑇) ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ (𝑥 + 𝑇) ∧ (𝑥 + 𝑇) < 𝑇)) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
8574, 41, 77, 83, 84syl22anc 1319 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
86 1zzd 11285 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 1 ∈ ℤ)
87 modcyc 12567 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8830, 41, 86, 87syl3anc 1318 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8973, 85, 883eqtr3a 2668 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) = (𝑥 mod 𝑇))
9068, 89breqtrd 4609 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π < (𝑥 mod 𝑇))
9134, 42, 90ltnsymd 10065 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → ¬ (𝑥 mod 𝑇) < π)
9291iffalsed 4047 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) = -1)
9333, 92eqtrd 2644 . . . . . . . 8 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = -1)
9493oveq1d 6564 . . . . . . 7 (𝑥 ∈ (-π(,)0) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
9594adantl 481 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
9695mpteq2dva 4672 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))))
97 1cnd 9935 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
9897negcld 10258 . . . . . 6 (𝜑 → -1 ∈ ℂ)
9924adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑁 ∈ ℝ)
10030adantl 481 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑥 ∈ ℝ)
10199, 100remulcld 9949 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) ∈ ℝ)
102101recoscld 14713 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
103 ioossicc 12130 . . . . . . . 8 (-π(,)0) ⊆ (-π[,]0)
104103a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ⊆ (-π[,]0))
105 ioombl 23140 . . . . . . . 8 (-π(,)0) ∈ dom vol
106105a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ∈ dom vol)
10724adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑁 ∈ ℝ)
108 iccssre 12126 . . . . . . . . . . . 12 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (-π[,]0) ⊆ ℝ)
1092, 5, 108mp2an 704 . . . . . . . . . . 11 (-π[,]0) ⊆ ℝ
110109sseli 3564 . . . . . . . . . 10 (𝑥 ∈ (-π[,]0) → 𝑥 ∈ ℝ)
111110adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑥 ∈ ℝ)
112107, 111remulcld 9949 . . . . . . . 8 ((𝜑𝑥 ∈ (-π[,]0)) → (𝑁 · 𝑥) ∈ ℝ)
113112recoscld 14713 . . . . . . 7 ((𝜑𝑥 ∈ (-π[,]0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
114 0red 9920 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
115 coscn 24003 . . . . . . . . . 10 cos ∈ (ℂ–cn→ℂ)
116115a1i 11 . . . . . . . . 9 (𝜑 → cos ∈ (ℂ–cn→ℂ))
117 ax-resscn 9872 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
118109, 117sstri 3577 . . . . . . . . . . . 12 (-π[,]0) ⊆ ℂ
119118a1i 11 . . . . . . . . . . 11 (𝜑 → (-π[,]0) ⊆ ℂ)
12024recnd 9947 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
121 ssid 3587 . . . . . . . . . . . 12 ℂ ⊆ ℂ
122121a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ⊆ ℂ)
123119, 120, 122constcncfg 38756 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑁) ∈ ((-π[,]0)–cn→ℂ))
124119, 122idcncfg 38757 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑥) ∈ ((-π[,]0)–cn→ℂ))
125123, 124mulcncf 23023 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (𝑁 · 𝑥)) ∈ ((-π[,]0)–cn→ℂ))
126116, 125cncfmpt1f 22524 . . . . . . . 8 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ))
127 cniccibl 23413 . . . . . . . 8 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ)) → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
1283, 114, 126, 127syl3anc 1318 . . . . . . 7 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
129104, 106, 113, 128iblss 23377 . . . . . 6 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
13098, 102, 129iblmulc2 23403 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
13196, 130eqeltrd 2688 . . . 4 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
132 elioore 12076 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℝ)
133132, 15syl 17 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
134132, 133, 32syl2anc 691 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
13540a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ+)
136 0red 9920 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ)
137136rexrd 9968 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ*)
1381rexri 9976 . . . . . . . . . . . . . . 15 π ∈ ℝ*
139138a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → π ∈ ℝ*)
140 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 𝑥 ∈ (0(,)π))
141 ioogtlb 38564 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 0 < 𝑥)
142137, 139, 140, 141syl3anc 1318 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 < 𝑥)
143136, 132, 142ltled 10064 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 0 ≤ 𝑥)
1441a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → π ∈ ℝ)
14558a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ)
146 iooltub 38582 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 𝑥 < π)
147137, 139, 140, 146syl3anc 1318 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑥 < π)
148 2timesgt 38441 . . . . . . . . . . . . . . . 16 (π ∈ ℝ+ → π < (2 · π))
14937, 148ax-mp 5 . . . . . . . . . . . . . . 15 π < (2 · π)
150149, 35breqtrri 4610 . . . . . . . . . . . . . 14 π < 𝑇
151150a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → π < 𝑇)
152132, 144, 145, 147, 151lttrd 10077 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 𝑥 < 𝑇)
153 modid 12557 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ 𝑥𝑥 < 𝑇)) → (𝑥 mod 𝑇) = 𝑥)
154132, 135, 143, 152, 153syl22anc 1319 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) = 𝑥)
155154, 147eqbrtrd 4605 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) < π)
156155iftrued 4044 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) = 1)
157134, 156eqtrd 2644 . . . . . . . 8 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = 1)
158157oveq1d 6564 . . . . . . 7 (𝑥 ∈ (0(,)π) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
159158adantl 481 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
160159mpteq2dva 4672 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))))
16124adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℝ)
162132adantl 481 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℝ)
163161, 162remulcld 9949 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
164163recoscld 14713 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
165 ioossicc 12130 . . . . . . . 8 (0(,)π) ⊆ (0[,]π)
166165a1i 11 . . . . . . 7 (𝜑 → (0(,)π) ⊆ (0[,]π))
167 ioombl 23140 . . . . . . . 8 (0(,)π) ∈ dom vol
168167a1i 11 . . . . . . 7 (𝜑 → (0(,)π) ∈ dom vol)
16924adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℝ)
170 iccssre 12126 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
1715, 1, 170mp2an 704 . . . . . . . . . . 11 (0[,]π) ⊆ ℝ
172171sseli 3564 . . . . . . . . . 10 (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℝ)
173172adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℝ)
174169, 173remulcld 9949 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → (𝑁 · 𝑥) ∈ ℝ)
175174recoscld 14713 . . . . . . 7 ((𝜑𝑥 ∈ (0[,]π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
176171, 117sstri 3577 . . . . . . . . . . . 12 (0[,]π) ⊆ ℂ
177176a1i 11 . . . . . . . . . . 11 (𝜑 → (0[,]π) ⊆ ℂ)
178177, 120, 122constcncfg 38756 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑁) ∈ ((0[,]π)–cn→ℂ))
179177, 122idcncfg 38757 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑥) ∈ ((0[,]π)–cn→ℂ))
180178, 179mulcncf 23023 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑁 · 𝑥)) ∈ ((0[,]π)–cn→ℂ))
181116, 180cncfmpt1f 22524 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ))
182 cniccibl 23413 . . . . . . . 8 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
183114, 4, 181, 182syl3anc 1318 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
184166, 168, 175, 183iblss 23377 . . . . . 6 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
18597, 164, 184iblmulc2 23403 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
186160, 185eqeltrd 2688 . . . 4 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
1873, 4, 12, 29, 131, 186itgsplitioo 23410 . . 3 (𝜑 → ∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = (∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥))
188187oveq1d 6564 . 2 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = ((∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π))
18995itgeq2dv 23354 . . . . 5 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
19098, 102, 129itgmulc2 23406 . . . . 5 (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
191 oveq1 6556 . . . . . . . . . . . . . 14 (𝑁 = 0 → (𝑁 · 𝑥) = (0 · 𝑥))
192 ioosscn 38563 . . . . . . . . . . . . . . . 16 (-π(,)0) ⊆ ℂ
193192sseli 3564 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℂ)
194193mul02d 10113 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (0 · 𝑥) = 0)
195191, 194sylan9eq 2664 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) = 0)
196195fveq2d 6107 . . . . . . . . . . . 12 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
197 cos0 14719 . . . . . . . . . . . 12 (cos‘0) = 1
198196, 197syl6eq 2660 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
199198adantll 746 . . . . . . . . . 10 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
200199itgeq2dv 23354 . . . . . . . . 9 ((𝜑𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(-π(,)0)1 d𝑥)
201 ioovolcl 23144 . . . . . . . . . . . . 13 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (vol‘(-π(,)0)) ∈ ℝ)
2022, 5, 201mp2an 704 . . . . . . . . . . . 12 (vol‘(-π(,)0)) ∈ ℝ
203202a1i 11 . . . . . . . . . . 11 (𝜑 → (vol‘(-π(,)0)) ∈ ℝ)
204 itgconst 23391 . . . . . . . . . . 11 (((-π(,)0) ∈ dom vol ∧ (vol‘(-π(,)0)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
205106, 203, 97, 204syl3anc 1318 . . . . . . . . . 10 (𝜑 → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
206205adantr 480 . . . . . . . . 9 ((𝜑𝑁 = 0) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
207 volioo 38840 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ -π ≤ 0) → (vol‘(-π(,)0)) = (0 − -π))
2082, 5, 7, 207mp3an 1416 . . . . . . . . . . . . . 14 (vol‘(-π(,)0)) = (0 − -π)
209 0cn 9911 . . . . . . . . . . . . . . 15 0 ∈ ℂ
210209, 43subnegi 10239 . . . . . . . . . . . . . 14 (0 − -π) = (0 + π)
211208, 210, 523eqtri 2636 . . . . . . . . . . . . 13 (vol‘(-π(,)0)) = π
212211a1i 11 . . . . . . . . . . . 12 (𝜑 → (vol‘(-π(,)0)) = π)
213212oveq2d 6565 . . . . . . . . . . 11 (𝜑 → (1 · (vol‘(-π(,)0))) = (1 · π))
21443a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℂ)
215214mulid2d 9937 . . . . . . . . . . 11 (𝜑 → (1 · π) = π)
216213, 215eqtrd 2644 . . . . . . . . . 10 (𝜑 → (1 · (vol‘(-π(,)0))) = π)
217216adantr 480 . . . . . . . . 9 ((𝜑𝑁 = 0) → (1 · (vol‘(-π(,)0))) = π)
218200, 206, 2173eqtrd 2648 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = π)
219218oveq2d 6565 . . . . . . 7 ((𝜑𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · π))
22043mulm1i 10354 . . . . . . . 8 (-1 · π) = -π
221220a1i 11 . . . . . . 7 ((𝜑𝑁 = 0) → (-1 · π) = -π)
222 iftrue 4042 . . . . . . . . 9 (𝑁 = 0 → if(𝑁 = 0, -π, 0) = -π)
223222eqcomd 2616 . . . . . . . 8 (𝑁 = 0 → -π = if(𝑁 = 0, -π, 0))
224223adantl 481 . . . . . . 7 ((𝜑𝑁 = 0) → -π = if(𝑁 = 0, -π, 0))
225219, 221, 2243eqtrd 2648 . . . . . 6 ((𝜑𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
22624adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℝ)
22723nn0ge0d 11231 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑁)
228227adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 0 ≤ 𝑁)
229 neqne 2790 . . . . . . . . 9 𝑁 = 0 → 𝑁 ≠ 0)
230229adantl 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
231226, 228, 230ne0gt0d 10053 . . . . . . 7 ((𝜑 ∧ ¬ 𝑁 = 0) → 0 < 𝑁)
232 1cnd 9935 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → 1 ∈ ℂ)
233232negcld 10258 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → -1 ∈ ℂ)
234233mul01d 10114 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → (-1 · 0) = 0)
235120adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 𝑁 ∈ ℂ)
2362a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → -π ∈ ℝ)
237 0red 9920 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 0 ∈ ℝ)
2387a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → -π ≤ 0)
239 simpr 476 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < 𝑁) → 0 < 𝑁)
240239gt0ne0d 10471 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 𝑁 ≠ 0)
241235, 236, 237, 238, 240itgcoscmulx 38861 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁))
242120mul01d 10114 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · 0) = 0)
243242fveq2d 6107 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘(𝑁 · 0)) = (sin‘0))
244 sin0 14718 . . . . . . . . . . . . . . 15 (sin‘0) = 0
245243, 244syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · 0)) = 0)
246120, 214mulneg2d 10363 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · -π) = -(𝑁 · π))
247246fveq2d 6107 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘(𝑁 · -π)) = (sin‘-(𝑁 · π)))
248120, 214mulcld 9939 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · π) ∈ ℂ)
249 sinneg 14715 . . . . . . . . . . . . . . . 16 ((𝑁 · π) ∈ ℂ → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
250248, 249syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
251247, 250eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · -π)) = -(sin‘(𝑁 · π)))
252245, 251oveq12d 6567 . . . . . . . . . . . . 13 (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (0 − -(sin‘(𝑁 · π))))
253 0cnd 9912 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ ℂ)
254248sincld 14699 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · π)) ∈ ℂ)
255253, 254subnegd 10278 . . . . . . . . . . . . 13 (𝜑 → (0 − -(sin‘(𝑁 · π))) = (0 + (sin‘(𝑁 · π))))
256254addid2d 10116 . . . . . . . . . . . . 13 (𝜑 → (0 + (sin‘(𝑁 · π))) = (sin‘(𝑁 · π)))
257252, 255, 2563eqtrd 2648 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
258257adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
259258oveq1d 6564 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁) = ((sin‘(𝑁 · π)) / 𝑁))
26023nn0zd 11356 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
261 sinkpi 24075 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (sin‘(𝑁 · π)) = 0)
262260, 261syl 17 . . . . . . . . . . . . 13 (𝜑 → (sin‘(𝑁 · π)) = 0)
263262oveq1d 6564 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
264263adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
265235, 240div0d 10679 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → (0 / 𝑁) = 0)
266264, 265eqtrd 2644 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = 0)
267241, 259, 2663eqtrd 2648 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = 0)
268267oveq2d 6565 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · 0))
269240neneqd 2787 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
270269iffalsed 4047 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, -π, 0) = 0)
271234, 268, 2703eqtr4d 2654 . . . . . . 7 ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
272231, 271syldan 486 . . . . . 6 ((𝜑 ∧ ¬ 𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
273225, 272pm2.61dan 828 . . . . 5 (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
274189, 190, 2733eqtr2d 2650 . . . 4 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, -π, 0))
275159itgeq2dv 23354 . . . . 5 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
27697, 164, 184itgmulc2 23406 . . . . 5 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
277164, 184itgcl 23356 . . . . . . 7 (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 ∈ ℂ)
278277mulid2d 9937 . . . . . 6 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥)
279 simpl 472 . . . . . . . . . . . . . 14 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 = 0)
280279oveq1d 6564 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = (0 · 𝑥))
281132recnd 9947 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℂ)
282281adantl 481 . . . . . . . . . . . . . 14 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℂ)
283282mul02d 10113 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (0 · 𝑥) = 0)
284280, 283eqtrd 2644 . . . . . . . . . . . 12 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = 0)
285284fveq2d 6107 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
286285, 197syl6eq 2660 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
287286adantll 746 . . . . . . . . 9 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
288287itgeq2dv 23354 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(0(,)π)1 d𝑥)
289 ioovolcl 23144 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ π ∈ ℝ) → (vol‘(0(,)π)) ∈ ℝ)
2905, 1, 289mp2an 704 . . . . . . . . . 10 (vol‘(0(,)π)) ∈ ℝ
291 ax-1cn 9873 . . . . . . . . . 10 1 ∈ ℂ
292 itgconst 23391 . . . . . . . . . 10 (((0(,)π) ∈ dom vol ∧ (vol‘(0(,)π)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
293167, 290, 291, 292mp3an 1416 . . . . . . . . 9 ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π)))
294293a1i 11 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
29543mulid2i 9922 . . . . . . . . . 10 (1 · π) = π
296 volioo 38840 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ 0 ≤ π) → (vol‘(0(,)π)) = (π − 0))
2975, 1, 9, 296mp3an 1416 . . . . . . . . . . . . 13 (vol‘(0(,)π)) = (π − 0)
29843subid1i 10232 . . . . . . . . . . . . 13 (π − 0) = π
299297, 298eqtri 2632 . . . . . . . . . . . 12 (vol‘(0(,)π)) = π
300299oveq2i 6560 . . . . . . . . . . 11 (1 · (vol‘(0(,)π))) = (1 · π)
301300a1i 11 . . . . . . . . . 10 (𝑁 = 0 → (1 · (vol‘(0(,)π))) = (1 · π))
302 iftrue 4042 . . . . . . . . . 10 (𝑁 = 0 → if(𝑁 = 0, π, 0) = π)
303295, 301, 3023eqtr4a 2670 . . . . . . . . 9 (𝑁 = 0 → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
304303adantl 481 . . . . . . . 8 ((𝜑𝑁 = 0) → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
305288, 294, 3043eqtrd 2648 . . . . . . 7 ((𝜑𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
306262, 245oveq12d 6567 . . . . . . . . . . . . 13 (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = (0 − 0))
307253subidd 10259 . . . . . . . . . . . . 13 (𝜑 → (0 − 0) = 0)
308306, 307eqtrd 2644 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = 0)
309308oveq1d 6564 . . . . . . . . . . 11 (𝜑 → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
310309adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
311310, 265eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = 0)
3121a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → π ∈ ℝ)
3139a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → 0 ≤ π)
314235, 237, 312, 313, 240itgcoscmulx 38861 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁))
315269iffalsed 4047 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, π, 0) = 0)
316311, 314, 3153eqtr4d 2654 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
317231, 316syldan 486 . . . . . . 7 ((𝜑 ∧ ¬ 𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
318305, 317pm2.61dan 828 . . . . . 6 (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
319278, 318eqtrd 2644 . . . . 5 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, π, 0))
320275, 276, 3193eqtr2d 2650 . . . 4 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, π, 0))
321274, 320oveq12d 6567 . . 3 (𝜑 → (∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) = (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)))
322321oveq1d 6564 . 2 (𝜑 → ((∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π) = ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π))
323222, 302oveq12d 6567 . . . . . . 7 (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (-π + π))
324323, 50syl6eq 2660 . . . . . 6 (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
325 iffalse 4045 . . . . . . . 8 𝑁 = 0 → if(𝑁 = 0, -π, 0) = 0)
326 iffalse 4045 . . . . . . . 8 𝑁 = 0 → if(𝑁 = 0, π, 0) = 0)
327325, 326oveq12d 6567 . . . . . . 7 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (0 + 0))
328 00id 10090 . . . . . . 7 (0 + 0) = 0
329327, 328syl6eq 2660 . . . . . 6 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
330324, 329pm2.61i 175 . . . . 5 (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0
331330oveq1i 6559 . . . 4 ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = (0 / π)
3325, 8gtneii 10028 . . . . 5 π ≠ 0
33343, 332div0i 10638 . . . 4 (0 / π) = 0
334331, 333eqtri 2632 . . 3 ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0
335334a1i 11 . 2 (𝜑 → ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0)
336188, 322, 3353eqtrd 2648 1 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ⊆ wss 3540  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℝ+crp 11708  (,)cioo 12046  [,]cicc 12049   mod cmo 12530  sincsin 14633  cosccos 14634  πcpi 14636  –cn→ccncf 22487  volcvol 23039  𝐿1cibl 23192  ∫citg 23193 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cc 9140  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-acn 8651  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196  df-ibl 23197  df-itg 23198  df-0p 23243  df-limc 23436  df-dv 23437 This theorem is referenced by:  fouriersw  39124
 Copyright terms: Public domain W3C validator