fourierdlem11

Description: If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem11.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))\})$
	fourierdlem11.m	$⊢ φ \to M \in ℕ$
	fourierdlem11.q	$⊢ φ \to Q \in P (M)$
Assertion	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem11.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		fourierdlem11.m	$⊢ φ \to M \in ℕ$
3		fourierdlem11.q	$⊢ φ \to Q \in P (M)$
4	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))))$
5	2 4	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))))$
6	3 5	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)))$
7	6	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
8	7	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
9	8	simpld	$⊢ φ \to Q (0) = A$
10	6	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
11		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
12	10 11	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
13		0red	$⊢ φ \to 0 \in ℝ$
14	13	leidd	$⊢ φ \to 0 \leq 0$
15	2	nnred	$⊢ φ \to M \in ℝ$
16	2	nngt0d	$⊢ φ \to 0 < M$
17	13 15 16	ltled	$⊢ φ \to 0 \leq M$
18		0zd	$⊢ φ \to 0 \in ℤ$
19	2	nnzd	$⊢ φ \to M \in ℤ$
20		elfz	$⊢ (0 \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (0 \in (0 \dots M) \leftrightarrow (0 \leq 0 \land 0 \leq M))$
21	18 18 19 20	syl3anc	$⊢ φ \to (0 \in (0 \dots M) \leftrightarrow (0 \leq 0 \land 0 \leq M))$
22	14 17 21	mpbir2and	$⊢ φ \to 0 \in (0 \dots M)$
23	12 22	ffvelrnd	$⊢ φ \to Q (0) \in ℝ$
24	9 23	eqeltrrd	$⊢ φ \to A \in ℝ$
25	8	simprd	$⊢ φ \to Q (M) = B$
26	15	leidd	$⊢ φ \to M \leq M$
27		elfz	$⊢ (M \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (M \in (0 \dots M) \leftrightarrow (0 \leq M \land M \leq M))$
28	19 18 19 27	syl3anc	$⊢ φ \to (M \in (0 \dots M) \leftrightarrow (0 \leq M \land M \leq M))$
29	17 26 28	mpbir2and	$⊢ φ \to M \in (0 \dots M)$
30	12 29	ffvelrnd	$⊢ φ \to Q (M) \in ℝ$
31	25 30	eqeltrrd	$⊢ φ \to B \in ℝ$
32		0le1	$⊢ 0 \leq 1$
33	32	a1i	$⊢ φ \to 0 \leq 1$
34	2	nnge1d	$⊢ φ \to 1 \leq M$
35		1zzd	$⊢ φ \to 1 \in ℤ$
36		elfz	$⊢ (1 \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (1 \in (0 \dots M) \leftrightarrow (0 \leq 1 \land 1 \leq M))$
37	35 18 19 36	syl3anc	$⊢ φ \to (1 \in (0 \dots M) \leftrightarrow (0 \leq 1 \land 1 \leq M))$
38	33 34 37	mpbir2and	$⊢ φ \to 1 \in (0 \dots M)$
39	12 38	ffvelrnd	$⊢ φ \to Q (1) \in ℝ$
40		elfzo	$⊢ (0 \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (0 \in (0 ..^M) \leftrightarrow (0 \leq 0 \land 0 < M))$
41	18 18 19 40	syl3anc	$⊢ φ \to (0 \in (0 ..^M) \leftrightarrow (0 \leq 0 \land 0 < M))$
42	14 16 41	mpbir2and	$⊢ φ \to 0 \in (0 ..^M)$
43		0re	$⊢ 0 \in ℝ$
44		eleq1	$⊢ i = 0 \to (i \in (0 ..^M) \leftrightarrow 0 \in (0 ..^M))$
45	44	anbi2d	$⊢ i = 0 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land 0 \in (0 ..^M)))$
46		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
47		oveq1	$⊢ i = 0 \to i + 1 = 0 + 1$
48	47	fveq2d	$⊢ i = 0 \to Q (i + 1) = Q (0 + 1)$
49	46 48	breq12d	$⊢ i = 0 \to (Q (i) < Q (i + 1) \leftrightarrow Q (0) < Q (0 + 1))$
50	45 49	imbi12d	$⊢ i = 0 \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)))$
51	7	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
52	51	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
53	50 52	vtoclg	$⊢ 0 \in ℝ \to ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1))$
54	43 53	ax-mp	$⊢ (φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)$
55	42 54	mpdan	$⊢ φ \to Q (0) < Q (0 + 1)$
56		0p1e1	$⊢ 0 + 1 = 1$
57	56	a1i	$⊢ φ \to 0 + 1 = 1$
58	57	fveq2d	$⊢ φ \to Q (0 + 1) = Q (1)$
59	55 9 58	3brtr3d	$⊢ φ \to A < Q (1)$
60		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
61	2 60	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
62	12	adantr	$⊢ (φ \land i \in (1 \dots M)) \to Q : (0 \dots M) ⟶ ℝ$
63		0red	$⊢ i \in (1 \dots M) \to 0 \in ℝ$
64		elfzelz	$⊢ i \in (1 \dots M) \to i \in ℤ$
65	64	zred	$⊢ i \in (1 \dots M) \to i \in ℝ$
66		1red	$⊢ i \in (1 \dots M) \to 1 \in ℝ$
67		0lt1	$⊢ 0 < 1$
68	67	a1i	$⊢ i \in (1 \dots M) \to 0 < 1$
69		elfzle1	$⊢ i \in (1 \dots M) \to 1 \leq i$
70	63 66 65 68 69	ltletrd	$⊢ i \in (1 \dots M) \to 0 < i$
71	63 65 70	ltled	$⊢ i \in (1 \dots M) \to 0 \leq i$
72		elfzle2	$⊢ i \in (1 \dots M) \to i \leq M$
73		0zd	$⊢ i \in (1 \dots M) \to 0 \in ℤ$
74		elfzel2	$⊢ i \in (1 \dots M) \to M \in ℤ$
75		elfz	$⊢ (i \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (i \in (0 \dots M) \leftrightarrow (0 \leq i \land i \leq M))$
76	64 73 74 75	syl3anc	$⊢ i \in (1 \dots M) \to (i \in (0 \dots M) \leftrightarrow (0 \leq i \land i \leq M))$
77	71 72 76	mpbir2and	$⊢ i \in (1 \dots M) \to i \in (0 \dots M)$
78	77	adantl	$⊢ (φ \land i \in (1 \dots M)) \to i \in (0 \dots M)$
79	62 78	ffvelrnd	$⊢ (φ \land i \in (1 \dots M)) \to Q (i) \in ℝ$
80	12	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to Q : (0 \dots M) ⟶ ℝ$
81		0red	$⊢ i \in (1 \dots M - 1) \to 0 \in ℝ$
82		elfzelz	$⊢ i \in (1 \dots M - 1) \to i \in ℤ$
83	82	zred	$⊢ i \in (1 \dots M - 1) \to i \in ℝ$
84		1red	$⊢ i \in (1 \dots M - 1) \to 1 \in ℝ$
85	67	a1i	$⊢ i \in (1 \dots M - 1) \to 0 < 1$
86		elfzle1	$⊢ i \in (1 \dots M - 1) \to 1 \leq i$
87	81 84 83 85 86	ltletrd	$⊢ i \in (1 \dots M - 1) \to 0 < i$
88	81 83 87	ltled	$⊢ i \in (1 \dots M - 1) \to 0 \leq i$
89	88	adantl	$⊢ (φ \land i \in (1 \dots M - 1)) \to 0 \leq i$
90	83	adantl	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in ℝ$
91	15	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to M \in ℝ$
92		peano2rem	$⊢ M \in ℝ \to M - 1 \in ℝ$
93	91 92	syl	$⊢ (φ \land i \in (1 \dots M - 1)) \to M - 1 \in ℝ$
94		elfzle2	$⊢ i \in (1 \dots M - 1) \to i \leq M - 1$
95	94	adantl	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \leq M - 1$
96	91	ltm1d	$⊢ (φ \land i \in (1 \dots M - 1)) \to M - 1 < M$
97	90 93 91 95 96	lelttrd	$⊢ (φ \land i \in (1 \dots M - 1)) \to i < M$
98	90 91 97	ltled	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \leq M$
99	82	adantl	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in ℤ$
100		0zd	$⊢ (φ \land i \in (1 \dots M - 1)) \to 0 \in ℤ$
101	19	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to M \in ℤ$
102	99 100 101 75	syl3anc	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i \in (0 \dots M) \leftrightarrow (0 \leq i \land i \leq M))$
103	89 98 102	mpbir2and	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in (0 \dots M)$
104	80 103	ffvelrnd	$⊢ (φ \land i \in (1 \dots M - 1)) \to Q (i) \in ℝ$
105		0red	$⊢ (φ \land i \in (1 \dots M - 1)) \to 0 \in ℝ$
106		peano2re	$⊢ i \in ℝ \to i + 1 \in ℝ$
107	90 106	syl	$⊢ (φ \land i \in (1 \dots M - 1)) \to i + 1 \in ℝ$
108		1red	$⊢ (φ \land i \in (1 \dots M - 1)) \to 1 \in ℝ$
109	67	a1i	$⊢ (φ \land i \in (1 \dots M - 1)) \to 0 < 1$
110	83 106	syl	$⊢ i \in (1 \dots M - 1) \to i + 1 \in ℝ$
111	83	ltp1d	$⊢ i \in (1 \dots M - 1) \to i < i + 1$
112	84 83 110 86 111	lelttrd	$⊢ i \in (1 \dots M - 1) \to 1 < i + 1$
113	112	adantl	$⊢ (φ \land i \in (1 \dots M - 1)) \to 1 < i + 1$
114	105 108 107 109 113	lttrd	$⊢ (φ \land i \in (1 \dots M - 1)) \to 0 < i + 1$
115	105 107 114	ltled	$⊢ (φ \land i \in (1 \dots M - 1)) \to 0 \leq i + 1$
116	90 93 108 95	leadd1dd	$⊢ (φ \land i \in (1 \dots M - 1)) \to i + 1 \leq M - 1 + 1$
117	2	nncnd	$⊢ φ \to M \in ℂ$
118		1cnd	$⊢ φ \to 1 \in ℂ$
119	117 118	npcand	$⊢ φ \to M - 1 + 1 = M$
120	119	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to M - 1 + 1 = M$
121	116 120	breqtrd	$⊢ (φ \land i \in (1 \dots M - 1)) \to i + 1 \leq M$
122	99	peano2zd	$⊢ (φ \land i \in (1 \dots M - 1)) \to i + 1 \in ℤ$
123		elfz	$⊢ (i + 1 \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (i + 1 \in (0 \dots M) \leftrightarrow (0 \leq i + 1 \land i + 1 \leq M))$
124	122 100 101 123	syl3anc	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i + 1 \in (0 \dots M) \leftrightarrow (0 \leq i + 1 \land i + 1 \leq M))$
125	115 121 124	mpbir2and	$⊢ (φ \land i \in (1 \dots M - 1)) \to i + 1 \in (0 \dots M)$
126	80 125	ffvelrnd	$⊢ (φ \land i \in (1 \dots M - 1)) \to Q (i + 1) \in ℝ$
127		elfzo	$⊢ (i \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (i \in (0 ..^M) \leftrightarrow (0 \leq i \land i < M))$
128	99 100 101 127	syl3anc	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i \in (0 ..^M) \leftrightarrow (0 \leq i \land i < M))$
129	89 97 128	mpbir2and	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in (0 ..^M)$
130	129 52	syldan	$⊢ (φ \land i \in (1 \dots M - 1)) \to Q (i) < Q (i + 1)$
131	104 126 130	ltled	$⊢ (φ \land i \in (1 \dots M - 1)) \to Q (i) \leq Q (i + 1)$
132	61 79 131	monoord	$⊢ φ \to Q (1) \leq Q (M)$
133	132 25	breqtrd	$⊢ φ \to Q (1) \leq B$
134	24 39 31 59 133	ltletrd	$⊢ φ \to A < B$
135	24 31 134	3jca	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$

Metamath Proof Explorer

Theorem fourierdlem11

Proof