fourierdlem37

Description: I is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem37.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))\})$
	fourierdlem37.m	$⊢ φ \to M \in ℕ$
	fourierdlem37.q	$⊢ φ \to Q \in P (M)$
	fourierdlem37.t	$⊢ T = B - A$
	fourierdlem37.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem37.l	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
	fourierdlem37.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
Assertion	fourierdlem37	$⊢ φ \to (I : ℝ ⟶ (0 ..^M) \land (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem37.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))\})$
2		fourierdlem37.m	$⊢ φ \to M \in ℕ$
3		fourierdlem37.q	$⊢ φ \to Q \in P (M)$
4		fourierdlem37.t	$⊢ T = B - A$
5		fourierdlem37.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
6		fourierdlem37.l	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
7		fourierdlem37.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
8		ssrab2	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \subseteq (0 ..^M)$
9		ltso	$⊢ < Or ℝ$
10	9	a1i	$⊢ (φ \land x \in ℝ) \to < Or ℝ$
11		fzfi	$⊢ (0 \dots M) \in Fin$
12		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
13	8 12	sstri	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \subseteq (0 \dots M)$
14		ssfi	$⊢ ((0 \dots M) \in Fin \land \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \subseteq (0 \dots M)) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \in Fin$
15	11 13 14	mp2an	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \in Fin$
16	15	a1i	$⊢ (φ \land x \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \in Fin$
17		0zd	$⊢ φ \to 0 \in ℤ$
18	2	nnzd	$⊢ φ \to M \in ℤ$
19	2	nngt0d	$⊢ φ \to 0 < M$
20		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
21	17 18 19 20	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
22	21	adantr	$⊢ (φ \land x \in ℝ) \to 0 \in (0 ..^M)$
23	1	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))))$
24	2 23	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))))$
25	3 24	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)))$
26	25	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
27	26	simplld	$⊢ φ \to Q (0) = A$
28	1 2 3	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
29	28	simp1d	$⊢ φ \to A \in ℝ$
30	27 29	eqeltrd	$⊢ φ \to Q (0) \in ℝ$
31	30 27	eqled	$⊢ φ \to Q (0) \leq A$
32	31	ad2antrr	$⊢ ((φ \land x \in ℝ) \land E (x) = B) \to Q (0) \leq A$
33		iftrue	$⊢ E (x) = B \to if (E (x) = B, A, E (x)) = A$
34	33	eqcomd	$⊢ E (x) = B \to A = if (E (x) = B, A, E (x))$
35	34	adantl	$⊢ ((φ \land x \in ℝ) \land E (x) = B) \to A = if (E (x) = B, A, E (x))$
36	32 35	breqtrd	$⊢ ((φ \land x \in ℝ) \land E (x) = B) \to Q (0) \leq if (E (x) = B, A, E (x))$
37	30	adantr	$⊢ (φ \land x \in ℝ) \to Q (0) \in ℝ$
38	29	adantr	$⊢ (φ \land x \in ℝ) \to A \in ℝ$
39	38	rexrd	$⊢ (φ \land x \in ℝ) \to A \in ℝ^{*}$
40	28	simp2d	$⊢ φ \to B \in ℝ$
41	40	adantr	$⊢ (φ \land x \in ℝ) \to B \in ℝ$
42		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
43	39 41 42	syl2anc	$⊢ (φ \land x \in ℝ) \to (A, B] \subseteq ℝ$
44	28	simp3d	$⊢ φ \to A < B$
45	29 40 44 4 5	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
46	45	ffvelrnda	$⊢ (φ \land x \in ℝ) \to E (x) \in (A, B]$
47	43 46	sseldd	$⊢ (φ \land x \in ℝ) \to E (x) \in ℝ$
48	27	adantr	$⊢ (φ \land x \in ℝ) \to Q (0) = A$
49		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (E (x) \in (A, B] \leftrightarrow (E (x) \in ℝ \land A < E (x) \land E (x) \leq B))$
50	39 41 49	syl2anc	$⊢ (φ \land x \in ℝ) \to (E (x) \in (A, B] \leftrightarrow (E (x) \in ℝ \land A < E (x) \land E (x) \leq B))$
51	46 50	mpbid	$⊢ (φ \land x \in ℝ) \to (E (x) \in ℝ \land A < E (x) \land E (x) \leq B)$
52	51	simp2d	$⊢ (φ \land x \in ℝ) \to A < E (x)$
53	48 52	eqbrtrd	$⊢ (φ \land x \in ℝ) \to Q (0) < E (x)$
54	37 47 53	ltled	$⊢ (φ \land x \in ℝ) \to Q (0) \leq E (x)$
55	54	adantr	$⊢ ((φ \land x \in ℝ) \land \neg E (x) = B) \to Q (0) \leq E (x)$
56		iffalse	$⊢ \neg E (x) = B \to if (E (x) = B, A, E (x)) = E (x)$
57	56	eqcomd	$⊢ \neg E (x) = B \to E (x) = if (E (x) = B, A, E (x))$
58	57	adantl	$⊢ ((φ \land x \in ℝ) \land \neg E (x) = B) \to E (x) = if (E (x) = B, A, E (x))$
59	55 58	breqtrd	$⊢ ((φ \land x \in ℝ) \land \neg E (x) = B) \to Q (0) \leq if (E (x) = B, A, E (x))$
60	36 59	pm2.61dan	$⊢ (φ \land x \in ℝ) \to Q (0) \leq if (E (x) = B, A, E (x))$
61	6	a1i	$⊢ (φ \land x \in ℝ) \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
62		eqeq1	$⊢ y = E (x) \to (y = B \leftrightarrow E (x) = B)$
63		id	$⊢ y = E (x) \to y = E (x)$
64	62 63	ifbieq2d	$⊢ y = E (x) \to if (y = B, A, y) = if (E (x) = B, A, E (x))$
65	64	adantl	$⊢ ((φ \land x \in ℝ) \land y = E (x)) \to if (y = B, A, y) = if (E (x) = B, A, E (x))$
66	38 47	ifcld	$⊢ (φ \land x \in ℝ) \to if (E (x) = B, A, E (x)) \in ℝ$
67	61 65 46 66	fvmptd	$⊢ (φ \land x \in ℝ) \to L (E (x)) = if (E (x) = B, A, E (x))$
68	60 67	breqtrrd	$⊢ (φ \land x \in ℝ) \to Q (0) \leq L (E (x))$
69		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
70	69	breq1d	$⊢ i = 0 \to (Q (i) \leq L (E (x)) \leftrightarrow Q (0) \leq L (E (x)))$
71	70	elrab	$⊢ 0 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \leftrightarrow (0 \in (0 ..^M) \land Q (0) \leq L (E (x)))$
72	22 68 71	sylanbrc	$⊢ (φ \land x \in ℝ) \to 0 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}$
73	72	ne0d	$⊢ (φ \land x \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \neq \emptyset$
74		fzssz	$⊢ (0 \dots M) \subseteq ℤ$
75	12 74	sstri	$⊢ (0 ..^M) \subseteq ℤ$
76		zssre	$⊢ ℤ \subseteq ℝ$
77	75 76	sstri	$⊢ (0 ..^M) \subseteq ℝ$
78	8 77	sstri	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \subseteq ℝ$
79	78	a1i	$⊢ (φ \land x \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \subseteq ℝ$
80		fisupcl	$⊢ (< Or ℝ \land (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \in Fin \land \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \neq \emptyset \land \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \subseteq ℝ)) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}$
81	10 16 73 79 80	syl13anc	$⊢ (φ \land x \in ℝ) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}$
82	8 81	sseldi	$⊢ (φ \land x \in ℝ) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in (0 ..^M)$
83	82 7	fmptd	$⊢ φ \to I : ℝ ⟶ (0 ..^M)$
84	81	ex	$⊢ φ \to (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\})$
85	83 84	jca	$⊢ φ \to (I : ℝ ⟶ (0 ..^M) \land (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}))$

Metamath Proof Explorer

Theorem fourierdlem37

Proof