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	$⊢ φ \to dom F \subseteq ℝ$
	fourierdlem71.f	$⊢ φ \to F : dom F ⟶ ℝ$
	fourierdlem71.a	$⊢ φ \to A \in ℝ$
	fourierdlem71.b	$⊢ φ \to B \in ℝ$
	fourierdlem71.altb	$⊢ φ \to A < B$
	fourierdlem71.t	$⊢ T = B - A$
	fourierdlem71.7	$⊢ φ \to M \in ℕ$
	fourierdlem71.q	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
	fourierdlem71.q0	$⊢ φ \to Q (0) = A$
	fourierdlem71.10	$⊢ φ \to Q (M) = B$
	fourierdlem71.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem71.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem71.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem71.xpt	$⊢ ((φ \land x \in dom F) \land k \in ℤ) \to x + k T \in dom F$
	fourierdlem71.fxpt	$⊢ ((φ \land x \in dom F) \land k \in ℤ) \to F (x + k T) = F (x)$
	fourierdlem71.i	$⊢ I = (i \in (0 ..^M) ⟼ (Q (i), Q (i + 1)))$
	fourierdlem71.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
Assertion	fourierdlem71	$⊢ φ \to \exists y \in ℝ \forall x \in dom F \|F (x)\| \leq y$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem71

Proof