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

Theorem fourierdlem39 42308
Description: Integration by parts of ∫(𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem39.a (𝜑𝐴 ∈ ℝ)
fourierdlem39.b (𝜑𝐵 ∈ ℝ)
fourierdlem39.aleb (𝜑𝐴𝐵)
fourierdlem39.f (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
fourierdlem39.g 𝐺 = (ℝ D 𝐹)
fourierdlem39.gcn (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
fourierdlem39.gbd (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦)
fourierdlem39.r (𝜑𝑅 ∈ ℝ+)
Assertion
Ref Expression
fourierdlem39 (𝜑 → ∫(𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥,𝑅,𝑦   𝜑,𝑥,𝑦

Proof of Theorem fourierdlem39
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem39.a . 2 (𝜑𝐴 ∈ ℝ)
2 fourierdlem39.b . 2 (𝜑𝐵 ∈ ℝ)
3 fourierdlem39.aleb . 2 (𝜑𝐴𝐵)
4 fourierdlem39.f . . . . . 6 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
5 cncff 23428 . . . . . 6 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
64, 5syl 17 . . . . 5 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
76feqmptd 6726 . . . 4 (𝜑𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)))
87eqcomd 2824 . . 3 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) = 𝐹)
98, 4eqeltrd 2910 . 2 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
10 coscn 24960 . . . . . 6 cos ∈ (ℂ–cn→ℂ)
1110a1i 11 . . . . 5 (𝜑 → cos ∈ (ℂ–cn→ℂ))
121, 2iccssred 41656 . . . . . . . 8 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
13 ax-resscn 10582 . . . . . . . 8 ℝ ⊆ ℂ
1412, 13sstrdi 3976 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
15 fourierdlem39.r . . . . . . . . 9 (𝜑𝑅 ∈ ℝ+)
1615rpred 12419 . . . . . . . 8 (𝜑𝑅 ∈ ℝ)
1716recnd 10657 . . . . . . 7 (𝜑𝑅 ∈ ℂ)
18 ssid 3986 . . . . . . . 8 ℂ ⊆ ℂ
1918a1i 11 . . . . . . 7 (𝜑 → ℂ ⊆ ℂ)
2014, 17, 19constcncfg 42030 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑅) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2114, 19idcncfg 42031 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2220, 21mulcncf 23974 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑅 · 𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2311, 22cncfmpt1f 23448 . . . 4 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (cos‘(𝑅 · 𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2415rpcnne0d 12428 . . . . . 6 (𝜑 → (𝑅 ∈ ℂ ∧ 𝑅 ≠ 0))
25 eldifsn 4711 . . . . . 6 (𝑅 ∈ (ℂ ∖ {0}) ↔ (𝑅 ∈ ℂ ∧ 𝑅 ≠ 0))
2624, 25sylibr 235 . . . . 5 (𝜑𝑅 ∈ (ℂ ∖ {0}))
27 difssd 4106 . . . . 5 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
2814, 26, 27constcncfg 42030 . . . 4 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑅) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})))
2923, 28divcncf 23975 . . 3 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
3029negcncfg 42040 . 2 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
31 fourierdlem39.gcn . . . . . 6 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
32 cncff 23428 . . . . . 6 (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
3331, 32syl 17 . . . . 5 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
3433feqmptd 6726 . . . 4 (𝜑𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)))
3534eqcomd 2824 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)) = 𝐺)
3635, 31eqeltrd 2910 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
37 sincn 24959 . . . 4 sin ∈ (ℂ–cn→ℂ)
3837a1i 11 . . 3 (𝜑 → sin ∈ (ℂ–cn→ℂ))
39 ioosscn 41645 . . . . . 6 (𝐴(,)𝐵) ⊆ ℂ
4039a1i 11 . . . . 5 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
4140, 17, 19constcncfg 42030 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑅) ∈ ((𝐴(,)𝐵)–cn→ℂ))
4240, 19idcncfg 42031 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑥) ∈ ((𝐴(,)𝐵)–cn→ℂ))
4341, 42mulcncf 23974 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝑅 · 𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
4438, 43cncfmpt1f 23448 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
45 ioombl 24093 . . . 4 (𝐴(,)𝐵) ∈ dom vol
4645a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ∈ dom vol)
47 volioo 24097 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵𝐴))
481, 2, 3, 47syl3anc 1363 . . . 4 (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵𝐴))
492, 1resubcld 11056 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ)
5048, 49eqeltrd 2910 . . 3 (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
51 eqid 2818 . . . . 5 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))
52 ioossicc 12810 . . . . . 6 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
5352a1i 11 . . . . 5 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
546adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
5553sselda 3964 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
5654, 55ffvelrnd 6844 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
5751, 9, 53, 19, 56cncfmptssg 42029 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
5857, 44mulcncf 23974 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
59 cniccbdd 23989 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
601, 2, 4, 59syl3anc 1363 . . . . 5 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
61 nfra1 3216 . . . . . . . 8 𝑧𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦
6252sseli 3960 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵))
63 rspa 3203 . . . . . . . . . 10 ((∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦𝑧 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹𝑧)) ≤ 𝑦)
6462, 63sylan2 592 . . . . . . . . 9 ((∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹𝑧)) ≤ 𝑦)
6564ex 413 . . . . . . . 8 (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → (𝑧 ∈ (𝐴(,)𝐵) → (abs‘(𝐹𝑧)) ≤ 𝑦))
6661, 65ralrimi 3213 . . . . . . 7 (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
6766a1i 11 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦))
6867reximdva 3271 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦))
6960, 68mpd 15 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
70 nfv 1906 . . . . . . . 8 𝑧(𝜑𝑦 ∈ ℝ)
71 nfra1 3216 . . . . . . . 8 𝑧𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦
7270, 71nfan 1891 . . . . . . 7 𝑧((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
73 simpll 763 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (𝜑𝑦 ∈ ℝ))
74 simpr 485 . . . . . . . . . . 11 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))))
7516adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ)
76 elioore 12756 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
7776adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ)
7875, 77remulcld 10659 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑥) ∈ ℝ)
7978resincld 15484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑥)) ∈ ℝ)
8079recnd 10657 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑥)) ∈ ℂ)
8156, 80mulcld 10649 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ)
8281ralrimiva 3179 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ)
83 dmmptg 6089 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵))
8482, 83syl 17 . . . . . . . . . . . 12 (𝜑 → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵))
8584adantr 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵))
8674, 85eleqtrd 2912 . . . . . . . . . 10 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵))
8786ad4ant14 748 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵))
88 simplr 765 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
8986adantlr 711 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵))
90 rspa 3203 . . . . . . . . . . 11 ((∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹𝑧)) ≤ 𝑦)
9188, 89, 90syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘(𝐹𝑧)) ≤ 𝑦)
9291adantllr 715 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘(𝐹𝑧)) ≤ 𝑦)
93 eqidd 2819 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))))
94 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
95 oveq2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑅 · 𝑥) = (𝑅 · 𝑧))
9695fveq2d 6667 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (sin‘(𝑅 · 𝑥)) = (sin‘(𝑅 · 𝑧)))
9794, 96oveq12d 7163 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) = ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))))
9897adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑧) → ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) = ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))))
99 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ (𝐴(,)𝐵))
1006adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
10152, 99sseldi 3962 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ (𝐴[,]𝐵))
102100, 101ffvelrnd 6844 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
10317adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
10439, 99sseldi 3962 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℂ)
105103, 104mulcld 10649 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℂ)
106105sincld 15471 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑧)) ∈ ℂ)
107102, 106mulcld 10649 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))) ∈ ℂ)
10893, 98, 99, 107fvmptd 6767 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧) = ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))))
109108fveq2d 6667 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = (abs‘((𝐹𝑧) · (sin‘(𝑅 · 𝑧)))))
110102, 106absmuld 14802 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹𝑧) · (sin‘(𝑅 · 𝑧)))) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
111109, 110eqtrd 2853 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
112111adantlr 711 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
113112adantr 481 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
114 simplll 771 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝜑)
115 simplr 765 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑧 ∈ (𝐴(,)𝐵))
116114, 115, 102syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝐹𝑧) ∈ ℂ)
117116abscld 14784 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘(𝐹𝑧)) ∈ ℝ)
11817ad3antrrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑅 ∈ ℂ)
11939, 115sseldi 3962 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑧 ∈ ℂ)
120118, 119mulcld 10649 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑅 · 𝑧) ∈ ℂ)
121120sincld 15471 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (sin‘(𝑅 · 𝑧)) ∈ ℂ)
122121abscld 14784 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘(sin‘(𝑅 · 𝑧))) ∈ ℝ)
123117, 122remulcld 10659 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ∈ ℝ)
124 1red 10630 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 1 ∈ ℝ)
125117, 124remulcld 10659 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · 1) ∈ ℝ)
126 simpllr 772 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑦 ∈ ℝ)
127126, 124remulcld 10659 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑦 · 1) ∈ ℝ)
128106abscld 14784 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(sin‘(𝑅 · 𝑧))) ∈ ℝ)
129 1red 10630 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ)
130102abscld 14784 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹𝑧)) ∈ ℝ)
131102absge0d 14792 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘(𝐹𝑧)))
13216adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ)
133 elioore 12756 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ ℝ)
134133adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℝ)
135132, 134remulcld 10659 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℝ)
136 abssinbd 41438 . . . . . . . . . . . . . . . 16 ((𝑅 · 𝑧) ∈ ℝ → (abs‘(sin‘(𝑅 · 𝑧))) ≤ 1)
137135, 136syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(sin‘(𝑅 · 𝑧))) ≤ 1)
138128, 129, 130, 131, 137lemul2ad 11568 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹𝑧)) · 1))
139138adantlr 711 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹𝑧)) · 1))
140139adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹𝑧)) · 1))
141 0le1 11151 . . . . . . . . . . . . . 14 0 ≤ 1
142141a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 0 ≤ 1)
143 simpr 485 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘(𝐹𝑧)) ≤ 𝑦)
144117, 126, 124, 142, 143lemul1ad 11567 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · 1) ≤ (𝑦 · 1))
145123, 125, 127, 140, 144letrd 10785 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ (𝑦 · 1))
146113, 145eqbrtrd 5079 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ (𝑦 · 1))
147126recnd 10657 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑦 ∈ ℂ)
148147mulid1d 10646 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑦 · 1) = 𝑦)
149146, 148breqtrd 5083 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
15073, 87, 92, 149syl21anc 833 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
151150ex 413 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦))
15272, 151ralrimi 3213 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
153152ex 413 . . . . 5 ((𝜑𝑦 ∈ ℝ) → (∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦))
154153reximdva 3271 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦))
15569, 154mpd 15 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
15646, 50, 58, 155cnbdibl 42123 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) ∈ 𝐿1)
15711, 43cncfmpt1f 23448 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑅 · 𝑥))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
15840, 26, 27constcncfg 42030 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑅) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
159157, 158divcncf 23975 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
160159negcncfg 42040 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
16136, 160mulcncf 23974 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
162 simpr 485 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
16316adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → 𝑅 ∈ ℝ)
16415rpne0d 12424 . . . . . . . 8 (𝜑𝑅 ≠ 0)
165164adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → 𝑅 ≠ 0)
166162, 163, 165redivcld 11456 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (𝑦 / 𝑅) ∈ ℝ)
167166adantr 481 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → (𝑦 / 𝑅) ∈ ℝ)
168 simpr 485 . . . . . . . . 9 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))))
16933ffvelrnda 6843 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) ∈ ℂ)
17017adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
17176recnd 10657 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℂ)
172171adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ)
173170, 172mulcld 10649 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑥) ∈ ℂ)
174173coscld 15472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑥)) ∈ ℂ)
175164adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0)
176174, 170, 175divcld 11404 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
177176negcld 10972 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
178169, 177mulcld 10649 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ)
179178ralrimiva 3179 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ)
180179adantr 481 . . . . . . . . . 10 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ)
181 dmmptg 6089 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝐴(,)𝐵))
182180, 181syl 17 . . . . . . . . 9 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝐴(,)𝐵))
183168, 182eleqtrd 2912 . . . . . . . 8 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ (𝐴(,)𝐵))
184183ad4ant14 748 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ (𝐴(,)𝐵))
185 eqidd 2819 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))))
186 fveq2 6663 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
18795fveq2d 6667 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝑧)))
188187oveq1d 7160 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝑧)) / 𝑅))
189188negeqd 10868 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝑧)) / 𝑅))
190186, 189oveq12d 7163 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))
191190adantl 482 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑧) → ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))
19233ffvelrnda 6843 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
193105coscld 15472 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑧)) ∈ ℂ)
194164adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0)
195193, 103, 194divcld 11404 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
196195negcld 10972 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
197192, 196mulcld 10649 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)) ∈ ℂ)
198185, 191, 99, 197fvmptd 6767 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧) = ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))
199198fveq2d 6667 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) = (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))))
200199ad4ant14 748 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) = (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))))
20133ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
202201ffvelrnda 6843 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
203202abscld 14784 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺𝑧)) ∈ ℝ)
204 simpllr 772 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ)
20517ad3antrrr 726 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
206104ad4ant14 748 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℂ)
207205, 206mulcld 10649 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℂ)
208207coscld 15472 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑧)) ∈ ℂ)
209164ad3antrrr 726 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0)
210208, 205, 209divcld 11404 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
211210negcld 10972 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
212211abscld 14784 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ∈ ℝ)
21315rprecred 12430 . . . . . . . . . . 11 (𝜑 → (1 / 𝑅) ∈ ℝ)
214213ad3antrrr 726 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (1 / 𝑅) ∈ ℝ)
215202absge0d 14792 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘(𝐺𝑧)))
216211absge0d 14792 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)))
217186fveq2d 6667 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (abs‘(𝐺𝑥)) = (abs‘(𝐺𝑧)))
218217breq1d 5067 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((abs‘(𝐺𝑥)) ≤ 𝑦 ↔ (abs‘(𝐺𝑧)) ≤ 𝑦))
219218rspccva 3619 . . . . . . . . . . 11 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺𝑧)) ≤ 𝑦)
220219adantll 710 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺𝑧)) ≤ 𝑦)
221195absnegd 14797 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) = (abs‘((cos‘(𝑅 · 𝑧)) / 𝑅)))
222193, 103, 194absdivd 14803 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((cos‘(𝑅 · 𝑧)) / 𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)))
22315rpge0d 12423 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑅)
22416, 223absidd 14770 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑅) = 𝑅)
225224oveq2d 7161 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅))
226225adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅))
227221, 222, 2263eqtrd 2857 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅))
228193abscld 14784 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑅 · 𝑧))) ∈ ℝ)
22915adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ+)
230 abscosbd 41420 . . . . . . . . . . . . . 14 ((𝑅 · 𝑧) ∈ ℝ → (abs‘(cos‘(𝑅 · 𝑧))) ≤ 1)
231135, 230syl 17 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑅 · 𝑧))) ≤ 1)
232228, 129, 229, 231lediv1dd 12477 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅) ≤ (1 / 𝑅))
233227, 232eqbrtrd 5079 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ≤ (1 / 𝑅))
234233ad4ant14 748 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ≤ (1 / 𝑅))
235203, 204, 212, 214, 215, 216, 220, 234lemul12ad 11570 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐺𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))) ≤ (𝑦 · (1 / 𝑅)))
236192, 196absmuld 14802 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) = ((abs‘(𝐺𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))))
237236ad4ant14 748 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) = ((abs‘(𝐺𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))))
238204recnd 10657 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℂ)
239238, 205, 209divrecd 11407 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑦 / 𝑅) = (𝑦 · (1 / 𝑅)))
240235, 237, 2393brtr4d 5089 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) ≤ (𝑦 / 𝑅))
241200, 240eqbrtrd 5079 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))
242184, 241syldan 591 . . . . . 6 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))
243242ralrimiva 3179 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))
244 breq2 5061 . . . . . . 7 (𝑤 = (𝑦 / 𝑅) → ((abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤 ↔ (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)))
245244ralbidv 3194 . . . . . 6 (𝑤 = (𝑦 / 𝑅) → (∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)))
246245rspcev 3620 . . . . 5 (((𝑦 / 𝑅) ∈ ℝ ∧ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤)
247167, 243, 246syl2anc 584 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤)
248 fourierdlem39.gbd . . . 4 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦)
249247, 248r19.29a 3286 . . 3 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤)
25046, 50, 161, 249cnbdibl 42123 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) ∈ 𝐿1)
2518oveq2d 7161 . . 3 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))) = (ℝ D 𝐹))
252 fourierdlem39.g . . . . 5 𝐺 = (ℝ D 𝐹)
253252eqcomi 2827 . . . 4 (ℝ D 𝐹) = 𝐺
254253a1i 11 . . 3 (𝜑 → (ℝ D 𝐹) = 𝐺)
255251, 254, 343eqtrd 2857 . 2 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)))
256 reelprrecn 10617 . . . . 5 ℝ ∈ {ℝ, ℂ}
257256a1i 11 . . . 4 (𝜑 → ℝ ∈ {ℝ, ℂ})
25817adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℂ)
259 recn 10615 . . . . . . . . 9 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
260259adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
261258, 260mulcld 10649 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝑅 · 𝑥) ∈ ℂ)
262261coscld 15472 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (cos‘(𝑅 · 𝑥)) ∈ ℂ)
263164adantr 481 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → 𝑅 ≠ 0)
264262, 258, 263divcld 11404 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
265264negcld 10972 . . . 4 ((𝜑𝑥 ∈ ℝ) → -((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
26616adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℝ)
267 simpr 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
268266, 267remulcld 10659 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑅 · 𝑥) ∈ ℝ)
269268resincld 15484 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (sin‘(𝑅 · 𝑥)) ∈ ℝ)
270269renegcld 11055 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → -(sin‘(𝑅 · 𝑥)) ∈ ℝ)
271270, 266remulcld 10659 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (-(sin‘(𝑅 · 𝑥)) · 𝑅) ∈ ℝ)
272271, 266, 263redivcld 11456 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℝ)
273272renegcld 11055 . . . 4 ((𝜑𝑥 ∈ ℝ) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℝ)
274 recoscl 15482 . . . . . . . . 9 (𝑦 ∈ ℝ → (cos‘𝑦) ∈ ℝ)
275274adantl 482 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (cos‘𝑦) ∈ ℝ)
276275recnd 10657 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → (cos‘𝑦) ∈ ℂ)
277 resincl 15481 . . . . . . . . 9 (𝑦 ∈ ℝ → (sin‘𝑦) ∈ ℝ)
278277renegcld 11055 . . . . . . . 8 (𝑦 ∈ ℝ → -(sin‘𝑦) ∈ ℝ)
279278adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → -(sin‘𝑦) ∈ ℝ)
280 1red 10630 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 1 ∈ ℝ)
281257dvmptid 24481 . . . . . . . . 9 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
282257, 260, 280, 281, 17dvmptcmul 24488 . . . . . . . 8 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝑅 · 𝑥))) = (𝑥 ∈ ℝ ↦ (𝑅 · 1)))
283258mulid1d 10646 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑅 · 1) = 𝑅)
284283mpteq2dva 5152 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑅 · 1)) = (𝑥 ∈ ℝ ↦ 𝑅))
285282, 284eqtrd 2853 . . . . . . 7 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝑅 · 𝑥))) = (𝑥 ∈ ℝ ↦ 𝑅))
286 dvcosre 42072 . . . . . . . 8 (ℝ D (𝑦 ∈ ℝ ↦ (cos‘𝑦))) = (𝑦 ∈ ℝ ↦ -(sin‘𝑦))
287286a1i 11 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (cos‘𝑦))) = (𝑦 ∈ ℝ ↦ -(sin‘𝑦)))
288 fveq2 6663 . . . . . . 7 (𝑦 = (𝑅 · 𝑥) → (cos‘𝑦) = (cos‘(𝑅 · 𝑥)))
289 fveq2 6663 . . . . . . . 8 (𝑦 = (𝑅 · 𝑥) → (sin‘𝑦) = (sin‘(𝑅 · 𝑥)))
290289negeqd 10868 . . . . . . 7 (𝑦 = (𝑅 · 𝑥) → -(sin‘𝑦) = -(sin‘(𝑅 · 𝑥)))
291257, 257, 268, 266, 276, 279, 285, 287, 288, 290dvmptco 24496 . . . . . 6 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (cos‘(𝑅 · 𝑥)))) = (𝑥 ∈ ℝ ↦ (-(sin‘(𝑅 · 𝑥)) · 𝑅)))
292257, 262, 271, 291, 17, 164dvmptdivc 24489 . . . . 5 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ ℝ ↦ ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)))
293257, 264, 272, 292dvmptneg 24490 . . . 4 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ ℝ ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)))
294 eqid 2818 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
295294tgioo2 23338 . . . 4 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
296 iccntr 23356 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
2971, 2, 296syl2anc 584 . . . 4 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
298257, 265, 273, 293, 12, 295, 294, 297dvmptres2 24486 . . 3 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)))
29980, 170mulneg1d 11081 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (-(sin‘(𝑅 · 𝑥)) · 𝑅) = -((sin‘(𝑅 · 𝑥)) · 𝑅))
300299oveq1d 7160 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (-((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
30180, 170mulcld 10649 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((sin‘(𝑅 · 𝑥)) · 𝑅) ∈ ℂ)
302301, 170, 175divnegd 11417 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (-((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
303300, 302eqtr4d 2856 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = -(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
304303negeqd 10868 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = --(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
305301, 170, 175divcld 11404 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℂ)
306305negnegd 10976 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → --(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
30780, 170, 175divcan4d 11410 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (sin‘(𝑅 · 𝑥)))
308304, 306, 3073eqtrd 2857 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (sin‘(𝑅 · 𝑥)))
309308mpteq2dva 5152 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))))
310298, 309eqtrd 2853 . 2 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))))
311 fveq2 6663 . . . 4 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
312 oveq2 7153 . . . . . . 7 (𝑥 = 𝐴 → (𝑅 · 𝑥) = (𝑅 · 𝐴))
313312fveq2d 6667 . . . . . 6 (𝑥 = 𝐴 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝐴)))
314313oveq1d 7160 . . . . 5 (𝑥 = 𝐴 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝐴)) / 𝑅))
315314negeqd 10868 . . . 4 (𝑥 = 𝐴 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝐴)) / 𝑅))
316311, 315oveq12d 7163 . . 3 (𝑥 = 𝐴 → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅)))
317316adantl 482 . 2 ((𝜑𝑥 = 𝐴) → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅)))
318 fveq2 6663 . . . 4 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
319 oveq2 7153 . . . . . . 7 (𝑥 = 𝐵 → (𝑅 · 𝑥) = (𝑅 · 𝐵))
320319fveq2d 6667 . . . . . 6 (𝑥 = 𝐵 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝐵)))
321320oveq1d 7160 . . . . 5 (𝑥 = 𝐵 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝐵)) / 𝑅))
322321negeqd 10868 . . . 4 (𝑥 = 𝐵 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝐵)) / 𝑅))
323318, 322oveq12d 7163 . . 3 (𝑥 = 𝐵 → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)))
324323adantl 482 . 2 ((𝜑𝑥 = 𝐵) → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)))
3251, 2, 3, 9, 30, 36, 44, 156, 250, 255, 310, 317, 324itgparts 24571 1 (𝜑 → ∫(𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  cdif 3930  wss 3933  {csn 4557  {cpr 4559   class class class wbr 5057  cmpt 5137  dom cdm 5548  ran crn 5549  wf 6344  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   · cmul 10530  cle 10664  cmin 10858  -cneg 10859   / cdiv 11285  +crp 12377  (,)cioo 12726  [,]cicc 12729  abscabs 14581  sincsin 15405  cosccos 15406  TopOpenctopn 16683  topGenctg 16699  fldccnfld 20473  intcnt 21553  cnccncf 23411  volcvol 23991  citg 24146   D cdv 24388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cc 9845  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-symdif 4216  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-disj 5023  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-ofr 7399  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-shft 14414  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-ef 15409  df-sin 15411  df-cos 15412  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-cmp 21923  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-ovol 23992  df-vol 23993  df-mbf 24147  df-itg1 24148  df-itg2 24149  df-ibl 24150  df-itg 24151  df-0p 24198  df-limc 24391  df-dv 24392
This theorem is referenced by:  fourierdlem73  42341
  Copyright terms: Public domain W3C validator