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

Theorem fourierdlem68 38864
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 12086 . . . . . . 7 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
7 fourierdlem68.ab . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
86, 7syl5ss 3578 . . . . . 6 (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
9 fourierdlem68.n0 . . . . . . 7 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
106sseli 3563 . . . . . . 7 (0 ∈ (𝐴(,)𝐵) → 0 ∈ (𝐴[,]𝐵))
119, 10nsyl 133 . . . . . 6 (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
12 fourierdlem68.c . . . . . 6 (𝜑𝐶 ∈ ℝ)
13 fourierdlem68.o . . . . . 6 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
141, 2, 3, 4, 5, 8, 11, 12, 13fourierdlem57 38853 . . . . 5 ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
1514simpli 472 . . . 4 (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
1615simpld 473 . . 3 (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
17 fdm 5950 . . 3 ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ → dom (ℝ D 𝑂) = (𝐴(,)𝐵))
1816, 17syl 17 . 2 (𝜑 → dom (ℝ D 𝑂) = (𝐴(,)𝐵))
19 eqid 2609 . . . . . 6 (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2))))
20 fourierdlem68.altb . . . . . . 7 (𝜑𝐴 < 𝐵)
213, 4, 20ltled 10036 . . . . . 6 (𝜑𝐴𝐵)
22 2re 10937 . . . . . . . . . . 11 2 ∈ ℝ
2322a1i 11 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℝ)
243, 4iccssred 38371 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
2524sselda 3567 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ)
2625rehalfcld 11126 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 / 2) ∈ ℝ)
2726resincld 14658 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℝ)
2823, 27remulcld 9926 . . . . . . . . 9 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ ℝ)
29 2cnd 10940 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
3027recnd 9924 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℂ)
31 2ne0 10960 . . . . . . . . . . 11 2 ≠ 0
3231a1i 11 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
337sselda 3567 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (-π[,]π))
34 eqcom 2616 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 ↔ 0 = 𝑡)
3534biimpi 204 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → 0 = 𝑡)
3635adantl 480 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 = 𝑡)
37 simpl 471 . . . . . . . . . . . . . . 15 ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 𝑡 ∈ (𝐴[,]𝐵))
3836, 37eqeltrd 2687 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
3938adantll 745 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
409ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
4139, 40pm2.65da 597 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → ¬ 𝑡 = 0)
4241neqned 2788 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≠ 0)
43 fourierdlem44 38841 . . . . . . . . . . 11 ((𝑡 ∈ (-π[,]π) ∧ 𝑡 ≠ 0) → (sin‘(𝑡 / 2)) ≠ 0)
4433, 42, 43syl2anc 690 . . . . . . . . . 10 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ≠ 0)
4529, 30, 32, 44mulne0d 10528 . . . . . . . . 9 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ≠ 0)
46 eldifsn 4259 . . . . . . . . 9 ((2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖ {0}) ↔ ((2 · (sin‘(𝑡 / 2))) ∈ ℝ ∧ (2 · (sin‘(𝑡 / 2))) ≠ 0))
4728, 45, 46sylanbrc 694 . . . . . . . 8 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖ {0}))
4847, 19fmptd 6277 . . . . . . 7 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0}))
49 difss 3698 . . . . . . . . . 10 (ℝ ∖ {0}) ⊆ ℝ
50 ax-resscn 9849 . . . . . . . . . 10 ℝ ⊆ ℂ
5149, 50sstri 3576 . . . . . . . . 9 (ℝ ∖ {0}) ⊆ ℂ
5251a1i 11 . . . . . . . 8 (𝜑 → (ℝ ∖ {0}) ⊆ ℂ)
5324, 50syl6ss 3579 . . . . . . . . . 10 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
54 2cnd 10940 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
55 ssid 3586 . . . . . . . . . . 11 ℂ ⊆ ℂ
5655a1i 11 . . . . . . . . . 10 (𝜑 → ℂ ⊆ ℂ)
5753, 54, 56constcncfg 38553 . . . . . . . . 9 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ))
58 sincn 23919 . . . . . . . . . . 11 sin ∈ (ℂ–cn→ℂ)
5958a1i 11 . . . . . . . . . 10 (𝜑 → sin ∈ (ℂ–cn→ℂ))
6053, 56idcncfg 38554 . . . . . . . . . . 11 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
61 eldifsn 4259 . . . . . . . . . . . . . 14 (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
6229, 32, 61sylanbrc 694 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ (ℂ ∖ {0}))
63 eqid 2609 . . . . . . . . . . . . 13 (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) = (𝑡 ∈ (𝐴[,]𝐵) ↦ 2)
6462, 63fmptd 6277 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0}))
65 difssd 3699 . . . . . . . . . . . . 13 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
66 cncffvrn 22440 . . . . . . . . . . . . 13 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0})))
6765, 57, 66syl2anc 690 . . . . . . . . . . . 12 (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0})))
6864, 67mpbird 245 . . . . . . . . . . 11 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})))
6960, 68divcncf 38566 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 / 2)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
7059, 69cncfmpt1f 22455 . . . . . . . . 9 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (sin‘(𝑡 / 2))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
7157, 70mulcncf 22940 . . . . . . . 8 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
72 cncffvrn 22440 . . . . . . . 8 (((ℝ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0})))
7352, 71, 72syl2anc 690 . . . . . . 7 (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0})))
7448, 73mpbird 245 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})))
7519, 3, 4, 21, 74cncficcgt0 38571 . . . . 5 (𝜑 → ∃𝑐 ∈ ℝ+𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))))
76 reelprrecn 9884 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
7776a1i 11 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ℝ ∈ {ℝ, ℂ})
781adantr 479 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
792adantr 479 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
80 elioore 12032 . . . . . . . . . . . . 13 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
8180adantl 480 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
8279, 81readdcld 9925 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
8378, 82ffvelrnd 6253 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
8412adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
8583, 84resubcld 10309 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
8685recnd 9924 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
87863ad2antl1 1215 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
8876a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ {ℝ, ℂ})
8983recnd 9924 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
905adantr 479 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
912, 3readdcld 9925 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
9291rexrd 9945 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + 𝐴) ∈ ℝ*)
9392adantr 479 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ*)
942, 4readdcld 9925 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
9594rexrd 9945 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + 𝐵) ∈ ℝ*)
9695adantr 479 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ*)
973adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
9897rexrd 9945 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ*)
994rexrd 9945 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ*)
10099adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ*)
101 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
102 ioogtlb 38361 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
10398, 100, 101, 102syl3anc 1317 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
10497, 81, 79, 103ltadd2dd 10047 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
1054adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
106 iooltub 38379 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
10798, 100, 101, 106syl3anc 1317 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
10881, 105, 79, 107ltadd2dd 10047 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
10993, 96, 82, 104, 108eliood 38364 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
11090, 109ffvelrnd 6253 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
111 eqid 2609 . . . . . . . . . . 11 (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
1121, 2, 3, 4, 111, 5fourierdlem28 38825 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
11384recnd 9924 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
114 0red 9897 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
115 iooretop 22311 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
116 eqid 2609 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
117116tgioo2 22346 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
118115, 117eleqtri 2685 . . . . . . . . . . . 12 (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ)
119118a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂfld) ↾t ℝ))
12012recnd 9924 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℂ)
12188, 119, 120dvmptconst 38600 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
12288, 89, 110, 112, 113, 114, 121dvmptsub 23453 . . . . . . . . 9 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
123110recnd 9924 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
124123subid1d 10232 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
125124mpteq2dva 4666 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
126122, 125eqtrd 2643 . . . . . . . 8 (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
1271263ad2ant1 1074 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
1281233ad2antl1 1215 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
129 2cnd 10940 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ)
13080recnd 9924 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ)
131130halfcld 11124 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ)
132131sincld 14645 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ)
133129, 132mulcld 9916 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
134133adantl 480 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
135 fourierdlem68.e . . . . . . . 8 (𝜑𝐸 ∈ ℝ)
1361353ad2ant1 1074 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝐸 ∈ ℝ)
137 1re 9895 . . . . . . . . 9 1 ∈ ℝ
13822, 137remulcli 9910 . . . . . . . 8 (2 · 1) ∈ ℝ
139138a1i 11 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (2 · 1) ∈ ℝ)
140 1red 9911 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 1 ∈ ℝ)
141 fourierdlem68.d . . . . . . . . 9 (𝜑𝐷 ∈ ℝ)
142120abscld 13969 . . . . . . . . 9 (𝜑 → (abs‘𝐶) ∈ ℝ)
143141, 142readdcld 9925 . . . . . . . 8 (𝜑 → (𝐷 + (abs‘𝐶)) ∈ ℝ)
1441433ad2ant1 1074 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
145 simpl 471 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝜑)
146145, 109jca 552 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
147 eleq1 2675 . . . . . . . . . . . 12 (𝑡 = (𝑋 + 𝑠) → (𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ↔ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
148147anbi2d 735 . . . . . . . . . . 11 (𝑡 = (𝑋 + 𝑠) → ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) ↔ (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))))
149 fveq2 6088 . . . . . . . . . . . . 13 (𝑡 = (𝑋 + 𝑠) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
150149fveq2d 6092 . . . . . . . . . . . 12 (𝑡 = (𝑋 + 𝑠) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
151150breq1d 4587 . . . . . . . . . . 11 (𝑡 = (𝑋 + 𝑠) → ((abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸 ↔ (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
152148, 151imbi12d 332 . . . . . . . . . 10 (𝑡 = (𝑋 + 𝑠) → (((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)))
153 fourierdlem68.fdvbd . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)
154152, 153vtoclg 3238 . . . . . . . . 9 ((𝑋 + 𝑠) ∈ ℝ → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
15582, 146, 154sylc 62 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
1561553ad2antl1 1215 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
157129, 132absmuld 13987 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) = ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))))
158 0le2 10958 . . . . . . . . . . . 12 0 ≤ 2
159 absid 13830 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
16022, 158, 159mp2an 703 . . . . . . . . . . 11 (abs‘2) = 2
161160oveq1i 6537 . . . . . . . . . 10 ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) = (2 · (abs‘(sin‘(𝑠 / 2))))
162132abscld 13969 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ∈ ℝ)
163 1red 9911 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 1 ∈ ℝ)
16422a1i 11 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℝ)
165158a1i 11 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → 0 ≤ 2)
16680rehalfcld 11126 . . . . . . . . . . . 12 (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℝ)
167 abssinbd 38246 . . . . . . . . . . . 12 ((𝑠 / 2) ∈ ℝ → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
168166, 167syl 17 . . . . . . . . . . 11 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
169162, 163, 164, 165, 168lemul2ad 10813 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐵) → (2 · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
170161, 169syl5eqbr 4612 . . . . . . . . 9 (𝑠 ∈ (𝐴(,)𝐵) → ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
171157, 170eqbrtrd 4599 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
172171adantl 480 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
173 abscosbd 38227 . . . . . . . . 9 ((𝑠 / 2) ∈ ℝ → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
174101, 166, 1733syl 18 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
1751743ad2antl1 1215 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
17686abscld 13969 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
17789abscld 13969 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ∈ ℝ)
178113abscld 13969 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘𝐶) ∈ ℝ)
179177, 178readdcld 9925 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ∈ ℝ)
180141adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℝ)
181180, 178readdcld 9925 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
18289, 113abs2dif2d 13991 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)))
183 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑡 = (𝑋 + 𝑠) → (𝐹𝑡) = (𝐹‘(𝑋 + 𝑠)))
184183fveq2d 6092 . . . . . . . . . . . . . 14 (𝑡 = (𝑋 + 𝑠) → (abs‘(𝐹𝑡)) = (abs‘(𝐹‘(𝑋 + 𝑠))))
185184breq1d 4587 . . . . . . . . . . . . 13 (𝑡 = (𝑋 + 𝑠) → ((abs‘(𝐹𝑡)) ≤ 𝐷 ↔ (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
186148, 185imbi12d 332 . . . . . . . . . . . 12 (𝑡 = (𝑋 + 𝑠) → (((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹𝑡)) ≤ 𝐷) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)))
187 fourierdlem68.fbd . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹𝑡)) ≤ 𝐷)
188186, 187vtoclg 3238 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
189109, 146, 188sylc 62 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)
190177, 180, 178, 189leadd1dd 10490 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ≤ (𝐷 + (abs‘𝐶)))
191176, 179, 181, 182, 190letrd 10045 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
1921913ad2antl1 1215 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
19314simpri 476 . . . . . . . 8 (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
194193a1i 11 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
195131coscld 14646 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
196195adantl 480 . . . . . . 7 (((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
197 simp2 1054 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝑐 ∈ ℝ+)
198 oveq1 6534 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (𝑡 / 2) = (𝑠 / 2))
199198fveq2d 6092 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (sin‘(𝑡 / 2)) = (sin‘(𝑠 / 2)))
200199oveq2d 6543 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (2 · (sin‘(𝑡 / 2))) = (2 · (sin‘(𝑠 / 2))))
201200fveq2d 6092 . . . . . . . . . . 11 (𝑡 = 𝑠 → (abs‘(2 · (sin‘(𝑡 / 2)))) = (abs‘(2 · (sin‘(𝑠 / 2)))))
202201breq2d 4589 . . . . . . . . . 10 (𝑡 = 𝑠 → (𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
203202cbvralv 3146 . . . . . . . . 9 (∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
204 nfv 1829 . . . . . . . . . . 11 𝑠𝜑
205 nfra1 2924 . . . . . . . . . . 11 𝑠𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))
206204, 205nfan 1815 . . . . . . . . . 10 𝑠(𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
207 simplr 787 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
2086, 101sseldi 3565 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
209208adantlr 746 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
210 rspa 2913 . . . . . . . . . . . 12 ((∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))) ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
211207, 209, 210syl2anc 690 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
212211ex 448 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → (𝑠 ∈ (𝐴(,)𝐵) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
213206, 212ralrimi 2939 . . . . . . . . 9 ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
214203, 213sylan2b 490 . . . . . . . 8 ((𝜑 ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
2152143adant2 1072 . . . . . . 7 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
216 eqid 2609 . . . . . . 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 38610 . . . . . 6 ((𝜑𝑐 ∈ ℝ+ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
218217rexlimdv3a 3014 . . . . 5 (𝜑 → (∃𝑐 ∈ ℝ+𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
21975, 218mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
220 nfcv 2750 . . . . . . . . 9 𝑠
221 nfcv 2750 . . . . . . . . 9 𝑠 D
222 nfmpt1 4669 . . . . . . . . . 10 𝑠(𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
22313, 222nfcxfr 2748 . . . . . . . . 9 𝑠𝑂
224220, 221, 223nfov 6553 . . . . . . . 8 𝑠(ℝ D 𝑂)
225224nfdm 5275 . . . . . . 7 𝑠dom (ℝ D 𝑂)
226 nfcv 2750 . . . . . . 7 𝑠(𝐴(,)𝐵)
227225, 226raleqf 3110 . . . . . 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 3033 . . . 4 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
230219, 229mpbird 245 . . 3 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
23113a1i 11 . . . . . . . 8 (𝜑𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
232231oveq2d 6543 . . . . . . 7 (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
233232fveq1d 6090 . . . . . 6 (𝜑 → ((ℝ D 𝑂)‘𝑠) = ((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠))
234233fveq2d 6092 . . . . 5 (𝜑 → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)))
235234breq1d 4587 . . . 4 (𝜑 → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
236235rexralbidv 3039 . . 3 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
237230, 236mpbird 245 . 2 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)
23818, 237jca 552 1 (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  cdif 3536  wss 3539  {csn 4124  {cpr 4126   class class class wbr 4577  cmpt 4637  dom cdm 5028  ran crn 5029  cres 5030  wf 5786  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  *cxr 9929   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10533  2c2 10917  +crp 11664  (,)cioo 12002  [,]cicc 12005  cexp 12677  abscabs 13768  sincsin 14579  cosccos 14580  πcpi 14582  t crest 15850  TopOpenctopn 15851  topGenctg 15867  fldccnfld 19513  cnccncf 22418   D cdv 23350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ioc 12007  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-fac 12878  df-bc 12907  df-hash 12935  df-shft 13601  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-limsup 13996  df-clim 14013  df-rlim 14014  df-sum 14211  df-ef 14583  df-sin 14585  df-cos 14586  df-pi 14588  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-sca 15730  df-vsca 15731  df-ip 15732  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-hom 15739  df-cco 15740  df-rest 15852  df-topn 15853  df-0g 15871  df-gsum 15872  df-topgen 15873  df-pt 15874  df-prds 15877  df-xrs 15931  df-qtop 15936  df-imas 15937  df-xps 15939  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-fbas 19510  df-fg 19511  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-topsp 20466  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-lp 20692  df-perf 20693  df-cn 20783  df-cnp 20784  df-t1 20870  df-haus 20871  df-cmp 20942  df-tx 21117  df-hmeo 21310  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-xms 21876  df-ms 21877  df-tms 21878  df-cncf 22420  df-limc 23353  df-dv 23354
This theorem is referenced by:  fourierdlem80  38876
  Copyright terms: Public domain W3C validator