fourierdlem63

Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem63.t	$⊢ T = B - A$
	fourierdlem63.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))\})$
	fourierdlem63.m	$⊢ φ \to M \in ℕ$
	fourierdlem63.q	$⊢ φ \to Q \in P (M)$
	fourierdlem63.c	$⊢ φ \to C \in ℝ$
	fourierdlem63.d	$⊢ φ \to D \in ℝ$
	fourierdlem63.cltd	$⊢ φ \to C < D$
	fourierdlem63.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))\})$
	fourierdlem63.h	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
	fourierdlem63.n	$⊢ N = \|H\| - 1$
	fourierdlem63.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem63.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem63.k	$⊢ φ \to K \in (0 \dots M)$
	fourierdlem63.j	$⊢ φ \to J \in (0 ..^N)$
	fourierdlem63.y	$⊢ φ \to Y \in [S (J), S (J + 1))$
	fourierdlem63.eyltqk	$⊢ φ \to E (Y) < Q (K)$
	fourierdlem63.x	$⊢ X = Q (K) - (E (Y) - Y)$
Assertion	fourierdlem63	$⊢ φ \to E (S (J + 1)) \leq Q (K)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem63.t	$⊢ T = B - A$
2		fourierdlem63.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		fourierdlem63.m	$⊢ φ \to M \in ℕ$
4		fourierdlem63.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem63.c	$⊢ φ \to C \in ℝ$
6		fourierdlem63.d	$⊢ φ \to D \in ℝ$
7		fourierdlem63.cltd	$⊢ φ \to C < D$
8		fourierdlem63.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		fourierdlem63.h	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
10		fourierdlem63.n	$⊢ N = \|H\| - 1$
11		fourierdlem63.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
12		fourierdlem63.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
13		fourierdlem63.k	$⊢ φ \to K \in (0 \dots M)$
14		fourierdlem63.j	$⊢ φ \to J \in (0 ..^N)$
15		fourierdlem63.y	$⊢ φ \to Y \in [S (J), S (J + 1))$
16		fourierdlem63.eyltqk	$⊢ φ \to E (Y) < Q (K)$
17		fourierdlem63.x	$⊢ X = Q (K) - (E (Y) - Y)$
18	12	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
19		id	$⊢ x = S (J + 1) \to x = S (J + 1)$
20		oveq2	$⊢ x = S (J + 1) \to B - x = B - S (J + 1)$
21	20	oveq1d	$⊢ x = S (J + 1) \to \frac{B - x}{T} = \frac{B - S (J + 1)}{T}$
22	21	fveq2d	$⊢ x = S (J + 1) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - S (J + 1)}{T}⌋$
23	22	oveq1d	$⊢ x = S (J + 1) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - S (J + 1)}{T}⌋ T$
24	19 23	oveq12d	$⊢ x = S (J + 1) \to x + ⌊\frac{B - x}{T}⌋ T = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
25	24	adantl	$⊢ (φ \land x = S (J + 1)) \to x + ⌊\frac{B - x}{T}⌋ T = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
26	1 2 3 4 5 6 7 8 9 10 11	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$
27	26	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
28	27	simprd	$⊢ φ \to S \in O (N)$
29	27	simpld	$⊢ φ \to N \in ℕ$
30	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))))$
31	29 30	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))))$
32	28 31	mpbid	$⊢ φ \to (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1)))$
33	32	simpld	$⊢ φ \to S \in (ℝ^{(0 \dots N)})$
34		elmapi	$⊢ S \in (ℝ^{(0 \dots N)}) \to S : (0 \dots N) ⟶ ℝ$
35	33 34	syl	$⊢ φ \to S : (0 \dots N) ⟶ ℝ$
36		fzofzp1	$⊢ J \in (0 ..^N) \to J + 1 \in (0 \dots N)$
37	14 36	syl	$⊢ φ \to J + 1 \in (0 \dots N)$
38	35 37	ffvelrnd	$⊢ φ \to S (J + 1) \in ℝ$
39	2 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
40	39	simp2d	$⊢ φ \to B \in ℝ$
41	40 38	resubcld	$⊢ φ \to B - S (J + 1) \in ℝ$
42	39	simp1d	$⊢ φ \to A \in ℝ$
43	40 42	resubcld	$⊢ φ \to B - A \in ℝ$
44	1 43	eqeltrid	$⊢ φ \to T \in ℝ$
45	39	simp3d	$⊢ φ \to A < B$
46	42 40	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
47	45 46	mpbid	$⊢ φ \to 0 < B - A$
48	47 1	breqtrrdi	$⊢ φ \to 0 < T$
49	48	gt0ne0d	$⊢ φ \to T \neq 0$
50	41 44 49	redivcld	$⊢ φ \to \frac{B - S (J + 1)}{T} \in ℝ$
51	50	flcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℤ$
52	51	zred	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℝ$
53	52 44	remulcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℝ$
54	38 53	readdcld	$⊢ φ \to S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℝ$
55	18 25 38 54	fvmptd	$⊢ φ \to E (S (J + 1)) = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
56	55 54	eqeltrd	$⊢ φ \to E (S (J + 1)) \in ℝ$
57	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))))$
58	3 57	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))))$
59	4 58	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)))$
60	59	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
61		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
62	60 61	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
63	62 13	ffvelrnd	$⊢ φ \to Q (K) \in ℝ$
64	5	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to C \in ℝ$
65	6	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to D \in ℝ$
66	42	rexrd	$⊢ φ \to A \in ℝ^{*}$
67		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
68	66 40 67	syl2anc	$⊢ φ \to (A, B] \subseteq ℝ$
69	42 40 45 1 12	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
70		elfzofz	$⊢ J \in (0 ..^N) \to J \in (0 \dots N)$
71	14 70	syl	$⊢ φ \to J \in (0 \dots N)$
72	35 71	ffvelrnd	$⊢ φ \to S (J) \in ℝ$
73	38	rexrd	$⊢ φ \to S (J + 1) \in ℝ^{*}$
74		elico2	$⊢ (S (J) \in ℝ \land S (J + 1) \in ℝ^{*}) \to (Y \in [S (J), S (J + 1)) \leftrightarrow (Y \in ℝ \land S (J) \leq Y \land Y < S (J + 1)))$
75	72 73 74	syl2anc	$⊢ φ \to (Y \in [S (J), S (J + 1)) \leftrightarrow (Y \in ℝ \land S (J) \leq Y \land Y < S (J + 1)))$
76	15 75	mpbid	$⊢ φ \to (Y \in ℝ \land S (J) \leq Y \land Y < S (J + 1))$
77	76	simp1d	$⊢ φ \to Y \in ℝ$
78	69 77	ffvelrnd	$⊢ φ \to E (Y) \in (A, B]$
79	68 78	sseldd	$⊢ φ \to E (Y) \in ℝ$
80	79 77	resubcld	$⊢ φ \to E (Y) - Y \in ℝ$
81	63 80	resubcld	$⊢ φ \to Q (K) - (E (Y) - Y) \in ℝ$
82	81	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) \in ℝ$
83		icossicc	$⊢ [S (J), S (J + 1)) \subseteq [S (J), S (J + 1)]$
84	5	rexrd	$⊢ φ \to C \in ℝ^{*}$
85	6	rexrd	$⊢ φ \to D \in ℝ^{*}$
86	8 29 28	fourierdlem15	$⊢ φ \to S : (0 \dots N) ⟶ [C, D]$
87	84 85 86 14	fourierdlem8	$⊢ φ \to [S (J), S (J + 1)] \subseteq [C, D]$
88	83 87	sstrid	$⊢ φ \to [S (J), S (J + 1)) \subseteq [C, D]$
89	88 15	sseldd	$⊢ φ \to Y \in [C, D]$
90		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (Y \in [C, D] \leftrightarrow (Y \in ℝ \land C \leq Y \land Y \leq D))$
91	5 6 90	syl2anc	$⊢ φ \to (Y \in [C, D] \leftrightarrow (Y \in ℝ \land C \leq Y \land Y \leq D))$
92	89 91	mpbid	$⊢ φ \to (Y \in ℝ \land C \leq Y \land Y \leq D)$
93	92	simp2d	$⊢ φ \to C \leq Y$
94	63 79	resubcld	$⊢ φ \to Q (K) - E (Y) \in ℝ$
95	79 63	posdifd	$⊢ φ \to (E (Y) < Q (K) \leftrightarrow 0 < Q (K) - E (Y))$
96	16 95	mpbid	$⊢ φ \to 0 < Q (K) - E (Y)$
97	94 96	elrpd	$⊢ φ \to Q (K) - E (Y) \in ℝ^{+}$
98	77 97	ltaddrpd	$⊢ φ \to Y < Y + Q (K) - E (Y)$
99	63	recnd	$⊢ φ \to Q (K) \in ℂ$
100	79	recnd	$⊢ φ \to E (Y) \in ℂ$
101	77	recnd	$⊢ φ \to Y \in ℂ$
102	99 100 101	subsub3d	$⊢ φ \to Q (K) - (E (Y) - Y) = Q (K) + Y - E (Y)$
103	99 101	addcomd	$⊢ φ \to Q (K) + Y = Y + Q (K)$
104	103	oveq1d	$⊢ φ \to Q (K) + Y - E (Y) = Y + Q (K) - E (Y)$
105	101 99 100	addsubassd	$⊢ φ \to Y + Q (K) - E (Y) = Y + Q (K) - E (Y)$
106	102 104 105	3eqtrrd	$⊢ φ \to Y + Q (K) - E (Y) = Q (K) - (E (Y) - Y)$
107	98 106	breqtrd	$⊢ φ \to Y < Q (K) - (E (Y) - Y)$
108	5 77 81 93 107	lelttrd	$⊢ φ \to C < Q (K) - (E (Y) - Y)$
109	5 81 108	ltled	$⊢ φ \to C \leq Q (K) - (E (Y) - Y)$
110	109	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to C \leq Q (K) - (E (Y) - Y)$
111	38	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to S (J + 1) \in ℝ$
112	63	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) \in ℝ$
113	56 38	resubcld	$⊢ φ \to E (S (J + 1)) - S (J + 1) \in ℝ$
114	113	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to E (S (J + 1)) - S (J + 1) \in ℝ$
115	112 114	resubcld	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (S (J + 1)) - S (J + 1)) \in ℝ$
116	76	simp3d	$⊢ φ \to Y < S (J + 1)$
117	77 38 116	ltled	$⊢ φ \to Y \leq S (J + 1)$
118	42 40 45 1 12 77 38 117	fourierdlem7	$⊢ φ \to E (S (J + 1)) - S (J + 1) \leq E (Y) - Y$
119	113 80 63 118	lesub2dd	$⊢ φ \to Q (K) - (E (Y) - Y) \leq Q (K) - (E (S (J + 1)) - S (J + 1))$
120	119	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) \leq Q (K) - (E (S (J + 1)) - S (J + 1))$
121	99	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) \in ℂ$
122	56	recnd	$⊢ φ \to E (S (J + 1)) \in ℂ$
123	122	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to E (S (J + 1)) \in ℂ$
124	111	recnd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to S (J + 1) \in ℂ$
125	121 123 124	subsubd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (S (J + 1)) - S (J + 1)) = Q (K) - E (S (J + 1)) + S (J + 1)$
126	99 122	subcld	$⊢ φ \to Q (K) - E (S (J + 1)) \in ℂ$
127	38	recnd	$⊢ φ \to S (J + 1) \in ℂ$
128	126 127	addcomd	$⊢ φ \to Q (K) - E (S (J + 1)) + S (J + 1) = S (J + 1) + Q (K) - E (S (J + 1))$
129	128	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - E (S (J + 1)) + S (J + 1) = S (J + 1) + Q (K) - E (S (J + 1))$
130	125 129	eqtrd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (S (J + 1)) - S (J + 1)) = S (J + 1) + Q (K) - E (S (J + 1))$
131		simpr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) < E (S (J + 1))$
132	56	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to E (S (J + 1)) \in ℝ$
133	112 132	sublt0d	$⊢ (φ \land Q (K) < E (S (J + 1))) \to (Q (K) - E (S (J + 1)) < 0 \leftrightarrow Q (K) < E (S (J + 1)))$
134	131 133	mpbird	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - E (S (J + 1)) < 0$
135	112 132	resubcld	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - E (S (J + 1)) \in ℝ$
136		ltaddneg	$⊢ (Q (K) - E (S (J + 1)) \in ℝ \land S (J + 1) \in ℝ) \to (Q (K) - E (S (J + 1)) < 0 \leftrightarrow S (J + 1) + Q (K) - E (S (J + 1)) < S (J + 1))$
137	135 111 136	syl2anc	$⊢ (φ \land Q (K) < E (S (J + 1))) \to (Q (K) - E (S (J + 1)) < 0 \leftrightarrow S (J + 1) + Q (K) - E (S (J + 1)) < S (J + 1))$
138	134 137	mpbid	$⊢ (φ \land Q (K) < E (S (J + 1))) \to S (J + 1) + Q (K) - E (S (J + 1)) < S (J + 1)$
139	130 138	eqbrtrd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (S (J + 1)) - S (J + 1)) < S (J + 1)$
140	82 115 111 120 139	lelttrd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) < S (J + 1)$
141	86 37	ffvelrnd	$⊢ φ \to S (J + 1) \in [C, D]$
142		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (S (J + 1) \in [C, D] \leftrightarrow (S (J + 1) \in ℝ \land C \leq S (J + 1) \land S (J + 1) \leq D))$
143	5 6 142	syl2anc	$⊢ φ \to (S (J + 1) \in [C, D] \leftrightarrow (S (J + 1) \in ℝ \land C \leq S (J + 1) \land S (J + 1) \leq D))$
144	141 143	mpbid	$⊢ φ \to (S (J + 1) \in ℝ \land C \leq S (J + 1) \land S (J + 1) \leq D)$
145	144	simp3d	$⊢ φ \to S (J + 1) \leq D$
146	145	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to S (J + 1) \leq D$
147	82 111 65 140 146	ltletrd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) < D$
148	82 65 147	ltled	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) \leq D$
149	64 65 82 110 148	eliccd	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) \in [C, D]$
150		id	$⊢ x = Y \to x = Y$
151		oveq2	$⊢ x = Y \to B - x = B - Y$
152	151	oveq1d	$⊢ x = Y \to \frac{B - x}{T} = \frac{B - Y}{T}$
153	152	fveq2d	$⊢ x = Y \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - Y}{T}⌋$
154	153	oveq1d	$⊢ x = Y \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - Y}{T}⌋ T$
155	150 154	oveq12d	$⊢ x = Y \to x + ⌊\frac{B - x}{T}⌋ T = Y + ⌊\frac{B - Y}{T}⌋ T$
156	155	adantl	$⊢ (φ \land x = Y) \to x + ⌊\frac{B - x}{T}⌋ T = Y + ⌊\frac{B - Y}{T}⌋ T$
157	40 77	resubcld	$⊢ φ \to B - Y \in ℝ$
158	157 44 49	redivcld	$⊢ φ \to \frac{B - Y}{T} \in ℝ$
159	158	flcld	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ \in ℤ$
160	159	zred	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ \in ℝ$
161	160 44	remulcld	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ T \in ℝ$
162	77 161	readdcld	$⊢ φ \to Y + ⌊\frac{B - Y}{T}⌋ T \in ℝ$
163	18 156 77 162	fvmptd	$⊢ φ \to E (Y) = Y + ⌊\frac{B - Y}{T}⌋ T$
164	163	oveq1d	$⊢ φ \to E (Y) - Y = Y + ⌊\frac{B - Y}{T}⌋ T - Y$
165	164	oveq1d	$⊢ φ \to \frac{E (Y) - Y}{T} = \frac{Y + ⌊\frac{B - Y}{T}⌋ T - Y}{T}$
166	161	recnd	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ T \in ℂ$
167	101 166	pncan2d	$⊢ φ \to Y + ⌊\frac{B - Y}{T}⌋ T - Y = ⌊\frac{B - Y}{T}⌋ T$
168	167	oveq1d	$⊢ φ \to \frac{Y + ⌊\frac{B - Y}{T}⌋ T - Y}{T} = \frac{⌊\frac{B - Y}{T}⌋ T}{T}$
169	160	recnd	$⊢ φ \to ⌊\frac{B - Y}{T}⌋ \in ℂ$
170	44	recnd	$⊢ φ \to T \in ℂ$
171	169 170 49	divcan4d	$⊢ φ \to \frac{⌊\frac{B - Y}{T}⌋ T}{T} = ⌊\frac{B - Y}{T}⌋$
172	165 168 171	3eqtrd	$⊢ φ \to \frac{E (Y) - Y}{T} = ⌊\frac{B - Y}{T}⌋$
173	172 159	eqeltrd	$⊢ φ \to \frac{E (Y) - Y}{T} \in ℤ$
174	80	recnd	$⊢ φ \to E (Y) - Y \in ℂ$
175	174 170 49	divcan1d	$⊢ φ \to (\frac{E (Y) - Y}{T}) T = E (Y) - Y$
176	175	oveq2d	$⊢ φ \to Q (K) - (E (Y) - Y) + (\frac{E (Y) - Y}{T}) T = (Q (K) - (E (Y) - Y)) + E (Y) - Y$
177	99 174	npcand	$⊢ φ \to (Q (K) - (E (Y) - Y)) + E (Y) - Y = Q (K)$
178	176 177	eqtrd	$⊢ φ \to Q (K) - (E (Y) - Y) + (\frac{E (Y) - Y}{T}) T = Q (K)$
179		ffun	$⊢ Q : (0 \dots M) ⟶ ℝ \to Fun Q$
180	62 179	syl	$⊢ φ \to Fun Q$
181	62	fdmd	$⊢ φ \to dom Q = (0 \dots M)$
182	13 181	eleqtrrd	$⊢ φ \to K \in dom Q$
183		fvelrn	$⊢ (Fun Q \land K \in dom Q) \to Q (K) \in ran Q$
184	180 182 183	syl2anc	$⊢ φ \to Q (K) \in ran Q$
185	178 184	eqeltrd	$⊢ φ \to Q (K) - (E (Y) - Y) + (\frac{E (Y) - Y}{T}) T \in ran Q$
186		oveq1	$⊢ k = \frac{E (Y) - Y}{T} \to k T = (\frac{E (Y) - Y}{T}) T$
187	186	oveq2d	$⊢ k = \frac{E (Y) - Y}{T} \to Q (K) - (E (Y) - Y) + k T = Q (K) - (E (Y) - Y) + (\frac{E (Y) - Y}{T}) T$
188	187	eleq1d	$⊢ k = \frac{E (Y) - Y}{T} \to (Q (K) - (E (Y) - Y) + k T \in ran Q \leftrightarrow Q (K) - (E (Y) - Y) + (\frac{E (Y) - Y}{T}) T \in ran Q)$
189	188	rspcev	$⊢ (\frac{E (Y) - Y}{T} \in ℤ \land Q (K) - (E (Y) - Y) + (\frac{E (Y) - Y}{T}) T \in ran Q) \to \exists k \in ℤ Q (K) - (E (Y) - Y) + k T \in ran Q$
190	173 185 189	syl2anc	$⊢ φ \to \exists k \in ℤ Q (K) - (E (Y) - Y) + k T \in ran Q$
191	190	adantr	$⊢ (φ \land Q (K) < E (S (J + 1))) \to \exists k \in ℤ Q (K) - (E (Y) - Y) + k T \in ran Q$
192		oveq1	$⊢ x = Q (K) - (E (Y) - Y) \to x + k T = Q (K) - (E (Y) - Y) + k T$
193	192	eleq1d	$⊢ x = Q (K) - (E (Y) - Y) \to (x + k T \in ran Q \leftrightarrow Q (K) - (E (Y) - Y) + k T \in ran Q)$
194	193	rexbidv	$⊢ x = Q (K) - (E (Y) - Y) \to (\exists k \in ℤ x + k T \in ran Q \leftrightarrow \exists k \in ℤ Q (K) - (E (Y) - Y) + k T \in ran Q)$
195	194	elrab	$⊢ Q (K) - (E (Y) - Y) \in \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \leftrightarrow (Q (K) - (E (Y) - Y) \in [C, D] \land \exists k \in ℤ Q (K) - (E (Y) - Y) + k T \in ran Q)$
196	149 191 195	sylanbrc	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) \in \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
197		elun2	$⊢ Q (K) - (E (Y) - Y) \in \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\} \to Q (K) - (E (Y) - Y) \in (\{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\})$
198	196 197	syl	$⊢ (φ \land Q (K) < E (S (J + 1))) \to Q (K) - (E (Y) - Y) \in (\{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\})$
199	198 17 9	3eltr4g	$⊢ (φ \land Q (K) < E (S (J + 1))) \to X \in H$
200		elfzelz	$⊢ j \in (0 \dots N) \to j \in ℤ$
201	200	ad2antlr	$⊢ ((φ \land j \in (0 \dots N)) \land (S (J) < S (j) \land S (j) < S (J + 1))) \to j \in ℤ$
202		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
203	14 202	syl	$⊢ φ \to J \in ℤ$
204	203	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land (S (J) < S (j) \land S (j) < S (J + 1))) \to J \in ℤ$
205		simpr	$⊢ ((φ \land j \in (0 \dots N)) \land S (J) < S (j)) \to S (J) < S (j)$
206	26	simprd	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), H)$
207	206	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (J) < S (j)) \to S {Isom}_{<, <} ((0 \dots N), H)$
208	71	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (J) < S (j)) \to J \in (0 \dots N)$
209		simplr	$⊢ ((φ \land j \in (0 \dots N)) \land S (J) < S (j)) \to j \in (0 \dots N)$
210		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), H) \land (J \in (0 \dots N) \land j \in (0 \dots N))) \to (J < j \leftrightarrow S (J) < S (j))$
211	207 208 209 210	syl12anc	$⊢ ((φ \land j \in (0 \dots N)) \land S (J) < S (j)) \to (J < j \leftrightarrow S (J) < S (j))$
212	205 211	mpbird	$⊢ ((φ \land j \in (0 \dots N)) \land S (J) < S (j)) \to J < j$
213	212	adantrr	$⊢ ((φ \land j \in (0 \dots N)) \land (S (J) < S (j) \land S (j) < S (J + 1))) \to J < j$
214		simpr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) < S (J + 1)) \to S (j) < S (J + 1)$
215	206	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) < S (J + 1)) \to S {Isom}_{<, <} ((0 \dots N), H)$
216		simplr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) < S (J + 1)) \to j \in (0 \dots N)$
217	37	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) < S (J + 1)) \to J + 1 \in (0 \dots N)$
218		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), H) \land (j \in (0 \dots N) \land J + 1 \in (0 \dots N))) \to (j < J + 1 \leftrightarrow S (j) < S (J + 1))$
219	215 216 217 218	syl12anc	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) < S (J + 1)) \to (j < J + 1 \leftrightarrow S (j) < S (J + 1))$
220	214 219	mpbird	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) < S (J + 1)) \to j < J + 1$
221	220	adantrl	$⊢ ((φ \land j \in (0 \dots N)) \land (S (J) < S (j) \land S (j) < S (J + 1))) \to j < J + 1$
222		btwnnz	$⊢ (J \in ℤ \land J < j \land j < J + 1) \to \neg j \in ℤ$
223	204 213 221 222	syl3anc	$⊢ ((φ \land j \in (0 \dots N)) \land (S (J) < S (j) \land S (j) < S (J + 1))) \to \neg j \in ℤ$
224	201 223	pm2.65da	$⊢ (φ \land j \in (0 \dots N)) \to \neg (S (J) < S (j) \land S (j) < S (J + 1))$
225	224	adantlr	$⊢ ((φ \land Q (K) < E (S (J + 1))) \land j \in (0 \dots N)) \to \neg (S (J) < S (j) \land S (j) < S (J + 1))$
226	72	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) = X) \to S (J) \in ℝ$
227	77	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) = X) \to Y \in ℝ$
228	35	ffvelrnda	$⊢ (φ \land j \in (0 \dots N)) \to S (j) \in ℝ$
229	228	adantr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) = X) \to S (j) \in ℝ$
230	76	simp2d	$⊢ φ \to S (J) \leq Y$
231	230	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) = X) \to S (J) \leq Y$
232	107 17	breqtrrdi	$⊢ φ \to Y < X$
233	232	adantr	$⊢ (φ \land S (j) = X) \to Y < X$
234		eqcom	$⊢ X = S (j) \leftrightarrow S (j) = X$
235	234	biimpri	$⊢ S (j) = X \to X = S (j)$
236	235	adantl	$⊢ (φ \land S (j) = X) \to X = S (j)$
237	233 236	breqtrd	$⊢ (φ \land S (j) = X) \to Y < S (j)$
238	237	adantlr	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) = X) \to Y < S (j)$
239	226 227 229 231 238	lelttrd	$⊢ ((φ \land j \in (0 \dots N)) \land S (j) = X) \to S (J) < S (j)$
240	239	adantllr	$⊢ (((φ \land Q (K) < E (S (J + 1))) \land j \in (0 \dots N)) \land S (j) = X) \to S (J) < S (j)$
241		simpr	$⊢ ((φ \land Q (K) < E (S (J + 1))) \land S (j) = X) \to S (j) = X$
242	17 140	eqbrtrid	$⊢ (φ \land Q (K) < E (S (J + 1))) \to X < S (J + 1)$
243	242	adantr	$⊢ ((φ \land Q (K) < E (S (J + 1))) \land S (j) = X) \to X < S (J + 1)$
244	241 243	eqbrtrd	$⊢ ((φ \land Q (K) < E (S (J + 1))) \land S (j) = X) \to S (j) < S (J + 1)$
245	244	adantlr	$⊢ (((φ \land Q (K) < E (S (J + 1))) \land j \in (0 \dots N)) \land S (j) = X) \to S (j) < S (J + 1)$
246	240 245	jca	$⊢ (((φ \land Q (K) < E (S (J + 1))) \land j \in (0 \dots N)) \land S (j) = X) \to (S (J) < S (j) \land S (j) < S (J + 1))$
247	225 246	mtand	$⊢ ((φ \land Q (K) < E (S (J + 1))) \land j \in (0 \dots N)) \to \neg S (j) = X$
248	247	nrexdv	$⊢ (φ \land Q (K) < E (S (J + 1))) \to \neg \exists j \in (0 \dots N) S (j) = X$
249		isof1o	$⊢ S {Isom}_{<, <} ((0 \dots N), H) \to S : (0 \dots N) \underset{1-1 onto}{⟶} H$
250	206 249	syl	$⊢ φ \to S : (0 \dots N) \underset{1-1 onto}{⟶} H$
251		f1ofo	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} H \to S : (0 \dots N) \underset{onto}{⟶} H$
252	250 251	syl	$⊢ φ \to S : (0 \dots N) \underset{onto}{⟶} H$
253		foelrn	$⊢ (S : (0 \dots N) \underset{onto}{⟶} H \land X \in H) \to \exists j \in (0 \dots N) X = S (j)$
254	252 253	sylan	$⊢ (φ \land X \in H) \to \exists j \in (0 \dots N) X = S (j)$
255	234	rexbii	$⊢ \exists j \in (0 \dots N) X = S (j) \leftrightarrow \exists j \in (0 \dots N) S (j) = X$
256	254 255	sylib	$⊢ (φ \land X \in H) \to \exists j \in (0 \dots N) S (j) = X$
257	256	adantlr	$⊢ ((φ \land Q (K) < E (S (J + 1))) \land X \in H) \to \exists j \in (0 \dots N) S (j) = X$
258	248 257	mtand	$⊢ (φ \land Q (K) < E (S (J + 1))) \to \neg X \in H$
259	199 258	pm2.65da	$⊢ φ \to \neg Q (K) < E (S (J + 1))$
260	56 63 259	nltled	$⊢ φ \to E (S (J + 1)) \leq Q (K)$

Metamath Proof Explorer

Theorem fourierdlem63

Proof