Theorem fourierdlem71

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)

	Ref	Expression
Hypotheses	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	fourierdlem71	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem71.dmf	⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
2		fourierdlem71.f	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
3		fourierdlem71.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		fourierdlem71.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		fourierdlem71.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
6		fourierdlem71.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
7		fourierdlem71.7	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
8		fourierdlem71.q	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
9		fourierdlem71.q0	⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
10		fourierdlem71.10	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
11		fourierdlem71.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
12		fourierdlem71.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
13		fourierdlem71.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
14		fourierdlem71.xpt	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 )
15		fourierdlem71.fxpt	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
16		fourierdlem71.i	⊢ 𝐼 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
17		fourierdlem71.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
18		prfi	⊢ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∈ Fin
19	18	a1i	⊢ ( 𝜑 → { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∈ Fin )
20	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝐹 : dom 𝐹 ⟶ ℝ )
21		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝜑 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } )
23		ovex	⊢ ( 0 ... 𝑀 ) ∈ V
24	23	a1i	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ V )
25	8 24	fexd	⊢ ( 𝜑 → 𝑄 ∈ V )
26		rnexg	⊢ ( 𝑄 ∈ V → ran 𝑄 ∈ V )
27		inex1g	⊢ ( ran 𝑄 ∈ V → ( ran 𝑄 ∩ dom 𝐹 ) ∈ V )
28	25 26 27	3syl	⊢ ( 𝜑 → ( ran 𝑄 ∩ dom 𝐹 ) ∈ V )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( ran 𝑄 ∩ dom 𝐹 ) ∈ V )
30		ovex	⊢ ( 0 ..^ 𝑀 ) ∈ V
31	30	mptex	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ V
32	16 31	eqeltri	⊢ 𝐼 ∈ V
33	32	rnex	⊢ ran 𝐼 ∈ V
34	33	a1i	⊢ ( 𝜑 → ran 𝐼 ∈ V )
35	34	uniexd	⊢ ( 𝜑 → ∪ ran 𝐼 ∈ V )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ∪ ran 𝐼 ∈ V )
37		uniprg	⊢ ( ( ( ran 𝑄 ∩ dom 𝐹 ) ∈ V ∧ ∪ ran 𝐼 ∈ V ) → ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } = ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
38	29 36 37	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } = ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
39	22 38	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
40		elinel2	⊢ ( 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) → 𝑥 ∈ dom 𝐹 )
41	40	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
42		simpll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝜑 )
43		elunnel1	⊢ ( ( 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ ∪ ran 𝐼 )
44	43	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ ∪ ran 𝐼 )
45	16	funmpt2	⊢ Fun 𝐼
46		elunirn	⊢ ( Fun 𝐼 → ( 𝑥 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) )
47	45 46	ax-mp	⊢ ( 𝑥 ∈ ∪ ran 𝐼 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
48	47	biimpi	⊢ ( 𝑥 ∈ ∪ ran 𝐼 → ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
49	48	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
50		id	⊢ ( 𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼 )
51		ovex	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V
52	51 16	dmmpti	⊢ dom 𝐼 = ( 0 ..^ 𝑀 )
53	50 52	eleqtrdi	⊢ ( 𝑖 ∈ dom 𝐼 → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
54	53	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
55	51	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V )
56	16	fvmpt2	⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∈ V ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
57	54 55 56	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
58		cncff	⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
59		fdm	⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ → dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
60	11 58 59	3syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
61	53 60	sylan2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
62		ssdmres	⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
63	61 62	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
64	57 63	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) ⊆ dom 𝐹 )
65	64	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) → ( 𝐼 ‘ 𝑖 ) ⊆ dom 𝐹 )
66		simp3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) → 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
67	65 66	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) → 𝑥 ∈ dom 𝐹 )
68	67	3exp	⊢ ( 𝜑 → ( 𝑖 ∈ dom 𝐼 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑥 ∈ dom 𝐹 ) ) )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝑖 ∈ dom 𝐼 → ( 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑥 ∈ dom 𝐹 ) ) )
70	69	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) → 𝑥 ∈ dom 𝐹 ) )
71	49 70	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → 𝑥 ∈ dom 𝐹 )
72	42 44 71	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) ∧ ¬ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
73	41 72	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ) → 𝑥 ∈ dom 𝐹 )
74	21 39 73	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → 𝑥 ∈ dom 𝐹 )
75	20 74	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
76	75	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
77	76	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
78		simpr	⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) )
79		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
80		rnffi	⊢ ( ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ∧ ( 0 ... 𝑀 ) ∈ Fin ) → ran 𝑄 ∈ Fin )
81	8 79 80	syl2anc	⊢ ( 𝜑 → ran 𝑄 ∈ Fin )
82		infi	⊢ ( ran 𝑄 ∈ Fin → ( ran 𝑄 ∩ dom 𝐹 ) ∈ Fin )
83	81 82	syl	⊢ ( 𝜑 → ( ran 𝑄 ∩ dom 𝐹 ) ∈ Fin )
84	83	adantr	⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ( ran 𝑄 ∩ dom 𝐹 ) ∈ Fin )
85	78 84	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 ∈ Fin )
86		simpll	⊢ ( ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ 𝑤 ) → 𝜑 )
87		simpr	⊢ ( ( 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ 𝑤 )
88		simpl	⊢ ( ( 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ∧ 𝑥 ∈ 𝑤 ) → 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) )
89	87 88	eleqtrd	⊢ ( ( 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) )
90	89	adantll	⊢ ( ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) )
91	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝐹 : dom 𝐹 ⟶ ℝ )
92	40	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
93	91 92	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
94	93	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
95	94	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
96	86 90 95	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ 𝑤 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
97	96	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
98		fimaxre3	⊢ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
99	85 97 98	syl2anc	⊢ ( ( 𝜑 ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
100	99	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
101		simpll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝜑 )
102		neqne	⊢ ( ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) → 𝑤 ≠ ( ran 𝑄 ∩ dom 𝐹 ) )
103		elprn1	⊢ ( ( 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∧ 𝑤 ≠ ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ∪ ran 𝐼 )
104	102 103	sylan2	⊢ ( ( 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ∪ ran 𝐼 )
105	104	adantll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → 𝑤 = ∪ ran 𝐼 )
106		fzofi	⊢ ( 0 ..^ 𝑀 ) ∈ Fin
107	16	rnmptfi	⊢ ( ( 0 ..^ 𝑀 ) ∈ Fin → ran 𝐼 ∈ Fin )
108	106 107	ax-mp	⊢ ran 𝐼 ∈ Fin
109	108	a1i	⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → ran 𝐼 ∈ Fin )
110	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → 𝐹 : dom 𝐹 ⟶ ℝ )
111	110 71	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
112	111	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
113	112	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
114	113	abscld	⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑥 ∈ ∪ ran 𝐼 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
115	51 16	fnmpti	⊢ 𝐼 Fn ( 0 ..^ 𝑀 )
116		fvelrnb	⊢ ( 𝐼 Fn ( 0 ..^ 𝑀 ) → ( 𝑡 ∈ ran 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 ) )
117	115 116	ax-mp	⊢ ( 𝑡 ∈ ran 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
118	117	biimpi	⊢ ( 𝑡 ∈ ran 𝐼 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
119	118	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 )
120	8	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
121		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
122	121	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
123	120 122	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
124		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
125	124	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
126	120 125	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
127	123 126 11 13 12	cncfioobd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 )
128	127	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 )
129		fvres	⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
130	129	fveq2d	⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
131	130	breq1d	⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
132	131	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
133	132	ralbidva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
134	133	rexbidv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
135	134	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
136	51 56	mpan2	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
137		id	⊢ ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ( 𝐼 ‘ 𝑖 ) = 𝑡 )
138	136 137	sylan9req	⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = 𝑡 )
139	138	3adant1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = 𝑡 )
140	139	raleqdv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
141	140	rexbidv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
142	135 141	bitrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
143	128 142	mpbid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐼 ‘ 𝑖 ) = 𝑡 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
144	143	3exp	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ) )
145	144	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ) )
146	145	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐼 ‘ 𝑖 ) = 𝑡 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) )
147	119 146	mpd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
148	147	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ 𝑡 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
149		eqimss	⊢ ( 𝑤 = ∪ ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼 )
150	149	adantl	⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → 𝑤 ⊆ ∪ ran 𝐼 )
151	109 114 148 150	ssfiunibd	⊢ ( ( 𝜑 ∧ 𝑤 = ∪ ran 𝐼 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
152	101 105 151	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) ∧ ¬ 𝑤 = ( ran 𝑄 ∩ dom 𝐹 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
153	100 152	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑤 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
154		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ran 𝑄 )
155		elinel2	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) → 𝑥 ∈ dom 𝐹 )
156	155	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ dom 𝐹 )
157	154 156	elind	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) )
158		elun1	⊢ ( 𝑥 ∈ ( ran 𝑄 ∩ dom 𝐹 ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
159	157 158	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
160	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑀 ∈ ℕ )
161	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
162		elinel1	⊢ ( 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
163	162	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
164	9	eqcomd	⊢ ( 𝜑 → 𝐴 = ( 𝑄 ‘ 0 ) )
165	164	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝐴 = ( 𝑄 ‘ 0 ) )
166	10	eqcomd	⊢ ( 𝜑 → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
167	166	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
168	165 167	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
169	163 168	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
170	169	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
171		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ¬ 𝑥 ∈ ran 𝑄 )
172		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝑗 ) )
173	172	breq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝑄 ‘ 𝑘 ) < 𝑥 ↔ ( 𝑄 ‘ 𝑗 ) < 𝑥 ) )
174	173	cbvrabv	⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝑥 } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) < 𝑥 }
175	174	supeq1i	⊢ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝑥 } , ℝ , < ) = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑗 ) < 𝑥 } , ℝ , < )
176	160 161 170 171 175	fourierdlem25	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
177	53	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
178		simprr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
179	177 136	syl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → ( 𝐼 ‘ 𝑖 ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
180	178 179	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
181	177 180	jca	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
182		id	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
183	182 52	eleqtrrdi	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ dom 𝐼 )
184	183	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → 𝑖 ∈ dom 𝐼 )
185		simprr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
186	136	eqcomd	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐼 ‘ 𝑖 ) )
187	186	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐼 ‘ 𝑖 ) )
188	185 187	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
189	184 188	jca	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) )
190	181 189	impbida	⊢ ( 𝜑 → ( ( 𝑖 ∈ dom 𝐼 ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
191	190	rexbidv2	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
192	191	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
193	176 192	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → ∃ 𝑖 ∈ dom 𝐼 𝑥 ∈ ( 𝐼 ‘ 𝑖 ) )
194	193 47	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ∪ ran 𝐼 )
195		elun2	⊢ ( 𝑥 ∈ ∪ ran 𝐼 → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
196	194 195	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) ∧ ¬ 𝑥 ∈ ran 𝑄 ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
197	159 196	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
198	197	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
199		dfss3	⊢ ( ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ⊆ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) ↔ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) 𝑥 ∈ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
200	198 199	sylibr	⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ⊆ ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
201	28 35 37	syl2anc	⊢ ( 𝜑 → ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } = ( ( ran 𝑄 ∩ dom 𝐹 ) ∪ ∪ ran 𝐼 ) )
202	200 201	sseqtrrd	⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ⊆ ∪ { ( ran 𝑄 ∩ dom 𝐹 ) , ∪ ran 𝐼 } )
203	19 77 153 202	ssfiunibd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
204		nfv	⊢ Ⅎ 𝑥 𝜑
205		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦
206	204 205	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
207	1	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ℝ )
208	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐵 ∈ ℝ )
209	208 207	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐵 − 𝑥 ) ∈ ℝ )
210	4 3	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
211	6 210	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
212	211	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑇 ∈ ℝ )
213	3 4	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
214	5 213	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
215	214 6	breqtrrdi	⊢ ( 𝜑 → 0 < 𝑇 )
216	215	gt0ne0d	⊢ ( 𝜑 → 𝑇 ≠ 0 )
217	216	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑇 ≠ 0 )
218	209 212 217	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) ∈ ℝ )
219	218	flcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
220	219	zred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
221	220 212	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
222	207 221	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
223	17	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
224	207 222 223	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
225	224	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
226		fvex	⊢ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ V
227		eleq1	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑘 ∈ ℤ ↔ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) )
228	227	anbi2d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) ) )
229		oveq1	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
230	229	oveq2d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
231	230	fveq2d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
232	231	eqeq1d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) )
233	228 232	imbi12d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) ) )
234	226 233 15	vtocl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
235	219 234	mpdan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
236	225 235	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) )
237	236	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
238	237	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
239		fveq2	⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
240	239	fveq2d	⊢ ( 𝑥 = 𝑤 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) )
241	240	breq1d	⊢ ( 𝑥 = 𝑤 → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 ) )
242	241	cbvralvw	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 )
243	242	biimpi	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 )
244	243	ad2antlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 )
245		iocssicc	⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
246	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐴 ∈ ℝ )
247	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐴 < 𝐵 )
248		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
249		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑦 ) )
250	249	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑦 ) / 𝑇 ) )
251	250	fveq2d	⊢ ( 𝑥 = 𝑦 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) )
252	251	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) )
253	248 252	oveq12d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) )
254	253	cbvmptv	⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) )
255	17 254	eqtri	⊢ 𝐸 = ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) )
256	246 208 247 6 255	fourierdlem4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
257	256 207	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
258	245 257	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 [,] 𝐵 ) )
259	230	eleq1d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 ↔ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 ) )
260	228 259	imbi12d	⊢ ( 𝑘 = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ dom 𝐹 ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 ) ) )
261	226 260 14	vtocl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) ∧ ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 )
262	219 261	mpdan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ dom 𝐹 )
263	224 262	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ dom 𝐹 )
264	258 263	elind	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) )
265	264	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) )
266		fveq2	⊢ ( 𝑤 = ( 𝐸 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) )
267	266	fveq2d	⊢ ( 𝑤 = ( 𝐸 ‘ 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
268	267	breq1d	⊢ ( 𝑤 = ( 𝐸 ‘ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) ≤ 𝑦 ) )
269	268	rspccva	⊢ ( ( ∀ 𝑤 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) ≤ 𝑦 ∧ ( 𝐸 ‘ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) ≤ 𝑦 )
270	244 265 269	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ ( 𝐸 ‘ 𝑥 ) ) ) ≤ 𝑦 )
271	238 270	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
272	271	ex	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) → ( 𝑥 ∈ dom 𝐹 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
273	206 272	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) → ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
274	273	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
275	274	reximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∩ dom 𝐹 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
276	203 275	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )