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

Theorem fourierdlem71 40917
Description: A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem71.dmf (𝜑 → dom 𝐹 ⊆ ℝ)
fourierdlem71.f (𝜑𝐹:dom 𝐹⟶ℝ)
fourierdlem71.a (𝜑𝐴 ∈ ℝ)
fourierdlem71.b (𝜑𝐵 ∈ ℝ)
fourierdlem71.altb (𝜑𝐴 < 𝐵)
fourierdlem71.t 𝑇 = (𝐵𝐴)
fourierdlem71.7 (𝜑𝑀 ∈ ℕ)
fourierdlem71.q (𝜑𝑄:(0...𝑀)⟶ℝ)
fourierdlem71.q0 (𝜑 → (𝑄‘0) = 𝐴)
fourierdlem71.10 (𝜑 → (𝑄𝑀) = 𝐵)
fourierdlem71.fcn ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem71.r ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
fourierdlem71.l ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
fourierdlem71.xpt (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹)
fourierdlem71.fxpt (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
fourierdlem71.i 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
fourierdlem71.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
Assertion
Ref Expression
fourierdlem71 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦)
Distinct variable groups:   𝑥,𝐴,𝑦   𝐵,𝑘,𝑥   𝑦,𝐵   𝑖,𝐹,𝑥,𝑘   𝑦,𝐹   𝑖,𝐼,𝑥   𝑦,𝐼   𝑥,𝐿   𝑖,𝑀,𝑥,𝑘   𝑄,𝑖,𝑥,𝑘   𝑦,𝑄   𝑥,𝑅   𝑇,𝑘,𝑥   𝑦,𝑇   𝜑,𝑖,𝑥,𝑘   𝜑,𝑦
Allowed substitution hints:   𝐴(𝑖,𝑘)   𝐵(𝑖)   𝑅(𝑦,𝑖,𝑘)   𝑇(𝑖)   𝐸(𝑥,𝑦,𝑖,𝑘)   𝐼(𝑘)   𝐿(𝑦,𝑖,𝑘)   𝑀(𝑦)

Proof of Theorem fourierdlem71
Dummy variables 𝑤 𝑏 𝑡 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prfi 8412 . . . 4 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∈ Fin
21a1i 11 . . 3 (𝜑 → {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∈ Fin)
3 fourierdlem71.f . . . . . . 7 (𝜑𝐹:dom 𝐹⟶ℝ)
43adantr 467 . . . . . 6 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝐹:dom 𝐹⟶ℝ)
5 simpl 469 . . . . . . 7 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝜑)
6 simpr 472 . . . . . . . 8 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼})
7 fourierdlem71.q . . . . . . . . . . . 12 (𝜑𝑄:(0...𝑀)⟶ℝ)
8 ovex 6844 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
98a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10 fex 6652 . . . . . . . . . . . 12 ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V)
117, 9, 10syl2anc 574 . . . . . . . . . . 11 (𝜑𝑄 ∈ V)
12 rnexg 7266 . . . . . . . . . . 11 (𝑄 ∈ V → ran 𝑄 ∈ V)
13 inex1g 4949 . . . . . . . . . . 11 (ran 𝑄 ∈ V → (ran 𝑄 ∩ dom 𝐹) ∈ V)
1411, 12, 133syl 18 . . . . . . . . . 10 (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ V)
1514adantr 467 . . . . . . . . 9 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (ran 𝑄 ∩ dom 𝐹) ∈ V)
16 fourierdlem71.i . . . . . . . . . . . . . 14 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
17 ovex 6844 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ V
1817mptex 6649 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ V
1916, 18eqeltri 2849 . . . . . . . . . . . . 13 𝐼 ∈ V
2019rnex 7268 . . . . . . . . . . . 12 ran 𝐼 ∈ V
2120a1i 11 . . . . . . . . . . 11 (𝜑 → ran 𝐼 ∈ V)
22 uniexg 7123 . . . . . . . . . . 11 (ran 𝐼 ∈ V → ran 𝐼 ∈ V)
2321, 22syl 17 . . . . . . . . . 10 (𝜑 ran 𝐼 ∈ V)
2423adantr 467 . . . . . . . . 9 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → ran 𝐼 ∈ V)
25 uniprg 4599 . . . . . . . . 9 (((ran 𝑄 ∩ dom 𝐹) ∈ V ∧ ran 𝐼 ∈ V) → {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
2615, 24, 25syl2anc 574 . . . . . . . 8 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
276, 26eleqtrd 2855 . . . . . . 7 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
28 elinel2 3958 . . . . . . . . 9 (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
2928adantl 468 . . . . . . . 8 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
30 simpll 772 . . . . . . . . 9 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝜑)
31 elunnel1 3912 . . . . . . . . . 10 ((𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ran 𝐼)
3231adantll 694 . . . . . . . . 9 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ran 𝐼)
3316funmpt2 6081 . . . . . . . . . . . . 13 Fun 𝐼
34 elunirn 6671 . . . . . . . . . . . . 13 (Fun 𝐼 → (𝑥 ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖)))
3533, 34ax-mp 5 . . . . . . . . . . . 12 (𝑥 ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
3635biimpi 207 . . . . . . . . . . 11 (𝑥 ran 𝐼 → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
3736adantl 468 . . . . . . . . . 10 ((𝜑𝑥 ran 𝐼) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
38 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ dom 𝐼𝑖 ∈ dom 𝐼)
39 ovex 6844 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V
4039, 16dmmpti 6174 . . . . . . . . . . . . . . . . . . 19 dom 𝐼 = (0..^𝑀)
4138, 40syl6eleq 2863 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ dom 𝐼𝑖 ∈ (0..^𝑀))
4241adantl 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀))
4339a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V)
4416fvmpt2 6450 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
4542, 43, 44syl2anc 574 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ dom 𝐼) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
46 fourierdlem71.fcn . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
47 cncff 22936 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
48 fdm 6204 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
4946, 47, 483syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
5041, 49sylan2 581 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
51 ssdmres 5572 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
5250, 51sylibr 225 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ dom 𝐼) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
5345, 52eqsstrd 3795 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ dom 𝐼) → (𝐼𝑖) ⊆ dom 𝐹)
54533adant3 1153 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) → (𝐼𝑖) ⊆ dom 𝐹)
55 simp3 1159 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) → 𝑥 ∈ (𝐼𝑖))
5654, 55sseldd 3759 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) → 𝑥 ∈ dom 𝐹)
57563exp 1139 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼𝑖) → 𝑥 ∈ dom 𝐹)))
5857adantr 467 . . . . . . . . . . 11 ((𝜑𝑥 ran 𝐼) → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼𝑖) → 𝑥 ∈ dom 𝐹)))
5958rexlimdv 3182 . . . . . . . . . 10 ((𝜑𝑥 ran 𝐼) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖) → 𝑥 ∈ dom 𝐹))
6037, 59mpd 15 . . . . . . . . 9 ((𝜑𝑥 ran 𝐼) → 𝑥 ∈ dom 𝐹)
6130, 32, 60syl2anc 574 . . . . . . . 8 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
6229, 61pm2.61dan 836 . . . . . . 7 ((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) → 𝑥 ∈ dom 𝐹)
635, 27, 62syl2anc 574 . . . . . 6 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝑥 ∈ dom 𝐹)
644, 63ffvelrnd 6520 . . . . 5 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (𝐹𝑥) ∈ ℝ)
6564recnd 10291 . . . 4 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (𝐹𝑥) ∈ ℂ)
6665abscld 14405 . . 3 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (abs‘(𝐹𝑥)) ∈ ℝ)
67 simpr 472 . . . . . . 7 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = (ran 𝑄 ∩ dom 𝐹))
68 fzfid 13002 . . . . . . . . . 10 (𝜑 → (0...𝑀) ∈ Fin)
69 rnffi 39887 . . . . . . . . . 10 ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
707, 68, 69syl2anc 574 . . . . . . . . 9 (𝜑 → ran 𝑄 ∈ Fin)
71 infi 8361 . . . . . . . . 9 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
7270, 71syl 17 . . . . . . . 8 (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
7372adantr 467 . . . . . . 7 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
7467, 73eqeltrd 2853 . . . . . 6 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 ∈ Fin)
75 simpll 772 . . . . . . . 8 (((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥𝑤) → 𝜑)
76 simpr 472 . . . . . . . . . 10 ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥𝑤) → 𝑥𝑤)
77 simpl 469 . . . . . . . . . 10 ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥𝑤) → 𝑤 = (ran 𝑄 ∩ dom 𝐹))
7876, 77eleqtrd 2855 . . . . . . . . 9 ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
7978adantll 694 . . . . . . . 8 (((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
803adantr 467 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝐹:dom 𝐹⟶ℝ)
8128adantl 468 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
8280, 81ffvelrnd 6520 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹𝑥) ∈ ℝ)
8382recnd 10291 . . . . . . . . 9 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹𝑥) ∈ ℂ)
8483abscld 14405 . . . . . . . 8 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (abs‘(𝐹𝑥)) ∈ ℝ)
8575, 79, 84syl2anc 574 . . . . . . 7 (((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥𝑤) → (abs‘(𝐹𝑥)) ∈ ℝ)
8685ralrimiva 3118 . . . . . 6 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∀𝑥𝑤 (abs‘(𝐹𝑥)) ∈ ℝ)
87 fimaxre3 11193 . . . . . 6 ((𝑤 ∈ Fin ∧ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
8874, 86, 87syl2anc 574 . . . . 5 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
8988adantlr 695 . . . 4 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
90 simpll 772 . . . . 5 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝜑)
91 neqne 2954 . . . . . . 7 𝑤 = (ran 𝑄 ∩ dom 𝐹) → 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹))
92 elprn1 40389 . . . . . . 7 ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∧ 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ran 𝐼)
9391, 92sylan2 581 . . . . . 6 ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ran 𝐼)
9493adantll 694 . . . . 5 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ran 𝐼)
95 fzofi 13003 . . . . . . . 8 (0..^𝑀) ∈ Fin
9616rnmptfi 39882 . . . . . . . 8 ((0..^𝑀) ∈ Fin → ran 𝐼 ∈ Fin)
9795, 96ax-mp 5 . . . . . . 7 ran 𝐼 ∈ Fin
9897a1i 11 . . . . . 6 ((𝜑𝑤 = ran 𝐼) → ran 𝐼 ∈ Fin)
993adantr 467 . . . . . . . . . 10 ((𝜑𝑥 ran 𝐼) → 𝐹:dom 𝐹⟶ℝ)
10099, 60ffvelrnd 6520 . . . . . . . . 9 ((𝜑𝑥 ran 𝐼) → (𝐹𝑥) ∈ ℝ)
101100recnd 10291 . . . . . . . 8 ((𝜑𝑥 ran 𝐼) → (𝐹𝑥) ∈ ℂ)
102101adantlr 695 . . . . . . 7 (((𝜑𝑤 = ran 𝐼) ∧ 𝑥 ran 𝐼) → (𝐹𝑥) ∈ ℂ)
103102abscld 14405 . . . . . 6 (((𝜑𝑤 = ran 𝐼) ∧ 𝑥 ran 𝐼) → (abs‘(𝐹𝑥)) ∈ ℝ)
10439, 16fnmpti 6173 . . . . . . . . . . 11 𝐼 Fn (0..^𝑀)
105 fvelrnb 6402 . . . . . . . . . . 11 (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡))
106104, 105ax-mp 5 . . . . . . . . . 10 (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡)
107106biimpi 207 . . . . . . . . 9 (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡)
108107adantl 468 . . . . . . . 8 ((𝜑𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡)
1097adantr 467 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
110 elfzofz 12715 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
111110adantl 468 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
112109, 111ffvelrnd 6520 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
113 fzofzp1 12795 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
114113adantl 468 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
115109, 114ffvelrnd 6520 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
116 fourierdlem71.l . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
117 fourierdlem71.r . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
118112, 115, 46, 116, 117cncfioobd 40634 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏)
1191183adant3 1153 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏)
120 fvres 6365 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹𝑥))
121120fveq2d 6352 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = (abs‘(𝐹𝑥)))
122121breq1d 4807 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹𝑥)) ≤ 𝑏))
123122adantl 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹𝑥)) ≤ 𝑏))
124123ralbidva 3137 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏))
125124rexbidv 3204 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏))
1261253adant3 1153 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏))
12739, 44mpan2 672 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0..^𝑀) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
128 id 22 . . . . . . . . . . . . . . . . 17 ((𝐼𝑖) = 𝑡 → (𝐼𝑖) = 𝑡)
129127, 128sylan9req 2829 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡)
1301293adant1 1151 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡)
131130raleqdv 3297 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏 ↔ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
132131rexbidv 3204 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
133126, 132bitrd 269 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
134119, 133mpbid 223 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)
1351343exp 1139 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)))
136135adantr 467 . . . . . . . . 9 ((𝜑𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)))
137136rexlimdv 3182 . . . . . . . 8 ((𝜑𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
138108, 137mpd 15 . . . . . . 7 ((𝜑𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)
139138adantlr 695 . . . . . 6 (((𝜑𝑤 = ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)
140 eqimss 3813 . . . . . . 7 (𝑤 = ran 𝐼𝑤 ran 𝐼)
141140adantl 468 . . . . . 6 ((𝜑𝑤 = ran 𝐼) → 𝑤 ran 𝐼)
14298, 103, 139, 141ssfiunibd 40048 . . . . 5 ((𝜑𝑤 = ran 𝐼) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
14390, 94, 142syl2anc 574 . . . 4 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
14489, 143pm2.61dan 836 . . 3 ((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
145 simpr 472 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄)
146 elinel2 3958 . . . . . . . . . 10 (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
147146ad2antlr 707 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ dom 𝐹)
148145, 147elind 3956 . . . . . . . 8 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
149 elun1 3938 . . . . . . . 8 (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
150148, 149syl 17 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
151 fourierdlem71.7 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
152151ad2antrr 706 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑀 ∈ ℕ)
1537ad2antrr 706 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
154 elinel1 3957 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ (𝐴[,]𝐵))
155154adantl 468 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ (𝐴[,]𝐵))
156 fourierdlem71.q0 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
157156eqcomd 2780 . . . . . . . . . . . . . . 15 (𝜑𝐴 = (𝑄‘0))
158157adantr 467 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐴 = (𝑄‘0))
159 fourierdlem71.10 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄𝑀) = 𝐵)
160159eqcomd 2780 . . . . . . . . . . . . . . 15 (𝜑𝐵 = (𝑄𝑀))
161160adantr 467 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐵 = (𝑄𝑀))
162158, 161oveq12d 6830 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
163155, 162eleqtrd 2855 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((𝑄‘0)[,](𝑄𝑀)))
164163adantr 467 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((𝑄‘0)[,](𝑄𝑀)))
165 simpr 472 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ¬ 𝑥 ∈ ran 𝑄)
166 fveq2 6348 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
167166breq1d 4807 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((𝑄𝑘) < 𝑥 ↔ (𝑄𝑗) < 𝑥))
168167cbvrabv 3353 . . . . . . . . . . . 12 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝑥} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < 𝑥}
169168supeq1i 8530 . . . . . . . . . . 11 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝑥}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < 𝑥}, ℝ, < )
170152, 153, 164, 165, 169fourierdlem25 40872 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
17141ad2antrl 708 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → 𝑖 ∈ (0..^𝑀))
172 simprr 778 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → 𝑥 ∈ (𝐼𝑖))
173171, 127syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
174172, 173eleqtrd 2855 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
175171, 174jca 502 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
176 id 22 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0..^𝑀))
177176, 40syl6eleqr 2864 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ dom 𝐼)
178177ad2antrl 708 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑖 ∈ dom 𝐼)
179 simprr 778 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
180127eqcomd 2780 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼𝑖))
181180ad2antrl 708 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼𝑖))
182179, 181eleqtrd 2855 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ (𝐼𝑖))
183178, 182jca 502 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)))
184175, 183impbida 824 . . . . . . . . . . . 12 (𝜑 → ((𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) ↔ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
185184rexbidv2 3200 . . . . . . . . . . 11 (𝜑 → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
186185ad2antrr 706 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
187170, 186mpbird 248 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
188187, 35sylibr 225 . . . . . . . 8 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ran 𝐼)
189 elun2 3939 . . . . . . . 8 (𝑥 ran 𝐼𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
190188, 189syl 17 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
191150, 190pm2.61dan 836 . . . . . 6 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
192191ralrimiva 3118 . . . . 5 (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
193 dfss3 3747 . . . . 5 (((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼) ↔ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
194192, 193sylibr 225 . . . 4 (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
19514, 23, 25syl2anc 574 . . . 4 (𝜑 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
196194, 195sseqtr4d 3798 . . 3 (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼})
1972, 66, 144, 196ssfiunibd 40048 . 2 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦)
198 nfv 1998 . . . . . 6 𝑥𝜑
199 nfra1 3093 . . . . . 6 𝑥𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦
200198, 199nfan 1983 . . . . 5 𝑥(𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦)
201 fourierdlem71.dmf . . . . . . . . . . . . 13 (𝜑 → dom 𝐹 ⊆ ℝ)
202201sselda 3758 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
203 fourierdlem71.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
204203adantr 467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ dom 𝐹) → 𝐵 ∈ ℝ)
205204, 202resubcld 10681 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ dom 𝐹) → (𝐵𝑥) ∈ ℝ)
206 fourierdlem71.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝐵𝐴)
207 fourierdlem71.a . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
208203, 207resubcld 10681 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝐴) ∈ ℝ)
209206, 208syl5eqel 2857 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ)
210209adantr 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ dom 𝐹) → 𝑇 ∈ ℝ)
211 fourierdlem71.altb . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 < 𝐵)
212207, 203posdifd 10837 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
213211, 212mpbid 223 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵𝐴))
214213, 206syl6breqr 4839 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
215214gt0ne0d 10815 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ≠ 0)
216215adantr 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ dom 𝐹) → 𝑇 ≠ 0)
217205, 210, 216redivcld 11076 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ dom 𝐹) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
218217flcld 12829 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ dom 𝐹) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
219218zred 11706 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ dom 𝐹) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
220219, 210remulcld 10293 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐹) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
221202, 220readdcld 10292 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
222 fourierdlem71.e . . . . . . . . . . . . 13 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
223222fvmpt2 6450 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸𝑥) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
224202, 221, 223syl2anc 574 . . . . . . . . . . 11 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
225224fveq2d 6352 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐹‘(𝐸𝑥)) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
226 fvex 6359 . . . . . . . . . . . 12 (⌊‘((𝐵𝑥) / 𝑇)) ∈ V
227 eleq1 2841 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ))
228227anbi2d 615 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) ↔ ((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)))
229 oveq1 6819 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
230229oveq2d 6828 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
231230fveq2d 6352 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
232231eqeq1d 2776 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
233228, 232imbi12d 334 . . . . . . . . . . . 12 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
234 fourierdlem71.fxpt . . . . . . . . . . . 12 (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
235226, 233, 234vtocl 3415 . . . . . . . . . . 11 (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥))
236218, 235mpdan 668 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥))
237225, 236eqtr2d 2809 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐹) → (𝐹𝑥) = (𝐹‘(𝐸𝑥)))
238237fveq2d 6352 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝐹) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐸𝑥))))
239238adantlr 695 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐸𝑥))))
240 fveq2 6348 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
241240fveq2d 6352 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (abs‘(𝐹𝑥)) = (abs‘(𝐹𝑤)))
242241breq1d 4807 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((abs‘(𝐹𝑥)) ≤ 𝑦 ↔ (abs‘(𝐹𝑤)) ≤ 𝑦))
243242cbvralv 3324 . . . . . . . . . 10 (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 ↔ ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦)
244243biimpi 207 . . . . . . . . 9 (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦)
245244ad2antlr 707 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦)
246 iocssicc 12486 . . . . . . . . . . 11 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
247207adantr 467 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐹) → 𝐴 ∈ ℝ)
248211adantr 467 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐹) → 𝐴 < 𝐵)
249 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦𝑥 = 𝑦)
250 oveq2 6820 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
251250oveq1d 6827 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑦) / 𝑇))
252251fveq2d 6352 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑦) / 𝑇)))
253252oveq1d 6827 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇))
254249, 253oveq12d 6830 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑦 + ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇)))
255254cbvmptv 4897 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇)))
256222, 255eqtri 2796 . . . . . . . . . . . . 13 𝐸 = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇)))
257247, 204, 248, 206, 256fourierdlem4 40851 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ dom 𝐹) → 𝐸:ℝ⟶(𝐴(,]𝐵))
258257, 202ffvelrnd 6520 . . . . . . . . . . 11 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ (𝐴(,]𝐵))
259246, 258sseldi 3756 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ (𝐴[,]𝐵))
260230eleq1d 2838 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹 ↔ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹))
261228, 260imbi12d 334 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) ↔ (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)))
262 fourierdlem71.xpt . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹)
263226, 261, 262vtocl 3415 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)
264218, 263mpdan 668 . . . . . . . . . . 11 ((𝜑𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)
265224, 264eqeltrd 2853 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ dom 𝐹)
266259, 265elind 3956 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹))
267266adantlr 695 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹))
268 fveq2 6348 . . . . . . . . . . 11 (𝑤 = (𝐸𝑥) → (𝐹𝑤) = (𝐹‘(𝐸𝑥)))
269268fveq2d 6352 . . . . . . . . . 10 (𝑤 = (𝐸𝑥) → (abs‘(𝐹𝑤)) = (abs‘(𝐹‘(𝐸𝑥))))
270269breq1d 4807 . . . . . . . . 9 (𝑤 = (𝐸𝑥) → ((abs‘(𝐹𝑤)) ≤ 𝑦 ↔ (abs‘(𝐹‘(𝐸𝑥))) ≤ 𝑦))
271270rspccva 3464 . . . . . . . 8 ((∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦 ∧ (𝐸𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (abs‘(𝐹‘(𝐸𝑥))) ≤ 𝑦)
272245, 267, 271syl2anc 574 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘(𝐸𝑥))) ≤ 𝑦)
273239, 272eqbrtrd 4819 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹𝑥)) ≤ 𝑦)
274273ex 398 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) → (𝑥 ∈ dom 𝐹 → (abs‘(𝐹𝑥)) ≤ 𝑦))
275200, 274ralrimi 3109 . . . 4 ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦)
276275ex 398 . . 3 (𝜑 → (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦))
277276reximdv 3167 . 2 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦))
278197, 277mpd 15 1 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  w3a 1098   = wceq 1634  wcel 2148  wne 2946  wral 3064  wrex 3065  {crab 3068  Vcvv 3355  cun 3727  cin 3728  wss 3729  {cpr 4328   cuni 4585   class class class wbr 4797  cmpt 4876  dom cdm 5263  ran crn 5264  cres 5265  Fun wfun 6036   Fn wfn 6037  wf 6038  cfv 6042  (class class class)co 6812  Fincfn 8130  supcsup 8523  cc 10157  cr 10158  0cc0 10159  1c1 10160   + caddc 10162   · cmul 10164   < clt 10297  cle 10298  cmin 10489   / cdiv 10907  cn 11243  cz 11601  (,)cioo 12399  (,]cioc 12400  [,]cicc 12402  ...cfz 12555  ..^cfzo 12695  cfl 12821  abscabs 14204  cnccncf 22919   lim climc 23867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237  ax-mulf 10239
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-iin 4668  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-of 7065  df-om 7234  df-1st 7336  df-2nd 7337  df-supp 7468  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-er 7917  df-map 8032  df-pm 8033  df-ixp 8084  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-fsupp 8453  df-fi 8494  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-4 11304  df-5 11305  df-6 11306  df-7 11307  df-8 11308  df-9 11309  df-n0 11517  df-z 11602  df-dec 11718  df-uz 11911  df-q 12014  df-rp 12053  df-xneg 12168  df-xadd 12169  df-xmul 12170  df-ioo 12403  df-ioc 12404  df-ico 12405  df-icc 12406  df-fz 12556  df-fzo 12696  df-fl 12823  df-seq 13031  df-exp 13090  df-hash 13344  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-struct 16086  df-ndx 16087  df-slot 16088  df-base 16090  df-sets 16091  df-ress 16092  df-plusg 16182  df-mulr 16183  df-starv 16184  df-sca 16185  df-vsca 16186  df-ip 16187  df-tset 16188  df-ple 16189  df-ds 16192  df-unif 16193  df-hom 16194  df-cco 16195  df-rest 16311  df-topn 16312  df-0g 16330  df-gsum 16331  df-topgen 16332  df-pt 16333  df-prds 16336  df-xrs 16390  df-qtop 16395  df-imas 16396  df-xps 16398  df-mre 16474  df-mrc 16475  df-acs 16477  df-mgm 17470  df-sgrp 17512  df-mnd 17523  df-submnd 17564  df-mulg 17769  df-cntz 17977  df-cmn 18422  df-psmet 19973  df-xmet 19974  df-met 19975  df-bl 19976  df-mopn 19977  df-cnfld 19982  df-top 20939  df-topon 20956  df-topsp 20978  df-bases 20991  df-cld 21064  df-ntr 21065  df-cls 21066  df-cn 21272  df-cnp 21273  df-cmp 21431  df-tx 21606  df-hmeo 21799  df-xms 22365  df-ms 22366  df-tms 22367  df-cncf 22921  df-limc 23871
This theorem is referenced by:  fourierdlem94  40940  fourierdlem113  40959
  Copyright terms: Public domain W3C validator