# Metamath Proof Explorer

## Theorem 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}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)={A}\wedge {p}\left({m}\right)={B}\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
fourierdlem11.m ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem11.q ${⊢}{\phi }\to {Q}\in {P}\left({M}\right)$
Assertion fourierdlem11 ${⊢}{\phi }\to \left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)$

### Proof

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