fourierdlem70

Description: A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem70.a	$⊢ φ \to A \in ℝ$
	fourierdlem70.2	$⊢ φ \to B \in ℝ$
	fourierdlem70.aleb	$⊢ φ \to A \leq B$
	fourierdlem70.f	$⊢ φ \to F : [A, B] ⟶ ℝ$
	fourierdlem70.m	$⊢ φ \to M \in ℕ$
	fourierdlem70.q	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
	fourierdlem70.q0	$⊢ φ \to Q (0) = A$
	fourierdlem70.qm	$⊢ φ \to Q (M) = B$
	fourierdlem70.qlt	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
	fourierdlem70.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem70.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem70.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem70.i	$⊢ I = (i \in (0 ..^M) ⟼ (Q (i), Q (i + 1)))$
Assertion	fourierdlem70	$⊢ φ \to \exists x \in ℝ \forall s \in [A, B] \|F (s)\| \leq x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem70.a	$⊢ φ \to A \in ℝ$
2		fourierdlem70.2	$⊢ φ \to B \in ℝ$
3		fourierdlem70.aleb	$⊢ φ \to A \leq B$
4		fourierdlem70.f	$⊢ φ \to F : [A, B] ⟶ ℝ$
5		fourierdlem70.m	$⊢ φ \to M \in ℕ$
6		fourierdlem70.q	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
7		fourierdlem70.q0	$⊢ φ \to Q (0) = A$
8		fourierdlem70.qm	$⊢ φ \to Q (M) = B$
9		fourierdlem70.qlt	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
10		fourierdlem70.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem70.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
12		fourierdlem70.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
13		fourierdlem70.i	$⊢ I = (i \in (0 ..^M) ⟼ (Q (i), Q (i + 1)))$
14		prfi	$⊢ \{ran Q, ⋃ ran I\} \in Fin$
15	14	a1i	$⊢ φ \to \{ran Q, ⋃ ran I\} \in Fin$
16		simpr	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to s \in ⋃ \{ran Q, ⋃ ran I\}$
17		ovex	$⊢ (0 \dots M) \in V$
18		fex	$⊢ (Q : (0 \dots M) ⟶ ℝ \land (0 \dots M) \in V) \to Q \in V$
19	6 17 18	sylancl	$⊢ φ \to Q \in V$
20		rnexg	$⊢ Q \in V \to ran Q \in V$
21	19 20	syl	$⊢ φ \to ran Q \in V$
22		fzofi	$⊢ (0 ..^M) \in Fin$
23	13	rnmptfi	$⊢ (0 ..^M) \in Fin \to ran I \in Fin$
24	22 23	ax-mp	$⊢ ran I \in Fin$
25	24	elexi	$⊢ ran I \in V$
26	25	uniex	$⊢ ⋃ ran I \in V$
27		uniprg	$⊢ (ran Q \in V \land ⋃ ran I \in V) \to ⋃ \{ran Q, ⋃ ran I\} = ran Q \cup ⋃ ran I$
28	21 26 27	sylancl	$⊢ φ \to ⋃ \{ran Q, ⋃ ran I\} = ran Q \cup ⋃ ran I$
29	28	adantr	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to ⋃ \{ran Q, ⋃ ran I\} = ran Q \cup ⋃ ran I$
30	16 29	eleqtrd	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to s \in (ran Q \cup ⋃ ran I)$
31		eqid	$⊢ (y \in ℕ ⟼ \{v \in (ℝ^{(0 \dots y)}) \| ((v (0) = A \land v (y) = B) \land \forall i \in (0 ..^y) v (i) < v (i + 1))\}) = (y \in ℕ ⟼ \{v \in (ℝ^{(0 \dots y)}) \| ((v (0) = A \land v (y) = B) \land \forall i \in (0 ..^y) v (i) < v (i + 1))\})$
32		reex	$⊢ ℝ \in V$
33	32 17	elmap	$⊢ Q \in (ℝ^{(0 \dots M)}) \leftrightarrow Q : (0 \dots M) ⟶ ℝ$
34	6 33	sylibr	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
35	7 8	jca	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
36	9	ralrimiva	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
37	34 35 36	jca32	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
38	31	fourierdlem2	$⊢ M \in ℕ \to (Q \in (y \in ℕ ⟼ \{v \in (ℝ^{(0 \dots y)}) \| ((v (0) = A \land v (y) = B) \land \forall i \in (0 ..^y) v (i) < v (i + 1))\}) (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
39	5 38	syl	$⊢ φ \to (Q \in (y \in ℕ ⟼ \{v \in (ℝ^{(0 \dots y)}) \| ((v (0) = A \land v (y) = B) \land \forall i \in (0 ..^y) v (i) < v (i + 1))\}) (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
40	37 39	mpbird	$⊢ φ \to Q \in (y \in ℕ ⟼ \{v \in (ℝ^{(0 \dots y)}) \| ((v (0) = A \land v (y) = B) \land \forall i \in (0 ..^y) v (i) < v (i + 1))\}) (M)$
41	31 5 40	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
42	41	frnd	$⊢ φ \to ran Q \subseteq [A, B]$
43	42	sselda	$⊢ (φ \land s \in ran Q) \to s \in [A, B]$
44	43	adantlr	$⊢ ((φ \land s \in (ran Q \cup ⋃ ran I)) \land s \in ran Q) \to s \in [A, B]$
45		simpll	$⊢ ((φ \land s \in (ran Q \cup ⋃ ran I)) \land \neg s \in ran Q) \to φ$
46		elunnel1	$⊢ (s \in (ran Q \cup ⋃ ran I) \land \neg s \in ran Q) \to s \in ⋃ ran I$
47	46	adantll	$⊢ ((φ \land s \in (ran Q \cup ⋃ ran I)) \land \neg s \in ran Q) \to s \in ⋃ ran I$
48		simpr	$⊢ (φ \land s \in ⋃ ran I) \to s \in ⋃ ran I$
49	13	funmpt2	$⊢ Fun I$
50		elunirn	$⊢ Fun I \to (s \in ⋃ ran I \leftrightarrow \exists i \in dom I s \in I (i))$
51	49 50	mp1i	$⊢ (φ \land s \in ⋃ ran I) \to (s \in ⋃ ran I \leftrightarrow \exists i \in dom I s \in I (i))$
52	48 51	mpbid	$⊢ (φ \land s \in ⋃ ran I) \to \exists i \in dom I s \in I (i)$
53		id	$⊢ i \in dom I \to i \in dom I$
54		ovex	$⊢ (Q (i), Q (i + 1)) \in V$
55	54 13	dmmpti	$⊢ dom I = (0 ..^M)$
56	53 55	eleqtrdi	$⊢ i \in dom I \to i \in (0 ..^M)$
57	13	fvmpt2	$⊢ (i \in (0 ..^M) \land (Q (i), Q (i + 1)) \in V) \to I (i) = (Q (i), Q (i + 1))$
58	56 54 57	sylancl	$⊢ i \in dom I \to I (i) = (Q (i), Q (i + 1))$
59	58	adantl	$⊢ (φ \land i \in dom I) \to I (i) = (Q (i), Q (i + 1))$
60		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
61	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
62	61	adantr	$⊢ (φ \land i \in dom I) \to A \in ℝ^{*}$
63	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
64	63	adantr	$⊢ (φ \land i \in dom I) \to B \in ℝ^{*}$
65	41	adantr	$⊢ (φ \land i \in dom I) \to Q : (0 \dots M) ⟶ [A, B]$
66	56	adantl	$⊢ (φ \land i \in dom I) \to i \in (0 ..^M)$
67	62 64 65 66	fourierdlem8	$⊢ (φ \land i \in dom I) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
68	60 67	sstrid	$⊢ (φ \land i \in dom I) \to (Q (i), Q (i + 1)) \subseteq [A, B]$
69	59 68	eqsstrd	$⊢ (φ \land i \in dom I) \to I (i) \subseteq [A, B]$
70	69	3adant3	$⊢ (φ \land i \in dom I \land s \in I (i)) \to I (i) \subseteq [A, B]$
71		simp3	$⊢ (φ \land i \in dom I \land s \in I (i)) \to s \in I (i)$
72	70 71	sseldd	$⊢ (φ \land i \in dom I \land s \in I (i)) \to s \in [A, B]$
73	72	3exp	$⊢ φ \to (i \in dom I \to (s \in I (i) \to s \in [A, B]))$
74	73	adantr	$⊢ (φ \land s \in ⋃ ran I) \to (i \in dom I \to (s \in I (i) \to s \in [A, B]))$
75	74	rexlimdv	$⊢ (φ \land s \in ⋃ ran I) \to (\exists i \in dom I s \in I (i) \to s \in [A, B])$
76	52 75	mpd	$⊢ (φ \land s \in ⋃ ran I) \to s \in [A, B]$
77	45 47 76	syl2anc	$⊢ ((φ \land s \in (ran Q \cup ⋃ ran I)) \land \neg s \in ran Q) \to s \in [A, B]$
78	44 77	pm2.61dan	$⊢ (φ \land s \in (ran Q \cup ⋃ ran I)) \to s \in [A, B]$
79	30 78	syldan	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to s \in [A, B]$
80	4	ffvelcdmda	$⊢ (φ \land s \in [A, B]) \to F (s) \in ℝ$
81	79 80	syldan	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to F (s) \in ℝ$
82	81	recnd	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to F (s) \in ℂ$
83	82	abscld	$⊢ (φ \land s \in ⋃ \{ran Q, ⋃ ran I\}) \to \|F (s)\| \in ℝ$
84		simpr	$⊢ (φ \land w = ran Q) \to w = ran Q$
85	6	adantr	$⊢ (φ \land w = ran Q) \to Q : (0 \dots M) ⟶ ℝ$
86		fzfid	$⊢ (φ \land w = ran Q) \to (0 \dots M) \in Fin$
87		rnffi	$⊢ (Q : (0 \dots M) ⟶ ℝ \land (0 \dots M) \in Fin) \to ran Q \in Fin$
88	85 86 87	syl2anc	$⊢ (φ \land w = ran Q) \to ran Q \in Fin$
89	84 88	eqeltrd	$⊢ (φ \land w = ran Q) \to w \in Fin$
90	89	adantlr	$⊢ ((φ \land w \in \{ran Q, ⋃ ran I\}) \land w = ran Q) \to w \in Fin$
91	4	ad2antrr	$⊢ ((φ \land w = ran Q) \land s \in w) \to F : [A, B] ⟶ ℝ$
92		simpll	$⊢ ((φ \land w = ran Q) \land s \in w) \to φ$
93		simpr	$⊢ (w = ran Q \land s \in w) \to s \in w$
94		simpl	$⊢ (w = ran Q \land s \in w) \to w = ran Q$
95	93 94	eleqtrd	$⊢ (w = ran Q \land s \in w) \to s \in ran Q$
96	95	adantll	$⊢ ((φ \land w = ran Q) \land s \in w) \to s \in ran Q$
97	92 96 43	syl2anc	$⊢ ((φ \land w = ran Q) \land s \in w) \to s \in [A, B]$
98	91 97	ffvelcdmd	$⊢ ((φ \land w = ran Q) \land s \in w) \to F (s) \in ℝ$
99	98	recnd	$⊢ ((φ \land w = ran Q) \land s \in w) \to F (s) \in ℂ$
100	99	abscld	$⊢ ((φ \land w = ran Q) \land s \in w) \to \|F (s)\| \in ℝ$
101	100	ralrimiva	$⊢ (φ \land w = ran Q) \to \forall s \in w \|F (s)\| \in ℝ$
102	101	adantlr	$⊢ ((φ \land w \in \{ran Q, ⋃ ran I\}) \land w = ran Q) \to \forall s \in w \|F (s)\| \in ℝ$
103		fimaxre3	$⊢ (w \in Fin \land \forall s \in w \|F (s)\| \in ℝ) \to \exists z \in ℝ \forall s \in w \|F (s)\| \leq z$
104	90 102 103	syl2anc	$⊢ ((φ \land w \in \{ran Q, ⋃ ran I\}) \land w = ran Q) \to \exists z \in ℝ \forall s \in w \|F (s)\| \leq z$
105		simpll	$⊢ ((φ \land w \in \{ran Q, ⋃ ran I\}) \land \neg w = ran Q) \to φ$
106		neqne	$⊢ \neg w = ran Q \to w \neq ran Q$
107		elprn1	$⊢ (w \in \{ran Q, ⋃ ran I\} \land w \neq ran Q) \to w = ⋃ ran I$
108	106 107	sylan2	$⊢ (w \in \{ran Q, ⋃ ran I\} \land \neg w = ran Q) \to w = ⋃ ran I$
109	108	adantll	$⊢ ((φ \land w \in \{ran Q, ⋃ ran I\}) \land \neg w = ran Q) \to w = ⋃ ran I$
110	22 23	mp1i	$⊢ (φ \land w = ⋃ ran I) \to ran I \in Fin$
111		ax-resscn	$⊢ ℝ \subseteq ℂ$
112	111	a1i	$⊢ φ \to ℝ \subseteq ℂ$
113	4 112	fssd	$⊢ φ \to F : [A, B] ⟶ ℂ$
114	113	ad2antrr	$⊢ ((φ \land w = ⋃ ran I) \land s \in ⋃ ran I) \to F : [A, B] ⟶ ℂ$
115	76	adantlr	$⊢ ((φ \land w = ⋃ ran I) \land s \in ⋃ ran I) \to s \in [A, B]$
116	114 115	ffvelcdmd	$⊢ ((φ \land w = ⋃ ran I) \land s \in ⋃ ran I) \to F (s) \in ℂ$
117	116	abscld	$⊢ ((φ \land w = ⋃ ran I) \land s \in ⋃ ran I) \to \|F (s)\| \in ℝ$
118	54 13	fnmpti	$⊢ I Fn (0 ..^M)$
119		fvelrnb	$⊢ I Fn (0 ..^M) \to (t \in ran I \leftrightarrow \exists i \in (0 ..^M) I (i) = t)$
120	118 119	ax-mp	$⊢ t \in ran I \leftrightarrow \exists i \in (0 ..^M) I (i) = t$
121	120	biimpi	$⊢ t \in ran I \to \exists i \in (0 ..^M) I (i) = t$
122	121	adantl	$⊢ (φ \land t \in ran I) \to \exists i \in (0 ..^M) I (i) = t$
123	6	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
124		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
125	124	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
126	123 125	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
127		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
128	127	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
129	123 128	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
130	126 129 10 12 11	cncfioobd	$⊢ (φ \land i \in (0 ..^M)) \to \exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|({F ↾}_{(Q (i), Q (i + 1))}) (s)\| \leq b$
131		fvres	$⊢ s \in (Q (i), Q (i + 1)) \to ({F ↾}_{(Q (i), Q (i + 1))}) (s) = F (s)$
132	131	fveq2d	$⊢ s \in (Q (i), Q (i + 1)) \to \|({F ↾}_{(Q (i), Q (i + 1))}) (s)\| = \|F (s)\|$
133	132	breq1d	$⊢ s \in (Q (i), Q (i + 1)) \to (\|({F ↾}_{(Q (i), Q (i + 1))}) (s)\| \leq b \leftrightarrow \|F (s)\| \leq b)$
134	133	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to (\|({F ↾}_{(Q (i), Q (i + 1))}) (s)\| \leq b \leftrightarrow \|F (s)\| \leq b)$
135	134	ralbidva	$⊢ (φ \land i \in (0 ..^M)) \to (\forall s \in (Q (i), Q (i + 1)) \|({F ↾}_{(Q (i), Q (i + 1))}) (s)\| \leq b \leftrightarrow \forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b)$
136	135	rexbidv	$⊢ (φ \land i \in (0 ..^M)) \to (\exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|({F ↾}_{(Q (i), Q (i + 1))}) (s)\| \leq b \leftrightarrow \exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b)$
137	130 136	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to \exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b$
138	137	3adant3	$⊢ (φ \land i \in (0 ..^M) \land I (i) = t) \to \exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b$
139	54 57	mpan2	$⊢ i \in (0 ..^M) \to I (i) = (Q (i), Q (i + 1))$
140	139	eqcomd	$⊢ i \in (0 ..^M) \to (Q (i), Q (i + 1)) = I (i)$
141	140	adantr	$⊢ (i \in (0 ..^M) \land I (i) = t) \to (Q (i), Q (i + 1)) = I (i)$
142		simpr	$⊢ (i \in (0 ..^M) \land I (i) = t) \to I (i) = t$
143	141 142	eqtrd	$⊢ (i \in (0 ..^M) \land I (i) = t) \to (Q (i), Q (i + 1)) = t$
144	143	raleqdv	$⊢ (i \in (0 ..^M) \land I (i) = t) \to (\forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b \leftrightarrow \forall s \in t \|F (s)\| \leq b)$
145	144	rexbidv	$⊢ (i \in (0 ..^M) \land I (i) = t) \to (\exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b \leftrightarrow \exists b \in ℝ \forall s \in t \|F (s)\| \leq b)$
146	145	3adant1	$⊢ (φ \land i \in (0 ..^M) \land I (i) = t) \to (\exists b \in ℝ \forall s \in (Q (i), Q (i + 1)) \|F (s)\| \leq b \leftrightarrow \exists b \in ℝ \forall s \in t \|F (s)\| \leq b)$
147	138 146	mpbid	$⊢ (φ \land i \in (0 ..^M) \land I (i) = t) \to \exists b \in ℝ \forall s \in t \|F (s)\| \leq b$
148	147	3exp	$⊢ φ \to (i \in (0 ..^M) \to (I (i) = t \to \exists b \in ℝ \forall s \in t \|F (s)\| \leq b))$
149	148	adantr	$⊢ (φ \land t \in ran I) \to (i \in (0 ..^M) \to (I (i) = t \to \exists b \in ℝ \forall s \in t \|F (s)\| \leq b))$
150	149	rexlimdv	$⊢ (φ \land t \in ran I) \to (\exists i \in (0 ..^M) I (i) = t \to \exists b \in ℝ \forall s \in t \|F (s)\| \leq b)$
151	122 150	mpd	$⊢ (φ \land t \in ran I) \to \exists b \in ℝ \forall s \in t \|F (s)\| \leq b$
152	151	adantlr	$⊢ ((φ \land w = ⋃ ran I) \land t \in ran I) \to \exists b \in ℝ \forall s \in t \|F (s)\| \leq b$
153		eqimss	$⊢ w = ⋃ ran I \to w \subseteq ⋃ ran I$
154	153	adantl	$⊢ (φ \land w = ⋃ ran I) \to w \subseteq ⋃ ran I$
155	110 117 152 154	ssfiunibd	$⊢ (φ \land w = ⋃ ran I) \to \exists z \in ℝ \forall s \in w \|F (s)\| \leq z$
156	105 109 155	syl2anc	$⊢ ((φ \land w \in \{ran Q, ⋃ ran I\}) \land \neg w = ran Q) \to \exists z \in ℝ \forall s \in w \|F (s)\| \leq z$
157	104 156	pm2.61dan	$⊢ (φ \land w \in \{ran Q, ⋃ ran I\}) \to \exists z \in ℝ \forall s \in w \|F (s)\| \leq z$
158	5	ad2antrr	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to M \in ℕ$
159	6	ad2antrr	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to Q : (0 \dots M) ⟶ ℝ$
160		simpr	$⊢ (φ \land t \in [A, B]) \to t \in [A, B]$
161	7	eqcomd	$⊢ φ \to A = Q (0)$
162	8	eqcomd	$⊢ φ \to B = Q (M)$
163	161 162	oveq12d	$⊢ φ \to [A, B] = [Q (0), Q (M)]$
164	163	adantr	$⊢ (φ \land t \in [A, B]) \to [A, B] = [Q (0), Q (M)]$
165	160 164	eleqtrd	$⊢ (φ \land t \in [A, B]) \to t \in [Q (0), Q (M)]$
166	165	adantr	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to t \in [Q (0), Q (M)]$
167		simpr	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to \neg t \in ran Q$
168		fveq2	$⊢ k = j \to Q (k) = Q (j)$
169	168	breq1d	$⊢ k = j \to (Q (k) < t \leftrightarrow Q (j) < t)$
170	169	cbvrabv	$⊢ \{k \in (0 ..^M) \| Q (k) < t\} = \{j \in (0 ..^M) \| Q (j) < t\}$
171	170	supeq1i	$⊢ sup (\{k \in (0 ..^M) \| Q (k) < t\} ℝ <) = sup (\{j \in (0 ..^M) \| Q (j) < t\} ℝ <)$
172	158 159 166 167 171	fourierdlem25	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to \exists i \in (0 ..^M) t \in (Q (i), Q (i + 1))$
173	139	eleq2d	$⊢ i \in (0 ..^M) \to (t \in I (i) \leftrightarrow t \in (Q (i), Q (i + 1)))$
174	173	rexbiia	$⊢ \exists i \in (0 ..^M) t \in I (i) \leftrightarrow \exists i \in (0 ..^M) t \in (Q (i), Q (i + 1))$
175	172 174	sylibr	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to \exists i \in (0 ..^M) t \in I (i)$
176	55	eqcomi	$⊢ (0 ..^M) = dom I$
177	176	rexeqi	$⊢ \exists i \in (0 ..^M) t \in I (i) \leftrightarrow \exists i \in dom I t \in I (i)$
178	175 177	sylib	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to \exists i \in dom I t \in I (i)$
179		elunirn	$⊢ Fun I \to (t \in ⋃ ran I \leftrightarrow \exists i \in dom I t \in I (i))$
180	49 179	mp1i	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to (t \in ⋃ ran I \leftrightarrow \exists i \in dom I t \in I (i))$
181	178 180	mpbird	$⊢ ((φ \land t \in [A, B]) \land \neg t \in ran Q) \to t \in ⋃ ran I$
182	181	ex	$⊢ (φ \land t \in [A, B]) \to (\neg t \in ran Q \to t \in ⋃ ran I)$
183	182	orrd	$⊢ (φ \land t \in [A, B]) \to (t \in ran Q \lor t \in ⋃ ran I)$
184		elun	$⊢ t \in (ran Q \cup ⋃ ran I) \leftrightarrow (t \in ran Q \lor t \in ⋃ ran I)$
185	183 184	sylibr	$⊢ (φ \land t \in [A, B]) \to t \in (ran Q \cup ⋃ ran I)$
186	185	ralrimiva	$⊢ φ \to \forall t \in [A, B] t \in (ran Q \cup ⋃ ran I)$
187		dfss3	$⊢ [A, B] \subseteq ran Q \cup ⋃ ran I \leftrightarrow \forall t \in [A, B] t \in (ran Q \cup ⋃ ran I)$
188	186 187	sylibr	$⊢ φ \to [A, B] \subseteq ran Q \cup ⋃ ran I$
189	188 28	sseqtrrd	$⊢ φ \to [A, B] \subseteq ⋃ \{ran Q, ⋃ ran I\}$
190	15 83 157 189	ssfiunibd	$⊢ φ \to \exists x \in ℝ \forall s \in [A, B] \|F (s)\| \leq x$

Metamath Proof Explorer

Theorem fourierdlem70

Proof