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

Theorem fourierdlem68 40709
 Description: The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem68.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem68.xre (𝜑𝑋 ∈ ℝ)
fourierdlem68.a (𝜑𝐴 ∈ ℝ)
fourierdlem68.b (𝜑𝐵 ∈ ℝ)
fourierdlem68.altb (𝜑𝐴 < 𝐵)
fourierdlem68.ab (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem68.n0 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem68.fdv (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
fourierdlem68.d (𝜑𝐷 ∈ ℝ)
fourierdlem68.fbd ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹𝑡)) ≤ 𝐷)
fourierdlem68.e (𝜑𝐸 ∈ ℝ)
fourierdlem68.fdvbd ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)
fourierdlem68.c (𝜑𝐶 ∈ ℝ)
fourierdlem68.o 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
Assertion
Ref Expression
fourierdlem68 (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))
Distinct variable groups:   𝐴,𝑏,𝑠   𝑡,𝐴,𝑠   𝐵,𝑏,𝑠   𝑡,𝐵   𝐶,𝑏,𝑠   𝐷,𝑏,𝑠   𝑡,𝐷   𝐸,𝑏,𝑠   𝑡,𝐸   𝐹,𝑏,𝑠   𝑡,𝐹   𝑋,𝑏,𝑠   𝑡,𝑋   𝜑,𝑏,𝑠   𝜑,𝑡
Allowed substitution hints:   𝐶(𝑡)   𝑂(𝑡,𝑠,𝑏)

Proof of Theorem fourierdlem68
Dummy variable 𝑐 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem68.f . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
2 fourierdlem68.xre . . . . . 6 (𝜑𝑋 ∈ ℝ)
3 fourierdlem68.a . . . . . 6 (𝜑𝐴 ∈ ℝ)
4 fourierdlem68.b . . . . . 6 (𝜑𝐵 ∈ ℝ)
5 fourierdlem68.fdv . . . . . 6 (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
6 ioossicc 12297 . . . . . . 7 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
7 fourierdlem68.ab . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
86, 7syl5ss 3647 . . . . . 6 (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
9 fourierdlem68.n0 . . . . . . 7 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
106sseli 3632 . . . . . . 7 (0 ∈ (𝐴(,)𝐵) → 0 ∈ (𝐴[,]𝐵))
119, 10nsyl 135 . . . . . 6 (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
12 fourierdlem68.c . . . . . 6 (𝜑𝐶 ∈ ℝ)
13 fourierdlem68.o . . . . . 6 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
141, 2, 3, 4, 5, 8, 11, 12, 13fourierdlem57 40698 . . . . 5 ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
1514simpli 473 . . . 4 (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
1615simpld 474 . . 3 (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
17 fdm 6089 . . 3 ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ → dom (ℝ D 𝑂) = (𝐴(,)𝐵))
1816, 17syl 17 . 2 (𝜑 → dom (ℝ D 𝑂) = (𝐴(,)𝐵))
19 eqid 2651 . . . . . 6 (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2))))
20 fourierdlem68.altb . . . . . . 7 (𝜑𝐴 < 𝐵)
213, 4, 20ltled 10223 . . . . . 6 (𝜑𝐴𝐵)
22 2re 11128 . . . . . . . . . . 11 2 ∈ ℝ
2322a1i 11 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℝ)
243, 4iccssred 40045 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
2524sselda 3636 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ)
2625rehalfcld 11317 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 / 2) ∈ ℝ)
2726resincld 14917 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℝ)
2823, 27remulcld 10108 . . . . . . . . 9 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ ℝ)
29 2cnd 11131 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
3027recnd 10106 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℂ)
31 2ne0 11151 . . . . . . . . . . 11 2 ≠ 0
3231a1i 11 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
337sselda 3636 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (-π[,]π))
34 eqcom 2658 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 ↔ 0 = 𝑡)
3534biimpi 206 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → 0 = 𝑡)
3635adantl 481 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 = 𝑡)
37 simpl 472 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 𝑡 ∈ (𝐴[,]𝐵))
3836, 37eqeltrd 2730 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
3938adantll 750 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
409ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
4139, 40pm2.65da 599 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → ¬ 𝑡 = 0)
4241neqned 2830 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≠ 0)
43 fourierdlem44 40686 . . . . . . . . . . 11 ((𝑡 ∈ (-π[,]π) ∧ 𝑡 ≠ 0) → (sin‘(𝑡 / 2)) ≠ 0)
4433, 42, 43syl2anc 694 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ≠ 0)
4529, 30, 32, 44mulne0d 10717 . . . . . . . . 9 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ≠ 0)
46 eldifsn 4350 . . . . . . . . 9 ((2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖ {0}) ↔ ((2 · (sin‘(𝑡 / 2))) ∈ ℝ ∧ (2 · (sin‘(𝑡 / 2))) ≠ 0))
4728, 45, 46sylanbrc 699 . . . . . . . 8 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖ {0}))
4847, 19fmptd 6425 . . . . . . 7 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0}))
49 difss 3770 . . . . . . . . . 10 (ℝ ∖ {0}) ⊆ ℝ
50 ax-resscn 10031 . . . . . . . . . 10 ℝ ⊆ ℂ
5149, 50sstri 3645 . . . . . . . . 9 (ℝ ∖ {0}) ⊆ ℂ
5251a1i 11 . . . . . . . 8 (𝜑 → (ℝ ∖ {0}) ⊆ ℂ)
5324, 50syl6ss 3648 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
54 2cnd 11131 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
55 ssid 3657 . . . . . . . . . . 11 ℂ ⊆ ℂ
5655a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ⊆ ℂ)
5753, 54, 56constcncfg 40402 . . . . . . . . 9 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ))
58 sincn 24243 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
5958a1i 11 . . . . . . . . . 10 (𝜑 → sin ∈ (ℂ–cn→ℂ))
6053, 56idcncfg 40403 . . . . . . . . . . 11 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
61 eldifsn 4350 . . . . . . . . . . . . . 14 (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
6229, 32, 61sylanbrc 699 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ (ℂ ∖ {0}))
63 eqid 2651 . . . . . . . . . . . . 13 (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) = (𝑡 ∈ (𝐴[,]𝐵) ↦ 2)
6462, 63fmptd 6425 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0}))
65 difssd 3771 . . . . . . . . . . . . 13 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
66 cncffvrn 22748 . . . . . . . . . . . . 13 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0})))
6765, 57, 66syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0})))
6864, 67mpbird 247 . . . . . . . . . . 11 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})))
6960, 68divcncf 23262 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 / 2)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
7059, 69cncfmpt1f 22763 . . . . . . . . 9 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (sin‘(𝑡 / 2))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
7157, 70mulcncf 23261 . . . . . . . 8 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
72 cncffvrn 22748 . . . . . . . 8 (((ℝ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0})))
7352, 71, 72syl2anc 694 . . . . . . 7 (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0})))
7448, 73mpbird 247 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})))
7519, 3, 4, 21, 74cncficcgt0 40419 . . . . 5 (𝜑 → ∃𝑐 ∈ ℝ+𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))))
76 reelprrecn 10066 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
7776a1i 11 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ℝ ∈ {ℝ, ℂ})
781adantr 480 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
792adantr 480 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
80 elioore 12243 . . . . . . . . . . . . 13 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
8180adantl 481 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
8279, 81readdcld 10107 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
8378, 82ffvelrnd 6400 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
8412adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
8583, 84resubcld 10496 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
8685recnd 10106 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
87863ad2antl1 1243 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
8876a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ {ℝ, ℂ})
8983recnd 10106 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
905adantr 480 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
912, 3readdcld 10107 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
9291rexrd 10127 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + 𝐴) ∈ ℝ*)
9392adantr 480 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ*)
942, 4readdcld 10107 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
9594rexrd 10127 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + 𝐵) ∈ ℝ*)
9695adantr 480 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ*)
973adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
9897rexrd 10127 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ*)
994rexrd 10127 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ*)
10099adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ*)
101 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
102 ioogtlb 40035 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
10398, 100, 101, 102syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
10497, 81, 79, 103ltadd2dd 10234 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
1054adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
106 iooltub 40053 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
10798, 100, 101, 106syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
10881, 105, 79, 107ltadd2dd 10234 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
10993, 96, 82, 104, 108eliood 40038 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
11090, 109ffvelrnd 6400 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
111 eqid 2651 . . . . . . . . . . 11 (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
1121, 2, 3, 4, 111, 5fourierdlem28 40670 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
11384recnd 10106 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
114 0red 10079 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
115 iooretop 22616 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
116 eqid 2651 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
117116tgioo2 22653 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
118115, 117eleqtri 2728 . . . . . . . . . . . 12 (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ)
119118a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ))
12012recnd 10106 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℂ)
12188, 119, 120dvmptconst 40447 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
12288, 89, 110, 112, 113, 114, 121dvmptsub 23775 . . . . . . . . 9 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
123110recnd 10106 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
124123subid1d 10419 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
125124mpteq2dva 4777 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
126122, 125eqtrd 2685 . . . . . . . 8 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
1271263ad2ant1 1102 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
1281233ad2antl1 1243 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
129 2cnd 11131 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ)
13080recnd 10106 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ)
131130halfcld 11315 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ)
132131sincld 14904 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ)
133129, 132mulcld 10098 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
134133adantl 481 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
135 fourierdlem68.e . . . . . . . 8 (𝜑𝐸 ∈ ℝ)
1361353ad2ant1 1102 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝐸 ∈ ℝ)
137 1re 10077 . . . . . . . . 9 1 ∈ ℝ
13822, 137remulcli 10092 . . . . . . . 8 (2 · 1) ∈ ℝ
139138a1i 11 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (2 · 1) ∈ ℝ)
140 1red 10093 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 1 ∈ ℝ)
141 fourierdlem68.d . . . . . . . . 9 (𝜑𝐷 ∈ ℝ)
142120abscld 14219 . . . . . . . . 9 (𝜑 → (abs‘𝐶) ∈ ℝ)
143141, 142readdcld 10107 . . . . . . . 8 (𝜑 → (𝐷 + (abs‘𝐶)) ∈ ℝ)
1441433ad2ant1 1102 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
145 simpl 472 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝜑)
146145, 109jca 553 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
147 eleq1 2718 . . . . . . . . . . . 12 (𝑡 = (𝑋 + 𝑠) → (𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ↔ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
148147anbi2d 740 . . . . . . . . . . 11 (𝑡 = (𝑋 + 𝑠) → ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) ↔ (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))))
149 fveq2 6229 . . . . . . . . . . . . 13 (𝑡 = (𝑋 + 𝑠) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
150149fveq2d 6233 . . . . . . . . . . . 12 (𝑡 = (𝑋 + 𝑠) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
151150breq1d 4695 . . . . . . . . . . 11 (𝑡 = (𝑋 + 𝑠) → ((abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸 ↔ (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
152148, 151imbi12d 333 . . . . . . . . . 10 (𝑡 = (𝑋 + 𝑠) → (((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)))
153 fourierdlem68.fdvbd . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)
154152, 153vtoclg 3297 . . . . . . . . 9 ((𝑋 + 𝑠) ∈ ℝ → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
15582, 146, 154sylc 65 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
1561553ad2antl1 1243 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
157129, 132absmuld 14237 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) = ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))))
158 0le2 11149 . . . . . . . . . . . 12 0 ≤ 2
159 absid 14080 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
16022, 158, 159mp2an 708 . . . . . . . . . . 11 (abs‘2) = 2
161160oveq1i 6700 . . . . . . . . . 10 ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) = (2 · (abs‘(sin‘(𝑠 / 2))))
162132abscld 14219 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ∈ ℝ)
163 1red 10093 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 1 ∈ ℝ)
16422a1i 11 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℝ)
165158a1i 11 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 0 ≤ 2)
16680rehalfcld 11317 . . . . . . . . . . . 12 (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℝ)
167 abssinbd 39823 . . . . . . . . . . . 12 ((𝑠 / 2) ∈ ℝ → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
168166, 167syl 17 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
169162, 163, 164, 165, 168lemul2ad 11002 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐵) → (2 · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
170161, 169syl5eqbr 4720 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
171157, 170eqbrtrd 4707 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
172171adantl 481 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
173 abscosbd 39804 . . . . . . . . 9 ((𝑠 / 2) ∈ ℝ → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
174101, 166, 1733syl 18 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
1751743ad2antl1 1243 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
17686abscld 14219 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
17789abscld 14219 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ∈ ℝ)
178113abscld 14219 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘𝐶) ∈ ℝ)
179177, 178readdcld 10107 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ∈ ℝ)
180141adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℝ)
181180, 178readdcld 10107 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
18289, 113abs2dif2d 14241 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)))
183 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑡 = (𝑋 + 𝑠) → (𝐹𝑡) = (𝐹‘(𝑋 + 𝑠)))
184183fveq2d 6233 . . . . . . . . . . . . . 14 (𝑡 = (𝑋 + 𝑠) → (abs‘(𝐹𝑡)) = (abs‘(𝐹‘(𝑋 + 𝑠))))
185184breq1d 4695 . . . . . . . . . . . . 13 (𝑡 = (𝑋 + 𝑠) → ((abs‘(𝐹𝑡)) ≤ 𝐷 ↔ (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
186148, 185imbi12d 333 . . . . . . . . . . . 12 (𝑡 = (𝑋 + 𝑠) → (((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹𝑡)) ≤ 𝐷) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)))
187 fourierdlem68.fbd . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹𝑡)) ≤ 𝐷)
188186, 187vtoclg 3297 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
189109, 146, 188sylc 65 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)
190177, 180, 178, 189leadd1dd 10679 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ≤ (𝐷 + (abs‘𝐶)))
191176, 179, 181, 182, 190letrd 10232 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
1921913ad2antl1 1243 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
19314simpri 477 . . . . . . . 8 (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
194193a1i 11 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
195131coscld 14905 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
196195adantl 481 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
197 simp2 1082 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝑐 ∈ ℝ+)
198 oveq1 6697 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (𝑡 / 2) = (𝑠 / 2))
199198fveq2d 6233 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (sin‘(𝑡 / 2)) = (sin‘(𝑠 / 2)))
200199oveq2d 6706 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (2 · (sin‘(𝑡 / 2))) = (2 · (sin‘(𝑠 / 2))))
201200fveq2d 6233 . . . . . . . . . . 11 (𝑡 = 𝑠 → (abs‘(2 · (sin‘(𝑡 / 2)))) = (abs‘(2 · (sin‘(𝑠 / 2)))))
202201breq2d 4697 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
203202cbvralv 3201 . . . . . . . . 9 (∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
204 nfv 1883 . . . . . . . . . . 11 𝑠𝜑
205 nfra1 2970 . . . . . . . . . . 11 𝑠𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))
206204, 205nfan 1868 . . . . . . . . . 10 𝑠(𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
207 simplr 807 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
2086, 101sseldi 3634 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
209208adantlr 751 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
210 rspa 2959 . . . . . . . . . . . 12 ((∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))) ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
211207, 209, 210syl2anc 694 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
212211ex 449 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → (𝑠 ∈ (𝐴(,)𝐵) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
213206, 212ralrimi 2986 . . . . . . . . 9 ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
214203, 213sylan2b 491 . . . . . . . 8 ((𝜑 ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
2152143adant2 1100 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
216 eqid 2651 . . . . . . 7 (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
21777, 87, 127, 128, 134, 136, 139, 140, 144, 156, 172, 175, 192, 194, 196, 197, 215, 216dvdivbd 40456 . . . . . 6 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
218217rexlimdv3a 3062 . . . . 5 (𝜑 → (∃𝑐 ∈ ℝ+𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
21975, 218mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
220 nfcv 2793 . . . . . . . . 9 𝑠
221 nfcv 2793 . . . . . . . . 9 𝑠 D
222 nfmpt1 4780 . . . . . . . . . 10 𝑠(𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
22313, 222nfcxfr 2791 . . . . . . . . 9 𝑠𝑂
224220, 221, 223nfov 6716 . . . . . . . 8 𝑠(ℝ D 𝑂)
225224nfdm 5399 . . . . . . 7 𝑠dom (ℝ D 𝑂)
226 nfcv 2793 . . . . . . 7 𝑠(𝐴(,)𝐵)
227225, 226raleqf 3164 . . . . . 6 (dom (ℝ D 𝑂) = (𝐴(,)𝐵) → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
22818, 227syl 17 . . . . 5 (𝜑 → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
229228rexbidv 3081 . . . 4 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
230219, 229mpbird 247 . . 3 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
23113a1i 11 . . . . . . . 8 (𝜑𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
232231oveq2d 6706 . . . . . . 7 (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
233232fveq1d 6231 . . . . . 6 (𝜑 → ((ℝ D 𝑂)‘𝑠) = ((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠))
234233fveq2d 6233 . . . . 5 (𝜑 → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)))
235234breq1d 4695 . . . 4 (𝜑 → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
236235rexralbidv 3087 . . 3 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
237230, 236mpbird 247 . 2 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)
23818, 237jca 553 1 (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942   ∖ cdif 3604   ⊆ wss 3607  {csn 4210  {cpr 4212   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143  ran crn 5144   ↾ cres 5145  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  2c2 11108  ℝ+crp 11870  (,)cioo 12213  [,]cicc 12216  ↑cexp 12900  abscabs 14018  sincsin 14838  cosccos 14839  πcpi 14841   ↾t crest 16128  TopOpenctopn 16129  topGenctg 16145  ℂfldccnfld 19794  –cn→ccncf 22726   D cdv 23672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-t1 21166  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676 This theorem is referenced by:  fourierdlem80  40721
 Copyright terms: Public domain W3C validator