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

Metamath Proof Explorer

Theorem fourierdlem71

Proof