# Metamath Proof Explorer

## Theorem fourierdlem15

Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem15.1 ${⊢}{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)$
fourierdlem15.2 ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem15.3 ${⊢}{\phi }\to {Q}\in {P}\left({M}\right)$
Assertion fourierdlem15 ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶\left[{A},{B}\right]$

### Proof

Step Hyp Ref Expression
1 fourierdlem15.1 ${⊢}{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 fourierdlem15.2 ${⊢}{\phi }\to {M}\in ℕ$
3 fourierdlem15.3 ${⊢}{\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 simpld ${⊢}{\phi }\to {Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)$
8 reex ${⊢}ℝ\in \mathrm{V}$
9 8 a1i ${⊢}{\phi }\to ℝ\in \mathrm{V}$
10 ovex ${⊢}\left(0\dots {M}\right)\in \mathrm{V}$
11 10 a1i ${⊢}{\phi }\to \left(0\dots {M}\right)\in \mathrm{V}$
12 9 11 elmapd ${⊢}{\phi }\to \left({Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)↔{Q}:\left(0\dots {M}\right)⟶ℝ\right)$
13 7 12 mpbid ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶ℝ$
14 ffn ${⊢}{Q}:\left(0\dots {M}\right)⟶ℝ\to {Q}Fn\left(0\dots {M}\right)$
15 13 14 syl ${⊢}{\phi }\to {Q}Fn\left(0\dots {M}\right)$
16 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)$
17 16 simpld ${⊢}{\phi }\to \left({Q}\left(0\right)={A}\wedge {Q}\left({M}\right)={B}\right)$
18 17 simpld ${⊢}{\phi }\to {Q}\left(0\right)={A}$
19 nnnn0 ${⊢}{M}\in ℕ\to {M}\in {ℕ}_{0}$
20 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
21 19 20 syl6eleq ${⊢}{M}\in ℕ\to {M}\in {ℤ}_{\ge 0}$
22 2 21 syl ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
23 eluzfz1 ${⊢}{M}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {M}\right)$
24 22 23 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
25 13 24 ffvelrnd ${⊢}{\phi }\to {Q}\left(0\right)\in ℝ$
26 18 25 eqeltrrd ${⊢}{\phi }\to {A}\in ℝ$
27 26 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {A}\in ℝ$
28 17 simprd ${⊢}{\phi }\to {Q}\left({M}\right)={B}$
29 eluzfz2 ${⊢}{M}\in {ℤ}_{\ge 0}\to {M}\in \left(0\dots {M}\right)$
30 22 29 syl ${⊢}{\phi }\to {M}\in \left(0\dots {M}\right)$
31 13 30 ffvelrnd ${⊢}{\phi }\to {Q}\left({M}\right)\in ℝ$
32 28 31 eqeltrrd ${⊢}{\phi }\to {B}\in ℝ$
33 32 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {B}\in ℝ$
34 13 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({i}\right)\in ℝ$
35 18 eqcomd ${⊢}{\phi }\to {A}={Q}\left(0\right)$
36 35 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {A}={Q}\left(0\right)$
37 elfzuz ${⊢}{i}\in \left(0\dots {M}\right)\to {i}\in {ℤ}_{\ge 0}$
38 37 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {i}\in {ℤ}_{\ge 0}$
39 13 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
40 elfzle1 ${⊢}{j}\in \left(0\dots {i}\right)\to 0\le {j}$
41 40 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to 0\le {j}$
42 elfzelz ${⊢}{j}\in \left(0\dots {i}\right)\to {j}\in ℤ$
43 42 zred ${⊢}{j}\in \left(0\dots {i}\right)\to {j}\in ℝ$
44 43 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {j}\in ℝ$
45 elfzelz ${⊢}{i}\in \left(0\dots {M}\right)\to {i}\in ℤ$
46 45 zred ${⊢}{i}\in \left(0\dots {M}\right)\to {i}\in ℝ$
47 46 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {i}\in ℝ$
48 elfzel2 ${⊢}{i}\in \left(0\dots {M}\right)\to {M}\in ℤ$
49 48 zred ${⊢}{i}\in \left(0\dots {M}\right)\to {M}\in ℝ$
50 49 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {M}\in ℝ$
51 elfzle2 ${⊢}{j}\in \left(0\dots {i}\right)\to {j}\le {i}$
52 51 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {j}\le {i}$
53 elfzle2 ${⊢}{i}\in \left(0\dots {M}\right)\to {i}\le {M}$
54 53 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {i}\le {M}$
55 44 47 50 52 54 letrd ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {j}\le {M}$
56 42 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {j}\in ℤ$
57 0zd ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to 0\in ℤ$
58 48 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {M}\in ℤ$
59 elfz ${⊢}\left({j}\in ℤ\wedge 0\in ℤ\wedge {M}\in ℤ\right)\to \left({j}\in \left(0\dots {M}\right)↔\left(0\le {j}\wedge {j}\le {M}\right)\right)$
60 56 57 58 59 syl3anc ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to \left({j}\in \left(0\dots {M}\right)↔\left(0\le {j}\wedge {j}\le {M}\right)\right)$
61 41 55 60 mpbir2and ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {j}\in \left(0\dots {M}\right)$
62 61 adantll ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {j}\in \left(0\dots {M}\right)$
63 39 62 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left(0\dots {i}\right)\right)\to {Q}\left({j}\right)\in ℝ$
64 simpll ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {\phi }$
65 elfzle1 ${⊢}{j}\in \left(0\dots {i}-1\right)\to 0\le {j}$
66 65 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to 0\le {j}$
67 elfzelz ${⊢}{j}\in \left(0\dots {i}-1\right)\to {j}\in ℤ$
68 67 zred ${⊢}{j}\in \left(0\dots {i}-1\right)\to {j}\in ℝ$
69 68 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}\in ℝ$
70 46 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {i}\in ℝ$
71 49 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {M}\in ℝ$
72 peano2rem ${⊢}{i}\in ℝ\to {i}-1\in ℝ$
73 70 72 syl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {i}-1\in ℝ$
74 elfzle2 ${⊢}{j}\in \left(0\dots {i}-1\right)\to {j}\le {i}-1$
75 74 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}\le {i}-1$
76 70 ltm1d ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {i}-1<{i}$
77 69 73 70 75 76 lelttrd ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}<{i}$
78 53 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {i}\le {M}$
79 69 70 71 77 78 ltletrd ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}<{M}$
80 67 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}\in ℤ$
81 0zd ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to 0\in ℤ$
82 48 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {M}\in ℤ$
83 elfzo ${⊢}\left({j}\in ℤ\wedge 0\in ℤ\wedge {M}\in ℤ\right)\to \left({j}\in \left(0..^{M}\right)↔\left(0\le {j}\wedge {j}<{M}\right)\right)$
84 80 81 82 83 syl3anc ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to \left({j}\in \left(0..^{M}\right)↔\left(0\le {j}\wedge {j}<{M}\right)\right)$
85 66 79 84 mpbir2and ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}\in \left(0..^{M}\right)$
86 85 adantll ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {j}\in \left(0..^{M}\right)$
87 13 adantr ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
88 elfzofz ${⊢}{j}\in \left(0..^{M}\right)\to {j}\in \left(0\dots {M}\right)$
89 88 adantl ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
90 87 89 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {Q}\left({j}\right)\in ℝ$
91 fzofzp1 ${⊢}{j}\in \left(0..^{M}\right)\to {j}+1\in \left(0\dots {M}\right)$
92 91 adantl ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {j}+1\in \left(0\dots {M}\right)$
93 87 92 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {Q}\left({j}+1\right)\in ℝ$
94 eleq1w ${⊢}{i}={j}\to \left({i}\in \left(0..^{M}\right)↔{j}\in \left(0..^{M}\right)\right)$
95 94 anbi2d ${⊢}{i}={j}\to \left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)↔\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\right)$
96 fveq2 ${⊢}{i}={j}\to {Q}\left({i}\right)={Q}\left({j}\right)$
97 oveq1 ${⊢}{i}={j}\to {i}+1={j}+1$
98 97 fveq2d ${⊢}{i}={j}\to {Q}\left({i}+1\right)={Q}\left({j}+1\right)$
99 96 98 breq12d ${⊢}{i}={j}\to \left({Q}\left({i}\right)<{Q}\left({i}+1\right)↔{Q}\left({j}\right)<{Q}\left({j}+1\right)\right)$
100 95 99 imbi12d ${⊢}{i}={j}\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 {j}\in \left(0..^{M}\right)\right)\to {Q}\left({j}\right)<{Q}\left({j}+1\right)\right)\right)$
101 16 simprd ${⊢}{\phi }\to \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)<{Q}\left({i}+1\right)$
102 101 r19.21bi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)<{Q}\left({i}+1\right)$
103 100 102 chvarv ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {Q}\left({j}\right)<{Q}\left({j}+1\right)$
104 90 93 103 ltled ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to {Q}\left({j}\right)\le {Q}\left({j}+1\right)$
105 64 86 104 syl2anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left(0\dots {i}-1\right)\right)\to {Q}\left({j}\right)\le {Q}\left({j}+1\right)$
106 38 63 105 monoord ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left(0\right)\le {Q}\left({i}\right)$
107 36 106 eqbrtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {A}\le {Q}\left({i}\right)$
108 elfzuz3 ${⊢}{i}\in \left(0\dots {M}\right)\to {M}\in {ℤ}_{\ge {i}}$
109 108 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {M}\in {ℤ}_{\ge {i}}$
110 13 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
111 fz0fzelfz0 ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
112 111 adantll ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}\right)\right)\to {j}\in \left(0\dots {M}\right)$
113 110 112 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}\right)\right)\to {Q}\left({j}\right)\in ℝ$
114 13 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
115 0red ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\in ℝ$
116 46 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {i}\in ℝ$
117 elfzelz ${⊢}{j}\in \left({i}\dots {M}-1\right)\to {j}\in ℤ$
118 117 zred ${⊢}{j}\in \left({i}\dots {M}-1\right)\to {j}\in ℝ$
119 118 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\in ℝ$
120 elfzle1 ${⊢}{i}\in \left(0\dots {M}\right)\to 0\le {i}$
121 120 adantr ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\le {i}$
122 elfzle1 ${⊢}{j}\in \left({i}\dots {M}-1\right)\to {i}\le {j}$
123 122 adantl ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {i}\le {j}$
124 115 116 119 121 123 letrd ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\le {j}$
125 124 adantll ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\le {j}$
126 118 adantl ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\in ℝ$
127 2 nnred ${⊢}{\phi }\to {M}\in ℝ$
128 127 adantr ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {M}\in ℝ$
129 1red ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 1\in ℝ$
130 128 129 resubcld ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {M}-1\in ℝ$
131 elfzle2 ${⊢}{j}\in \left({i}\dots {M}-1\right)\to {j}\le {M}-1$
132 131 adantl ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\le {M}-1$
133 128 ltm1d ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {M}-1<{M}$
134 126 130 128 132 133 lelttrd ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}<{M}$
135 126 128 134 ltled ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\le {M}$
136 135 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\le {M}$
137 117 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\in ℤ$
138 0zd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\in ℤ$
139 48 ad2antlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {M}\in ℤ$
140 137 138 139 59 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to \left({j}\in \left(0\dots {M}\right)↔\left(0\le {j}\wedge {j}\le {M}\right)\right)$
141 125 136 140 mpbir2and ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\in \left(0\dots {M}\right)$
142 114 141 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {Q}\left({j}\right)\in ℝ$
143 118 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\in ℝ$
144 1red ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 1\in ℝ$
145 0le1 ${⊢}0\le 1$
146 145 a1i ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\le 1$
147 143 144 125 146 addge0d ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 0\le {j}+1$
148 126 130 129 132 leadd1dd ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}+1\le {M}-1+1$
149 2 nncnd ${⊢}{\phi }\to {M}\in ℂ$
150 149 adantr ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {M}\in ℂ$
151 1cnd ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to 1\in ℂ$
152 150 151 npcand ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {M}-1+1={M}$
153 148 152 breqtrd ${⊢}\left({\phi }\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}+1\le {M}$
154 153 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}+1\le {M}$
155 137 peano2zd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}+1\in ℤ$
156 elfz ${⊢}\left({j}+1\in ℤ\wedge 0\in ℤ\wedge {M}\in ℤ\right)\to \left({j}+1\in \left(0\dots {M}\right)↔\left(0\le {j}+1\wedge {j}+1\le {M}\right)\right)$
157 155 138 139 156 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to \left({j}+1\in \left(0\dots {M}\right)↔\left(0\le {j}+1\wedge {j}+1\le {M}\right)\right)$
158 147 154 157 mpbir2and ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}+1\in \left(0\dots {M}\right)$
159 114 158 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {Q}\left({j}+1\right)\in ℝ$
160 simpll ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {\phi }$
161 134 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}<{M}$
162 137 138 139 83 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to \left({j}\in \left(0..^{M}\right)↔\left(0\le {j}\wedge {j}<{M}\right)\right)$
163 125 161 162 mpbir2and ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {j}\in \left(0..^{M}\right)$
164 160 163 103 syl2anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {Q}\left({j}\right)<{Q}\left({j}+1\right)$
165 142 159 164 ltled ${⊢}\left(\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\wedge {j}\in \left({i}\dots {M}-1\right)\right)\to {Q}\left({j}\right)\le {Q}\left({j}+1\right)$
166 109 113 165 monoord ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({i}\right)\le {Q}\left({M}\right)$
167 28 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({M}\right)={B}$
168 166 167 breqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({i}\right)\le {B}$
169 27 33 34 107 168 eliccd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({i}\right)\in \left[{A},{B}\right]$
170 169 ralrimiva ${⊢}{\phi }\to \forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)\in \left[{A},{B}\right]$
171 fnfvrnss ${⊢}\left({Q}Fn\left(0\dots {M}\right)\wedge \forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)\in \left[{A},{B}\right]\right)\to \mathrm{ran}{Q}\subseteq \left[{A},{B}\right]$
172 15 170 171 syl2anc ${⊢}{\phi }\to \mathrm{ran}{Q}\subseteq \left[{A},{B}\right]$
173 df-f ${⊢}{Q}:\left(0\dots {M}\right)⟶\left[{A},{B}\right]↔\left({Q}Fn\left(0\dots {M}\right)\wedge \mathrm{ran}{Q}\subseteq \left[{A},{B}\right]\right)$
174 15 172 173 sylanbrc ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶\left[{A},{B}\right]$