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

Metamath Proof Explorer

Theorem fourierdlem71

Proof