fourierdlem64

Description: The partition V is finer than Q , when Q is moved on the same interval where V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem64.t	$⊢ T = B - A$
	fourierdlem64.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))\})$
	fourierdlem64.m	$⊢ φ \to M \in ℕ$
	fourierdlem64.q	$⊢ φ \to Q \in P (M)$
	fourierdlem64.c	$⊢ φ \to C \in ℝ$
	fourierdlem64.d	$⊢ φ \to D \in ℝ$
	fourierdlem64.cltd	$⊢ φ \to C < D$
	fourierdlem64.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
	fourierdlem64.n	$⊢ N = \|H\| - 1$
	fourierdlem64.v	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem64.j	$⊢ φ \to J \in (0 ..^N)$
	fourierdlem64.l	$⊢ L = sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <)$
	fourierdlem64.i	$⊢ I = sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <)$
Assertion	fourierdlem64	$⊢ φ \to ((I \in (0 ..^M) \land L \in ℤ) \land \exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem64.t	$⊢ T = B - A$
2		fourierdlem64.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		fourierdlem64.m	$⊢ φ \to M \in ℕ$
4		fourierdlem64.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem64.c	$⊢ φ \to C \in ℝ$
6		fourierdlem64.d	$⊢ φ \to D \in ℝ$
7		fourierdlem64.cltd	$⊢ φ \to C < D$
8		fourierdlem64.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
9		fourierdlem64.n	$⊢ N = \|H\| - 1$
10		fourierdlem64.v	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
11		fourierdlem64.j	$⊢ φ \to J \in (0 ..^N)$
12		fourierdlem64.l	$⊢ L = sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <)$
13		fourierdlem64.i	$⊢ I = sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <)$
14		ssrab2	$⊢ \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq (0 ..^M)$
15		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
16		fzssz	$⊢ (0 \dots M) \subseteq ℤ$
17	15 16	sstri	$⊢ (0 ..^M) \subseteq ℤ$
18	14 17	sstri	$⊢ \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq ℤ$
19	18	a1i	$⊢ φ \to \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq ℤ$
20		0zd	$⊢ φ \to 0 \in ℤ$
21	3	nnzd	$⊢ φ \to M \in ℤ$
22	3	nngt0d	$⊢ φ \to 0 < M$
23		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
24	20 21 22 23	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
25		ssrab2	$⊢ \{k \in ℤ \| Q (0) + k T \leq V (J)\} \subseteq ℤ$
26	25	a1i	$⊢ φ \to \{k \in ℤ \| Q (0) + k T \leq V (J)\} \subseteq ℤ$
27		prssi	$⊢ (C \in ℝ \land D \in ℝ) \to \{C, D\} \subseteq ℝ$
28	5 6 27	syl2anc	$⊢ φ \to \{C, D\} \subseteq ℝ$
29		ssrab2	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \subseteq [C, D]$
30	29	a1i	$⊢ φ \to \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \subseteq [C, D]$
31	5 6	iccssred	$⊢ φ \to [C, D] \subseteq ℝ$
32	30 31	sstrd	$⊢ φ \to \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \subseteq ℝ$
33	28 32	unssd	$⊢ φ \to \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \subseteq ℝ$
34	8 33	eqsstrid	$⊢ φ \to H \subseteq ℝ$
35		eqid	$⊢ (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))\}) = (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))\})$
36	1 2 3 4 5 6 7 35 8 9 10	fourierdlem54	$⊢ φ \to ((N \in ℕ \land V \in (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))\}) (N)) \land V {Isom}_{<, <} ((0 \dots N), H))$
37	36	simprd	$⊢ φ \to V {Isom}_{<, <} ((0 \dots N), H)$
38		isof1o	$⊢ V {Isom}_{<, <} ((0 \dots N), H) \to V : (0 \dots N) \underset{1-1 onto}{⟶} H$
39		f1of	$⊢ V : (0 \dots N) \underset{1-1 onto}{⟶} H \to V : (0 \dots N) ⟶ H$
40	37 38 39	3syl	$⊢ φ \to V : (0 \dots N) ⟶ H$
41		elfzofz	$⊢ J \in (0 ..^N) \to J \in (0 \dots N)$
42	11 41	syl	$⊢ φ \to J \in (0 \dots N)$
43	40 42	ffvelrnd	$⊢ φ \to V (J) \in H$
44	34 43	sseldd	$⊢ φ \to V (J) \in ℝ$
45	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))))$
46	3 45	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))))$
47	4 46	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)))$
48	47	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
49		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
50	48 49	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
51	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
52		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
53	51 52	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
54		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
55	53 54	syl	$⊢ φ \to 0 \in (0 \dots M)$
56	50 55	ffvelrnd	$⊢ φ \to Q (0) \in ℝ$
57	44 56	resubcld	$⊢ φ \to V (J) - Q (0) \in ℝ$
58	2 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
59	58	simp2d	$⊢ φ \to B \in ℝ$
60	58	simp1d	$⊢ φ \to A \in ℝ$
61	59 60	resubcld	$⊢ φ \to B - A \in ℝ$
62	1 61	eqeltrid	$⊢ φ \to T \in ℝ$
63	58	simp3d	$⊢ φ \to A < B$
64	60 59	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
65	63 64	mpbid	$⊢ φ \to 0 < B - A$
66	65 1	breqtrrdi	$⊢ φ \to 0 < T$
67	66	gt0ne0d	$⊢ φ \to T \neq 0$
68	57 62 67	redivcld	$⊢ φ \to \frac{V (J) - Q (0)}{T} \in ℝ$
69		btwnz	$⊢ \frac{V (J) - Q (0)}{T} \in ℝ \to (\exists k \in ℤ k < \frac{V (J) - Q (0)}{T} \land \exists z \in ℤ \frac{V (J) - Q (0)}{T} < z)$
70	68 69	syl	$⊢ φ \to (\exists k \in ℤ k < \frac{V (J) - Q (0)}{T} \land \exists z \in ℤ \frac{V (J) - Q (0)}{T} < z)$
71	70	simpld	$⊢ φ \to \exists k \in ℤ k < \frac{V (J) - Q (0)}{T}$
72		zre	$⊢ k \in ℤ \to k \in ℝ$
73	56	ad2antrr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to Q (0) \in ℝ$
74		simplr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to k \in ℝ$
75	62	ad2antrr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to T \in ℝ$
76	74 75	remulcld	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to k T \in ℝ$
77	73 76	readdcld	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to Q (0) + k T \in ℝ$
78	44	ad2antrr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to V (J) \in ℝ$
79		simpr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to k < \frac{V (J) - Q (0)}{T}$
80	57	ad2antrr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to V (J) - Q (0) \in ℝ$
81	62 66	elrpd	$⊢ φ \to T \in ℝ^{+}$
82	81	ad2antrr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to T \in ℝ^{+}$
83	74 80 82	ltmuldivd	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to (k T < V (J) - Q (0) \leftrightarrow k < \frac{V (J) - Q (0)}{T})$
84	79 83	mpbird	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to k T < V (J) - Q (0)$
85	56	adantr	$⊢ (φ \land k \in ℝ) \to Q (0) \in ℝ$
86		simpr	$⊢ (φ \land k \in ℝ) \to k \in ℝ$
87	62	adantr	$⊢ (φ \land k \in ℝ) \to T \in ℝ$
88	86 87	remulcld	$⊢ (φ \land k \in ℝ) \to k T \in ℝ$
89	44	adantr	$⊢ (φ \land k \in ℝ) \to V (J) \in ℝ$
90	85 88 89	ltaddsub2d	$⊢ (φ \land k \in ℝ) \to (Q (0) + k T < V (J) \leftrightarrow k T < V (J) - Q (0))$
91	90	adantr	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to (Q (0) + k T < V (J) \leftrightarrow k T < V (J) - Q (0))$
92	84 91	mpbird	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to Q (0) + k T < V (J)$
93	77 78 92	ltled	$⊢ ((φ \land k \in ℝ) \land k < \frac{V (J) - Q (0)}{T}) \to Q (0) + k T \leq V (J)$
94	93	ex	$⊢ (φ \land k \in ℝ) \to (k < \frac{V (J) - Q (0)}{T} \to Q (0) + k T \leq V (J))$
95	72 94	sylan2	$⊢ (φ \land k \in ℤ) \to (k < \frac{V (J) - Q (0)}{T} \to Q (0) + k T \leq V (J))$
96	95	reximdva	$⊢ φ \to (\exists k \in ℤ k < \frac{V (J) - Q (0)}{T} \to \exists k \in ℤ Q (0) + k T \leq V (J))$
97	71 96	mpd	$⊢ φ \to \exists k \in ℤ Q (0) + k T \leq V (J)$
98		rabn0	$⊢ \{k \in ℤ \| Q (0) + k T \leq V (J)\} \neq \emptyset \leftrightarrow \exists k \in ℤ Q (0) + k T \leq V (J)$
99	97 98	sylibr	$⊢ φ \to \{k \in ℤ \| Q (0) + k T \leq V (J)\} \neq \emptyset$
100		simpl	$⊢ (φ \land j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}) \to φ$
101	26	sselda	$⊢ (φ \land j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}) \to j \in ℤ$
102		oveq1	$⊢ k = j \to k T = j T$
103	102	oveq2d	$⊢ k = j \to Q (0) + k T = Q (0) + j T$
104	103	breq1d	$⊢ k = j \to (Q (0) + k T \leq V (J) \leftrightarrow Q (0) + j T \leq V (J))$
105	104	elrab	$⊢ j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} \leftrightarrow (j \in ℤ \land Q (0) + j T \leq V (J))$
106	105	simprbi	$⊢ j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} \to Q (0) + j T \leq V (J)$
107	106	adantl	$⊢ (φ \land j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}) \to Q (0) + j T \leq V (J)$
108		zre	$⊢ j \in ℤ \to j \in ℝ$
109		simpr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to Q (0) + j T \leq V (J)$
110	56	ad2antrr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to Q (0) \in ℝ$
111		simpr	$⊢ (φ \land j \in ℝ) \to j \in ℝ$
112	62	adantr	$⊢ (φ \land j \in ℝ) \to T \in ℝ$
113	111 112	remulcld	$⊢ (φ \land j \in ℝ) \to j T \in ℝ$
114	113	adantr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to j T \in ℝ$
115	44	ad2antrr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to V (J) \in ℝ$
116	110 114 115	leaddsub2d	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to (Q (0) + j T \leq V (J) \leftrightarrow j T \leq V (J) - Q (0))$
117	109 116	mpbid	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to j T \leq V (J) - Q (0)$
118		simplr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to j \in ℝ$
119	57	ad2antrr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to V (J) - Q (0) \in ℝ$
120	81	ad2antrr	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to T \in ℝ^{+}$
121	118 119 120	lemuldivd	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to (j T \leq V (J) - Q (0) \leftrightarrow j \leq \frac{V (J) - Q (0)}{T})$
122	117 121	mpbid	$⊢ ((φ \land j \in ℝ) \land Q (0) + j T \leq V (J)) \to j \leq \frac{V (J) - Q (0)}{T}$
123	108 122	sylanl2	$⊢ ((φ \land j \in ℤ) \land Q (0) + j T \leq V (J)) \to j \leq \frac{V (J) - Q (0)}{T}$
124	100 101 107 123	syl21anc	$⊢ (φ \land j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}) \to j \leq \frac{V (J) - Q (0)}{T}$
125	124	ralrimiva	$⊢ φ \to \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq \frac{V (J) - Q (0)}{T}$
126		breq2	$⊢ b = \frac{V (J) - Q (0)}{T} \to (j \leq b \leftrightarrow j \leq \frac{V (J) - Q (0)}{T})$
127	126	ralbidv	$⊢ b = \frac{V (J) - Q (0)}{T} \to (\forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq b \leftrightarrow \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq \frac{V (J) - Q (0)}{T})$
128	127	rspcev	$⊢ (\frac{V (J) - Q (0)}{T} \in ℝ \land \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq \frac{V (J) - Q (0)}{T}) \to \exists b \in ℝ \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq b$
129	68 125 128	syl2anc	$⊢ φ \to \exists b \in ℝ \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq b$
130		suprzcl	$⊢ (\{k \in ℤ \| Q (0) + k T \leq V (J)\} \subseteq ℤ \land \{k \in ℤ \| Q (0) + k T \leq V (J)\} \neq \emptyset \land \exists b \in ℝ \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq b) \to sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}$
131	26 99 129 130	syl3anc	$⊢ φ \to sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}$
132	12 131	eqeltrid	$⊢ φ \to L \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}$
133		oveq1	$⊢ k = L \to k T = L T$
134	133	oveq2d	$⊢ k = L \to Q (0) + k T = Q (0) + L T$
135	134	breq1d	$⊢ k = L \to (Q (0) + k T \leq V (J) \leftrightarrow Q (0) + L T \leq V (J))$
136	135	elrab	$⊢ L \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} \leftrightarrow (L \in ℤ \land Q (0) + L T \leq V (J))$
137	132 136	sylib	$⊢ φ \to (L \in ℤ \land Q (0) + L T \leq V (J))$
138	137	simprd	$⊢ φ \to Q (0) + L T \leq V (J)$
139		fveq2	$⊢ j = 0 \to Q (j) = Q (0)$
140	139	oveq1d	$⊢ j = 0 \to Q (j) + L T = Q (0) + L T$
141	140	breq1d	$⊢ j = 0 \to (Q (j) + L T \leq V (J) \leftrightarrow Q (0) + L T \leq V (J))$
142	141	elrab	$⊢ 0 \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \leftrightarrow (0 \in (0 ..^M) \land Q (0) + L T \leq V (J))$
143	24 138 142	sylanbrc	$⊢ φ \to 0 \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}$
144		ne0i	$⊢ 0 \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \to \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \neq \emptyset$
145	143 144	syl	$⊢ φ \to \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \neq \emptyset$
146	3	nnred	$⊢ φ \to M \in ℝ$
147	14	a1i	$⊢ φ \to \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq (0 ..^M)$
148	147	sselda	$⊢ (φ \land k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}) \to k \in (0 ..^M)$
149		elfzoelz	$⊢ k \in (0 ..^M) \to k \in ℤ$
150	149	zred	$⊢ k \in (0 ..^M) \to k \in ℝ$
151	150	adantl	$⊢ (φ \land k \in (0 ..^M)) \to k \in ℝ$
152	146	adantr	$⊢ (φ \land k \in (0 ..^M)) \to M \in ℝ$
153		elfzolt2	$⊢ k \in (0 ..^M) \to k < M$
154	153	adantl	$⊢ (φ \land k \in (0 ..^M)) \to k < M$
155	151 152 154	ltled	$⊢ (φ \land k \in (0 ..^M)) \to k \leq M$
156	148 155	syldan	$⊢ (φ \land k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}) \to k \leq M$
157	156	ralrimiva	$⊢ φ \to \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq M$
158		breq2	$⊢ b = M \to (k \leq b \leftrightarrow k \leq M)$
159	158	ralbidv	$⊢ b = M \to (\forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq b \leftrightarrow \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq M)$
160	159	rspcev	$⊢ (M \in ℝ \land \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq M) \to \exists b \in ℝ \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq b$
161	146 157 160	syl2anc	$⊢ φ \to \exists b \in ℝ \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq b$
162		suprzcl	$⊢ (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq ℤ \land \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \neq \emptyset \land \exists b \in ℝ \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq b) \to sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <) \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}$
163	19 145 161 162	syl3anc	$⊢ φ \to sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <) \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}$
164	14 163	sseldi	$⊢ φ \to sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <) \in (0 ..^M)$
165	13 164	eqeltrid	$⊢ φ \to I \in (0 ..^M)$
166	25 131	sseldi	$⊢ φ \to sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <) \in ℤ$
167	12 166	eqeltrid	$⊢ φ \to L \in ℤ$
168	15 165	sseldi	$⊢ φ \to I \in (0 \dots M)$
169	50 168	ffvelrnd	$⊢ φ \to Q (I) \in ℝ$
170	167	zred	$⊢ φ \to L \in ℝ$
171	170 62	remulcld	$⊢ φ \to L T \in ℝ$
172	169 171	readdcld	$⊢ φ \to Q (I) + L T \in ℝ$
173	172	rexrd	$⊢ φ \to Q (I) + L T \in ℝ^{*}$
174	173	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to Q (I) + L T \in ℝ^{*}$
175		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
176	165 175	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
177	50 176	ffvelrnd	$⊢ φ \to Q (I + 1) \in ℝ$
178	177 171	readdcld	$⊢ φ \to Q (I + 1) + L T \in ℝ$
179	178	rexrd	$⊢ φ \to Q (I + 1) + L T \in ℝ^{*}$
180	179	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to Q (I + 1) + L T \in ℝ^{*}$
181		elioore	$⊢ x \in (V (J), V (J + 1)) \to x \in ℝ$
182	181	adantl	$⊢ (φ \land x \in (V (J), V (J + 1))) \to x \in ℝ$
183	172	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to Q (I) + L T \in ℝ$
184	44	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to V (J) \in ℝ$
185	13 163	eqeltrid	$⊢ φ \to I \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}$
186		fveq2	$⊢ j = I \to Q (j) = Q (I)$
187	186	oveq1d	$⊢ j = I \to Q (j) + L T = Q (I) + L T$
188	187	breq1d	$⊢ j = I \to (Q (j) + L T \leq V (J) \leftrightarrow Q (I) + L T \leq V (J))$
189	188	elrab	$⊢ I \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \leftrightarrow (I \in (0 ..^M) \land Q (I) + L T \leq V (J))$
190	185 189	sylib	$⊢ φ \to (I \in (0 ..^M) \land Q (I) + L T \leq V (J))$
191	190	simprd	$⊢ φ \to Q (I) + L T \leq V (J)$
192	191	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to Q (I) + L T \leq V (J)$
193	184	rexrd	$⊢ (φ \land x \in (V (J), V (J + 1))) \to V (J) \in ℝ^{*}$
194		fzofzp1	$⊢ J \in (0 ..^N) \to J + 1 \in (0 \dots N)$
195	11 194	syl	$⊢ φ \to J + 1 \in (0 \dots N)$
196	40 195	ffvelrnd	$⊢ φ \to V (J + 1) \in H$
197	34 196	sseldd	$⊢ φ \to V (J + 1) \in ℝ$
198	197	rexrd	$⊢ φ \to V (J + 1) \in ℝ^{*}$
199	198	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to V (J + 1) \in ℝ^{*}$
200		simpr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to x \in (V (J), V (J + 1))$
201		ioogtlb	$⊢ (V (J) \in ℝ^{} \land V (J + 1) \in ℝ^{} \land x \in (V (J), V (J + 1))) \to V (J) < x$
202	193 199 200 201	syl3anc	$⊢ (φ \land x \in (V (J), V (J + 1))) \to V (J) < x$
203	183 184 182 192 202	lelttrd	$⊢ (φ \land x \in (V (J), V (J + 1))) \to Q (I) + L T < x$
204		zssre	$⊢ ℤ \subseteq ℝ$
205	25 204	sstri	$⊢ \{k \in ℤ \| Q (0) + k T \leq V (J)\} \subseteq ℝ$
206	205	a1i	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to \{k \in ℤ \| Q (0) + k T \leq V (J)\} \subseteq ℝ$
207	99	ad2antrr	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to \{k \in ℤ \| Q (0) + k T \leq V (J)\} \neq \emptyset$
208	129	ad2antrr	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to \exists b \in ℝ \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq b$
209	167	peano2zd	$⊢ φ \to L + 1 \in ℤ$
210	209	ad2antrr	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to L + 1 \in ℤ$
211		oveq1	$⊢ I = M - 1 \to I + 1 = M - 1 + 1$
212	146	recnd	$⊢ φ \to M \in ℂ$
213		1cnd	$⊢ φ \to 1 \in ℂ$
214	212 213	npcand	$⊢ φ \to M - 1 + 1 = M$
215	211 214	sylan9eqr	$⊢ (φ \land I = M - 1) \to I + 1 = M$
216	215	fveq2d	$⊢ (φ \land I = M - 1) \to Q (I + 1) = Q (M)$
217	47	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
218	217	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
219	218	simprd	$⊢ φ \to Q (M) = B$
220	219	adantr	$⊢ (φ \land I = M - 1) \to Q (M) = B$
221	59	recnd	$⊢ φ \to B \in ℂ$
222	60	recnd	$⊢ φ \to A \in ℂ$
223	221 222	npcand	$⊢ φ \to B - A + A = B$
224	223	eqcomd	$⊢ φ \to B = B - A + A$
225	1	eqcomi	$⊢ B - A = T$
226	225	a1i	$⊢ φ \to B - A = T$
227	226	oveq1d	$⊢ φ \to B - A + A = T + A$
228	218	simpld	$⊢ φ \to Q (0) = A$
229	228	eqcomd	$⊢ φ \to A = Q (0)$
230	229	oveq2d	$⊢ φ \to T + A = T + Q (0)$
231	224 227 230	3eqtrd	$⊢ φ \to B = T + Q (0)$
232	231	adantr	$⊢ (φ \land I = M - 1) \to B = T + Q (0)$
233	216 220 232	3eqtrd	$⊢ (φ \land I = M - 1) \to Q (I + 1) = T + Q (0)$
234	62	recnd	$⊢ φ \to T \in ℂ$
235	228 222	eqeltrd	$⊢ φ \to Q (0) \in ℂ$
236	234 235	addcomd	$⊢ φ \to T + Q (0) = Q (0) + T$
237	236	adantr	$⊢ (φ \land I = M - 1) \to T + Q (0) = Q (0) + T$
238	233 237	eqtrd	$⊢ (φ \land I = M - 1) \to Q (I + 1) = Q (0) + T$
239	238	oveq1d	$⊢ (φ \land I = M - 1) \to Q (I + 1) + L T = Q (0) + T + L T$
240	171	recnd	$⊢ φ \to L T \in ℂ$
241	235 234 240	addassd	$⊢ φ \to Q (0) + T + L T = Q (0) + T + L T$
242	234	mulid2d	$⊢ φ \to 1 T = T$
243	242 234	eqeltrd	$⊢ φ \to 1 T \in ℂ$
244	243 240	addcomd	$⊢ φ \to 1 T + L T = L T + 1 T$
245	242	eqcomd	$⊢ φ \to T = 1 T$
246	245	oveq1d	$⊢ φ \to T + L T = 1 T + L T$
247	170	recnd	$⊢ φ \to L \in ℂ$
248	247 213 234	adddird	$⊢ φ \to (L + 1) T = L T + 1 T$
249	244 246 248	3eqtr4d	$⊢ φ \to T + L T = (L + 1) T$
250	249	oveq2d	$⊢ φ \to Q (0) + T + L T = Q (0) + (L + 1) T$
251	241 250	eqtrd	$⊢ φ \to Q (0) + T + L T = Q (0) + (L + 1) T$
252	251	adantr	$⊢ (φ \land I = M - 1) \to Q (0) + T + L T = Q (0) + (L + 1) T$
253	239 252	eqtr2d	$⊢ (φ \land I = M - 1) \to Q (0) + (L + 1) T = Q (I + 1) + L T$
254	253	adantr	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to Q (0) + (L + 1) T = Q (I + 1) + L T$
255		simpr	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to Q (I + 1) + L T \leq V (J)$
256	254 255	eqbrtrd	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to Q (0) + (L + 1) T \leq V (J)$
257		oveq1	$⊢ k = L + 1 \to k T = (L + 1) T$
258	257	oveq2d	$⊢ k = L + 1 \to Q (0) + k T = Q (0) + (L + 1) T$
259	258	breq1d	$⊢ k = L + 1 \to (Q (0) + k T \leq V (J) \leftrightarrow Q (0) + (L + 1) T \leq V (J))$
260	259	elrab	$⊢ L + 1 \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} \leftrightarrow (L + 1 \in ℤ \land Q (0) + (L + 1) T \leq V (J))$
261	210 256 260	sylanbrc	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to L + 1 \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}$
262		suprub	$⊢ ((\{k \in ℤ \| Q (0) + k T \leq V (J)\} \subseteq ℝ \land \{k \in ℤ \| Q (0) + k T \leq V (J)\} \neq \emptyset \land \exists b \in ℝ \forall j \in \{k \in ℤ \| Q (0) + k T \leq V (J)\} j \leq b) \land L + 1 \in \{k \in ℤ \| Q (0) + k T \leq V (J)\}) \to L + 1 \leq sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <)$
263	206 207 208 261 262	syl31anc	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to L + 1 \leq sup (\{k \in ℤ \| Q (0) + k T \leq V (J)\} ℝ <)$
264	263 12	breqtrrdi	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to L + 1 \leq L$
265	170	ltp1d	$⊢ φ \to L < L + 1$
266		peano2re	$⊢ L \in ℝ \to L + 1 \in ℝ$
267	170 266	syl	$⊢ φ \to L + 1 \in ℝ$
268	170 267	ltnled	$⊢ φ \to (L < L + 1 \leftrightarrow \neg L + 1 \leq L)$
269	265 268	mpbid	$⊢ φ \to \neg L + 1 \leq L$
270	269	ad2antrr	$⊢ ((φ \land I = M - 1) \land Q (I + 1) + L T \leq V (J)) \to \neg L + 1 \leq L$
271	264 270	pm2.65da	$⊢ (φ \land I = M - 1) \to \neg Q (I + 1) + L T \leq V (J)$
272	17 165	sseldi	$⊢ φ \to I \in ℤ$
273	272	zred	$⊢ φ \to I \in ℝ$
274	273	adantr	$⊢ (φ \land \neg I = M - 1) \to I \in ℝ$
275		peano2rem	$⊢ M \in ℝ \to M - 1 \in ℝ$
276	146 275	syl	$⊢ φ \to M - 1 \in ℝ$
277	276	adantr	$⊢ (φ \land \neg I = M - 1) \to M - 1 \in ℝ$
278		elfzolt2	$⊢ I \in (0 ..^M) \to I < M$
279		elfzoelz	$⊢ I \in (0 ..^M) \to I \in ℤ$
280		elfzoel2	$⊢ I \in (0 ..^M) \to M \in ℤ$
281		zltlem1	$⊢ (I \in ℤ \land M \in ℤ) \to (I < M \leftrightarrow I \leq M - 1)$
282	279 280 281	syl2anc	$⊢ I \in (0 ..^M) \to (I < M \leftrightarrow I \leq M - 1)$
283	278 282	mpbid	$⊢ I \in (0 ..^M) \to I \leq M - 1$
284	165 283	syl	$⊢ φ \to I \leq M - 1$
285	284	adantr	$⊢ (φ \land \neg I = M - 1) \to I \leq M - 1$
286		neqne	$⊢ \neg I = M - 1 \to I \neq M - 1$
287	286	necomd	$⊢ \neg I = M - 1 \to M - 1 \neq I$
288	287	adantl	$⊢ (φ \land \neg I = M - 1) \to M - 1 \neq I$
289	274 277 285 288	leneltd	$⊢ (φ \land \neg I = M - 1) \to I < M - 1$
290	18 204	sstri	$⊢ \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq ℝ$
291	290	a1i	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq ℝ$
292	145	ad2antrr	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \neq \emptyset$
293	161	ad2antrr	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to \exists b \in ℝ \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq b$
294	176	adantr	$⊢ (φ \land I < M - 1) \to I + 1 \in (0 \dots M)$
295	273	adantr	$⊢ (φ \land I < M - 1) \to I \in ℝ$
296	276	adantr	$⊢ (φ \land I < M - 1) \to M - 1 \in ℝ$
297		1red	$⊢ (φ \land I < M - 1) \to 1 \in ℝ$
298		simpr	$⊢ (φ \land I < M - 1) \to I < M - 1$
299	295 296 297 298	ltadd1dd	$⊢ (φ \land I < M - 1) \to I + 1 < M - 1 + 1$
300	214	adantr	$⊢ (φ \land I < M - 1) \to M - 1 + 1 = M$
301	299 300	breqtrd	$⊢ (φ \land I < M - 1) \to I + 1 < M$
302		elfzfzo	$⊢ I + 1 \in (0 ..^M) \leftrightarrow (I + 1 \in (0 \dots M) \land I + 1 < M)$
303	294 301 302	sylanbrc	$⊢ (φ \land I < M - 1) \to I + 1 \in (0 ..^M)$
304	303	anim1i	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to (I + 1 \in (0 ..^M) \land Q (I + 1) + L T \leq V (J))$
305		fveq2	$⊢ j = I + 1 \to Q (j) = Q (I + 1)$
306	305	oveq1d	$⊢ j = I + 1 \to Q (j) + L T = Q (I + 1) + L T$
307	306	breq1d	$⊢ j = I + 1 \to (Q (j) + L T \leq V (J) \leftrightarrow Q (I + 1) + L T \leq V (J))$
308	307	elrab	$⊢ I + 1 \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \leftrightarrow (I + 1 \in (0 ..^M) \land Q (I + 1) + L T \leq V (J))$
309	304 308	sylibr	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to I + 1 \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}$
310		suprub	$⊢ ((\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \subseteq ℝ \land \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} \neq \emptyset \land \exists b \in ℝ \forall k \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} k \leq b) \land I + 1 \in \{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\}) \to I + 1 \leq sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <)$
311	291 292 293 309 310	syl31anc	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to I + 1 \leq sup (\{j \in (0 ..^M) \| Q (j) + L T \leq V (J)\} ℝ <)$
312	311 13	breqtrrdi	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to I + 1 \leq I$
313	273	ltp1d	$⊢ φ \to I < I + 1$
314		peano2re	$⊢ I \in ℝ \to I + 1 \in ℝ$
315	273 314	syl	$⊢ φ \to I + 1 \in ℝ$
316	273 315	ltnled	$⊢ φ \to (I < I + 1 \leftrightarrow \neg I + 1 \leq I)$
317	313 316	mpbid	$⊢ φ \to \neg I + 1 \leq I$
318	317	ad2antrr	$⊢ ((φ \land I < M - 1) \land Q (I + 1) + L T \leq V (J)) \to \neg I + 1 \leq I$
319	312 318	pm2.65da	$⊢ (φ \land I < M - 1) \to \neg Q (I + 1) + L T \leq V (J)$
320	289 319	syldan	$⊢ (φ \land \neg I = M - 1) \to \neg Q (I + 1) + L T \leq V (J)$
321	271 320	pm2.61dan	$⊢ φ \to \neg Q (I + 1) + L T \leq V (J)$
322	44 178	ltnled	$⊢ φ \to (V (J) < Q (I + 1) + L T \leftrightarrow \neg Q (I + 1) + L T \leq V (J))$
323	321 322	mpbird	$⊢ φ \to V (J) < Q (I + 1) + L T$
324	197	adantr	$⊢ (φ \land D \leq Q (I + 1) + L T) \to V (J + 1) \in ℝ$
325	6	adantr	$⊢ (φ \land D \leq Q (I + 1) + L T) \to D \in ℝ$
326	178	adantr	$⊢ (φ \land D \leq Q (I + 1) + L T) \to Q (I + 1) + L T \in ℝ$
327	5	rexrd	$⊢ φ \to C \in ℝ^{*}$
328	6	rexrd	$⊢ φ \to D \in ℝ^{*}$
329	5 6 7	ltled	$⊢ φ \to C \leq D$
330		lbicc2	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C \leq D) \to C \in [C, D]$
331	327 328 329 330	syl3anc	$⊢ φ \to C \in [C, D]$
332		ubicc2	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C \leq D) \to D \in [C, D]$
333	327 328 329 332	syl3anc	$⊢ φ \to D \in [C, D]$
334	331 333	jca	$⊢ φ \to (C \in [C, D] \land D \in [C, D])$
335		prssg	$⊢ (C \in ℝ \land D \in ℝ) \to ((C \in [C, D] \land D \in [C, D]) \leftrightarrow \{C, D\} \subseteq [C, D])$
336	5 6 335	syl2anc	$⊢ φ \to ((C \in [C, D] \land D \in [C, D]) \leftrightarrow \{C, D\} \subseteq [C, D])$
337	334 336	mpbid	$⊢ φ \to \{C, D\} \subseteq [C, D]$
338	337 30	unssd	$⊢ φ \to \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \subseteq [C, D]$
339	8 338	eqsstrid	$⊢ φ \to H \subseteq [C, D]$
340	339 196	sseldd	$⊢ φ \to V (J + 1) \in [C, D]$
341		iccleub	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land V (J + 1) \in [C, D]) \to V (J + 1) \leq D$
342	327 328 340 341	syl3anc	$⊢ φ \to V (J + 1) \leq D$
343	342	adantr	$⊢ (φ \land D \leq Q (I + 1) + L T) \to V (J + 1) \leq D$
344		simpr	$⊢ (φ \land D \leq Q (I + 1) + L T) \to D \leq Q (I + 1) + L T$
345	324 325 326 343 344	letrd	$⊢ (φ \land D \leq Q (I + 1) + L T) \to V (J + 1) \leq Q (I + 1) + L T$
346	345	adantlr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land D \leq Q (I + 1) + L T) \to V (J + 1) \leq Q (I + 1) + L T$
347		simpr	$⊢ (φ \land \neg D \leq Q (I + 1) + L T) \to \neg D \leq Q (I + 1) + L T$
348	178	adantr	$⊢ (φ \land \neg D \leq Q (I + 1) + L T) \to Q (I + 1) + L T \in ℝ$
349	6	adantr	$⊢ (φ \land \neg D \leq Q (I + 1) + L T) \to D \in ℝ$
350	348 349	ltnled	$⊢ (φ \land \neg D \leq Q (I + 1) + L T) \to (Q (I + 1) + L T < D \leftrightarrow \neg D \leq Q (I + 1) + L T)$
351	347 350	mpbird	$⊢ (φ \land \neg D \leq Q (I + 1) + L T) \to Q (I + 1) + L T < D$
352	351	adantlr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land \neg D \leq Q (I + 1) + L T) \to Q (I + 1) + L T < D$
353		simpll	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \land \neg V (J + 1) \leq Q (I + 1) + L T) \to (φ \land V (J) < Q (I + 1) + L T)$
354		simpr	$⊢ (φ \land \neg V (J + 1) \leq Q (I + 1) + L T) \to \neg V (J + 1) \leq Q (I + 1) + L T$
355	178	adantr	$⊢ (φ \land \neg V (J + 1) \leq Q (I + 1) + L T) \to Q (I + 1) + L T \in ℝ$
356	197	adantr	$⊢ (φ \land \neg V (J + 1) \leq Q (I + 1) + L T) \to V (J + 1) \in ℝ$
357	355 356	ltnled	$⊢ (φ \land \neg V (J + 1) \leq Q (I + 1) + L T) \to (Q (I + 1) + L T < V (J + 1) \leftrightarrow \neg V (J + 1) \leq Q (I + 1) + L T)$
358	354 357	mpbird	$⊢ (φ \land \neg V (J + 1) \leq Q (I + 1) + L T) \to Q (I + 1) + L T < V (J + 1)$
359	358	ad4ant14	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \land \neg V (J + 1) \leq Q (I + 1) + L T) \to Q (I + 1) + L T < V (J + 1)$
360	5	ad2antrr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to C \in ℝ$
361	6	ad2antrr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to D \in ℝ$
362	178	ad2antrr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \in ℝ$
363	5	adantr	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to C \in ℝ$
364	178	adantr	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to Q (I + 1) + L T \in ℝ$
365	44	adantr	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to V (J) \in ℝ$
366	339 43	sseldd	$⊢ φ \to V (J) \in [C, D]$
367		iccgelb	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land V (J) \in [C, D]) \to C \leq V (J)$
368	327 328 366 367	syl3anc	$⊢ φ \to C \leq V (J)$
369	368	adantr	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to C \leq V (J)$
370		simpr	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to V (J) < Q (I + 1) + L T$
371	363 365 364 369 370	lelttrd	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to C < Q (I + 1) + L T$
372	363 364 371	ltled	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to C \leq Q (I + 1) + L T$
373	372	adantr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to C \leq Q (I + 1) + L T$
374	178	adantr	$⊢ (φ \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \in ℝ$
375	6	adantr	$⊢ (φ \land Q (I + 1) + L T < D) \to D \in ℝ$
376		simpr	$⊢ (φ \land Q (I + 1) + L T < D) \to Q (I + 1) + L T < D$
377	374 375 376	ltled	$⊢ (φ \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \leq D$
378	377	adantlr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \leq D$
379	360 361 362 373 378	eliccd	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \in [C, D]$
380	167	znegcld	$⊢ φ \to - L \in ℤ$
381	247 234	mulneg1d	$⊢ φ \to (- L) T = - L T$
382	381	oveq2d	$⊢ φ \to Q (I + 1) + L T + (- L) T = Q (I + 1) + L T + (- L T)$
383	178	recnd	$⊢ φ \to Q (I + 1) + L T \in ℂ$
384	383 240	negsubd	$⊢ φ \to Q (I + 1) + L T + (- L T) = Q (I + 1) + L T - L T$
385	177	recnd	$⊢ φ \to Q (I + 1) \in ℂ$
386	385 240	pncand	$⊢ φ \to Q (I + 1) + L T - L T = Q (I + 1)$
387	382 384 386	3eqtrd	$⊢ φ \to Q (I + 1) + L T + (- L) T = Q (I + 1)$
388		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
389	50 388	syl	$⊢ φ \to Q Fn (0 \dots M)$
390		fnfvelrn	$⊢ (Q Fn (0 \dots M) \land I + 1 \in (0 \dots M)) \to Q (I + 1) \in ran Q$
391	389 176 390	syl2anc	$⊢ φ \to Q (I + 1) \in ran Q$
392	387 391	eqeltrd	$⊢ φ \to Q (I + 1) + L T + (- L) T \in ran Q$
393		oveq1	$⊢ k = - L \to k T = (- L) T$
394	393	oveq2d	$⊢ k = - L \to Q (I + 1) + L T + k T = Q (I + 1) + L T + (- L) T$
395	394	eleq1d	$⊢ k = - L \to (Q (I + 1) + L T + k T \in ran Q \leftrightarrow Q (I + 1) + L T + (- L) T \in ran Q)$
396	395	rspcev	$⊢ (- L \in ℤ \land Q (I + 1) + L T + (- L) T \in ran Q) \to \exists k \in ℤ Q (I + 1) + L T + k T \in ran Q$
397	380 392 396	syl2anc	$⊢ φ \to \exists k \in ℤ Q (I + 1) + L T + k T \in ran Q$
398	397	ad2antrr	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to \exists k \in ℤ Q (I + 1) + L T + k T \in ran Q$
399		oveq1	$⊢ y = Q (I + 1) + L T \to y + k T = Q (I + 1) + L T + k T$
400	399	eleq1d	$⊢ y = Q (I + 1) + L T \to (y + k T \in ran Q \leftrightarrow Q (I + 1) + L T + k T \in ran Q)$
401	400	rexbidv	$⊢ y = Q (I + 1) + L T \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ Q (I + 1) + L T + k T \in ran Q)$
402	401	elrab	$⊢ Q (I + 1) + L T \in \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \leftrightarrow (Q (I + 1) + L T \in [C, D] \land \exists k \in ℤ Q (I + 1) + L T + k T \in ran Q)$
403	379 398 402	sylanbrc	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \in \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
404		elun2	$⊢ Q (I + 1) + L T \in \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} \to Q (I + 1) + L T \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\})$
405	403 404	syl	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\})$
406	8	eqcomi	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = H$
407	405 406	eleqtrdi	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to Q (I + 1) + L T \in H$
408	407	adantr	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \land \neg V (J + 1) \leq Q (I + 1) + L T) \to Q (I + 1) + L T \in H$
409		f1ofo	$⊢ V : (0 \dots N) \underset{1-1 onto}{⟶} H \to V : (0 \dots N) \underset{onto}{⟶} H$
410	37 38 409	3syl	$⊢ φ \to V : (0 \dots N) \underset{onto}{⟶} H$
411		foelrn	$⊢ (V : (0 \dots N) \underset{onto}{⟶} H \land Q (I + 1) + L T \in H) \to \exists j \in (0 \dots N) Q (I + 1) + L T = V (j)$
412	410 411	sylan	$⊢ (φ \land Q (I + 1) + L T \in H) \to \exists j \in (0 \dots N) Q (I + 1) + L T = V (j)$
413		id	$⊢ Q (I + 1) + L T = V (j) \to Q (I + 1) + L T = V (j)$
414	413	eqcomd	$⊢ Q (I + 1) + L T = V (j) \to V (j) = Q (I + 1) + L T$
415	414	a1i	$⊢ (φ \land Q (I + 1) + L T \in H) \to (Q (I + 1) + L T = V (j) \to V (j) = Q (I + 1) + L T)$
416	415	reximdv	$⊢ (φ \land Q (I + 1) + L T \in H) \to (\exists j \in (0 \dots N) Q (I + 1) + L T = V (j) \to \exists j \in (0 \dots N) V (j) = Q (I + 1) + L T)$
417	412 416	mpd	$⊢ (φ \land Q (I + 1) + L T \in H) \to \exists j \in (0 \dots N) V (j) = Q (I + 1) + L T$
418	417	ad4ant14	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land Q (I + 1) + L T \in H) \to \exists j \in (0 \dots N) V (j) = Q (I + 1) + L T$
419		simpl	$⊢ (V (J) < Q (I + 1) + L T \land V (j) = Q (I + 1) + L T) \to V (J) < Q (I + 1) + L T$
420	413	eqcoms	$⊢ V (j) = Q (I + 1) + L T \to Q (I + 1) + L T = V (j)$
421	420	adantl	$⊢ (V (J) < Q (I + 1) + L T \land V (j) = Q (I + 1) + L T) \to Q (I + 1) + L T = V (j)$
422	419 421	breqtrd	$⊢ (V (J) < Q (I + 1) + L T \land V (j) = Q (I + 1) + L T) \to V (J) < V (j)$
423	422	adantll	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land V (j) = Q (I + 1) + L T) \to V (J) < V (j)$
424	423	adantlr	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to V (J) < V (j)$
425	37	ad3antrrr	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to V {Isom}_{<, <} ((0 \dots N), H)$
426	42	ad3antrrr	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to J \in (0 \dots N)$
427		simplr	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to j \in (0 \dots N)$
428		isorel	$⊢ (V {Isom}_{<, <} ((0 \dots N), H) \land (J \in (0 \dots N) \land j \in (0 \dots N))) \to (J < j \leftrightarrow V (J) < V (j))$
429	425 426 427 428	syl12anc	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to (J < j \leftrightarrow V (J) < V (j))$
430	424 429	mpbird	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to J < j$
431	430	adantllr	$⊢ ((((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to J < j$
432		simpr	$⊢ (Q (I + 1) + L T < V (J + 1) \land V (j) = Q (I + 1) + L T) \to V (j) = Q (I + 1) + L T$
433		simpl	$⊢ (Q (I + 1) + L T < V (J + 1) \land V (j) = Q (I + 1) + L T) \to Q (I + 1) + L T < V (J + 1)$
434	432 433	eqbrtrd	$⊢ (Q (I + 1) + L T < V (J + 1) \land V (j) = Q (I + 1) + L T) \to V (j) < V (J + 1)$
435	434	adantll	$⊢ ((φ \land Q (I + 1) + L T < V (J + 1)) \land V (j) = Q (I + 1) + L T) \to V (j) < V (J + 1)$
436	435	adantlr	$⊢ (((φ \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to V (j) < V (J + 1)$
437	37	ad3antrrr	$⊢ (((φ \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to V {Isom}_{<, <} ((0 \dots N), H)$
438		simplr	$⊢ (((φ \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to j \in (0 \dots N)$
439	195	ad3antrrr	$⊢ (((φ \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to J + 1 \in (0 \dots N)$
440		isorel	$⊢ (V {Isom}_{<, <} ((0 \dots N), H) \land (j \in (0 \dots N) \land J + 1 \in (0 \dots N))) \to (j < J + 1 \leftrightarrow V (j) < V (J + 1))$
441	437 438 439 440	syl12anc	$⊢ (((φ \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to (j < J + 1 \leftrightarrow V (j) < V (J + 1))$
442	436 441	mpbird	$⊢ (((φ \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to j < J + 1$
443	442	adantl3r	$⊢ ((((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to j < J + 1$
444	431 443	jca	$⊢ ((((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \land V (j) = Q (I + 1) + L T) \to (J < j \land j < J + 1)$
445	444	ex	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land j \in (0 \dots N)) \to (V (j) = Q (I + 1) + L T \to (J < j \land j < J + 1))$
446	445	adantlr	$⊢ ((((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land Q (I + 1) + L T \in H) \land j \in (0 \dots N)) \to (V (j) = Q (I + 1) + L T \to (J < j \land j < J + 1))$
447	446	reximdva	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land Q (I + 1) + L T \in H) \to (\exists j \in (0 \dots N) V (j) = Q (I + 1) + L T \to \exists j \in (0 \dots N) (J < j \land j < J + 1))$
448	418 447	mpd	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < V (J + 1)) \land Q (I + 1) + L T \in H) \to \exists j \in (0 \dots N) (J < j \land j < J + 1)$
449	353 359 408 448	syl21anc	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \land \neg V (J + 1) \leq Q (I + 1) + L T) \to \exists j \in (0 \dots N) (J < j \land j < J + 1)$
450		elfzelz	$⊢ j \in (0 \dots N) \to j \in ℤ$
451	450	ad2antlr	$⊢ ((φ \land j \in (0 \dots N)) \land (J < j \land j < J + 1)) \to j \in ℤ$
452		elfzelz	$⊢ J \in (0 \dots N) \to J \in ℤ$
453	42 452	syl	$⊢ φ \to J \in ℤ$
454	453	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land (J < j \land j < J + 1)) \to J \in ℤ$
455		simprl	$⊢ ((φ \land j \in (0 \dots N)) \land (J < j \land j < J + 1)) \to J < j$
456		simprr	$⊢ ((φ \land j \in (0 \dots N)) \land (J < j \land j < J + 1)) \to j < J + 1$
457		btwnnz	$⊢ (J \in ℤ \land J < j \land j < J + 1) \to \neg j \in ℤ$
458	454 455 456 457	syl3anc	$⊢ ((φ \land j \in (0 \dots N)) \land (J < j \land j < J + 1)) \to \neg j \in ℤ$
459	451 458	pm2.65da	$⊢ (φ \land j \in (0 \dots N)) \to \neg (J < j \land j < J + 1)$
460	459	nrexdv	$⊢ φ \to \neg \exists j \in (0 \dots N) (J < j \land j < J + 1)$
461	460	ad3antrrr	$⊢ (((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \land \neg V (J + 1) \leq Q (I + 1) + L T) \to \neg \exists j \in (0 \dots N) (J < j \land j < J + 1)$
462	449 461	condan	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land Q (I + 1) + L T < D) \to V (J + 1) \leq Q (I + 1) + L T$
463	352 462	syldan	$⊢ ((φ \land V (J) < Q (I + 1) + L T) \land \neg D \leq Q (I + 1) + L T) \to V (J + 1) \leq Q (I + 1) + L T$
464	346 463	pm2.61dan	$⊢ (φ \land V (J) < Q (I + 1) + L T) \to V (J + 1) \leq Q (I + 1) + L T$
465	323 464	mpdan	$⊢ φ \to V (J + 1) \leq Q (I + 1) + L T$
466	465	adantr	$⊢ (φ \land x \in (V (J), V (J + 1))) \to V (J + 1) \leq Q (I + 1) + L T$
467	182	adantr	$⊢ ((φ \land x \in (V (J), V (J + 1))) \land V (J + 1) \leq Q (I + 1) + L T) \to x \in ℝ$
468	197	ad2antrr	$⊢ ((φ \land x \in (V (J), V (J + 1))) \land V (J + 1) \leq Q (I + 1) + L T) \to V (J + 1) \in ℝ$
469	178	ad2antrr	$⊢ ((φ \land x \in (V (J), V (J + 1))) \land V (J + 1) \leq Q (I + 1) + L T) \to Q (I + 1) + L T \in ℝ$
470		iooltub	$⊢ (V (J) \in ℝ^{} \land V (J + 1) \in ℝ^{} \land x \in (V (J), V (J + 1))) \to x < V (J + 1)$
471	193 199 200 470	syl3anc	$⊢ (φ \land x \in (V (J), V (J + 1))) \to x < V (J + 1)$
472	471	adantr	$⊢ ((φ \land x \in (V (J), V (J + 1))) \land V (J + 1) \leq Q (I + 1) + L T) \to x < V (J + 1)$
473		simpr	$⊢ ((φ \land x \in (V (J), V (J + 1))) \land V (J + 1) \leq Q (I + 1) + L T) \to V (J + 1) \leq Q (I + 1) + L T$
474	467 468 469 472 473	ltletrd	$⊢ ((φ \land x \in (V (J), V (J + 1))) \land V (J + 1) \leq Q (I + 1) + L T) \to x < Q (I + 1) + L T$
475	466 474	mpdan	$⊢ (φ \land x \in (V (J), V (J + 1))) \to x < Q (I + 1) + L T$
476	174 180 182 203 475	eliood	$⊢ (φ \land x \in (V (J), V (J + 1))) \to x \in (Q (I) + L T, Q (I + 1) + L T)$
477	476	ralrimiva	$⊢ φ \to \forall x \in (V (J), V (J + 1)) x \in (Q (I) + L T, Q (I + 1) + L T)$
478		dfss3	$⊢ (V (J), V (J + 1)) \subseteq (Q (I) + L T, Q (I + 1) + L T) \leftrightarrow \forall x \in (V (J), V (J + 1)) x \in (Q (I) + L T, Q (I + 1) + L T)$
479	477 478	sylibr	$⊢ φ \to (V (J), V (J + 1)) \subseteq (Q (I) + L T, Q (I + 1) + L T)$
480		fveq2	$⊢ i = I \to Q (i) = Q (I)$
481	480	oveq1d	$⊢ i = I \to Q (i) + l T = Q (I) + l T$
482		oveq1	$⊢ i = I \to i + 1 = I + 1$
483	482	fveq2d	$⊢ i = I \to Q (i + 1) = Q (I + 1)$
484	483	oveq1d	$⊢ i = I \to Q (i + 1) + l T = Q (I + 1) + l T$
485	481 484	oveq12d	$⊢ i = I \to (Q (i) + l T, Q (i + 1) + l T) = (Q (I) + l T, Q (I + 1) + l T)$
486	485	sseq2d	$⊢ i = I \to ((V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T) \leftrightarrow (V (J), V (J + 1)) \subseteq (Q (I) + l T, Q (I + 1) + l T))$
487		oveq1	$⊢ l = L \to l T = L T$
488	487	oveq2d	$⊢ l = L \to Q (I) + l T = Q (I) + L T$
489	487	oveq2d	$⊢ l = L \to Q (I + 1) + l T = Q (I + 1) + L T$
490	488 489	oveq12d	$⊢ l = L \to (Q (I) + l T, Q (I + 1) + l T) = (Q (I) + L T, Q (I + 1) + L T)$
491	490	sseq2d	$⊢ l = L \to ((V (J), V (J + 1)) \subseteq (Q (I) + l T, Q (I + 1) + l T) \leftrightarrow (V (J), V (J + 1)) \subseteq (Q (I) + L T, Q (I + 1) + L T))$
492	486 491	rspc2ev	$⊢ (I \in (0 ..^M) \land L \in ℤ \land (V (J), V (J + 1)) \subseteq (Q (I) + L T, Q (I + 1) + L T)) \to \exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)$
493	165 167 479 492	syl3anc	$⊢ φ \to \exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T)$
494	165 167 493	jca31	$⊢ φ \to ((I \in (0 ..^M) \land L \in ℤ) \land \exists i \in (0 ..^M) \exists l \in ℤ (V (J), V (J + 1)) \subseteq (Q (i) + l T, Q (i + 1) + l T))$

Metamath Proof Explorer

Theorem fourierdlem64

Proof