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

Metamath Proof Explorer

Theorem fourierdlem11

Proof