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

Theorem fourierdlem80 40882
Description: The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem80.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem80.xre (𝜑𝑋 ∈ ℝ)
fourierdlem80.a (𝜑𝐴 ∈ ℝ)
fourierdlem80.b (𝜑𝐵 ∈ ℝ)
fourierdlem80.ab (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem80.n0 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem80.c (𝜑𝐶 ∈ ℝ)
fourierdlem80.o 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
fourierdlem80.i 𝐼 = ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
fourierdlem80.fbdioo ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤)
fourierdlem80.fdvbdioo ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)
fourierdlem80.sf (𝜑𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
fourierdlem80.slt ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
fourierdlem80.sjss ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
fourierdlem80.relioo (((𝜑𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1))))
fdv ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹𝐼)):𝐼⟶ℝ)
fourierdlem80.y 𝑌 = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
fourierdlem80.ch (𝜒 ↔ (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧))
Assertion
Ref Expression
fourierdlem80 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)
Distinct variable groups:   𝐴,𝑏,𝑟,𝑠,𝑡   𝐵,𝑏,𝑟,𝑠,𝑡   𝐶,𝑏,𝑟,𝑠,𝑡   𝐹,𝑏,𝑟,𝑠,𝑡   𝑤,𝐹,𝑧,𝑠,𝑡   𝑤,𝐼,𝑧   𝑁,𝑏,𝑗,𝑟,𝑠   𝑘,𝑁,𝑗,𝑟   𝑤,𝑁,𝑧,𝑗   𝑂,𝑏,𝑗,𝑟   𝑤,𝑂,𝑧   𝑆,𝑏,𝑗,𝑟,𝑠,𝑡   𝑆,𝑘   𝑤,𝑆,𝑧   𝑋,𝑏,𝑟,𝑠,𝑡   𝑌,𝑠   𝜑,𝑏,𝑗,𝑟,𝑠   𝜒,𝑠,𝑡   𝜑,𝑤,𝑧
Allowed substitution hints:   𝜑(𝑡,𝑘)   𝜒(𝑧,𝑤,𝑗,𝑘,𝑟,𝑏)   𝐴(𝑧,𝑤,𝑗,𝑘)   𝐵(𝑧,𝑤,𝑗,𝑘)   𝐶(𝑧,𝑤,𝑗,𝑘)   𝐹(𝑗,𝑘)   𝐼(𝑡,𝑗,𝑘,𝑠,𝑟,𝑏)   𝑁(𝑡)   𝑂(𝑡,𝑘,𝑠)   𝑋(𝑧,𝑤,𝑗,𝑘)   𝑌(𝑧,𝑤,𝑡,𝑗,𝑘,𝑟,𝑏)

Proof of Theorem fourierdlem80
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem80.o . . . . . . . . 9 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
2 oveq2 6882 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
32fveq2d 6412 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
43oveq1d 6889 . . . . . . . . . . 11 (𝑠 = 𝑡 → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) = ((𝐹‘(𝑋 + 𝑡)) − 𝐶))
5 oveq1 6881 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → (𝑠 / 2) = (𝑡 / 2))
65fveq2d 6412 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (sin‘(𝑠 / 2)) = (sin‘(𝑡 / 2)))
76oveq2d 6890 . . . . . . . . . . 11 (𝑠 = 𝑡 → (2 · (sin‘(𝑠 / 2))) = (2 · (sin‘(𝑡 / 2))))
84, 7oveq12d 6892 . . . . . . . . . 10 (𝑠 = 𝑡 → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) = (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
98cbvmptv 4944 . . . . . . . . 9 (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
101, 9eqtr2i 2829 . . . . . . . 8 (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))) = 𝑂
1110oveq2i 6885 . . . . . . 7 (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = (ℝ D 𝑂)
1211dmeqi 5526 . . . . . 6 dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = dom (ℝ D 𝑂)
1312ineq2i 4010 . . . . 5 (ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))))) = (ran 𝑆 ∩ dom (ℝ D 𝑂))
1413sneqi 4381 . . . 4 {(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} = {(ran 𝑆 ∩ dom (ℝ D 𝑂))}
1514uneq1i 3962 . . 3 ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
16 snfi 8277 . . . . 5 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin
17 fzofi 12997 . . . . . 6 (0..^𝑁) ∈ Fin
18 eqid 2806 . . . . . . 7 (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
1918rnmptfi 39840 . . . . . 6 ((0..^𝑁) ∈ Fin → ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin)
2017, 19ax-mp 5 . . . . 5 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin
21 unfi 8466 . . . . 5 (({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin ∧ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin) → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
2216, 20, 21mp2an 675 . . . 4 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin
2322a1i 11 . . 3 (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
2415, 23syl5eqel 2889 . 2 (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
25 id 22 . . . 4 (𝑠 ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
2615unieqi 4639 . . . 4 ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
2725, 26syl6eleq 2895 . . 3 (𝑠 ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
28 simpl 470 . . . . 5 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → 𝜑)
29 uniun 4651 . . . . . . . . 9 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ( {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
3029eleq2i 2877 . . . . . . . 8 (𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ 𝑠 ∈ ( {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
31 elun 3952 . . . . . . . 8 (𝑠 ∈ ( {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
3230, 31sylbb 210 . . . . . . 7 (𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑠 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
3332adantl 469 . . . . . 6 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
34 fourierdlem80.sf . . . . . . . . . . . . 13 (𝜑𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
35 ovex 6906 . . . . . . . . . . . . . 14 (0...𝑁) ∈ V
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → (0...𝑁) ∈ V)
37 fex 6714 . . . . . . . . . . . . 13 ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ V) → 𝑆 ∈ V)
3834, 36, 37syl2anc 575 . . . . . . . . . . . 12 (𝜑𝑆 ∈ V)
39 rnexg 7328 . . . . . . . . . . . 12 (𝑆 ∈ V → ran 𝑆 ∈ V)
4038, 39syl 17 . . . . . . . . . . 11 (𝜑 → ran 𝑆 ∈ V)
41 inex1g 4996 . . . . . . . . . . 11 (ran 𝑆 ∈ V → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
4240, 41syl 17 . . . . . . . . . 10 (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
43 unisng 4645 . . . . . . . . . 10 ((ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V → {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
4442, 43syl 17 . . . . . . . . 9 (𝜑 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
4544eleq2d 2871 . . . . . . . 8 (𝜑 → (𝑠 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
4645adantr 468 . . . . . . 7 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
4746orbi1d 931 . . . . . 6 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((𝑠 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))))
4833, 47mpbid 223 . . . . 5 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
49 dvf 23885 . . . . . . . . 9 (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ
5049a1i 11 . . . . . . . 8 (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
51 elinel2 3999 . . . . . . . 8 (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → 𝑠 ∈ dom (ℝ D 𝑂))
5250, 51ffvelrnd 6582 . . . . . . 7 (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
5352adantl 469 . . . . . 6 ((𝜑𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
54 ovex 6906 . . . . . . . . . . . 12 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∈ V
5554dfiun3 5581 . . . . . . . . . . 11 𝑗 ∈ (0..^𝑁)((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) = ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
5655eleq2i 2877 . . . . . . . . . 10 (𝑠 𝑗 ∈ (0..^𝑁)((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
5756biimpri 219 . . . . . . . . 9 (𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 𝑗 ∈ (0..^𝑁)((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
5857adantl 469 . . . . . . . 8 ((𝜑𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 𝑗 ∈ (0..^𝑁)((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
59 eliun 4716 . . . . . . . 8 (𝑠 𝑗 ∈ (0..^𝑁)((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
6058, 59sylib 209 . . . . . . 7 ((𝜑𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
61 nfv 2005 . . . . . . . . 9 𝑗𝜑
62 nfmpt1 4941 . . . . . . . . . . . 12 𝑗(𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
6362nfrn 5569 . . . . . . . . . . 11 𝑗ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
6463nfuni 4636 . . . . . . . . . 10 𝑗 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
6564nfcri 2942 . . . . . . . . 9 𝑗 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
6661, 65nfan 1990 . . . . . . . 8 𝑗(𝜑𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
67 nfv 2005 . . . . . . . 8 𝑗((ℝ D 𝑂)‘𝑠) ∈ ℂ
6849a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
691reseq1i 5593 . . . . . . . . . . . . . . . . . . . 20 (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
70 ioossicc 12477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
71 fourierdlem80.sjss . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
7270, 71syl5ss 3809 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
7372resmptd 5657 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
7469, 73syl5eq 2852 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
75 fourierdlem80.y . . . . . . . . . . . . . . . . . . 19 𝑌 = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
7674, 75syl6reqr 2859 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑌 = (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
7776oveq2d 6890 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
78 ax-resscn 10278 . . . . . . . . . . . . . . . . . . . . 21 ℝ ⊆ ℂ
7978a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ℝ ⊆ ℂ)
80 fourierdlem80.f . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹:ℝ⟶ℝ)
8180adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
82 fourierdlem80.xre . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋 ∈ ℝ)
8382adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
84 fourierdlem80.a . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐴 ∈ ℝ)
85 fourierdlem80.b . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ℝ)
8684, 85iccssred 40211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
8786sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
8883, 87readdcld 10354 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
8981, 88ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
9089recnd 10353 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
91 fourierdlem80.c . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐶 ∈ ℝ)
9291recnd 10353 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐶 ∈ ℂ)
9392adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)
9490, 93subcld 10677 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
95 2cnd 11377 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
9686, 79sstrd 3808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
9796sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℂ)
9897halfcld 11544 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (𝑠 / 2) ∈ ℂ)
9998sincld 15080 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
10095, 99mulcld 10345 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
101 2ne0 11396 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ≠ 0
102101a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
103 fourierdlem80.ab . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
104103sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (-π[,]π))
105 eqcom 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑠 = 0 ↔ 0 = 𝑠)
106105biimpi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = 0 → 0 = 𝑠)
107106adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
108 simpl 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴[,]𝐵))
109107, 108eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
110109adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
111 fourierdlem80.n0 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
112111ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
113110, 112pm2.65da 842 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → ¬ 𝑠 = 0)
114113neqned 2985 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
115 fourierdlem44 40847 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
116104, 114, 115syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
11795, 99, 102, 116mulne0d 10964 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
11894, 100, 117divcld 11086 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑠 ∈ (𝐴[,]𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
119118, 1fmptd 6606 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑂:(𝐴[,]𝐵)⟶ℂ)
120 ioossre 12453 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
121120a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
122 eqid 2806 . . . . . . . . . . . . . . . . . . . . 21 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
123122tgioo2 22819 . . . . . . . . . . . . . . . . . . . . 21 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
124122, 123dvres 23889 . . . . . . . . . . . . . . . . . . . 20 (((ℝ ⊆ ℂ ∧ 𝑂:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)) → (ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
12579, 119, 86, 121, 124syl22anc 858 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
126 ioontr 40218 . . . . . . . . . . . . . . . . . . . 20 ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))
127126reseq2i 5594 . . . . . . . . . . . . . . . . . . 19 ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
128125, 127syl6eq 2856 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
129128adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
13077, 129eqtr2d 2841 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (ℝ D 𝑌))
131130dmeqd 5527 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = dom (ℝ D 𝑌))
13280adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℝ)
13382adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑋 ∈ ℝ)
13486adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
13534adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
136 elfzofz 12709 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
137136adantl 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
138135, 137ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ (𝐴[,]𝐵))
139134, 138sseldd 3799 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ)
140 fzofzp1 12789 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
141140adantl 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
142135, 141ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
143134, 142sseldd 3799 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
144 fdv . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹𝐼)):𝐼⟶ℝ)
145 fourierdlem80.i . . . . . . . . . . . . . . . . . . . . . 22 𝐼 = ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
146145feq2i 6248 . . . . . . . . . . . . . . . . . . . . 21 ((ℝ D (𝐹𝐼)):𝐼⟶ℝ ↔ (ℝ D (𝐹𝐼)):((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
147144, 146sylib 209 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹𝐼)):((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
148145reseq2i 5594 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝐼) = (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
149148oveq2i 6885 . . . . . . . . . . . . . . . . . . . . 21 (ℝ D (𝐹𝐼)) = (ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))
150149feq1i 6247 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D (𝐹𝐼)):((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ ↔ (ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
151147, 150sylib 209 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
152103adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ (-π[,]π))
15372, 152sstrd 3808 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
154111adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ (𝐴[,]𝐵))
15572, 154ssneldd 3801 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
15691adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
157132, 133, 139, 143, 151, 153, 155, 156, 75fourierdlem57 40859 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (cos‘(𝑠 / 2))))
158157simpli 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
159158simpld 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ)
160 fdm 6264 . . . . . . . . . . . . . . . 16 ((ℝ D 𝑌):((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ → dom (ℝ D 𝑌) = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
161159, 160syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → dom (ℝ D 𝑌) = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
162131, 161eqtr2d 2841 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) = dom ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
163 resss 5625 . . . . . . . . . . . . . . 15 ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂)
164 dmss 5524 . . . . . . . . . . . . . . 15 (((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂) → dom ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
165163, 164mp1i 13 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
166162, 165eqsstrd 3836 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
1671663adant3 1155 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
168 simp3 1161 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
169167, 168sseldd 3799 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ dom (ℝ D 𝑂))
17068, 169ffvelrnd 6582 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
1711703exp 1141 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
172171adantr 468 . . . . . . . 8 ((𝜑𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
17366, 67, 172rexlimd 3214 . . . . . . 7 ((𝜑𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ))
17460, 173mpd 15 . . . . . 6 ((𝜑𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
17553, 174jaodan 971 . . . . 5 ((𝜑 ∧ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
17628, 48, 175syl2anc 575 . . . 4 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
177176abscld 14398 . . 3 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
17827, 177sylan2 582 . 2 ((𝜑𝑠 ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
179 id 22 . . . 4 (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
180179, 15syl6eleq 2895 . . 3 (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
181 elsni 4387 . . . . . 6 (𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
182 simpr 473 . . . . . . . 8 ((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
183 fzfid 12996 . . . . . . . . . . 11 (𝜑 → (0...𝑁) ∈ Fin)
184 rnffi 39845 . . . . . . . . . . 11 ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ Fin) → ran 𝑆 ∈ Fin)
18534, 183, 184syl2anc 575 . . . . . . . . . 10 (𝜑 → ran 𝑆 ∈ Fin)
186 infi 8423 . . . . . . . . . 10 (ran 𝑆 ∈ Fin → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
187185, 186syl 17 . . . . . . . . 9 (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
188187adantr 468 . . . . . . . 8 ((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
189182, 188eqeltrd 2885 . . . . . . 7 ((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 ∈ Fin)
190 nfv 2005 . . . . . . . . 9 𝑠𝜑
191 nfcv 2948 . . . . . . . . . . 11 𝑠ran 𝑆
192 nfcv 2948 . . . . . . . . . . . . 13 𝑠
193 nfcv 2948 . . . . . . . . . . . . 13 𝑠 D
194 nfmpt1 4941 . . . . . . . . . . . . . 14 𝑠(𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
1951, 194nfcxfr 2946 . . . . . . . . . . . . 13 𝑠𝑂
196192, 193, 195nfov 6904 . . . . . . . . . . . 12 𝑠(ℝ D 𝑂)
197196nfdm 5568 . . . . . . . . . . 11 𝑠dom (ℝ D 𝑂)
198191, 197nfin 4017 . . . . . . . . . 10 𝑠(ran 𝑆 ∩ dom (ℝ D 𝑂))
199198nfeq2 2964 . . . . . . . . 9 𝑠 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))
200190, 199nfan 1990 . . . . . . . 8 𝑠(𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
201 simpr 473 . . . . . . . . . . . . 13 ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠𝑟) → 𝑠𝑟)
202 simpl 470 . . . . . . . . . . . . 13 ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠𝑟) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
203201, 202eleqtrd 2887 . . . . . . . . . . . 12 ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠𝑟) → 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
204203, 51syl 17 . . . . . . . . . . 11 ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
205204adantll 696 . . . . . . . . . 10 (((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
20649ffvelrni 6580 . . . . . . . . . . 11 (𝑠 ∈ dom (ℝ D 𝑂) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
207206abscld 14398 . . . . . . . . . 10 (𝑠 ∈ dom (ℝ D 𝑂) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
208205, 207syl 17 . . . . . . . . 9 (((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠𝑟) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
209208ex 399 . . . . . . . 8 ((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (𝑠𝑟 → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ))
210200, 209ralrimi 3145 . . . . . . 7 ((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
211 fimaxre3 11255 . . . . . . 7 ((𝑟 ∈ Fin ∧ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
212189, 210, 211syl2anc 575 . . . . . 6 ((𝜑𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
213181, 212sylan2 582 . . . . 5 ((𝜑𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
214213adantlr 697 . . . 4 (((𝜑𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
215 simpll 774 . . . . 5 (((𝜑𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝜑)
216 elunnel1 3953 . . . . . 6 ((𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
217216adantll 696 . . . . 5 (((𝜑𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
218 vex 3394 . . . . . . . . 9 𝑟 ∈ V
21918elrnmpt 5573 . . . . . . . . 9 (𝑟 ∈ V → (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
220218, 219ax-mp 5 . . . . . . . 8 (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
221220biimpi 207 . . . . . . 7 (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
222221adantl 469 . . . . . 6 ((𝜑𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
22363nfcri 2942 . . . . . . . 8 𝑗 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
22461, 223nfan 1990 . . . . . . 7 𝑗(𝜑𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
225 nfv 2005 . . . . . . 7 𝑗𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦
226 fourierdlem80.fbdioo . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤)
227 fourierdlem80.fdvbdioo . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)
228 reeanv 3295 . . . . . . . . . . . . 13 (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) ↔ (∃𝑤 ∈ ℝ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧))
229226, 227, 228sylanbrc 574 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧))
230 simp1 1159 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → (𝜑𝑗 ∈ (0..^𝑁)))
231 simp2l 1249 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → 𝑤 ∈ ℝ)
232 simp2r 1250 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → 𝑧 ∈ ℝ)
233230, 231, 232jca31 506 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ))
234 simp3l 1251 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤)
235 simp3r 1252 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)
236233, 234, 235jca31 506 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧))
237 fourierdlem80.ch . . . . . . . . . . . . . . . 16 (𝜒 ↔ (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧))
238236, 237sylibr 225 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → 𝜒)
239237biimpi 207 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧))
240 simp-5l 796 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) → 𝜑)
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝜑)
242241, 80syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐹:ℝ⟶ℝ)
243241, 82syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑋 ∈ ℝ)
244 simp-4l 792 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) → (𝜑𝑗 ∈ (0..^𝑁)))
245239, 244syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝜑𝑗 ∈ (0..^𝑁)))
246245, 139syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆𝑗) ∈ ℝ)
247245, 143syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
248 fourierdlem80.slt . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
249245, 248syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
25071, 152sstrd 3808 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
251245, 250syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
25271, 154ssneldd 3801 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))))
253245, 252syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ¬ 0 ∈ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))))
254245, 151syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
255 simp-4r 794 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) → 𝑤 ∈ ℝ)
256239, 255syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑤 ∈ ℝ)
257239simplrd 777 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤)
258 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
259258, 145syl6eleqr 2896 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡𝐼)
260 rspa 3118 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤𝑡𝐼) → (abs‘(𝐹𝑡)) ≤ 𝑤)
261257, 259, 260syl2an 585 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑡 ∈ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘(𝐹𝑡)) ≤ 𝑤)
262 simpllr 784 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤) ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) → 𝑧 ∈ ℝ)
263239, 262syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 ∈ ℝ)
264149fveq1i 6409 . . . . . . . . . . . . . . . . . . . . . 22 ((ℝ D (𝐹𝐼))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)
265264fveq2i 6411 . . . . . . . . . . . . . . . . . . . . 21 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡))
266239simprd 485 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)
267266r19.21bi 3120 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒𝑡𝐼) → (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)
268265, 267syl5eqbrr 4880 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑡𝐼) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
269259, 268sylan2 582 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑡 ∈ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
270241, 91syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐶 ∈ ℝ)
271242, 243, 246, 247, 249, 251, 253, 254, 256, 261, 263, 269, 270, 75fourierdlem68 40870 . . . . . . . . . . . . . . . . . 18 (𝜒 → (dom (ℝ D 𝑌) = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
272271simprd 485 . . . . . . . . . . . . . . . . 17 (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
273271simpld 484 . . . . . . . . . . . . . . . . . . 19 (𝜒 → dom (ℝ D 𝑌) = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
274273raleqdv 3333 . . . . . . . . . . . . . . . . . 18 (𝜒 → (∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
275274rexbidv 3240 . . . . . . . . . . . . . . . . 17 (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
276272, 275mpbid 223 . . . . . . . . . . . . . . . 16 (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
277126eqcomi 2815 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) = ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
278277reseq2i 5594 . . . . . . . . . . . . . . . . . . . . . 22 ((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
279278fveq1i 6409 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠)
280 fvres 6427 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
281280adantl 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
282245, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
283282resmptd 5657 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
28469, 283syl5eq 2852 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
285284, 75syl6reqr 2859 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑌 = (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
286285oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
287286fveq1d 6410 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((ℝ D 𝑌)‘𝑠) = ((ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
288125fveq1d 6410 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
289241, 288syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((ℝ D (𝑂 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
290287, 289eqtr2d 2841 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
291290adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
292279, 281, 2913eqtr3a 2864 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) = ((ℝ D 𝑌)‘𝑠))
293292fveq2d 6412 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D 𝑌)‘𝑠)))
294293breq1d 4854 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ (abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
295294ralbidva 3173 . . . . . . . . . . . . . . . . 17 (𝜒 → (∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
296295rexbidv 3240 . . . . . . . . . . . . . . . 16 (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
297276, 296mpbird 248 . . . . . . . . . . . . . . 15 (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
298238, 297syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
2992983exp 1141 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
300299rexlimdvv 3225 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡𝐼 (abs‘(𝐹𝑡)) ≤ 𝑤 ∧ ∀𝑡𝐼 (abs‘((ℝ D (𝐹𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
301229, 300mpd 15 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
3023013adant3 1155 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
303 raleq 3327 . . . . . . . . . . . 12 (𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → (∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
3043033ad2ant3 1158 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
305304rexbidv 3240 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
306302, 305mpbird 248 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
3073063exp 1141 . . . . . . . 8 (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
308307adantr 468 . . . . . . 7 ((𝜑𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
309224, 225, 308rexlimd 3214 . . . . . 6 ((𝜑𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
310222, 309mpd 15 . . . . 5 ((𝜑𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
311215, 217, 310syl2anc 575 . . . 4 (((𝜑𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
312214, 311pm2.61dan 838 . . 3 ((𝜑𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
313180, 312sylan2 582 . 2 ((𝜑𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
314 pm3.22 449 . . . . . . . . . . . 12 ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ran 𝑆𝑟 ∈ dom (ℝ D 𝑂)))
315 elin 3995 . . . . . . . . . . . 12 (𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ↔ (𝑟 ∈ ran 𝑆𝑟 ∈ dom (ℝ D 𝑂)))
316314, 315sylibr 225 . . . . . . . . . . 11 ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
317316adantll 696 . . . . . . . . . 10 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
31844eqcomd 2812 . . . . . . . . . . 11 (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
319318ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
320317, 319eleqtrd 2887 . . . . . . . . 9 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
321320orcd 891 . . . . . . . 8 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
322 simpll 774 . . . . . . . . . . 11 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝜑)
32378a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → ℝ ⊆ ℂ)
324119adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝑂:(𝐴[,]𝐵)⟶ℂ)
32584adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝐴 ∈ ℝ)
32685adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝐵 ∈ ℝ)
327325, 326iccssred 40211 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → (𝐴[,]𝐵) ⊆ ℝ)
328323, 324, 327dvbss 23879 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → dom (ℝ D 𝑂) ⊆ (𝐴[,]𝐵))
329 simpr 473 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ dom (ℝ D 𝑂))
330328, 329sseldd 3799 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (𝐴[,]𝐵))
331330adantr 468 . . . . . . . . . . 11 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (𝐴[,]𝐵))
332 simpr 473 . . . . . . . . . . 11 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ¬ 𝑟 ∈ ran 𝑆)
333 fourierdlem80.relioo . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1))))
334 fveq2 6408 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑘 → (𝑆𝑗) = (𝑆𝑘))
335 oveq1 6881 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
336335fveq2d 6412 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑘 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝑘 + 1)))
337334, 336oveq12d 6892 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑘 → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) = ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1))))
338 ovex 6906 . . . . . . . . . . . . . . . 16 ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1))) ∈ V
339337, 18, 338fvmpt 6503 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0..^𝑁) → ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) = ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1))))
340339eleq2d 2871 . . . . . . . . . . . . . 14 (𝑘 ∈ (0..^𝑁) → (𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ 𝑟 ∈ ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1)))))
341340rexbiia 3228 . . . . . . . . . . . . 13 (∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆𝑘)(,)(𝑆‘(𝑘 + 1))))
342333, 341sylibr 225 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
34354, 18dmmpti 6234 . . . . . . . . . . . . 13 dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (0..^𝑁)
344343rexeqi 3332 . . . . . . . . . . . 12 (∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
345342, 344sylibr 225 . . . . . . . . . . 11 (((𝜑𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
346322, 331, 332, 345syl21anc 857 . . . . . . . . . 10 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
347 funmpt 6139 . . . . . . . . . . 11 Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))
348 elunirn 6733 . . . . . . . . . . 11 (Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
349347, 348mp1i 13 . . . . . . . . . 10 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
350346, 349mpbird 248 . . . . . . . . 9 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
351350olcd 892 . . . . . . . 8 (((𝜑𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
352321, 351pm2.61dan 838 . . . . . . 7 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → (𝑟 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
353 elun 3952 . . . . . . 7 (𝑟 ∈ ( {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑟 {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
354352, 353sylibr 225 . . . . . 6 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ ( {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
355354, 29syl6eleqr 2896 . . . . 5 ((𝜑𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
356355ralrimiva 3154 . . . 4 (𝜑 → ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
357 dfss3 3787 . . . 4 (dom (ℝ D 𝑂) ⊆ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
358356, 357sylibr 225 . . 3 (𝜑 → dom (ℝ D 𝑂) ⊆ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
359358, 26syl6sseqr 3849 . 2 (𝜑 → dom (ℝ D 𝑂) ⊆ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))))))
36024, 178, 313, 359ssfiunibd 40004 1 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  Vcvv 3391  cun 3767  cin 3768  wss 3769  {csn 4370   cuni 4630   ciun 4712   class class class wbr 4844  cmpt 4923  dom cdm 5311  ran crn 5312  cres 5313  Fun wfun 6095  wf 6097  cfv 6101  (class class class)co 6874  Fincfn 8192  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226   < clt 10359  cle 10360  cmin 10551  -cneg 10552   / cdiv 10969  2c2 11356  (,)cioo 12393  [,]cicc 12396  ...cfz 12549  ..^cfzo 12689  cexp 13083  abscabs 14197  sincsin 15014  cosccos 15015  πcpi 15017  TopOpenctopn 16287  topGenctg 16303  fldccnfld 19954  intcnt 21035   D cdv 23841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-ixp 8146  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-fi 8556  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-z 11644  df-dec 11760  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-ioo 12397  df-ioc 12398  df-ico 12399  df-icc 12400  df-fz 12550  df-fzo 12690  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-fac 13281  df-bc 13310  df-hash 13338  df-shft 14030  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-limsup 14425  df-clim 14442  df-rlim 14443  df-sum 14640  df-ef 15018  df-sin 15020  df-cos 15021  df-pi 15023  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-hom 16177  df-cco 16178  df-rest 16288  df-topn 16289  df-0g 16307  df-gsum 16308  df-topgen 16309  df-pt 16310  df-prds 16313  df-xrs 16367  df-qtop 16372  df-imas 16373  df-xps 16375  df-mre 16451  df-mrc 16452  df-acs 16454  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-submnd 17541  df-mulg 17746  df-cntz 17951  df-cmn 18396  df-psmet 19946  df-xmet 19947  df-met 19948  df-bl 19949  df-mopn 19950  df-fbas 19951  df-fg 19952  df-cnfld 19955  df-top 20912  df-topon 20929  df-topsp 20951  df-bases 20964  df-cld 21037  df-ntr 21038  df-cls 21039  df-nei 21116  df-lp 21154  df-perf 21155  df-cn 21245  df-cnp 21246  df-t1 21332  df-haus 21333  df-cmp 21404  df-tx 21579  df-hmeo 21772  df-fil 21863  df-fm 21955  df-flim 21956  df-flf 21957  df-xms 22338  df-ms 22339  df-tms 22340  df-cncf 22894  df-limc 23844  df-dv 23845
This theorem is referenced by:  fourierdlem103  40905  fourierdlem104  40906
  Copyright terms: Public domain W3C validator