fourierdlem54

Description: Given a partition Q and an arbitrary interval [ C , D ] , a partition S on [ C , D ] is built such that it preserves any periodic function piecewise continuous on Q will be piecewise continuous on S , with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem54.t	$⊢ T = B - A$
	fourierdlem54.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem54.m	$⊢ φ \to M \in ℕ$
	fourierdlem54.q	$⊢ φ \to Q \in P (M)$
	fourierdlem54.c	$⊢ φ \to C \in ℝ$
	fourierdlem54.d	$⊢ φ \to D \in ℝ$
	fourierdlem54.cd	$⊢ φ \to C < D$
	fourierdlem54.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem54.h	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
	fourierdlem54.n	$⊢ N = \|H\| - 1$
	fourierdlem54.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
Assertion	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem54.t	$⊢ T = B - A$
2		fourierdlem54.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
3		fourierdlem54.m	$⊢ φ \to M \in ℕ$
4		fourierdlem54.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem54.c	$⊢ φ \to C \in ℝ$
6		fourierdlem54.d	$⊢ φ \to D \in ℝ$
7		fourierdlem54.cd	$⊢ φ \to C < D$
8		fourierdlem54.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
9		fourierdlem54.h	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
10		fourierdlem54.n	$⊢ N = \|H\| - 1$
11		fourierdlem54.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
12		2z	$⊢ 2 \in ℤ$
13	12	a1i	$⊢ φ \to 2 \in ℤ$
14		prid1g	$⊢ C \in ℝ \to C \in \{C, D\}$
15		elun1	$⊢ C \in \{C, D\} \to C \in (\{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\})$
16	5 14 15	3syl	$⊢ φ \to C \in (\{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\})$
17	16 9	eleqtrrdi	$⊢ φ \to C \in H$
18	17	ne0d	$⊢ φ \to H \neq \emptyset$
19		prfi	$⊢ \{C, D\} \in Fin$
20	2 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
21	20	simp1d	$⊢ φ \to A \in ℝ$
22	20	simp2d	$⊢ φ \to B \in ℝ$
23	20	simp3d	$⊢ φ \to A < B$
24	2 3 4	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
25		frn	$⊢ Q : (0 \dots M) ⟶ [A, B] \to ran Q \subseteq [A, B]$
26	24 25	syl	$⊢ φ \to ran Q \subseteq [A, B]$
27	2	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (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))))$
28	3 27	syl	$⊢ φ \to (Q \in P (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))))$
29	4 28	mpbid	$⊢ φ \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)))$
30	29	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
31		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
32		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
33	30 31 32	3syl	$⊢ φ \to Q Fn (0 \dots M)$
34		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
35		fnfi	$⊢ (Q Fn (0 \dots M) \land (0 \dots M) \in Fin) \to Q \in Fin$
36	33 34 35	syl2anc	$⊢ φ \to Q \in Fin$
37		rnfi	$⊢ Q \in Fin \to ran Q \in Fin$
38	36 37	syl	$⊢ φ \to ran Q \in Fin$
39	29	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
40	39	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
41	40	simpld	$⊢ φ \to Q (0) = A$
42	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
43		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
44	42 43	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
45		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
46	44 45	syl	$⊢ φ \to 0 \in (0 \dots M)$
47		fnfvelrn	$⊢ (Q Fn (0 \dots M) \land 0 \in (0 \dots M)) \to Q (0) \in ran Q$
48	33 46 47	syl2anc	$⊢ φ \to Q (0) \in ran Q$
49	41 48	eqeltrrd	$⊢ φ \to A \in ran Q$
50	40	simprd	$⊢ φ \to Q (M) = B$
51		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
52	44 51	syl	$⊢ φ \to M \in (0 \dots M)$
53		fnfvelrn	$⊢ (Q Fn (0 \dots M) \land M \in (0 \dots M)) \to Q (M) \in ran Q$
54	33 52 53	syl2anc	$⊢ φ \to Q (M) \in ran Q$
55	50 54	eqeltrrd	$⊢ φ \to B \in ran Q$
56		eqid	$⊢ abs \circ - = abs \circ -$
57		eqid	$⊢ (ran Q \times ran Q) ∖ I = (ran Q \times ran Q) ∖ I$
58		eqid	$⊢ ran ({(abs \circ -) ↾}_{((ran Q \times ran Q) ∖ I)}) = ran ({(abs \circ -) ↾}_{((ran Q \times ran Q) ∖ I)})$
59		eqid	$⊢ inf (ran ({(abs \circ -) ↾}_{((ran Q \times ran Q) ∖ I)}) ℝ <) = inf (ran ({(abs \circ -) ↾}_{((ran Q \times ran Q) ∖ I)}) ℝ <)$
60		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
61		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [C, D] = topGen (ran (.)) ↾_{𝑡} [C, D]$
62		oveq1	$⊢ x = w \to x + k T = w + k T$
63	62	eleq1d	$⊢ x = w \to (x + k T \in ran Q \leftrightarrow w + k T \in ran Q)$
64	63	rexbidv	$⊢ x = w \to (\exists k \in ℤ x + k T \in ran Q \leftrightarrow \exists k \in ℤ w + k T \in ran Q)$
65	64	cbvrabv	$⊢ \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} = \{w \in [C, D] \| \exists k \in ℤ w + k T \in ran Q\}$
66		oveq1	$⊢ i = j \to i T = j T$
67	66	oveq2d	$⊢ i = j \to y + i T = y + j T$
68	67	eleq1d	$⊢ i = j \to (y + i T \in ran Q \leftrightarrow y + j T \in ran Q)$
69	68	anbi1d	$⊢ i = j \to ((y + i T \in ran Q \land z + l T \in ran Q) \leftrightarrow (y + j T \in ran Q \land z + l T \in ran Q))$
70		oveq1	$⊢ l = k \to l T = k T$
71	70	oveq2d	$⊢ l = k \to z + l T = z + k T$
72	71	eleq1d	$⊢ l = k \to (z + l T \in ran Q \leftrightarrow z + k T \in ran Q)$
73	72	anbi2d	$⊢ l = k \to ((y + j T \in ran Q \land z + l T \in ran Q) \leftrightarrow (y + j T \in ran Q \land z + k T \in ran Q))$
74	69 73	cbvrex2vw	$⊢ \exists i \in ℤ \exists l \in ℤ (y + i T \in ran Q \land z + l T \in ran Q) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (y + j T \in ran Q \land z + k T \in ran Q)$
75	74	anbi2i	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y < z)) \land \exists i \in ℤ \exists l \in ℤ (y + i T \in ran Q \land z + l T \in ran Q)) \leftrightarrow ((φ \land (y \in ℝ \land z \in ℝ \land y < z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in ran Q \land z + k T \in ran Q))$
76	21 22 23 1 26 38 49 55 56 57 58 59 5 6 60 61 65 75	fourierdlem42	$⊢ φ \to \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \in Fin$
77		unfi	$⊢ (\{C, D\} \in Fin \land \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \in Fin) \to \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \in Fin$
78	19 76 77	sylancr	$⊢ φ \to \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \in Fin$
79	9 78	eqeltrid	$⊢ φ \to H \in Fin$
80		hashnncl	$⊢ H \in Fin \to (\|H\| \in ℕ \leftrightarrow H \neq \emptyset)$
81	79 80	syl	$⊢ φ \to (\|H\| \in ℕ \leftrightarrow H \neq \emptyset)$
82	18 81	mpbird	$⊢ φ \to \|H\| \in ℕ$
83	82	nnzd	$⊢ φ \to \|H\| \in ℤ$
84	5 7	ltned	$⊢ φ \to C \neq D$
85		hashprg	$⊢ (C \in ℝ \land D \in ℝ) \to (C \neq D \leftrightarrow \|\{C, D\}\| = 2)$
86	5 6 85	syl2anc	$⊢ φ \to (C \neq D \leftrightarrow \|\{C, D\}\| = 2)$
87	84 86	mpbid	$⊢ φ \to \|\{C, D\}\| = 2$
88	87	eqcomd	$⊢ φ \to 2 = \|\{C, D\}\|$
89		ssun1	$⊢ \{C, D\} \subseteq \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
90	89	a1i	$⊢ φ \to \{C, D\} \subseteq \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
91	90 9	sseqtrrdi	$⊢ φ \to \{C, D\} \subseteq H$
92		hashssle	$⊢ (H \in Fin \land \{C, D\} \subseteq H) \to \|\{C, D\}\| \leq \|H\|$
93	79 91 92	syl2anc	$⊢ φ \to \|\{C, D\}\| \leq \|H\|$
94	88 93	eqbrtrd	$⊢ φ \to 2 \leq \|H\|$
95		eluz2	$⊢ \|H\| \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land \|H\| \in ℤ \land 2 \leq \|H\|)$
96	13 83 94 95	syl3anbrc	$⊢ φ \to \|H\| \in ℤ_{\geq 2}$
97		uz2m1nn	$⊢ \|H\| \in ℤ_{\geq 2} \to \|H\| - 1 \in ℕ$
98	96 97	syl	$⊢ φ \to \|H\| - 1 \in ℕ$
99	10 98	eqeltrid	$⊢ φ \to N \in ℕ$
100		prssg	$⊢ (C \in ℝ \land D \in ℝ) \to ((C \in ℝ \land D \in ℝ) \leftrightarrow \{C, D\} \subseteq ℝ)$
101	5 6 100	syl2anc	$⊢ φ \to ((C \in ℝ \land D \in ℝ) \leftrightarrow \{C, D\} \subseteq ℝ)$
102	5 6 101	mpbi2and	$⊢ φ \to \{C, D\} \subseteq ℝ$
103		ssrab2	$⊢ \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \subseteq [C, D]$
104	5 6	iccssred	$⊢ φ \to [C, D] \subseteq ℝ$
105	103 104	sstrid	$⊢ φ \to \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \subseteq ℝ$
106	102 105	unssd	$⊢ φ \to \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \subseteq ℝ$
107	9 106	eqsstrid	$⊢ φ \to H \subseteq ℝ$
108	79 107 11 10	fourierdlem36	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), H)$
109		df-isom	$⊢ S {Isom}_{<, <} ((0 \dots N), H) \leftrightarrow (S : (0 \dots N) \underset{1-1 onto}{⟶} H \land \forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)))$
110	108 109	sylib	$⊢ φ \to (S : (0 \dots N) \underset{1-1 onto}{⟶} H \land \forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)))$
111	110	simpld	$⊢ φ \to S : (0 \dots N) \underset{1-1 onto}{⟶} H$
112		f1of	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} H \to S : (0 \dots N) ⟶ H$
113	111 112	syl	$⊢ φ \to S : (0 \dots N) ⟶ H$
114	113 107	fssd	$⊢ φ \to S : (0 \dots N) ⟶ ℝ$
115		reex	$⊢ ℝ \in V$
116		ovex	$⊢ (0 \dots N) \in V$
117	116	a1i	$⊢ φ \to (0 \dots N) \in V$
118		elmapg	$⊢ (ℝ \in V \land (0 \dots N) \in V) \to (S \in (ℝ^{(0 \dots N)}) \leftrightarrow S : (0 \dots N) ⟶ ℝ)$
119	115 117 118	sylancr	$⊢ φ \to (S \in (ℝ^{(0 \dots N)}) \leftrightarrow S : (0 \dots N) ⟶ ℝ)$
120	114 119	mpbird	$⊢ φ \to S \in (ℝ^{(0 \dots N)})$
121		df-f1o	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} H \leftrightarrow (S : (0 \dots N) \underset{1-1}{⟶} H \land S : (0 \dots N) \underset{onto}{⟶} H)$
122	111 121	sylib	$⊢ φ \to (S : (0 \dots N) \underset{1-1}{⟶} H \land S : (0 \dots N) \underset{onto}{⟶} H)$
123	122	simprd	$⊢ φ \to S : (0 \dots N) \underset{onto}{⟶} H$
124		dffo3	$⊢ S : (0 \dots N) \underset{onto}{⟶} H \leftrightarrow (S : (0 \dots N) ⟶ H \land \forall h \in H \exists y \in (0 \dots N) h = S (y))$
125	123 124	sylib	$⊢ φ \to (S : (0 \dots N) ⟶ H \land \forall h \in H \exists y \in (0 \dots N) h = S (y))$
126	125	simprd	$⊢ φ \to \forall h \in H \exists y \in (0 \dots N) h = S (y)$
127		eqeq1	$⊢ h = C \to (h = S (y) \leftrightarrow C = S (y))$
128		eqcom	$⊢ C = S (y) \leftrightarrow S (y) = C$
129	127 128	bitrdi	$⊢ h = C \to (h = S (y) \leftrightarrow S (y) = C)$
130	129	rexbidv	$⊢ h = C \to (\exists y \in (0 \dots N) h = S (y) \leftrightarrow \exists y \in (0 \dots N) S (y) = C)$
131	130	rspcv	$⊢ C \in H \to (\forall h \in H \exists y \in (0 \dots N) h = S (y) \to \exists y \in (0 \dots N) S (y) = C)$
132	17 126 131	sylc	$⊢ φ \to \exists y \in (0 \dots N) S (y) = C$
133		fveq2	$⊢ y = 0 \to S (y) = S (0)$
134	133	eqcomd	$⊢ y = 0 \to S (0) = S (y)$
135	134	adantl	$⊢ ((φ \land S (y) = C) \land y = 0) \to S (0) = S (y)$
136		simplr	$⊢ ((φ \land S (y) = C) \land y = 0) \to S (y) = C$
137	135 136	eqtrd	$⊢ ((φ \land S (y) = C) \land y = 0) \to S (0) = C$
138	5	ad2antrr	$⊢ ((φ \land S (y) = C) \land y = 0) \to C \in ℝ$
139	137 138	eqeltrd	$⊢ ((φ \land S (y) = C) \land y = 0) \to S (0) \in ℝ$
140	139 137	eqled	$⊢ ((φ \land S (y) = C) \land y = 0) \to S (0) \leq C$
141	140	3adantl2	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land y = 0) \to S (0) \leq C$
142	5	rexrd	$⊢ φ \to C \in ℝ^{*}$
143	6	rexrd	$⊢ φ \to D \in ℝ^{*}$
144	5 6 7	ltled	$⊢ φ \to C \leq D$
145		lbicc2	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C \leq D) \to C \in [C, D]$
146	142 143 144 145	syl3anc	$⊢ φ \to C \in [C, D]$
147		ubicc2	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C \leq D) \to D \in [C, D]$
148	142 143 144 147	syl3anc	$⊢ φ \to D \in [C, D]$
149		prssg	$⊢ (C \in [C, D] \land D \in [C, D]) \to ((C \in [C, D] \land D \in [C, D]) \leftrightarrow \{C, D\} \subseteq [C, D])$
150	146 148 149	syl2anc	$⊢ φ \to ((C \in [C, D] \land D \in [C, D]) \leftrightarrow \{C, D\} \subseteq [C, D])$
151	146 148 150	mpbi2and	$⊢ φ \to \{C, D\} \subseteq [C, D]$
152	103	a1i	$⊢ φ \to \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \subseteq [C, D]$
153	151 152	unssd	$⊢ φ \to \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \subseteq [C, D]$
154	9 153	eqsstrid	$⊢ φ \to H \subseteq [C, D]$
155		nnm1nn0	$⊢ \|H\| \in ℕ \to \|H\| - 1 \in ℕ_{0}$
156	82 155	syl	$⊢ φ \to \|H\| - 1 \in ℕ_{0}$
157	10 156	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
158	157 43	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
159		eluzfz1	$⊢ N \in ℤ_{\geq 0} \to 0 \in (0 \dots N)$
160	158 159	syl	$⊢ φ \to 0 \in (0 \dots N)$
161	113 160	ffvelcdmd	$⊢ φ \to S (0) \in H$
162	154 161	sseldd	$⊢ φ \to S (0) \in [C, D]$
163	104 162	sseldd	$⊢ φ \to S (0) \in ℝ$
164	163	adantr	$⊢ (φ \land \neg y = 0) \to S (0) \in ℝ$
165	164	3ad2antl1	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to S (0) \in ℝ$
166	5	adantr	$⊢ (φ \land \neg y = 0) \to C \in ℝ$
167	166	3ad2antl1	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to C \in ℝ$
168		elfzelz	$⊢ y \in (0 \dots N) \to y \in ℤ$
169	168	zred	$⊢ y \in (0 \dots N) \to y \in ℝ$
170	169	adantr	$⊢ (y \in (0 \dots N) \land \neg y = 0) \to y \in ℝ$
171		elfzle1	$⊢ y \in (0 \dots N) \to 0 \leq y$
172	171	adantr	$⊢ (y \in (0 \dots N) \land \neg y = 0) \to 0 \leq y$
173		neqne	$⊢ \neg y = 0 \to y \neq 0$
174	173	adantl	$⊢ (y \in (0 \dots N) \land \neg y = 0) \to y \neq 0$
175	170 172 174	ne0gt0d	$⊢ (y \in (0 \dots N) \land \neg y = 0) \to 0 < y$
176	175	3ad2antl2	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to 0 < y$
177		simpl1	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to φ$
178		simpl2	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to y \in (0 \dots N)$
179	110	simprd	$⊢ φ \to \forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y))$
180		breq1	$⊢ x = 0 \to (x < y \leftrightarrow 0 < y)$
181		fveq2	$⊢ x = 0 \to S (x) = S (0)$
182	181	breq1d	$⊢ x = 0 \to (S (x) < S (y) \leftrightarrow S (0) < S (y))$
183	180 182	bibi12d	$⊢ x = 0 \to ((x < y \leftrightarrow S (x) < S (y)) \leftrightarrow (0 < y \leftrightarrow S (0) < S (y)))$
184	183	ralbidv	$⊢ x = 0 \to (\forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)) \leftrightarrow \forall y \in (0 \dots N) (0 < y \leftrightarrow S (0) < S (y)))$
185	184	rspcv	$⊢ 0 \in (0 \dots N) \to (\forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)) \to \forall y \in (0 \dots N) (0 < y \leftrightarrow S (0) < S (y)))$
186	160 179 185	sylc	$⊢ φ \to \forall y \in (0 \dots N) (0 < y \leftrightarrow S (0) < S (y))$
187	186	r19.21bi	$⊢ (φ \land y \in (0 \dots N)) \to (0 < y \leftrightarrow S (0) < S (y))$
188	177 178 187	syl2anc	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to (0 < y \leftrightarrow S (0) < S (y))$
189	176 188	mpbid	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to S (0) < S (y)$
190		simpl3	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to S (y) = C$
191	189 190	breqtrd	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to S (0) < C$
192	165 167 191	ltled	$⊢ ((φ \land y \in (0 \dots N) \land S (y) = C) \land \neg y = 0) \to S (0) \leq C$
193	141 192	pm2.61dan	$⊢ (φ \land y \in (0 \dots N) \land S (y) = C) \to S (0) \leq C$
194	193	rexlimdv3a	$⊢ φ \to (\exists y \in (0 \dots N) S (y) = C \to S (0) \leq C)$
195	132 194	mpd	$⊢ φ \to S (0) \leq C$
196		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (S (0) \in [C, D] \leftrightarrow (S (0) \in ℝ \land C \leq S (0) \land S (0) \leq D))$
197	5 6 196	syl2anc	$⊢ φ \to (S (0) \in [C, D] \leftrightarrow (S (0) \in ℝ \land C \leq S (0) \land S (0) \leq D))$
198	162 197	mpbid	$⊢ φ \to (S (0) \in ℝ \land C \leq S (0) \land S (0) \leq D)$
199	198	simp2d	$⊢ φ \to C \leq S (0)$
200	163 5	letri3d	$⊢ φ \to (S (0) = C \leftrightarrow (S (0) \leq C \land C \leq S (0)))$
201	195 199 200	mpbir2and	$⊢ φ \to S (0) = C$
202		eluzfz2	$⊢ N \in ℤ_{\geq 0} \to N \in (0 \dots N)$
203	158 202	syl	$⊢ φ \to N \in (0 \dots N)$
204	113 203	ffvelcdmd	$⊢ φ \to S (N) \in H$
205	154 204	sseldd	$⊢ φ \to S (N) \in [C, D]$
206		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (S (N) \in [C, D] \leftrightarrow (S (N) \in ℝ \land C \leq S (N) \land S (N) \leq D))$
207	5 6 206	syl2anc	$⊢ φ \to (S (N) \in [C, D] \leftrightarrow (S (N) \in ℝ \land C \leq S (N) \land S (N) \leq D))$
208	205 207	mpbid	$⊢ φ \to (S (N) \in ℝ \land C \leq S (N) \land S (N) \leq D)$
209	208	simp3d	$⊢ φ \to S (N) \leq D$
210		prid2g	$⊢ D \in ℝ \to D \in \{C, D\}$
211		elun1	$⊢ D \in \{C, D\} \to D \in (\{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\})$
212	6 210 211	3syl	$⊢ φ \to D \in (\{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\})$
213	212 9	eleqtrrdi	$⊢ φ \to D \in H$
214		eqeq1	$⊢ h = D \to (h = S (y) \leftrightarrow D = S (y))$
215		eqcom	$⊢ D = S (y) \leftrightarrow S (y) = D$
216	214 215	bitrdi	$⊢ h = D \to (h = S (y) \leftrightarrow S (y) = D)$
217	216	rexbidv	$⊢ h = D \to (\exists y \in (0 \dots N) h = S (y) \leftrightarrow \exists y \in (0 \dots N) S (y) = D)$
218	217	rspcv	$⊢ D \in H \to (\forall h \in H \exists y \in (0 \dots N) h = S (y) \to \exists y \in (0 \dots N) S (y) = D)$
219	213 126 218	sylc	$⊢ φ \to \exists y \in (0 \dots N) S (y) = D$
220	215	biimpri	$⊢ S (y) = D \to D = S (y)$
221	220	3ad2ant3	$⊢ (φ \land y \in (0 \dots N) \land S (y) = D) \to D = S (y)$
222	114	ffvelcdmda	$⊢ (φ \land y \in (0 \dots N)) \to S (y) \in ℝ$
223	104 205	sseldd	$⊢ φ \to S (N) \in ℝ$
224	223	adantr	$⊢ (φ \land y \in (0 \dots N)) \to S (N) \in ℝ$
225	169	adantl	$⊢ (φ \land y \in (0 \dots N)) \to y \in ℝ$
226		elfzel2	$⊢ y \in (0 \dots N) \to N \in ℤ$
227	226	zred	$⊢ y \in (0 \dots N) \to N \in ℝ$
228	227	adantl	$⊢ (φ \land y \in (0 \dots N)) \to N \in ℝ$
229		elfzle2	$⊢ y \in (0 \dots N) \to y \leq N$
230	229	adantl	$⊢ (φ \land y \in (0 \dots N)) \to y \leq N$
231	225 228 230	lensymd	$⊢ (φ \land y \in (0 \dots N)) \to \neg N < y$
232		breq1	$⊢ x = N \to (x < y \leftrightarrow N < y)$
233		fveq2	$⊢ x = N \to S (x) = S (N)$
234	233	breq1d	$⊢ x = N \to (S (x) < S (y) \leftrightarrow S (N) < S (y))$
235	232 234	bibi12d	$⊢ x = N \to ((x < y \leftrightarrow S (x) < S (y)) \leftrightarrow (N < y \leftrightarrow S (N) < S (y)))$
236	235	ralbidv	$⊢ x = N \to (\forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)) \leftrightarrow \forall y \in (0 \dots N) (N < y \leftrightarrow S (N) < S (y)))$
237	236	rspcv	$⊢ N \in (0 \dots N) \to (\forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)) \to \forall y \in (0 \dots N) (N < y \leftrightarrow S (N) < S (y)))$
238	203 179 237	sylc	$⊢ φ \to \forall y \in (0 \dots N) (N < y \leftrightarrow S (N) < S (y))$
239	238	r19.21bi	$⊢ (φ \land y \in (0 \dots N)) \to (N < y \leftrightarrow S (N) < S (y))$
240	231 239	mtbid	$⊢ (φ \land y \in (0 \dots N)) \to \neg S (N) < S (y)$
241	222 224 240	nltled	$⊢ (φ \land y \in (0 \dots N)) \to S (y) \leq S (N)$
242	241	3adant3	$⊢ (φ \land y \in (0 \dots N) \land S (y) = D) \to S (y) \leq S (N)$
243	221 242	eqbrtrd	$⊢ (φ \land y \in (0 \dots N) \land S (y) = D) \to D \leq S (N)$
244	243	rexlimdv3a	$⊢ φ \to (\exists y \in (0 \dots N) S (y) = D \to D \leq S (N))$
245	219 244	mpd	$⊢ φ \to D \leq S (N)$
246	223 6	letri3d	$⊢ φ \to (S (N) = D \leftrightarrow (S (N) \leq D \land D \leq S (N)))$
247	209 245 246	mpbir2and	$⊢ φ \to S (N) = D$
248		elfzoelz	$⊢ i \in (0 ..^N) \to i \in ℤ$
249	248	zred	$⊢ i \in (0 ..^N) \to i \in ℝ$
250	249	ltp1d	$⊢ i \in (0 ..^N) \to i < i + 1$
251	250	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i < i + 1$
252	179	adantr	$⊢ (φ \land i \in (0 ..^N)) \to \forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y))$
253		elfzofz	$⊢ i \in (0 ..^N) \to i \in (0 \dots N)$
254	253	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i \in (0 \dots N)$
255		fzofzp1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 \dots N)$
256	255	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i + 1 \in (0 \dots N)$
257		breq1	$⊢ x = i \to (x < y \leftrightarrow i < y)$
258		fveq2	$⊢ x = i \to S (x) = S (i)$
259	258	breq1d	$⊢ x = i \to (S (x) < S (y) \leftrightarrow S (i) < S (y))$
260	257 259	bibi12d	$⊢ x = i \to ((x < y \leftrightarrow S (x) < S (y)) \leftrightarrow (i < y \leftrightarrow S (i) < S (y)))$
261		breq2	$⊢ y = i + 1 \to (i < y \leftrightarrow i < i + 1)$
262		fveq2	$⊢ y = i + 1 \to S (y) = S (i + 1)$
263	262	breq2d	$⊢ y = i + 1 \to (S (i) < S (y) \leftrightarrow S (i) < S (i + 1))$
264	261 263	bibi12d	$⊢ y = i + 1 \to ((i < y \leftrightarrow S (i) < S (y)) \leftrightarrow (i < i + 1 \leftrightarrow S (i) < S (i + 1)))$
265	260 264	rspc2v	$⊢ (i \in (0 \dots N) \land i + 1 \in (0 \dots N)) \to (\forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)) \to (i < i + 1 \leftrightarrow S (i) < S (i + 1)))$
266	254 256 265	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to (\forall x \in (0 \dots N) \forall y \in (0 \dots N) (x < y \leftrightarrow S (x) < S (y)) \to (i < i + 1 \leftrightarrow S (i) < S (i + 1)))$
267	252 266	mpd	$⊢ (φ \land i \in (0 ..^N)) \to (i < i + 1 \leftrightarrow S (i) < S (i + 1))$
268	251 267	mpbid	$⊢ (φ \land i \in (0 ..^N)) \to S (i) < S (i + 1)$
269	268	ralrimiva	$⊢ φ \to \forall i \in (0 ..^N) S (i) < S (i + 1)$
270	201 247 269	jca31	$⊢ φ \to ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))$
271	8	fourierdlem2	$⊢ N \in ℕ \to (S \in O (N) \leftrightarrow (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))))$
272	99 271	syl	$⊢ φ \to (S \in O (N) \leftrightarrow (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))))$
273	120 270 272	mpbir2and	$⊢ φ \to S \in O (N)$
274	99 273 108	jca31	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$

Metamath Proof Explorer

Theorem fourierdlem54

Proof