Theorem fourierdlem71 46891

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.

Step	Hyp	Ref	Expression
1		prfi 9279	. . . 4 ⊢ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∈ Fin
2	1	a1i 11	. . 3 ⊢ (𝜑 → {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∈ Fin)
3		fourierdlem71.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)
4	3	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → 𝐹:dom 𝐹⟶ℝ)
5		simpl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → 𝜑)
6		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼})
7		fourierdlem71.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
8		ovex 7443	. . . . . . . . . . . . 13 ⊢ (0...𝑀) ∈ V
9	8	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...𝑀) ∈ V)
10	7, 9	fexd 7225	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ V)
11		rnexg 7895	. . . . . . . . . . 11 ⊢ (𝑄 ∈ V → ran 𝑄 ∈ V)
12		inex1g 5288	. . . . . . . . . . 11 ⊢ (ran 𝑄 ∈ V → (ran 𝑄 ∩ dom 𝐹) ∈ V)
13	10, 11, 12	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ V)
14	13	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → (ran 𝑄 ∩ dom 𝐹) ∈ V)
15		fourierdlem71.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
16		ovex 7443	. . . . . . . . . . . . . . 15 ⊢ (0..^𝑀) ∈ V
17	16	mptex 7221	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ V
18	15, 17	eqeltri 2859	. . . . . . . . . . . . 13 ⊢ 𝐼 ∈ V
19	18	rnex 7903	. . . . . . . . . . . 12 ⊢ ran 𝐼 ∈ V
20	19	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐼 ∈ V)
21	20	uniexd 7740	. . . . . . . . . 10 ⊢ (𝜑 → ∪ ran 𝐼 ∈ V)
22	21	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → ∪ ran 𝐼 ∈ V)
23		uniprg 4888	. . . . . . . . 9 ⊢ (((ran 𝑄 ∩ dom 𝐹) ∈ V ∧ ∪ ran 𝐼 ∈ V) → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
24	14, 22, 23	syl2anc 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
25	6, 24	eleqtrd 2865	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
26		elinel2 4155	. . . . . . . . 9 ⊢ (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
27	26	adantl 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼)) ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
28		simpll 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝜑)
29		elunnel1 4108	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ ∪ ran 𝐼)
30	29	adantll 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ ∪ ran 𝐼)
31	15	funmpt2 6575	. . . . . . . . . . . 12 ⊢ Fun 𝐼
32		elunirn 7249	. . . . . . . . . . . 12 ⊢ (Fun 𝐼 → (𝑥 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖)))
33	31, 32	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖))
34	33	bilani 509	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖))
35		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼)
36		ovex 7443	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V
37	36, 15	dmmpti 6679	. . . . . . . . . . . . . . . . . . 19 ⊢ dom 𝐼 = (0..^𝑀)
38	35, 37	eleqtrdi 2873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ (0..^𝑀))
39	38	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀))
40	36	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V)
41	15	fvmpt2 7001	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
42	39, 40, 41	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
43		fourierdlem71.fcn	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
44		cncff 25052	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
45		fdm 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
46	43, 44, 45	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
47	38, 46	sylan2 604	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
48		ssdmres 6012	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
49	47, 48	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
50	42, 49	eqsstrd 3971	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ⊆ dom 𝐹)
51	50	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → (𝐼‘𝑖) ⊆ dom 𝐹)
52		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → 𝑥 ∈ (𝐼‘𝑖))
53	51, 52	sseldd 3938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) → 𝑥 ∈ dom 𝐹)
54	53	3exp 1137	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹)))
55	54	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → (𝑖 ∈ dom 𝐼 → (𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹)))
56	55	rexlimdv 3164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) → 𝑥 ∈ dom 𝐹))
57	34, 56	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → 𝑥 ∈ dom 𝐹)
58	28, 30, 57	syl2anc 595	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼)) ∧ ¬ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
59	27, 58	pm2.61dan 824	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼)) → 𝑥 ∈ dom 𝐹)
60	5, 25, 59	syl2anc 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → 𝑥 ∈ dom 𝐹)
61	4, 60	ffvelcdmd 7080	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → (𝐹‘𝑥) ∈ ℝ)
62	61	recnd 11232	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → (𝐹‘𝑥) ∈ ℂ)
63	62	abscld 15486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
64		simpr 489	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = (ran 𝑄 ∩ dom 𝐹))
65		fzfid 14005	. . . . . . . . . 10 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
66		rnffi 45893	. . . . . . . . . 10 ⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
67	7, 65, 66	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
68		infi 9226	. . . . . . . . 9 ⊢ (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
69	67, 68	syl 18	. . . . . . . 8 ⊢ (𝜑 → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
70	69	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → (ran 𝑄 ∩ dom 𝐹) ∈ Fin)
71	64, 70	eqeltrd 2863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 ∈ Fin)
72		simpll 778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → 𝜑)
73		simpr 489	. . . . . . . . . 10 ⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ 𝑤)
74		simpl 487	. . . . . . . . . 10 ⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑤 = (ran 𝑄 ∩ dom 𝐹))
75	73, 74	eleqtrd 2865	. . . . . . . . 9 ⊢ ((𝑤 = (ran 𝑄 ∩ dom 𝐹) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
76	75	adantll 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
77	3	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝐹:dom 𝐹⟶ℝ)
78	26	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
79	77, 78	ffvelcdmd 7080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹‘𝑥) ∈ ℝ)
80	79	recnd 11232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (𝐹‘𝑥) ∈ ℂ)
81	80	abscld 15486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹)) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
82	72, 76, 81	syl2anc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) ∧ 𝑥 ∈ 𝑤) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
83	82	ralrimiva 3157	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ∈ ℝ)
84		fimaxre3 12156	. . . . . 6 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦)
85	71, 83, 84	syl2anc 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦)
86	85	adantlr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦)
87		simpll 778	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝜑)
88		neqne 2966	. . . . . . 7 ⊢ (¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹) → 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹))
89		elprn1 4617	. . . . . . 7 ⊢ ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∧ 𝑤 ≠ (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼)
90	88, 89	sylan2 604	. . . . . 6 ⊢ ((𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼)
91	90	adantll 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → 𝑤 = ∪ ran 𝐼)
92		fzofi 14006	. . . . . . . 8 ⊢ (0..^𝑀) ∈ Fin
93	15	rnmptfi 45889	. . . . . . . 8 ⊢ ((0..^𝑀) ∈ Fin → ran 𝐼 ∈ Fin)
94	92, 93	ax-mp 5	. . . . . . 7 ⊢ ran 𝐼 ∈ Fin
95	94	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ran 𝐼 ∈ Fin)
96	3	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → 𝐹:dom 𝐹⟶ℝ)
97	96, 57	ffvelcdmd 7080	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → (𝐹‘𝑥) ∈ ℝ)
98	97	recnd 11232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼) → (𝐹‘𝑥) ∈ ℂ)
99	98	adantlr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑥 ∈ ∪ ran 𝐼) → (𝐹‘𝑥) ∈ ℂ)
100	99	abscld 15486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑥 ∈ ∪ ran 𝐼) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
101	36, 15	fnmpti 6678	. . . . . . . . . 10 ⊢ 𝐼 Fn (0..^𝑀)
102		fvelrnb 6941	. . . . . . . . . 10 ⊢ (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡))
103	101, 102	ax-mp 5	. . . . . . . . 9 ⊢ (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)
104	103	bilani 509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)
105	7	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106		elfzofz 13700	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
107	106	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
108	105, 107	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
109		fzofzp1 13789	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
110	109	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
111	105, 110	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
112		fourierdlem71.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
113		fourierdlem71.r	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))
114	108, 111, 43, 112, 113	cncfioobd 46611	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏)
115	114	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏)
116		fvres 6900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥))
117	116	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = (abs‘(𝐹‘𝑥)))
118	117	breq1d 5119	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑥)) ≤ 𝑏))
119	118	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑥)) ≤ 𝑏))
120	119	ralbidva 3186	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏))
121	120	rexbidv 3189	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏))
122	121	3adant3 1150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏))
123	36, 41	mpan2 703	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0..^𝑀) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
124		id 23	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼‘𝑖) = 𝑡 → (𝐼‘𝑖) = 𝑡)
125	123, 124	sylan9req 2819	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡)
126	125	3adant1 1148	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡)
127	126	raleqdv 3323	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))
128	127	rexbidv 3189	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))
129	122, 128	bitrd 282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))
130	115, 129	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)
131	130	3exp 1137	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)))
132	131	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)))
133	132	rexlimdv 3164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏))
134	104, 133	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)
135	134	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ 𝑡 (abs‘(𝐹‘𝑥)) ≤ 𝑏)
136		eqimss 3995	. . . . . . 7 ⊢ (𝑤 = ∪ ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼)
137	136	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → 𝑤 ⊆ ∪ ran 𝐼)
138	95, 100, 135, 137	ssfiunibd 46028	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦)
139	87, 91, 138	syl2anc 595	. . . 4 ⊢ (((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) ∧ ¬ 𝑤 = (ran 𝑄 ∩ dom 𝐹)) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦)
140	86, 139	pm2.61dan 824	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼}) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑤 (abs‘(𝐹‘𝑥)) ≤ 𝑦)
141		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄)
142		elinel2 4155	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ dom 𝐹)
143	142	ad2antlr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ dom 𝐹)
144	141, 143	elind 4153	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ (ran 𝑄 ∩ dom 𝐹))
145		elun1 4135	. . . . . . . 8 ⊢ (𝑥 ∈ (ran 𝑄 ∩ dom 𝐹) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
146	144, 145	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
147		fourierdlem71.7	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
148	147	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑀 ∈ ℕ)
149	7	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ)
150		elinel1 4154	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹) → 𝑥 ∈ (𝐴[,]𝐵))
151	150	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ (𝐴[,]𝐵))
152		fourierdlem71.q0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘0) = 𝐴)
153	152	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 = (𝑄‘0))
154	153	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐴 = (𝑄‘0))
155		fourierdlem71.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
156	155	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 = (𝑄‘𝑀))
157	156	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝐵 = (𝑄‘𝑀))
158	154, 157	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀)))
159	151, 158	eleqtrd 2865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
160	159	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
161		simpr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ¬ 𝑥 ∈ ran 𝑄)
162		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗))
163	162	breq1d 5119	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < 𝑥 ↔ (𝑄‘𝑗) < 𝑥))
164	163	cbvrabv 3426	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑥} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑥}
165	164	supeq1i 9403	. . . . . . . . . . 11 ⊢ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑥}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑥}, ℝ, < )
166	148, 149, 160, 161, 165	fourierdlem25 46846	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
167	38	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑖 ∈ (0..^𝑀))
168		simprr 784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑥 ∈ (𝐼‘𝑖))
169	167, 123	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
170	168, 169	eleqtrd 2865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
171	167, 170	jca 520	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
172		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0..^𝑀))
173	172, 37	eleqtrrdi 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ dom 𝐼)
174	173	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑖 ∈ dom 𝐼)
175		simprr 784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
176	123	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0..^𝑀) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖))
177	176	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖))
178	175, 177	eleqtrd 2865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → 𝑥 ∈ (𝐼‘𝑖))
179	174, 178	jca 520	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) → (𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)))
180	171, 179	impbida 812	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ (𝐼‘𝑖)) ↔ (𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
181	180	rexbidv2 3185	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
182	181	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → (∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
183	166, 182	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑥 ∈ (𝐼‘𝑖))
184	183, 33	sylibr 237	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ∪ ran 𝐼)
185		elun2 4136	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ ran 𝐼 → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
186	184, 185	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) ∧ ¬ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
187	146, 186	pm2.61dan 824	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → 𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
188	187	ralrimiva 3157	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
189		dfss3 3926	. . . . 5 ⊢ (((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼) ↔ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)𝑥 ∈ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
190	188, 189	sylibr 237	. . . 4 ⊢ (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
191	13, 21, 23	syl2anc 595	. . . 4 ⊢ (𝜑 → ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼} = ((ran 𝑄 ∩ dom 𝐹) ∪ ∪ ran 𝐼))
192	190, 191	sseqtrrd 3974	. . 3 ⊢ (𝜑 → ((𝐴[,]𝐵) ∩ dom 𝐹) ⊆ ∪ {(ran 𝑄 ∩ dom 𝐹), ∪ ran 𝐼})
193	2, 63, 140, 192	ssfiunibd 46028	. 2 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦)
194		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑥𝜑
195		nfra1 3289	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦
196	194, 195	nfan 1929	. . . . 5 ⊢ Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦)
197		fourierdlem71.dmf	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom 𝐹 ⊆ ℝ)
198	197	sselda 3937	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ℝ)
199		fourierdlem71.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ ℝ)
200	199	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐵 ∈ ℝ)
201	200, 198	resubcld 11637	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐵 − 𝑥) ∈ ℝ)
202		fourierdlem71.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (𝐵 − 𝐴)
203		fourierdlem71.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ)
204	199, 203	resubcld 11637	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
205	202, 204	eqeltrid 2867	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ ℝ)
206	205	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑇 ∈ ℝ)
207		fourierdlem71.altb	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 < 𝐵)
208	203, 199	posdifd 11796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
209	207, 208	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
210	209, 202	breqtrrdi 5153	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝑇)
211	210	gt0ne0d 11773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ≠ 0)
212	211	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝑇 ≠ 0)
213	201, 206, 212	redivcld 12038	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
214	213	flcld 13827	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
215	214	zred 12695	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
216	215, 206	remulcld 11234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
217	198, 216	readdcld 11233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
218		fourierdlem71.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
219	218	fvmpt2 7001	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
220	198, 217, 219	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
221	220	fveq2d 6885	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘(𝐸‘𝑥)) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
222		fvex 6894	. . . . . . . . . . . 12 ⊢ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ V
223		eleq1 2851	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 ∈ ℤ ↔ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ))
224	223	anbi2d 641	. . . . . . . . . . . . 13 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) ↔ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)))
225		oveq1 7417	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑘 · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
226	225	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝑥 + (𝑘 · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
227	226	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
228	227	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥) ↔ (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥)))
229	224, 228	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) ↔ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))))
230		fourierdlem71.fxpt	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
231	222, 229, 230	vtocl 3525	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))
232	214, 231	mpdan 699	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘(𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝐹‘𝑥))
233	221, 232	eqtr2d 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘(𝐸‘𝑥)))
234	233	fveq2d 6885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐸‘𝑥))))
235	234	adantlr 727	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐸‘𝑥))))
236		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
237	236	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘𝑤)))
238	237	breq1d 5119	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((abs‘(𝐹‘𝑥)) ≤ 𝑦 ↔ (abs‘(𝐹‘𝑤)) ≤ 𝑦))
239	238	cbvralvw 3243	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 ↔ ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦)
240	239	biimpi 219	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦)
241	240	ad2antlr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → ∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦)
242		iocssicc 13459	. . . . . . . . . . 11 ⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
243	203	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐴 ∈ ℝ)
244	207	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐴 < 𝐵)
245		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
246		oveq2 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → (𝐵 − 𝑥) = (𝐵 − 𝑦))
247	246	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑦) / 𝑇))
248	247	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑦) / 𝑇)))
249	248	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇))
250	245, 249	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇)))
251	250	cbvmptv 5215	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇)))
252	218, 251	eqtri 2786	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((𝐵 − 𝑦) / 𝑇)) · 𝑇)))
253	243, 200, 244, 202, 252	fourierdlem4 46825	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → 𝐸:ℝ⟶(𝐴(,]𝐵))
254	253, 198	ffvelcdmd 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
255	242, 254	sselid 3935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ (𝐴[,]𝐵))
256	226	eleq1d 2848	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹 ↔ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹))
257	224, 256	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = (⌊‘((𝐵 − 𝑥) / 𝑇)) → ((((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) ↔ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)))
258		fourierdlem71.xpt	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹)
259	222, 257, 258	vtocl 3525	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)
260	214, 259	mpdan 699	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ dom 𝐹)
261	220, 260	eqeltrd 2863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ dom 𝐹)
262	255, 261	elind 4153	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹))
263	262	adantlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹))
264		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐸‘𝑥) → (𝐹‘𝑤) = (𝐹‘(𝐸‘𝑥)))
265	264	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑤 = (𝐸‘𝑥) → (abs‘(𝐹‘𝑤)) = (abs‘(𝐹‘(𝐸‘𝑥))))
266	265	breq1d 5119	. . . . . . . . 9 ⊢ (𝑤 = (𝐸‘𝑥) → ((abs‘(𝐹‘𝑤)) ≤ 𝑦 ↔ (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦))
267	266	rspccva 3580	. . . . . . . 8 ⊢ ((∀𝑤 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑤)) ≤ 𝑦 ∧ (𝐸‘𝑥) ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)) → (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦)
268	241, 263, 267	syl2anc 595	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘(𝐸‘𝑥))) ≤ 𝑦)
269	235, 268	eqbrtrd 5133	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) ∧ 𝑥 ∈ dom 𝐹) → (abs‘(𝐹‘𝑥)) ≤ 𝑦)
270	269	ex 417	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) → (𝑥 ∈ dom 𝐹 → (abs‘(𝐹‘𝑥)) ≤ 𝑦))
271	196, 270	ralrimi 3263	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦) → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)
272	271	ex 417	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦))
273	272	reximdv 3180	. 2 ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ ((𝐴[,]𝐵) ∩ dom 𝐹)(abs‘(𝐹‘𝑥)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦))
274	193, 273	mpd 16	1 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  {crab 3416  Vcvv 3455   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  {cpr 4591  ∪ cuni 4872   class class class wbr 5109   ↦ cmpt 5192  dom cdm 5661  ran crn 5662   ↾ cres 5663  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  Fincfn 8939  supcsup 9396  ℂcc 11093  ℝcr 11094  0cc0 11095  1c1 11096   + caddc 11098   · cmul 11100   < clt 11238   ≤ cle 11239   − cmin 11436   / cdiv 11866  ℕcn 12228  ℤcz 12586  (,)cioo 13367  (,]cioc 13368  [,]cicc 13370  ...cfz 13530  ..^cfzo 13678  ⌊cfl 13819  abscabs 15281  –cn→ccncf 25035   lim_ℂ climc 26021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-card 9921  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305  df-n0 12500  df-z 12587  df-dec 12707  df-uz 12858  df-q 12968  df-rp 13012  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13371  df-ioc 13372  df-ico 13373  df-icc 13374  df-fz 13531  df-fzo 13679  df-fl 13821  df-seq 14034  df-exp 14094  df-hash 14363  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-struct 17202  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-starv 17320  df-sca 17321  df-vsca 17322  df-ip 17323  df-tset 17324  df-ple 17325  df-ds 17327  df-unif 17328  df-hom 17329  df-cco 17330  df-rest 17470  df-topn 17471  df-0g 17489  df-gsum 17490  df-topgen 17491  df-pt 17492  df-prds 17495  df-xrs 17551  df-qtop 17556  df-imas 17557  df-xps 17559  df-mre 17633  df-mrc 17634  df-acs 17636  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-submnd 18837  df-mulg 19129  df-cntz 19382  df-cmn 19847  df-psmet 21514  df-xmet 21515  df-met 21516  df-bl 21517  df-mopn 21518  df-cnfld 21523  df-top 23051  df-topon 23068  df-topsp 23090  df-bases 23103  df-cld 23176  df-ntr 23177  df-cls 23178  df-cn 23384  df-cnp 23385  df-cmp 23544  df-tx 23719  df-hmeo 23912  df-xms 24477  df-ms 24478  df-tms 24479  df-cncf 25037  df-limc 26025

This theorem is referenced by:  fourierdlem94  46914  fourierdlem113  46933