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

Theorem fourierdlem71 42004
 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 8639 . . . 4 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∈ Fin
21a1i 11 . . 3 (𝜑 → {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∈ Fin)
3 fourierdlem71.f . . . . . . 7 (𝜑𝐹:dom 𝐹⟶ℝ)
43adantr 481 . . . . . 6 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝐹:dom 𝐹⟶ℝ)
5 simpl 483 . . . . . . 7 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝜑)
6 simpr 485 . . . . . . . 8 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼})
7 fourierdlem71.q . . . . . . . . . . . 12 (𝜑𝑄:(0...𝑀)⟶ℝ)
8 ovex 7048 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
98a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10 fex 6855 . . . . . . . . . . . 12 ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V)
117, 9, 10syl2anc 584 . . . . . . . . . . 11 (𝜑𝑄 ∈ V)
12 rnexg 7470 . . . . . . . . . . 11 (𝑄 ∈ V → ran 𝑄 ∈ V)
13 inex1g 5114 . . . . . . . . . . 11 (ran 𝑄 ∈ V → (ran 𝑄 ∩ dom 𝐹) ∈ V)
1411, 12, 133syl 18 . . . . . . . . . 10 (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ V)
1514adantr 481 . . . . . . . . 9 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (ran 𝑄 ∩ dom 𝐹) ∈ V)
16 fourierdlem71.i . . . . . . . . . . . . . 14 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
17 ovex 7048 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ V
1817mptex 6852 . . . . . . . . . . . . . 14 (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ V
1916, 18eqeltri 2879 . . . . . . . . . . . . 13 𝐼 ∈ V
2019rnex 7473 . . . . . . . . . . . 12 ran 𝐼 ∈ V
2120a1i 11 . . . . . . . . . . 11 (𝜑 → ran 𝐼 ∈ V)
22 uniexg 7325 . . . . . . . . . . 11 (ran 𝐼 ∈ V → ran 𝐼 ∈ V)
2321, 22syl 17 . . . . . . . . . 10 (𝜑 ran 𝐼 ∈ V)
2423adantr 481 . . . . . . . . 9 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → ran 𝐼 ∈ V)
25 uniprg 4759 . . . . . . . . 9 (((ran 𝑄 ∩ dom 𝐹) ∈ V ∧ ran 𝐼 ∈ V) → {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
2615, 24, 25syl2anc 584 . . . . . . . 8 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
276, 26eleqtrd 2885 . . . . . . 7 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
28 elinel2 4094 . . . . . . . . 9 (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
2928adantl 482 . . . . . . . 8 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
30 simpll 763 . . . . . . . . 9 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝜑)
31 elunnel1 4047 . . . . . . . . . 10 ((𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ran 𝐼)
3231adantll 710 . . . . . . . . 9 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ran 𝐼)
3316funmpt2 6264 . . . . . . . . . . . . 13 Fun 𝐼
34 elunirn 6875 . . . . . . . . . . . . 13 (Fun 𝐼 → (𝑥 ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖)))
3533, 34ax-mp 5 . . . . . . . . . . . 12 (𝑥 ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
3635biimpi 217 . . . . . . . . . . 11 (𝑥 ran 𝐼 → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
3736adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ran 𝐼) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
38 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ dom 𝐼𝑖 ∈ dom 𝐼)
39 ovex 7048 . . . . . . . . . . . . . . . . . . . 20 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V
4039, 16dmmpti 6360 . . . . . . . . . . . . . . . . . . 19 dom 𝐼 = (0..^𝑀)
4138, 40syl6eleq 2893 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ dom 𝐼𝑖 ∈ (0..^𝑀))
4241adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀))
4339a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V)
4416fvmpt2 6645 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
4542, 43, 44syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ dom 𝐼) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
46 fourierdlem71.fcn . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
47 cncff 23184 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
48 fdm 6390 . . . . . . . . . . . . . . . . . . 19 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
4946, 47, 483syl 18 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
5041, 49sylan2 592 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ dom 𝐼) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
51 ssdmres 5757 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
5250, 51sylibr 235 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ dom 𝐼) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
5345, 52eqsstrd 3926 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ dom 𝐼) → (𝐼𝑖) ⊆ dom 𝐹)
54533adant3 1125 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) → (𝐼𝑖) ⊆ dom 𝐹)
55 simp3 1131 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) → 𝑥 ∈ (𝐼𝑖))
5654, 55sseldd 3890 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) → 𝑥 ∈ dom 𝐹)
57563exp 1112 . . . . . . . . . . . 12 (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼𝑖) → 𝑥 ∈ dom 𝐹)))
5857adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ran 𝐼) → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼𝑖) → 𝑥 ∈ dom 𝐹)))
5958rexlimdv 3246 . . . . . . . . . 10 ((𝜑𝑥 ran 𝐼) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖) → 𝑥 ∈ dom 𝐹))
6037, 59mpd 15 . . . . . . . . 9 ((𝜑𝑥 ran 𝐼) → 𝑥 ∈ dom 𝐹)
6130, 32, 60syl2anc 584 . . . . . . . 8 (((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
6229, 61pm2.61dan 809 . . . . . . 7 ((𝜑𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼)) → 𝑥 ∈ dom 𝐹)
635, 27, 62syl2anc 584 . . . . . 6 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → 𝑥 ∈ dom 𝐹)
644, 63ffvelrnd 6717 . . . . 5 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (𝐹𝑥) ∈ ℝ)
6564recnd 10515 . . . 4 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (𝐹𝑥) ∈ ℂ)
6665abscld 14630 . . 3 ((𝜑𝑥 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → (abs‘(𝐹𝑥)) ∈ ℝ)
67 simpr 485 . . . . . . 7 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = (ran 𝑄 ∩ dom 𝐹))
68 fzfid 13191 . . . . . . . . . 10 (𝜑 → (0...𝑀) ∈ Fin)
69 rnffi 40971 . . . . . . . . . 10 ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
707, 68, 69syl2anc 584 . . . . . . . . 9 (𝜑 → ran 𝑄 ∈ Fin)
71 infi 8588 . . . . . . . . 9 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
7270, 71syl 17 . . . . . . . 8 (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
7372adantr 481 . . . . . . 7 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
7467, 73eqeltrd 2883 . . . . . 6 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 ∈ Fin)
75 simpll 763 . . . . . . . 8 (((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥𝑤) → 𝜑)
76 simpr 485 . . . . . . . . . 10 ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥𝑤) → 𝑥𝑤)
77 simpl 483 . . . . . . . . . 10 ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥𝑤) → 𝑤 = (ran 𝑄 ∩ dom 𝐹))
7876, 77eleqtrd 2885 . . . . . . . . 9 ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
7978adantll 710 . . . . . . . 8 (((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
803adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝐹:dom 𝐹⟶ℝ)
8128adantl 482 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
8280, 81ffvelrnd 6717 . . . . . . . . . 10 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹𝑥) ∈ ℝ)
8382recnd 10515 . . . . . . . . 9 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹𝑥) ∈ ℂ)
8483abscld 14630 . . . . . . . 8 ((𝜑𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (abs‘(𝐹𝑥)) ∈ ℝ)
8575, 79, 84syl2anc 584 . . . . . . 7 (((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥𝑤) → (abs‘(𝐹𝑥)) ∈ ℝ)
8685ralrimiva 3149 . . . . . 6 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∀𝑥𝑤 (abs‘(𝐹𝑥)) ∈ ℝ)
87 fimaxre3 11435 . . . . . 6 ((𝑤 ∈ Fin ∧ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
8874, 86, 87syl2anc 584 . . . . 5 ((𝜑𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
8988adantlr 711 . . . 4 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
90 simpll 763 . . . . 5 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝜑)
91 neqne 2992 . . . . . . 7 𝑤 = (ran 𝑄 ∩ dom 𝐹) → 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹))
92 elprn1 41456 . . . . . . 7 ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∧ 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ran 𝐼)
9391, 92sylan2 592 . . . . . 6 ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ran 𝐼)
9493adantll 710 . . . . 5 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ran 𝐼)
95 fzofi 13192 . . . . . . . 8 (0..^𝑀) ∈ Fin
9616rnmptfi 40967 . . . . . . . 8 ((0..^𝑀) ∈ Fin → ran 𝐼 ∈ Fin)
9795, 96ax-mp 5 . . . . . . 7 ran 𝐼 ∈ Fin
9897a1i 11 . . . . . 6 ((𝜑𝑤 = ran 𝐼) → ran 𝐼 ∈ Fin)
993adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ran 𝐼) → 𝐹:dom 𝐹⟶ℝ)
10099, 60ffvelrnd 6717 . . . . . . . . 9 ((𝜑𝑥 ran 𝐼) → (𝐹𝑥) ∈ ℝ)
101100recnd 10515 . . . . . . . 8 ((𝜑𝑥 ran 𝐼) → (𝐹𝑥) ∈ ℂ)
102101adantlr 711 . . . . . . 7 (((𝜑𝑤 = ran 𝐼) ∧ 𝑥 ran 𝐼) → (𝐹𝑥) ∈ ℂ)
103102abscld 14630 . . . . . 6 (((𝜑𝑤 = ran 𝐼) ∧ 𝑥 ran 𝐼) → (abs‘(𝐹𝑥)) ∈ ℝ)
10439, 16fnmpti 6359 . . . . . . . . . . 11 𝐼 Fn (0..^𝑀)
105 fvelrnb 6594 . . . . . . . . . . 11 (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡))
106104, 105ax-mp 5 . . . . . . . . . 10 (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡)
107106biimpi 217 . . . . . . . . 9 (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡)
108107adantl 482 . . . . . . . 8 ((𝜑𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡)
1097adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
110 elfzofz 12903 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
111110adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
112109, 111ffvelrnd 6717 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
113 fzofzp1 12984 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
114113adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
115109, 114ffvelrnd 6717 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
116 fourierdlem71.l . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
117 fourierdlem71.r . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
118112, 115, 46, 116, 117cncfioobd 41721 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏)
1191183adant3 1125 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏)
120 fvres 6557 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹𝑥))
121120fveq2d 6542 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = (abs‘(𝐹𝑥)))
122121breq1d 4972 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹𝑥)) ≤ 𝑏))
123122adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹𝑥)) ≤ 𝑏))
124123ralbidva 3163 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏))
125124rexbidv 3260 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏))
1261253adant3 1125 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏))
12739, 44mpan2 687 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0..^𝑀) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
128 id 22 . . . . . . . . . . . . . . . . 17 ((𝐼𝑖) = 𝑡 → (𝐼𝑖) = 𝑡)
129127, 128sylan9req 2852 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡)
1301293adant1 1123 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡)
131130raleqdv 3375 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏 ↔ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
132131rexbidv 3260 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
133126, 132bitrd 280 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
134119, 133mpbid 233 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀) ∧ (𝐼𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)
1351343exp 1112 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)))
136135adantr 481 . . . . . . . . 9 ((𝜑𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)))
137136rexlimdv 3246 . . . . . . . 8 ((𝜑𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏))
138108, 137mpd 15 . . . . . . 7 ((𝜑𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)
139138adantlr 711 . . . . . 6 (((𝜑𝑤 = ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥𝑡 (abs‘(𝐹𝑥)) ≤ 𝑏)
140 eqimss 3944 . . . . . . 7 (𝑤 = ran 𝐼𝑤 ran 𝐼)
141140adantl 482 . . . . . 6 ((𝜑𝑤 = ran 𝐼) → 𝑤 ran 𝐼)
14298, 103, 139, 141ssfiunibd 41117 . . . . 5 ((𝜑𝑤 = ran 𝐼) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
14390, 94, 142syl2anc 584 . . . 4 (((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
14489, 143pm2.61dan 809 . . 3 ((𝜑𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼}) → ∃𝑦 ∈ ℝ ∀𝑥𝑤 (abs‘(𝐹𝑥)) ≤ 𝑦)
145 simpr 485 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄)
146 elinel2 4094 . . . . . . . . . 10 (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
147146ad2antlr 723 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ dom 𝐹)
148145, 147elind 4092 . . . . . . . 8 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
149 elun1 4073 . . . . . . . 8 (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
150148, 149syl 17 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
151 fourierdlem71.7 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
152151ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑀 ∈ ℕ)
1537ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
154 elinel1 4093 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ (𝐴[,]𝐵))
155154adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ (𝐴[,]𝐵))
156 fourierdlem71.q0 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
157156eqcomd 2801 . . . . . . . . . . . . . . 15 (𝜑𝐴 = (𝑄‘0))
158157adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐴 = (𝑄‘0))
159 fourierdlem71.10 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄𝑀) = 𝐵)
160159eqcomd 2801 . . . . . . . . . . . . . . 15 (𝜑𝐵 = (𝑄𝑀))
161160adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐵 = (𝑄𝑀))
162158, 161oveq12d 7034 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄𝑀)))
163155, 162eleqtrd 2885 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((𝑄‘0)[,](𝑄𝑀)))
164163adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((𝑄‘0)[,](𝑄𝑀)))
165 simpr 485 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ¬ 𝑥 ∈ ran 𝑄)
166 fveq2 6538 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑄𝑘) = (𝑄𝑗))
167166breq1d 4972 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((𝑄𝑘) < 𝑥 ↔ (𝑄𝑗) < 𝑥))
168167cbvrabv 3434 . . . . . . . . . . . 12 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝑥} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < 𝑥}
169168supeq1i 8757 . . . . . . . . . . 11 sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝑥}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄𝑗) < 𝑥}, ℝ, < )
170152, 153, 164, 165, 169fourierdlem25 41959 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
17141ad2antrl 724 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → 𝑖 ∈ (0..^𝑀))
172 simprr 769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → 𝑥 ∈ (𝐼𝑖))
173171, 127syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → (𝐼𝑖) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
174172, 173eleqtrd 2885 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
175171, 174jca 512 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
176 id 22 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0..^𝑀))
177176, 40syl6eleqr 2894 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ dom 𝐼)
178177ad2antrl 724 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑖 ∈ dom 𝐼)
179 simprr 769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
180127eqcomd 2801 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0..^𝑀) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼𝑖))
181180ad2antrl 724 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼𝑖))
182179, 181eleqtrd 2885 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ (𝐼𝑖))
183178, 182jca 512 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) → (𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)))
184175, 183impbida 797 . . . . . . . . . . . 12 (𝜑 → ((𝑖 ∈ dom 𝐼𝑥 ∈ (𝐼𝑖)) ↔ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
185184rexbidv2 3258 . . . . . . . . . . 11 (𝜑 → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
186185ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
187170, 186mpbird 258 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼𝑖))
188187, 35sylibr 235 . . . . . . . 8 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ran 𝐼)
189 elun2 4074 . . . . . . . 8 (𝑥 ran 𝐼𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
190188, 189syl 17 . . . . . . 7 (((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
191150, 190pm2.61dan 809 . . . . . 6 ((𝜑𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
192191ralrimiva 3149 . . . . 5 (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
193 dfss3 3878 . . . . 5 (((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼) ↔ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
194192, 193sylibr 235 . . . 4 (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
19514, 23, 25syl2anc 584 . . . 4 (𝜑 {(ran 𝑄 ∩ dom 𝐹), ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ran 𝐼))
196194, 195sseqtr4d 3929 . . 3 (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ {(ran 𝑄 ∩ dom 𝐹), ran 𝐼})
1972, 66, 144, 196ssfiunibd 41117 . 2 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦)
198 nfv 1892 . . . . . 6 𝑥𝜑
199 nfra1 3186 . . . . . 6 𝑥𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦
200198, 199nfan 1881 . . . . 5 𝑥(𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦)
201 fourierdlem71.dmf . . . . . . . . . . . . 13 (𝜑 → dom 𝐹 ⊆ ℝ)
202201sselda 3889 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
203 fourierdlem71.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
204203adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ dom 𝐹) → 𝐵 ∈ ℝ)
205204, 202resubcld 10916 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ dom 𝐹) → (𝐵𝑥) ∈ ℝ)
206 fourierdlem71.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝐵𝐴)
207 fourierdlem71.a . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
208203, 207resubcld 10916 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵𝐴) ∈ ℝ)
209206, 208syl5eqel 2887 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ)
210209adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ dom 𝐹) → 𝑇 ∈ ℝ)
211 fourierdlem71.altb . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 < 𝐵)
212207, 203posdifd 11075 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
213211, 212mpbid 233 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵𝐴))
214213, 206syl6breqr 5004 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
215214gt0ne0d 11052 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ≠ 0)
216215adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ dom 𝐹) → 𝑇 ≠ 0)
217205, 210, 216redivcld 11316 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ dom 𝐹) → ((𝐵𝑥) / 𝑇) ∈ ℝ)
218217flcld 13018 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ dom 𝐹) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)
219218zred 11936 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ dom 𝐹) → (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℝ)
220219, 210remulcld 10517 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐹) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
221202, 220readdcld 10516 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
222 fourierdlem71.e . . . . . . . . . . . . 13 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
223222fvmpt2 6645 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸𝑥) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
224202, 221, 223syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
225224fveq2d 6542 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐹‘(𝐸𝑥)) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
226 fvex 6551 . . . . . . . . . . . 12 (⌊‘((𝐵𝑥) / 𝑇)) ∈ V
227 eleq1 2870 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ))
228227anbi2d 628 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) ↔ ((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ)))
229 oveq1 7023 . . . . . . . . . . . . . . . 16 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
230229oveq2d 7032 . . . . . . . . . . . . . . 15 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
231230fveq2d 6542 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
232231eqeq1d 2797 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥)))
233228, 232imbi12d 346 . . . . . . . . . . . 12 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥)) ↔ (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥))))
234 fourierdlem71.fxpt . . . . . . . . . . . 12 (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
235226, 233, 234vtocl 3502 . . . . . . . . . . 11 (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥))
236218, 235mpdan 683 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐹‘(𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝐹𝑥))
237225, 236eqtr2d 2832 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐹) → (𝐹𝑥) = (𝐹‘(𝐸𝑥)))
238237fveq2d 6542 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝐹) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐸𝑥))))
239238adantlr 711 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐸𝑥))))
240 fveq2 6538 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
241240fveq2d 6542 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (abs‘(𝐹𝑥)) = (abs‘(𝐹𝑤)))
242241breq1d 4972 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((abs‘(𝐹𝑥)) ≤ 𝑦 ↔ (abs‘(𝐹𝑤)) ≤ 𝑦))
243242cbvralv 3403 . . . . . . . . . 10 (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 ↔ ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦)
244243biimpi 217 . . . . . . . . 9 (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦)
245244ad2antlr 723 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦)
246 iocssicc 12675 . . . . . . . . . . 11 (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
247207adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐹) → 𝐴 ∈ ℝ)
248211adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ dom 𝐹) → 𝐴 < 𝐵)
249 id 22 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦𝑥 = 𝑦)
250 oveq2 7024 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐵𝑥) = (𝐵𝑦))
251250oveq1d 7031 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑦) / 𝑇))
252251fveq2d 6542 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑦) / 𝑇)))
253252oveq1d 7031 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇))
254249, 253oveq12d 7034 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑦 + ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇)))
255254cbvmptv 5061 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))) = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇)))
256222, 255eqtri 2819 . . . . . . . . . . . . 13 𝐸 = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵𝑦) / 𝑇)) · 𝑇)))
257247, 204, 248, 206, 256fourierdlem4 41938 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ dom 𝐹) → 𝐸:ℝ⟶(𝐴(,]𝐵))
258257, 202ffvelrnd 6717 . . . . . . . . . . 11 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ (𝐴(,]𝐵))
259246, 258sseldi 3887 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ (𝐴[,]𝐵))
260230eleq1d 2867 . . . . . . . . . . . . . 14 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹 ↔ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹))
261228, 260imbi12d 346 . . . . . . . . . . . . 13 (𝑘 = (⌊‘((𝐵𝑥) / 𝑇)) → ((((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) ↔ (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)))
262 fourierdlem71.xpt . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹)
263226, 261, 262vtocl 3502 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)
264218, 263mpdan 683 . . . . . . . . . . 11 ((𝜑𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)
265224, 264eqeltrd 2883 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ dom 𝐹)
266259, 265elind 4092 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹))
267266adantlr 711 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (𝐸𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹))
268 fveq2 6538 . . . . . . . . . . 11 (𝑤 = (𝐸𝑥) → (𝐹𝑤) = (𝐹‘(𝐸𝑥)))
269268fveq2d 6542 . . . . . . . . . 10 (𝑤 = (𝐸𝑥) → (abs‘(𝐹𝑤)) = (abs‘(𝐹‘(𝐸𝑥))))
270269breq1d 4972 . . . . . . . . 9 (𝑤 = (𝐸𝑥) → ((abs‘(𝐹𝑤)) ≤ 𝑦 ↔ (abs‘(𝐹‘(𝐸𝑥))) ≤ 𝑦))
271270rspccva 3558 . . . . . . . 8 ((∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑤)) ≤ 𝑦 ∧ (𝐸𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (abs‘(𝐹‘(𝐸𝑥))) ≤ 𝑦)
272245, 267, 271syl2anc 584 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘(𝐸𝑥))) ≤ 𝑦)
273239, 272eqbrtrd 4984 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹𝑥)) ≤ 𝑦)
274273ex 413 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) → (𝑥 ∈ dom 𝐹 → (abs‘(𝐹𝑥)) ≤ 𝑦))
275200, 274ralrimi 3183 . . . 4 ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦) → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦)
276275ex 413 . . 3 (𝜑 → (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦))
277276reximdv 3236 . 2 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹𝑥)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦))
278197, 277mpd 15 1 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹𝑥)) ≤ 𝑦)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081   ≠ wne 2984  ∀wral 3105  ∃wrex 3106  {crab 3109  Vcvv 3437   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  {cpr 4474  ∪ cuni 4745   class class class wbr 4962   ↦ cmpt 5041  dom cdm 5443  ran crn 5444   ↾ cres 5445  Fun wfun 6219   Fn wfn 6220  ⟶wf 6221  ‘cfv 6225  (class class class)co 7016  Fincfn 8357  supcsup 8750  ℂcc 10381  ℝcr 10382  0cc0 10383  1c1 10384   + caddc 10386   · cmul 10388   < clt 10521   ≤ cle 10522   − cmin 10717   / cdiv 11145  ℕcn 11486  ℤcz 11829  (,)cioo 12588  (,]cioc 12589  [,]cicc 12591  ...cfz 12742  ..^cfzo 12883  ⌊cfl 13010  abscabs 14427  –cn→ccncf 23167   limℂ climc 24143 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461  ax-mulf 10463 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-supp 7682  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-oadd 7957  df-er 8139  df-map 8258  df-pm 8259  df-ixp 8311  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fsupp 8680  df-fi 8721  df-sup 8752  df-inf 8753  df-oi 8820  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-7 11553  df-8 11554  df-9 11555  df-n0 11746  df-z 11830  df-dec 11948  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-ioo 12592  df-ioc 12593  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-fl 13012  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-starv 16409  df-sca 16410  df-vsca 16411  df-ip 16412  df-tset 16413  df-ple 16414  df-ds 16416  df-unif 16417  df-hom 16418  df-cco 16419  df-rest 16525  df-topn 16526  df-0g 16544  df-gsum 16545  df-topgen 16546  df-pt 16547  df-prds 16550  df-xrs 16604  df-qtop 16609  df-imas 16610  df-xps 16612  df-mre 16686  df-mrc 16687  df-acs 16689  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-submnd 17775  df-mulg 17982  df-cntz 18188  df-cmn 18635  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-cnfld 20228  df-top 21186  df-topon 21203  df-topsp 21225  df-bases 21238  df-cld 21311  df-ntr 21312  df-cls 21313  df-cn 21519  df-cnp 21520  df-cmp 21679  df-tx 21854  df-hmeo 22047  df-xms 22613  df-ms 22614  df-tms 22615  df-cncf 23169  df-limc 24147 This theorem is referenced by:  fourierdlem94  42027  fourierdlem113  42046
 Copyright terms: Public domain W3C validator