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 39670
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 22604 . . . . . 6 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
64, 5syl 17 . . . . 5 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
76feqmptd 6206 . . . 4 (𝜑𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)))
87eqcomd 2627 . . 3 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) = 𝐹)
98, 4eqeltrd 2698 . 2 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
10 coscn 24103 . . . . . 6 cos ∈ (ℂ–cn→ℂ)
1110a1i 11 . . . . 5 (𝜑 → cos ∈ (ℂ–cn→ℂ))
121, 2iccssred 39138 . . . . . . . 8 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
13 ax-resscn 9937 . . . . . . . 8 ℝ ⊆ ℂ
1412, 13syl6ss 3595 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
15 fourierdlem39.r . . . . . . . . 9 (𝜑𝑅 ∈ ℝ+)
1615rpred 11816 . . . . . . . 8 (𝜑𝑅 ∈ ℝ)
1716recnd 10012 . . . . . . 7 (𝜑𝑅 ∈ ℂ)
18 ssid 3603 . . . . . . . 8 ℂ ⊆ ℂ
1918a1i 11 . . . . . . 7 (𝜑 → ℂ ⊆ ℂ)
2014, 17, 19constcncfg 39387 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑅) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2114, 19idcncfg 39388 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2220, 21mulcncf 23123 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑅 · 𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2311, 22cncfmpt1f 22624 . . . 4 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (cos‘(𝑅 · 𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2415rpcnne0d 11825 . . . . . 6 (𝜑 → (𝑅 ∈ ℂ ∧ 𝑅 ≠ 0))
25 eldifsn 4287 . . . . . 6 (𝑅 ∈ (ℂ ∖ {0}) ↔ (𝑅 ∈ ℂ ∧ 𝑅 ≠ 0))
2624, 25sylibr 224 . . . . 5 (𝜑𝑅 ∈ (ℂ ∖ {0}))
27 difssd 3716 . . . . 5 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
2814, 26, 27constcncfg 39387 . . . 4 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑅) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})))
2923, 28divcncf 39400 . . 3 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
3029negcncfg 39397 . 2 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
31 fourierdlem39.gcn . . . . . 6 (𝜑𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))
32 cncff 22604 . . . . . 6 (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
3331, 32syl 17 . . . . 5 (𝜑𝐺:(𝐴(,)𝐵)⟶ℂ)
3433feqmptd 6206 . . . 4 (𝜑𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)))
3534eqcomd 2627 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)) = 𝐺)
3635, 31eqeltrd 2698 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
37 sincn 24102 . . . 4 sin ∈ (ℂ–cn→ℂ)
3837a1i 11 . . 3 (𝜑 → sin ∈ (ℂ–cn→ℂ))
39 ioosscn 39127 . . . . . 6 (𝐴(,)𝐵) ⊆ ℂ
4039a1i 11 . . . . 5 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
4140, 17, 19constcncfg 39387 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑅) ∈ ((𝐴(,)𝐵)–cn→ℂ))
4240, 19idcncfg 39388 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑥) ∈ ((𝐴(,)𝐵)–cn→ℂ))
4341, 42mulcncf 23123 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝑅 · 𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
4438, 43cncfmpt1f 22624 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
45 ioombl 23240 . . . 4 (𝐴(,)𝐵) ∈ dom vol
4645a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ∈ dom vol)
47 volioo 39471 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵𝐴))
481, 2, 3, 47syl3anc 1323 . . . 4 (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵𝐴))
492, 1resubcld 10402 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ)
5048, 49eqeltrd 2698 . . 3 (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
51 eqid 2621 . . . . 5 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))
52 ioossicc 12201 . . . . . 6 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
5352a1i 11 . . . . 5 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
546adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
5553sselda 3583 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
5654, 55ffvelrnd 6316 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐹𝑥) ∈ ℂ)
5751, 9, 53, 19, 56cncfmptssg 39386 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
5857, 44mulcncf 23123 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
59 cniccbdd 23137 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
601, 2, 4, 59syl3anc 1323 . . . . 5 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
61 nfra1 2936 . . . . . . . 8 𝑧𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦
6252sseli 3579 . . . . . . . . . 10 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵))
63 rspa 2925 . . . . . . . . . 10 ((∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦𝑧 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹𝑧)) ≤ 𝑦)
6462, 63sylan2 491 . . . . . . . . 9 ((∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹𝑧)) ≤ 𝑦)
6564ex 450 . . . . . . . 8 (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → (𝑧 ∈ (𝐴(,)𝐵) → (abs‘(𝐹𝑧)) ≤ 𝑦))
6661, 65ralrimi 2951 . . . . . . 7 (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
6766a1i 11 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦))
6867reximdva 3011 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦))
6960, 68mpd 15 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
70 nfv 1840 . . . . . . . 8 𝑧(𝜑𝑦 ∈ ℝ)
71 nfra1 2936 . . . . . . . 8 𝑧𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦
7270, 71nfan 1825 . . . . . . 7 𝑧((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
73 simpll 789 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (𝜑𝑦 ∈ ℝ))
74 simpr 477 . . . . . . . . . . 11 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))))
7516adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ)
76 elioore 12147 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
7776adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ)
7875, 77remulcld 10014 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑥) ∈ ℝ)
7978resincld 14798 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑥)) ∈ ℝ)
8079recnd 10012 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑥)) ∈ ℂ)
8156, 80mulcld 10004 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ)
8281ralrimiva 2960 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ)
83 dmmptg 5591 . . . . . . . . . . . . 13 (∀𝑥 ∈ (𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵))
8482, 83syl 17 . . . . . . . . . . . 12 (𝜑 → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵))
8584adantr 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵))
8674, 85eleqtrd 2700 . . . . . . . . . 10 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵))
8786ad4ant14 1290 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵))
88 simplr 791 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦)
8986adantlr 750 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵))
90 rspa 2925 . . . . . . . . . . 11 ((∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹𝑧)) ≤ 𝑦)
9188, 89, 90syl2anc 692 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘(𝐹𝑧)) ≤ 𝑦)
9291adantllr 754 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘(𝐹𝑧)) ≤ 𝑦)
93 eqidd 2622 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))))
94 fveq2 6148 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
95 oveq2 6612 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑅 · 𝑥) = (𝑅 · 𝑧))
9695fveq2d 6152 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (sin‘(𝑅 · 𝑥)) = (sin‘(𝑅 · 𝑧)))
9794, 96oveq12d 6622 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) = ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))))
9897adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑧) → ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) = ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))))
99 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ (𝐴(,)𝐵))
1006adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
10152, 99sseldi 3581 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ (𝐴[,]𝐵))
102100, 101ffvelrnd 6316 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
10317adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
10439, 99sseldi 3581 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℂ)
105103, 104mulcld 10004 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℂ)
106105sincld 14785 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑧)) ∈ ℂ)
107102, 106mulcld 10004 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))) ∈ ℂ)
10893, 98, 99, 107fvmptd 6245 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧) = ((𝐹𝑧) · (sin‘(𝑅 · 𝑧))))
109108fveq2d 6152 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = (abs‘((𝐹𝑧) · (sin‘(𝑅 · 𝑧)))))
110102, 106absmuld 14127 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹𝑧) · (sin‘(𝑅 · 𝑧)))) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
111109, 110eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
112111adantlr 750 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
113112adantr 481 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))))
114 simplll 797 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝜑)
115 simplr 791 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑧 ∈ (𝐴(,)𝐵))
116114, 115, 102syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝐹𝑧) ∈ ℂ)
117116abscld 14109 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘(𝐹𝑧)) ∈ ℝ)
11817ad3antrrr 765 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑅 ∈ ℂ)
11939, 115sseldi 3581 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑧 ∈ ℂ)
120118, 119mulcld 10004 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑅 · 𝑧) ∈ ℂ)
121120sincld 14785 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (sin‘(𝑅 · 𝑧)) ∈ ℂ)
122121abscld 14109 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘(sin‘(𝑅 · 𝑧))) ∈ ℝ)
123117, 122remulcld 10014 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ∈ ℝ)
124 1red 9999 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 1 ∈ ℝ)
125117, 124remulcld 10014 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · 1) ∈ ℝ)
126 simpllr 798 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑦 ∈ ℝ)
127126, 124remulcld 10014 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑦 · 1) ∈ ℝ)
128106abscld 14109 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(sin‘(𝑅 · 𝑧))) ∈ ℝ)
129 1red 9999 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ)
130102abscld 14109 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹𝑧)) ∈ ℝ)
131102absge0d 14117 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘(𝐹𝑧)))
13216adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ)
133 elioore 12147 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ ℝ)
134133adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℝ)
135132, 134remulcld 10014 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℝ)
136 abssinbd 38973 . . . . . . . . . . . . . . . 16 ((𝑅 · 𝑧) ∈ ℝ → (abs‘(sin‘(𝑅 · 𝑧))) ≤ 1)
137135, 136syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(sin‘(𝑅 · 𝑧))) ≤ 1)
138128, 129, 130, 131, 137lemul2ad 10908 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹𝑧)) · 1))
139138adantlr 750 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹𝑧)) · 1))
140139adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹𝑧)) · 1))
141 0le1 10495 . . . . . . . . . . . . . 14 0 ≤ 1
142141a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 0 ≤ 1)
143 simpr 477 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘(𝐹𝑧)) ≤ 𝑦)
144117, 126, 124, 142, 143lemul1ad 10907 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · 1) ≤ (𝑦 · 1))
145123, 125, 127, 140, 144letrd 10138 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → ((abs‘(𝐹𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ (𝑦 · 1))
146113, 145eqbrtrd 4635 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ (𝑦 · 1))
147126recnd 10012 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → 𝑦 ∈ ℂ)
148147mulid1d 10001 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑦 · 1) = 𝑦)
149146, 148breqtrd 4639 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
15073, 87, 92, 149syl21anc 1322 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
151150ex 450 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) → (𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦))
15272, 151ralrimi 2951 . . . . . 6 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦) → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
153152ex 450 . . . . 5 ((𝜑𝑦 ∈ ℝ) → (∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦))
154153reximdva 3011 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦))
15569, 154mpd 15 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)
15646, 50, 58, 155cnbdibl 39485 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹𝑥) · (sin‘(𝑅 · 𝑥)))) ∈ 𝐿1)
15711, 43cncfmpt1f 22624 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑅 · 𝑥))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
15840, 26, 27constcncfg 39387 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑅) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
159157, 158divcncf 39400 . . . . 5 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
160159negcncfg 39397 . . . 4 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
16136, 160mulcncf 23123 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
162 simpr 477 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
16316adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → 𝑅 ∈ ℝ)
16415rpne0d 11821 . . . . . . . 8 (𝜑𝑅 ≠ 0)
165164adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → 𝑅 ≠ 0)
166162, 163, 165redivcld 10797 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (𝑦 / 𝑅) ∈ ℝ)
167166adantr 481 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → (𝑦 / 𝑅) ∈ ℝ)
168 simpr 477 . . . . . . . . 9 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))))
16933ffvelrnda 6315 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝐺𝑥) ∈ ℂ)
17017adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
17176recnd 10012 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℂ)
172171adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ)
173170, 172mulcld 10004 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑥) ∈ ℂ)
174173coscld 14786 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑥)) ∈ ℂ)
175164adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0)
176174, 170, 175divcld 10745 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
177176negcld 10323 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
178169, 177mulcld 10004 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ)
179178ralrimiva 2960 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ)
180179adantr 481 . . . . . . . . . 10 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ)
181 dmmptg 5591 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝐴(,)𝐵))
182180, 181syl 17 . . . . . . . . 9 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝐴(,)𝐵))
183168, 182eleqtrd 2700 . . . . . . . 8 ((𝜑𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ (𝐴(,)𝐵))
184183ad4ant14 1290 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ (𝐴(,)𝐵))
185 eqidd 2622 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))))
186 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
18795fveq2d 6152 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝑧)))
188187oveq1d 6619 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝑧)) / 𝑅))
189188negeqd 10219 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝑧)) / 𝑅))
190186, 189oveq12d 6622 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))
191190adantl 482 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑧) → ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))
19233ffvelrnda 6315 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
193105coscld 14786 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑧)) ∈ ℂ)
194164adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0)
195193, 103, 194divcld 10745 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
196195negcld 10323 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
197192, 196mulcld 10004 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)) ∈ ℂ)
198185, 191, 99, 197fvmptd 6245 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧) = ((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))
199198fveq2d 6152 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) = (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))))
200199ad4ant14 1290 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) = (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))))
20133ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → 𝐺:(𝐴(,)𝐵)⟶ℂ)
202201ffvelrnda 6315 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
203202abscld 14109 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺𝑧)) ∈ ℝ)
204 simpllr 798 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ)
20517ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ)
206104ad4ant14 1290 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℂ)
207205, 206mulcld 10004 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℂ)
208207coscld 14786 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑧)) ∈ ℂ)
209164ad3antrrr 765 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0)
210208, 205, 209divcld 10745 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
211210negcld 10323 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ)
212211abscld 14109 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ∈ ℝ)
21315rprecred 11827 . . . . . . . . . . 11 (𝜑 → (1 / 𝑅) ∈ ℝ)
214213ad3antrrr 765 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (1 / 𝑅) ∈ ℝ)
215202absge0d 14117 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘(𝐺𝑧)))
216211absge0d 14117 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)))
217186fveq2d 6152 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (abs‘(𝐺𝑥)) = (abs‘(𝐺𝑧)))
218217breq1d 4623 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((abs‘(𝐺𝑥)) ≤ 𝑦 ↔ (abs‘(𝐺𝑧)) ≤ 𝑦))
219218rspccva 3294 . . . . . . . . . . 11 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺𝑧)) ≤ 𝑦)
220219adantll 749 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺𝑧)) ≤ 𝑦)
221195absnegd 14122 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) = (abs‘((cos‘(𝑅 · 𝑧)) / 𝑅)))
222193, 103, 194absdivd 14128 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((cos‘(𝑅 · 𝑧)) / 𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)))
22315rpge0d 11820 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑅)
22416, 223absidd 14095 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑅) = 𝑅)
225224oveq2d 6620 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅))
226225adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅))
227221, 222, 2263eqtrd 2659 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅))
228193abscld 14109 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑅 · 𝑧))) ∈ ℝ)
22915adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ+)
230 abscosbd 38954 . . . . . . . . . . . . . 14 ((𝑅 · 𝑧) ∈ ℝ → (abs‘(cos‘(𝑅 · 𝑧))) ≤ 1)
231135, 230syl 17 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑅 · 𝑧))) ≤ 1)
232228, 129, 229, 231lediv1dd 11874 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅) ≤ (1 / 𝑅))
233227, 232eqbrtrd 4635 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ≤ (1 / 𝑅))
234233ad4ant14 1290 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ≤ (1 / 𝑅))
235203, 204, 212, 214, 215, 216, 220, 234lemul12ad 10910 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐺𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))) ≤ (𝑦 · (1 / 𝑅)))
236192, 196absmuld 14127 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) = ((abs‘(𝐺𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))))
237236ad4ant14 1290 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) = ((abs‘(𝐺𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))))
238204recnd 10012 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℂ)
239238, 205, 209divrecd 10748 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑦 / 𝑅) = (𝑦 · (1 / 𝑅)))
240235, 237, 2393brtr4d 4645 . . . . . . . 8 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) ≤ (𝑦 / 𝑅))
241200, 240eqbrtrd 4635 . . . . . . 7 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))
242184, 241syldan 487 . . . . . 6 ((((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))
243242ralrimiva 2960 . . . . 5 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))
244 breq2 4617 . . . . . . 7 (𝑤 = (𝑦 / 𝑅) → ((abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤 ↔ (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)))
245244ralbidv 2980 . . . . . 6 (𝑤 = (𝑦 / 𝑅) → (∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)))
246245rspcev 3295 . . . . 5 (((𝑦 / 𝑅) ∈ ℝ ∧ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤)
247167, 243, 246syl2anc 692 . . . 4 (((𝜑𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤)
248 fourierdlem39.gbd . . . 4 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺𝑥)) ≤ 𝑦)
249247, 248r19.29a 3071 . . 3 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤)
25046, 50, 161, 249cnbdibl 39485 . 2 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) ∈ 𝐿1)
2518oveq2d 6620 . . 3 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))) = (ℝ D 𝐹))
252 fourierdlem39.g . . . . 5 𝐺 = (ℝ D 𝐹)
253252eqcomi 2630 . . . 4 (ℝ D 𝐹) = 𝐺
254253a1i 11 . . 3 (𝜑 → (ℝ D 𝐹) = 𝐺)
255251, 254, 343eqtrd 2659 . 2 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑥)))
256 reelprrecn 9972 . . . . 5 ℝ ∈ {ℝ, ℂ}
257256a1i 11 . . . 4 (𝜑 → ℝ ∈ {ℝ, ℂ})
25817adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℂ)
259 recn 9970 . . . . . . . . 9 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
260259adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
261258, 260mulcld 10004 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝑅 · 𝑥) ∈ ℂ)
262261coscld 14786 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (cos‘(𝑅 · 𝑥)) ∈ ℂ)
263164adantr 481 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → 𝑅 ≠ 0)
264262, 258, 263divcld 10745 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
265264negcld 10323 . . . 4 ((𝜑𝑥 ∈ ℝ) → -((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ)
26616adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℝ)
267 simpr 477 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
268266, 267remulcld 10014 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑅 · 𝑥) ∈ ℝ)
269268resincld 14798 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (sin‘(𝑅 · 𝑥)) ∈ ℝ)
270269renegcld 10401 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → -(sin‘(𝑅 · 𝑥)) ∈ ℝ)
271270, 266remulcld 10014 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (-(sin‘(𝑅 · 𝑥)) · 𝑅) ∈ ℝ)
272271, 266, 263redivcld 10797 . . . . 5 ((𝜑𝑥 ∈ ℝ) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℝ)
273272renegcld 10401 . . . 4 ((𝜑𝑥 ∈ ℝ) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℝ)
274 recoscl 14796 . . . . . . . . 9 (𝑦 ∈ ℝ → (cos‘𝑦) ∈ ℝ)
275274adantl 482 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (cos‘𝑦) ∈ ℝ)
276275recnd 10012 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → (cos‘𝑦) ∈ ℂ)
277 resincl 14795 . . . . . . . . 9 (𝑦 ∈ ℝ → (sin‘𝑦) ∈ ℝ)
278277renegcld 10401 . . . . . . . 8 (𝑦 ∈ ℝ → -(sin‘𝑦) ∈ ℝ)
279278adantl 482 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → -(sin‘𝑦) ∈ ℝ)
280 1red 9999 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 1 ∈ ℝ)
281257dvmptid 23626 . . . . . . . . 9 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
282257, 260, 280, 281, 17dvmptcmul 23633 . . . . . . . 8 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝑅 · 𝑥))) = (𝑥 ∈ ℝ ↦ (𝑅 · 1)))
283258mulid1d 10001 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → (𝑅 · 1) = 𝑅)
284283mpteq2dva 4704 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ ↦ (𝑅 · 1)) = (𝑥 ∈ ℝ ↦ 𝑅))
285282, 284eqtrd 2655 . . . . . . 7 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝑅 · 𝑥))) = (𝑥 ∈ ℝ ↦ 𝑅))
286 dvcosre 39430 . . . . . . . 8 (ℝ D (𝑦 ∈ ℝ ↦ (cos‘𝑦))) = (𝑦 ∈ ℝ ↦ -(sin‘𝑦))
287286a1i 11 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (cos‘𝑦))) = (𝑦 ∈ ℝ ↦ -(sin‘𝑦)))
288 fveq2 6148 . . . . . . 7 (𝑦 = (𝑅 · 𝑥) → (cos‘𝑦) = (cos‘(𝑅 · 𝑥)))
289 fveq2 6148 . . . . . . . 8 (𝑦 = (𝑅 · 𝑥) → (sin‘𝑦) = (sin‘(𝑅 · 𝑥)))
290289negeqd 10219 . . . . . . 7 (𝑦 = (𝑅 · 𝑥) → -(sin‘𝑦) = -(sin‘(𝑅 · 𝑥)))
291257, 257, 268, 266, 276, 279, 285, 287, 288, 290dvmptco 23641 . . . . . 6 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (cos‘(𝑅 · 𝑥)))) = (𝑥 ∈ ℝ ↦ (-(sin‘(𝑅 · 𝑥)) · 𝑅)))
292257, 262, 271, 291, 17, 164dvmptdivc 23634 . . . . 5 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ ℝ ↦ ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)))
293257, 264, 272, 292dvmptneg 23635 . . . 4 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ ℝ ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)))
294 eqid 2621 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
295294tgioo2 22514 . . . 4 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
296 iccntr 22532 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
2971, 2, 296syl2anc 692 . . . 4 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
298257, 265, 273, 293, 12, 295, 294, 297dvmptres2 23631 . . 3 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)))
29980, 170mulneg1d 10427 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (-(sin‘(𝑅 · 𝑥)) · 𝑅) = -((sin‘(𝑅 · 𝑥)) · 𝑅))
300299oveq1d 6619 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (-((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
30180, 170mulcld 10004 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((sin‘(𝑅 · 𝑥)) · 𝑅) ∈ ℂ)
302301, 170, 175divnegd 10758 . . . . . . 7 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (-((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
303300, 302eqtr4d 2658 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = -(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
304303negeqd 10219 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = --(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
305301, 170, 175divcld 10745 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℂ)
306305negnegd 10327 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → --(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))
30780, 170, 175divcan4d 10751 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (sin‘(𝑅 · 𝑥)))
308304, 306, 3073eqtrd 2659 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (sin‘(𝑅 · 𝑥)))
309308mpteq2dva 4704 . . 3 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))))
310298, 309eqtrd 2655 . 2 (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))))
311 fveq2 6148 . . . 4 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
312 oveq2 6612 . . . . . . 7 (𝑥 = 𝐴 → (𝑅 · 𝑥) = (𝑅 · 𝐴))
313312fveq2d 6152 . . . . . 6 (𝑥 = 𝐴 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝐴)))
314313oveq1d 6619 . . . . 5 (𝑥 = 𝐴 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝐴)) / 𝑅))
315314negeqd 10219 . . . 4 (𝑥 = 𝐴 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝐴)) / 𝑅))
316311, 315oveq12d 6622 . . 3 (𝑥 = 𝐴 → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅)))
317316adantl 482 . 2 ((𝜑𝑥 = 𝐴) → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅)))
318 fveq2 6148 . . . 4 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
319 oveq2 6612 . . . . . . 7 (𝑥 = 𝐵 → (𝑅 · 𝑥) = (𝑅 · 𝐵))
320319fveq2d 6152 . . . . . 6 (𝑥 = 𝐵 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝐵)))
321320oveq1d 6619 . . . . 5 (𝑥 = 𝐵 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝐵)) / 𝑅))
322321negeqd 10219 . . . 4 (𝑥 = 𝐵 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝐵)) / 𝑅))
323318, 322oveq12d 6622 . . 3 (𝑥 = 𝐵 → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)))
324323adantl 482 . 2 ((𝜑𝑥 = 𝐵) → ((𝐹𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)))
3251, 2, 3, 9, 30, 36, 44, 156, 250, 255, 310, 317, 324itgparts 23714 1 (𝜑 → ∫(𝐴(,)𝐵)((𝐹𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  cdif 3552  wss 3555  {csn 4148  {cpr 4150   class class class wbr 4613  cmpt 4673  dom cdm 5074  ran crn 5075  wf 5843  cfv 5847  (class class class)co 6604  cc 9878  cr 9879  0cc0 9880  1c1 9881   · cmul 9885  cle 10019  cmin 10210  -cneg 10211   / cdiv 10628  +crp 11776  (,)cioo 12117  [,]cicc 12120  abscabs 13908  sincsin 14719  cosccos 14720  TopOpenctopn 16003  topGenctg 16019  fldccnfld 19665  intcnt 20731  cnccncf 22587  volcvol 23139  citg 23293   D cdv 23533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cc 9201  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-ofr 6851  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-omul 7510  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-acn 8712  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ioc 12122  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-fac 13001  df-bc 13030  df-hash 13058  df-shft 13741  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-limsup 14136  df-clim 14153  df-rlim 14154  df-sum 14351  df-ef 14723  df-sin 14725  df-cos 14726  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-fbas 19662  df-fg 19663  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-lp 20850  df-perf 20851  df-cn 20941  df-cnp 20942  df-haus 21029  df-cmp 21100  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-xms 22035  df-ms 22036  df-tms 22037  df-cncf 22589  df-ovol 23140  df-vol 23141  df-mbf 23294  df-itg1 23295  df-itg2 23296  df-ibl 23297  df-itg 23298  df-0p 23343  df-limc 23536  df-dv 23537
This theorem is referenced by:  fourierdlem73  39703
  Copyright terms: Public domain W3C validator