# Metamath Proof Explorer

## Theorem fourierdlem50

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem50.xre ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem50.p ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\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)$
fourierdlem50.m ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem50.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
fourierdlem50.a ${⊢}{\phi }\to {A}\in ℝ$
fourierdlem50.b ${⊢}{\phi }\to {B}\in ℝ$
fourierdlem50.altb ${⊢}{\phi }\to {A}<{B}$
fourierdlem50.ab ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
fourierdlem50.q ${⊢}{Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
fourierdlem50.t ${⊢}{T}=\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)$
fourierdlem50.n ${⊢}{N}=\left|{T}\right|-1$
fourierdlem50.s ${⊢}{S}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)\right)$
fourierdlem50.j ${⊢}{\phi }\to {J}\in \left(0..^{N}\right)$
fourierdlem50.u ${⊢}{U}=\left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)$
fourierdlem50.ch ${⊢}{\chi }↔\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)$
Assertion fourierdlem50 ${⊢}{\phi }\to \left({U}\in \left(0..^{M}\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 fourierdlem50.xre ${⊢}{\phi }\to {X}\in ℝ$
2 fourierdlem50.p ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\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)$
3 fourierdlem50.m ${⊢}{\phi }\to {M}\in ℕ$
4 fourierdlem50.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
5 fourierdlem50.a ${⊢}{\phi }\to {A}\in ℝ$
6 fourierdlem50.b ${⊢}{\phi }\to {B}\in ℝ$
7 fourierdlem50.altb ${⊢}{\phi }\to {A}<{B}$
8 fourierdlem50.ab ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
9 fourierdlem50.q ${⊢}{Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
10 fourierdlem50.t ${⊢}{T}=\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)$
11 fourierdlem50.n ${⊢}{N}=\left|{T}\right|-1$
12 fourierdlem50.s ${⊢}{S}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)\right)$
13 fourierdlem50.j ${⊢}{\phi }\to {J}\in \left(0..^{N}\right)$
14 fourierdlem50.u ${⊢}{U}=\left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)$
15 fourierdlem50.ch ${⊢}{\chi }↔\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)$
16 5 6 7 ltled ${⊢}{\phi }\to {A}\le {B}$
17 2 3 4 fourierdlem15 ${⊢}{\phi }\to {V}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
18 pire ${⊢}\mathrm{\pi }\in ℝ$
19 18 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
20 19 a1i ${⊢}{\phi }\to -\mathrm{\pi }\in ℝ$
21 20 1 readdcld ${⊢}{\phi }\to -\mathrm{\pi }+{X}\in ℝ$
22 18 a1i ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
23 22 1 readdcld ${⊢}{\phi }\to \mathrm{\pi }+{X}\in ℝ$
24 21 23 iccssred ${⊢}{\phi }\to \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\subseteq ℝ$
25 17 24 fssd ${⊢}{\phi }\to {V}:\left(0\dots {M}\right)⟶ℝ$
26 25 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {V}\left({i}\right)\in ℝ$
27 1 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {X}\in ℝ$
28 26 27 resubcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {V}\left({i}\right)-{X}\in ℝ$
29 28 9 fmptd ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶ℝ$
30 9 a1i ${⊢}{\phi }\to {Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
31 fveq2 ${⊢}{i}=0\to {V}\left({i}\right)={V}\left(0\right)$
32 31 oveq1d ${⊢}{i}=0\to {V}\left({i}\right)-{X}={V}\left(0\right)-{X}$
33 32 adantl ${⊢}\left({\phi }\wedge {i}=0\right)\to {V}\left({i}\right)-{X}={V}\left(0\right)-{X}$
34 nnssnn0 ${⊢}ℕ\subseteq {ℕ}_{0}$
35 34 a1i ${⊢}{\phi }\to ℕ\subseteq {ℕ}_{0}$
36 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
37 35 36 sseqtrdi ${⊢}{\phi }\to ℕ\subseteq {ℤ}_{\ge 0}$
38 37 3 sseldd ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
39 eluzfz1 ${⊢}{M}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {M}\right)$
40 38 39 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
41 25 40 ffvelrnd ${⊢}{\phi }\to {V}\left(0\right)\in ℝ$
42 41 1 resubcld ${⊢}{\phi }\to {V}\left(0\right)-{X}\in ℝ$
43 30 33 40 42 fvmptd ${⊢}{\phi }\to {Q}\left(0\right)={V}\left(0\right)-{X}$
44 2 fourierdlem2 ${⊢}{M}\in ℕ\to \left({V}\in {P}\left({M}\right)↔\left({V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)\right)\right)$
45 3 44 syl ${⊢}{\phi }\to \left({V}\in {P}\left({M}\right)↔\left({V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)\right)\right)$
46 4 45 mpbid ${⊢}{\phi }\to \left({V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)\right)$
47 46 simprd ${⊢}{\phi }\to \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)$
48 47 simpld ${⊢}{\phi }\to \left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)$
49 48 simpld ${⊢}{\phi }\to {V}\left(0\right)=-\mathrm{\pi }+{X}$
50 49 oveq1d ${⊢}{\phi }\to {V}\left(0\right)-{X}=\left(-\mathrm{\pi }\right)+{X}-{X}$
51 20 recnd ${⊢}{\phi }\to -\mathrm{\pi }\in ℂ$
52 1 recnd ${⊢}{\phi }\to {X}\in ℂ$
53 51 52 pncand ${⊢}{\phi }\to \left(-\mathrm{\pi }\right)+{X}-{X}=-\mathrm{\pi }$
54 43 50 53 3eqtrd ${⊢}{\phi }\to {Q}\left(0\right)=-\mathrm{\pi }$
55 20 rexrd ${⊢}{\phi }\to -\mathrm{\pi }\in {ℝ}^{*}$
56 22 rexrd ${⊢}{\phi }\to \mathrm{\pi }\in {ℝ}^{*}$
57 5 leidd ${⊢}{\phi }\to {A}\le {A}$
58 5 6 5 57 16 eliccd ${⊢}{\phi }\to {A}\in \left[{A},{B}\right]$
59 8 58 sseldd ${⊢}{\phi }\to {A}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
60 iccgelb ${⊢}\left(-\mathrm{\pi }\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {A}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to -\mathrm{\pi }\le {A}$
61 55 56 59 60 syl3anc ${⊢}{\phi }\to -\mathrm{\pi }\le {A}$
62 54 61 eqbrtrd ${⊢}{\phi }\to {Q}\left(0\right)\le {A}$
63 6 leidd ${⊢}{\phi }\to {B}\le {B}$
64 5 6 6 16 63 eliccd ${⊢}{\phi }\to {B}\in \left[{A},{B}\right]$
65 8 64 sseldd ${⊢}{\phi }\to {B}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
66 iccleub ${⊢}\left(-\mathrm{\pi }\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {B}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {B}\le \mathrm{\pi }$
67 55 56 65 66 syl3anc ${⊢}{\phi }\to {B}\le \mathrm{\pi }$
68 fveq2 ${⊢}{i}={M}\to {V}\left({i}\right)={V}\left({M}\right)$
69 68 oveq1d ${⊢}{i}={M}\to {V}\left({i}\right)-{X}={V}\left({M}\right)-{X}$
70 69 adantl ${⊢}\left({\phi }\wedge {i}={M}\right)\to {V}\left({i}\right)-{X}={V}\left({M}\right)-{X}$
71 eluzfz2 ${⊢}{M}\in {ℤ}_{\ge 0}\to {M}\in \left(0\dots {M}\right)$
72 38 71 syl ${⊢}{\phi }\to {M}\in \left(0\dots {M}\right)$
73 25 72 ffvelrnd ${⊢}{\phi }\to {V}\left({M}\right)\in ℝ$
74 73 1 resubcld ${⊢}{\phi }\to {V}\left({M}\right)-{X}\in ℝ$
75 30 70 72 74 fvmptd ${⊢}{\phi }\to {Q}\left({M}\right)={V}\left({M}\right)-{X}$
76 48 simprd ${⊢}{\phi }\to {V}\left({M}\right)=\mathrm{\pi }+{X}$
77 76 oveq1d ${⊢}{\phi }\to {V}\left({M}\right)-{X}=\mathrm{\pi }+{X}-{X}$
78 22 recnd ${⊢}{\phi }\to \mathrm{\pi }\in ℂ$
79 78 52 pncand ${⊢}{\phi }\to \mathrm{\pi }+{X}-{X}=\mathrm{\pi }$
80 75 77 79 3eqtrrd ${⊢}{\phi }\to \mathrm{\pi }={Q}\left({M}\right)$
81 67 80 breqtrd ${⊢}{\phi }\to {B}\le {Q}\left({M}\right)$
82 prfi ${⊢}\left\{{A},{B}\right\}\in \mathrm{Fin}$
83 82 a1i ${⊢}{\phi }\to \left\{{A},{B}\right\}\in \mathrm{Fin}$
84 fzfid ${⊢}{\phi }\to \left(0\dots {M}\right)\in \mathrm{Fin}$
85 9 rnmptfi ${⊢}\left(0\dots {M}\right)\in \mathrm{Fin}\to \mathrm{ran}{Q}\in \mathrm{Fin}$
86 84 85 syl ${⊢}{\phi }\to \mathrm{ran}{Q}\in \mathrm{Fin}$
87 infi ${⊢}\mathrm{ran}{Q}\in \mathrm{Fin}\to \mathrm{ran}{Q}\cap \left({A},{B}\right)\in \mathrm{Fin}$
88 86 87 syl ${⊢}{\phi }\to \mathrm{ran}{Q}\cap \left({A},{B}\right)\in \mathrm{Fin}$
89 unfi ${⊢}\left(\left\{{A},{B}\right\}\in \mathrm{Fin}\wedge \mathrm{ran}{Q}\cap \left({A},{B}\right)\in \mathrm{Fin}\right)\to \left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\in \mathrm{Fin}$
90 83 88 89 syl2anc ${⊢}{\phi }\to \left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\in \mathrm{Fin}$
91 10 90 eqeltrid ${⊢}{\phi }\to {T}\in \mathrm{Fin}$
92 5 6 jca ${⊢}{\phi }\to \left({A}\in ℝ\wedge {B}\in ℝ\right)$
93 prssg ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)↔\left\{{A},{B}\right\}\subseteq ℝ\right)$
94 5 6 93 syl2anc ${⊢}{\phi }\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)↔\left\{{A},{B}\right\}\subseteq ℝ\right)$
95 92 94 mpbid ${⊢}{\phi }\to \left\{{A},{B}\right\}\subseteq ℝ$
96 inss2 ${⊢}\mathrm{ran}{Q}\cap \left({A},{B}\right)\subseteq \left({A},{B}\right)$
97 ioossre ${⊢}\left({A},{B}\right)\subseteq ℝ$
98 96 97 sstri ${⊢}\mathrm{ran}{Q}\cap \left({A},{B}\right)\subseteq ℝ$
99 98 a1i ${⊢}{\phi }\to \mathrm{ran}{Q}\cap \left({A},{B}\right)\subseteq ℝ$
100 95 99 unssd ${⊢}{\phi }\to \left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\subseteq ℝ$
101 10 100 eqsstrid ${⊢}{\phi }\to {T}\subseteq ℝ$
102 91 101 12 11 fourierdlem36 ${⊢}{\phi }\to {S}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)$
103 eqid ${⊢}sup\left(\left\{{x}\in \left(0..^{M}\right)|{Q}\left({x}\right)\le {S}\left({J}\right)\right\},ℝ,<\right)=sup\left(\left\{{x}\in \left(0..^{M}\right)|{Q}\left({x}\right)\le {S}\left({J}\right)\right\},ℝ,<\right)$
104 3 5 6 16 29 62 81 13 10 102 103 fourierdlem20 ${⊢}{\phi }\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
105 15 biimpi ${⊢}{\chi }\to \left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)$
106 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to {\phi }$
107 105 106 syl ${⊢}{\chi }\to {\phi }$
108 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to {k}\in \left(0..^{M}\right)$
109 105 108 syl ${⊢}{\chi }\to {k}\in \left(0..^{M}\right)$
110 107 109 jca ${⊢}{\chi }\to \left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)$
111 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to {i}\in \left(0..^{M}\right)$
112 105 111 syl ${⊢}{\chi }\to {i}\in \left(0..^{M}\right)$
113 elfzofz ${⊢}{k}\in \left(0..^{M}\right)\to {k}\in \left(0\dots {M}\right)$
114 113 ad2antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to {k}\in \left(0\dots {M}\right)$
115 105 114 syl ${⊢}{\chi }\to {k}\in \left(0\dots {M}\right)$
116 107 25 syl ${⊢}{\chi }\to {V}:\left(0\dots {M}\right)⟶ℝ$
117 116 115 ffvelrnd ${⊢}{\chi }\to {V}\left({k}\right)\in ℝ$
118 107 1 syl ${⊢}{\chi }\to {X}\in ℝ$
119 117 118 resubcld ${⊢}{\chi }\to {V}\left({k}\right)-{X}\in ℝ$
120 fveq2 ${⊢}{i}={k}\to {V}\left({i}\right)={V}\left({k}\right)$
121 120 oveq1d ${⊢}{i}={k}\to {V}\left({i}\right)-{X}={V}\left({k}\right)-{X}$
122 121 9 fvmptg ${⊢}\left({k}\in \left(0\dots {M}\right)\wedge {V}\left({k}\right)-{X}\in ℝ\right)\to {Q}\left({k}\right)={V}\left({k}\right)-{X}$
123 115 119 122 syl2anc ${⊢}{\chi }\to {Q}\left({k}\right)={V}\left({k}\right)-{X}$
124 123 119 eqeltrd ${⊢}{\chi }\to {Q}\left({k}\right)\in ℝ$
125 29 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
126 fzofzp1 ${⊢}{i}\in \left(0..^{M}\right)\to {i}+1\in \left(0\dots {M}\right)$
127 126 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}+1\in \left(0\dots {M}\right)$
128 125 127 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in ℝ$
129 107 112 128 syl2anc ${⊢}{\chi }\to {Q}\left({i}+1\right)\in ℝ$
130 isof1o ${⊢}{S}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)\to {S}:\left(0\dots {N}\right)\underset{1-1 onto}{⟶}{T}$
131 102 130 syl ${⊢}{\phi }\to {S}:\left(0\dots {N}\right)\underset{1-1 onto}{⟶}{T}$
132 f1of ${⊢}{S}:\left(0\dots {N}\right)\underset{1-1 onto}{⟶}{T}\to {S}:\left(0\dots {N}\right)⟶{T}$
133 131 132 syl ${⊢}{\phi }\to {S}:\left(0\dots {N}\right)⟶{T}$
134 fzofzp1 ${⊢}{J}\in \left(0..^{N}\right)\to {J}+1\in \left(0\dots {N}\right)$
135 13 134 syl ${⊢}{\phi }\to {J}+1\in \left(0\dots {N}\right)$
136 133 135 ffvelrnd ${⊢}{\phi }\to {S}\left({J}+1\right)\in {T}$
137 101 136 sseldd ${⊢}{\phi }\to {S}\left({J}+1\right)\in ℝ$
138 107 137 syl ${⊢}{\chi }\to {S}\left({J}+1\right)\in ℝ$
139 elfzofz ${⊢}{J}\in \left(0..^{N}\right)\to {J}\in \left(0\dots {N}\right)$
140 13 139 syl ${⊢}{\phi }\to {J}\in \left(0\dots {N}\right)$
141 133 140 ffvelrnd ${⊢}{\phi }\to {S}\left({J}\right)\in {T}$
142 101 141 sseldd ${⊢}{\phi }\to {S}\left({J}\right)\in ℝ$
143 107 142 syl ${⊢}{\chi }\to {S}\left({J}\right)\in ℝ$
144 105 simprd ${⊢}{\chi }\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
145 124 rexrd ${⊢}{\chi }\to {Q}\left({k}\right)\in {ℝ}^{*}$
146 29 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
147 fzofzp1 ${⊢}{k}\in \left(0..^{M}\right)\to {k}+1\in \left(0\dots {M}\right)$
148 147 adantl ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {k}+1\in \left(0\dots {M}\right)$
149 146 148 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {Q}\left({k}+1\right)\in ℝ$
150 149 rexrd ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {Q}\left({k}+1\right)\in {ℝ}^{*}$
151 110 150 syl ${⊢}{\chi }\to {Q}\left({k}+1\right)\in {ℝ}^{*}$
152 143 rexrd ${⊢}{\chi }\to {S}\left({J}\right)\in {ℝ}^{*}$
153 138 rexrd ${⊢}{\chi }\to {S}\left({J}+1\right)\in {ℝ}^{*}$
154 elfzoelz ${⊢}{J}\in \left(0..^{N}\right)\to {J}\in ℤ$
155 154 zred ${⊢}{J}\in \left(0..^{N}\right)\to {J}\in ℝ$
156 155 ltp1d ${⊢}{J}\in \left(0..^{N}\right)\to {J}<{J}+1$
157 13 156 syl ${⊢}{\phi }\to {J}<{J}+1$
158 isoeq5 ${⊢}{T}=\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\to \left({S}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)↔{S}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\right)\right)$
159 10 158 ax-mp ${⊢}{S}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)↔{S}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\right)$
160 102 159 sylib ${⊢}{\phi }\to {S}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\right)$
161 isorel ${⊢}\left({S}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{{A},{B}\right\}\cup \left(\mathrm{ran}{Q}\cap \left({A},{B}\right)\right)\right)\wedge \left({J}\in \left(0\dots {N}\right)\wedge {J}+1\in \left(0\dots {N}\right)\right)\right)\to \left({J}<{J}+1↔{S}\left({J}\right)<{S}\left({J}+1\right)\right)$
162 160 140 135 161 syl12anc ${⊢}{\phi }\to \left({J}<{J}+1↔{S}\left({J}\right)<{S}\left({J}+1\right)\right)$
163 157 162 mpbid ${⊢}{\phi }\to {S}\left({J}\right)<{S}\left({J}+1\right)$
164 107 163 syl ${⊢}{\chi }\to {S}\left({J}\right)<{S}\left({J}+1\right)$
165 145 151 152 153 164 ioossioobi ${⊢}{\chi }\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔\left({Q}\left({k}\right)\le {S}\left({J}\right)\wedge {S}\left({J}+1\right)\le {Q}\left({k}+1\right)\right)\right)$
166 144 165 mpbid ${⊢}{\chi }\to \left({Q}\left({k}\right)\le {S}\left({J}\right)\wedge {S}\left({J}+1\right)\le {Q}\left({k}+1\right)\right)$
167 166 simpld ${⊢}{\chi }\to {Q}\left({k}\right)\le {S}\left({J}\right)$
168 124 143 138 167 164 lelttrd ${⊢}{\chi }\to {Q}\left({k}\right)<{S}\left({J}+1\right)$
169 elfzofz ${⊢}{i}\in \left(0..^{M}\right)\to {i}\in \left(0\dots {M}\right)$
170 169 ad2antlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {i}\in \left(0\dots {M}\right)$
171 170 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to {i}\in \left(0\dots {M}\right)$
172 105 171 syl ${⊢}{\chi }\to {i}\in \left(0\dots {M}\right)$
173 107 172 28 syl2anc ${⊢}{\chi }\to {V}\left({i}\right)-{X}\in ℝ$
174 9 fvmpt2 ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {V}\left({i}\right)-{X}\in ℝ\right)\to {Q}\left({i}\right)={V}\left({i}\right)-{X}$
175 172 173 174 syl2anc ${⊢}{\chi }\to {Q}\left({i}\right)={V}\left({i}\right)-{X}$
176 175 173 eqeltrd ${⊢}{\chi }\to {Q}\left({i}\right)\in ℝ$
177 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
178 105 177 syl ${⊢}{\chi }\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
179 176 129 143 138 164 178 fourierdlem10 ${⊢}{\chi }\to \left({Q}\left({i}\right)\le {S}\left({J}\right)\wedge {S}\left({J}+1\right)\le {Q}\left({i}+1\right)\right)$
180 179 simprd ${⊢}{\chi }\to {S}\left({J}+1\right)\le {Q}\left({i}+1\right)$
181 124 138 129 168 180 ltletrd ${⊢}{\chi }\to {Q}\left({k}\right)<{Q}\left({i}+1\right)$
182 124 129 118 181 ltadd2dd ${⊢}{\chi }\to {X}+{Q}\left({k}\right)<{X}+{Q}\left({i}+1\right)$
183 123 oveq2d ${⊢}{\chi }\to {X}+{Q}\left({k}\right)={X}+{V}\left({k}\right)-{X}$
184 107 52 syl ${⊢}{\chi }\to {X}\in ℂ$
185 117 recnd ${⊢}{\chi }\to {V}\left({k}\right)\in ℂ$
186 184 185 pncan3d ${⊢}{\chi }\to {X}+{V}\left({k}\right)-{X}={V}\left({k}\right)$
187 183 186 eqtr2d ${⊢}{\chi }\to {V}\left({k}\right)={X}+{Q}\left({k}\right)$
188 112 126 syl ${⊢}{\chi }\to {i}+1\in \left(0\dots {M}\right)$
189 25 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}:\left(0\dots {M}\right)⟶ℝ$
190 189 127 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}+1\right)\in ℝ$
191 107 112 190 syl2anc ${⊢}{\chi }\to {V}\left({i}+1\right)\in ℝ$
192 191 118 resubcld ${⊢}{\chi }\to {V}\left({i}+1\right)-{X}\in ℝ$
193 188 192 jca ${⊢}{\chi }\to \left({i}+1\in \left(0\dots {M}\right)\wedge {V}\left({i}+1\right)-{X}\in ℝ\right)$
194 eleq1 ${⊢}{k}={i}+1\to \left({k}\in \left(0\dots {M}\right)↔{i}+1\in \left(0\dots {M}\right)\right)$
195 fveq2 ${⊢}{k}={i}+1\to {V}\left({k}\right)={V}\left({i}+1\right)$
196 195 oveq1d ${⊢}{k}={i}+1\to {V}\left({k}\right)-{X}={V}\left({i}+1\right)-{X}$
197 196 eleq1d ${⊢}{k}={i}+1\to \left({V}\left({k}\right)-{X}\in ℝ↔{V}\left({i}+1\right)-{X}\in ℝ\right)$
198 194 197 anbi12d ${⊢}{k}={i}+1\to \left(\left({k}\in \left(0\dots {M}\right)\wedge {V}\left({k}\right)-{X}\in ℝ\right)↔\left({i}+1\in \left(0\dots {M}\right)\wedge {V}\left({i}+1\right)-{X}\in ℝ\right)\right)$
199 fveq2 ${⊢}{k}={i}+1\to {Q}\left({k}\right)={Q}\left({i}+1\right)$
200 199 196 eqeq12d ${⊢}{k}={i}+1\to \left({Q}\left({k}\right)={V}\left({k}\right)-{X}↔{Q}\left({i}+1\right)={V}\left({i}+1\right)-{X}\right)$
201 198 200 imbi12d ${⊢}{k}={i}+1\to \left(\left(\left({k}\in \left(0\dots {M}\right)\wedge {V}\left({k}\right)-{X}\in ℝ\right)\to {Q}\left({k}\right)={V}\left({k}\right)-{X}\right)↔\left(\left({i}+1\in \left(0\dots {M}\right)\wedge {V}\left({i}+1\right)-{X}\in ℝ\right)\to {Q}\left({i}+1\right)={V}\left({i}+1\right)-{X}\right)\right)$
202 201 122 vtoclg ${⊢}{i}+1\in \left(0\dots {M}\right)\to \left(\left({i}+1\in \left(0\dots {M}\right)\wedge {V}\left({i}+1\right)-{X}\in ℝ\right)\to {Q}\left({i}+1\right)={V}\left({i}+1\right)-{X}\right)$
203 188 193 202 sylc ${⊢}{\chi }\to {Q}\left({i}+1\right)={V}\left({i}+1\right)-{X}$
204 203 oveq2d ${⊢}{\chi }\to {X}+{Q}\left({i}+1\right)={X}+{V}\left({i}+1\right)-{X}$
205 191 recnd ${⊢}{\chi }\to {V}\left({i}+1\right)\in ℂ$
206 184 205 pncan3d ${⊢}{\chi }\to {X}+{V}\left({i}+1\right)-{X}={V}\left({i}+1\right)$
207 204 206 eqtr2d ${⊢}{\chi }\to {V}\left({i}+1\right)={X}+{Q}\left({i}+1\right)$
208 182 187 207 3brtr4d ${⊢}{\chi }\to {V}\left({k}\right)<{V}\left({i}+1\right)$
209 eleq1w ${⊢}{l}={i}\to \left({l}\in \left(0..^{M}\right)↔{i}\in \left(0..^{M}\right)\right)$
210 209 anbi2d ${⊢}{l}={i}\to \left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)↔\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\right)$
211 oveq1 ${⊢}{l}={i}\to {l}+1={i}+1$
212 211 fveq2d ${⊢}{l}={i}\to {V}\left({l}+1\right)={V}\left({i}+1\right)$
213 212 breq2d ${⊢}{l}={i}\to \left({V}\left({k}\right)<{V}\left({l}+1\right)↔{V}\left({k}\right)<{V}\left({i}+1\right)\right)$
214 210 213 anbi12d ${⊢}{l}={i}\to \left(\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({l}+1\right)\right)↔\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({i}+1\right)\right)\right)$
215 fveq2 ${⊢}{l}={i}\to {V}\left({l}\right)={V}\left({i}\right)$
216 215 breq2d ${⊢}{l}={i}\to \left({V}\left({k}\right)\le {V}\left({l}\right)↔{V}\left({k}\right)\le {V}\left({i}\right)\right)$
217 214 216 imbi12d ${⊢}{l}={i}\to \left(\left(\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({l}+1\right)\right)\to {V}\left({k}\right)\le {V}\left({l}\right)\right)↔\left(\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({i}+1\right)\right)\to {V}\left({k}\right)\le {V}\left({i}\right)\right)\right)$
218 eleq1w ${⊢}{h}={k}\to \left({h}\in \left(0..^{M}\right)↔{k}\in \left(0..^{M}\right)\right)$
219 218 anbi2d ${⊢}{h}={k}\to \left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)↔\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\right)$
220 219 anbi1d ${⊢}{h}={k}\to \left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)↔\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\right)$
221 fveq2 ${⊢}{h}={k}\to {V}\left({h}\right)={V}\left({k}\right)$
222 221 breq1d ${⊢}{h}={k}\to \left({V}\left({h}\right)<{V}\left({l}+1\right)↔{V}\left({k}\right)<{V}\left({l}+1\right)\right)$
223 220 222 anbi12d ${⊢}{h}={k}\to \left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)↔\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({l}+1\right)\right)\right)$
224 221 breq1d ${⊢}{h}={k}\to \left({V}\left({h}\right)\le {V}\left({l}\right)↔{V}\left({k}\right)\le {V}\left({l}\right)\right)$
225 223 224 imbi12d ${⊢}{h}={k}\to \left(\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {V}\left({h}\right)\le {V}\left({l}\right)\right)↔\left(\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({l}+1\right)\right)\to {V}\left({k}\right)\le {V}\left({l}\right)\right)\right)$
226 elfzoelz ${⊢}{h}\in \left(0..^{M}\right)\to {h}\in ℤ$
227 226 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {h}\in ℤ$
228 elfzoelz ${⊢}{l}\in \left(0..^{M}\right)\to {l}\in ℤ$
229 228 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {l}\in ℤ$
230 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge ¬{h}<{l}+1\right)\to {V}\left({h}\right)<{V}\left({l}+1\right)$
231 25 adantr ${⊢}\left({\phi }\wedge {l}\in \left(0..^{M}\right)\right)\to {V}:\left(0\dots {M}\right)⟶ℝ$
232 fzofzp1 ${⊢}{l}\in \left(0..^{M}\right)\to {l}+1\in \left(0\dots {M}\right)$
233 232 adantl ${⊢}\left({\phi }\wedge {l}\in \left(0..^{M}\right)\right)\to {l}+1\in \left(0\dots {M}\right)$
234 231 233 ffvelrnd ${⊢}\left({\phi }\wedge {l}\in \left(0..^{M}\right)\right)\to {V}\left({l}+1\right)\in ℝ$
235 234 adantlr ${⊢}\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\to {V}\left({l}+1\right)\in ℝ$
236 235 adantr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to {V}\left({l}+1\right)\in ℝ$
237 25 adantr ${⊢}\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\to {V}:\left(0\dots {M}\right)⟶ℝ$
238 elfzofz ${⊢}{h}\in \left(0..^{M}\right)\to {h}\in \left(0\dots {M}\right)$
239 238 adantl ${⊢}\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\to {h}\in \left(0\dots {M}\right)$
240 237 239 ffvelrnd ${⊢}\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\to {V}\left({h}\right)\in ℝ$
241 240 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to {V}\left({h}\right)\in ℝ$
242 228 zred ${⊢}{l}\in \left(0..^{M}\right)\to {l}\in ℝ$
243 peano2re ${⊢}{l}\in ℝ\to {l}+1\in ℝ$
244 242 243 syl ${⊢}{l}\in \left(0..^{M}\right)\to {l}+1\in ℝ$
245 244 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to {l}+1\in ℝ$
246 226 zred ${⊢}{h}\in \left(0..^{M}\right)\to {h}\in ℝ$
247 246 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to {h}\in ℝ$
248 simpr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to ¬{h}<{l}+1$
249 245 247 248 nltled ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to {l}+1\le {h}$
250 228 peano2zd ${⊢}{l}\in \left(0..^{M}\right)\to {l}+1\in ℤ$
251 250 ad2antlr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\to {l}+1\in ℤ$
252 226 ad2antrr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\to {h}\in ℤ$
253 simpr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\to {l}+1\le {h}$
254 eluz2 ${⊢}{h}\in {ℤ}_{\ge \left({l}+1\right)}↔\left({l}+1\in ℤ\wedge {h}\in ℤ\wedge {l}+1\le {h}\right)$
255 251 252 253 254 syl3anbrc ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\to {h}\in {ℤ}_{\ge \left({l}+1\right)}$
256 255 adantlll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\to {h}\in {ℤ}_{\ge \left({l}+1\right)}$
257 simplll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {\phi }$
258 0zd ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to 0\in ℤ$
259 elfzoel2 ${⊢}{h}\in \left(0..^{M}\right)\to {M}\in ℤ$
260 259 ad2antrr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {M}\in ℤ$
261 elfzelz ${⊢}{i}\in \left({l}+1\dots {h}\right)\to {i}\in ℤ$
262 261 adantl ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\in ℤ$
263 258 260 262 3jca ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to \left(0\in ℤ\wedge {M}\in ℤ\wedge {i}\in ℤ\right)$
264 0red ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to 0\in ℝ$
265 261 zred ${⊢}{i}\in \left({l}+1\dots {h}\right)\to {i}\in ℝ$
266 265 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\in ℝ$
267 242 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {l}\in ℝ$
268 elfzole1 ${⊢}{l}\in \left(0..^{M}\right)\to 0\le {l}$
269 268 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to 0\le {l}$
270 267 243 syl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {l}+1\in ℝ$
271 267 ltp1d ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {l}<{l}+1$
272 elfzle1 ${⊢}{i}\in \left({l}+1\dots {h}\right)\to {l}+1\le {i}$
273 272 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {l}+1\le {i}$
274 267 270 266 271 273 ltletrd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {l}<{i}$
275 264 267 266 269 274 lelttrd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to 0<{i}$
276 264 266 275 ltled ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to 0\le {i}$
277 276 adantll ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to 0\le {i}$
278 265 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\in ℝ$
279 259 zred ${⊢}{h}\in \left(0..^{M}\right)\to {M}\in ℝ$
280 279 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {M}\in ℝ$
281 246 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {h}\in ℝ$
282 elfzle2 ${⊢}{i}\in \left({l}+1\dots {h}\right)\to {i}\le {h}$
283 282 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\le {h}$
284 elfzolt2 ${⊢}{h}\in \left(0..^{M}\right)\to {h}<{M}$
285 284 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {h}<{M}$
286 278 281 280 283 285 lelttrd ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}<{M}$
287 278 280 286 ltled ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\le {M}$
288 287 adantlr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\le {M}$
289 263 277 288 jca32 ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to \left(\left(0\in ℤ\wedge {M}\in ℤ\wedge {i}\in ℤ\right)\wedge \left(0\le {i}\wedge {i}\le {M}\right)\right)$
290 elfz2 ${⊢}{i}\in \left(0\dots {M}\right)↔\left(\left(0\in ℤ\wedge {M}\in ℤ\wedge {i}\in ℤ\right)\wedge \left(0\le {i}\wedge {i}\le {M}\right)\right)$
291 289 290 sylibr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\in \left(0\dots {M}\right)$
292 291 adantlll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {i}\in \left(0\dots {M}\right)$
293 257 292 26 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {V}\left({i}\right)\in ℝ$
294 293 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\wedge {i}\in \left({l}+1\dots {h}\right)\right)\to {V}\left({i}\right)\in ℝ$
295 simplll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {\phi }$
296 0zd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to 0\in ℤ$
297 elfzelz ${⊢}{i}\in \left({l}+1\dots {h}-1\right)\to {i}\in ℤ$
298 297 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\in ℤ$
299 0red ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to 0\in ℝ$
300 298 zred ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\in ℝ$
301 242 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {l}\in ℝ$
302 268 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to 0\le {l}$
303 301 243 syl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {l}+1\in ℝ$
304 301 ltp1d ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {l}<{l}+1$
305 elfzle1 ${⊢}{i}\in \left({l}+1\dots {h}-1\right)\to {l}+1\le {i}$
306 305 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {l}+1\le {i}$
307 301 303 300 304 306 ltletrd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {l}<{i}$
308 299 301 300 302 307 lelttrd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to 0<{i}$
309 299 300 308 ltled ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to 0\le {i}$
310 eluz2 ${⊢}{i}\in {ℤ}_{\ge 0}↔\left(0\in ℤ\wedge {i}\in ℤ\wedge 0\le {i}\right)$
311 296 298 309 310 syl3anbrc ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\in {ℤ}_{\ge 0}$
312 311 adantll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\in {ℤ}_{\ge 0}$
313 elfzoel2 ${⊢}{l}\in \left(0..^{M}\right)\to {M}\in ℤ$
314 313 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {M}\in ℤ$
315 297 zred ${⊢}{i}\in \left({l}+1\dots {h}-1\right)\to {i}\in ℝ$
316 315 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\in ℝ$
317 peano2rem ${⊢}{h}\in ℝ\to {h}-1\in ℝ$
318 246 317 syl ${⊢}{h}\in \left(0..^{M}\right)\to {h}-1\in ℝ$
319 318 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {h}-1\in ℝ$
320 279 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {M}\in ℝ$
321 elfzle2 ${⊢}{i}\in \left({l}+1\dots {h}-1\right)\to {i}\le {h}-1$
322 321 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\le {h}-1$
323 246 ltm1d ${⊢}{h}\in \left(0..^{M}\right)\to {h}-1<{h}$
324 318 246 279 323 284 lttrd ${⊢}{h}\in \left(0..^{M}\right)\to {h}-1<{M}$
325 324 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {h}-1<{M}$
326 316 319 320 322 325 lelttrd ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}<{M}$
327 326 adantll ${⊢}\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}<{M}$
328 327 adantlr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}<{M}$
329 elfzo2 ${⊢}{i}\in \left(0..^{M}\right)↔\left({i}\in {ℤ}_{\ge 0}\wedge {M}\in ℤ\wedge {i}<{M}\right)$
330 312 314 328 329 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {i}\in \left(0..^{M}\right)$
331 169 26 sylan2 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)\in ℝ$
332 47 simprd ${⊢}{\phi }\to \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)$
333 332 r19.21bi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)<{V}\left({i}+1\right)$
334 331 190 333 ltled ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)\le {V}\left({i}+1\right)$
335 295 330 334 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {V}\left({i}\right)\le {V}\left({i}+1\right)$
336 335 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\wedge {i}\in \left({l}+1\dots {h}-1\right)\right)\to {V}\left({i}\right)\le {V}\left({i}+1\right)$
337 256 294 336 monoord ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {l}+1\le {h}\right)\to {V}\left({l}+1\right)\le {V}\left({h}\right)$
338 249 337 syldan ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to {V}\left({l}+1\right)\le {V}\left({h}\right)$
339 236 241 338 lensymd ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge ¬{h}<{l}+1\right)\to ¬{V}\left({h}\right)<{V}\left({l}+1\right)$
340 339 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge ¬{h}<{l}+1\right)\to ¬{V}\left({h}\right)<{V}\left({l}+1\right)$
341 230 340 condan ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {h}<{l}+1$
342 zleltp1 ${⊢}\left({h}\in ℤ\wedge {l}\in ℤ\right)\to \left({h}\le {l}↔{h}<{l}+1\right)$
343 227 229 342 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to \left({h}\le {l}↔{h}<{l}+1\right)$
344 341 343 mpbird ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {h}\le {l}$
345 eluz2 ${⊢}{l}\in {ℤ}_{\ge {h}}↔\left({h}\in ℤ\wedge {l}\in ℤ\wedge {h}\le {l}\right)$
346 227 229 344 345 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {l}\in {ℤ}_{\ge {h}}$
347 25 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {V}:\left(0\dots {M}\right)⟶ℝ$
348 0zd ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to 0\in ℤ$
349 259 ad2antrr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {M}\in ℤ$
350 elfzelz ${⊢}{i}\in \left({h}\dots {l}\right)\to {i}\in ℤ$
351 350 adantl ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\in ℤ$
352 348 349 351 3jca ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to \left(0\in ℤ\wedge {M}\in ℤ\wedge {i}\in ℤ\right)$
353 0red ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to 0\in ℝ$
354 246 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {h}\in ℝ$
355 350 zred ${⊢}{i}\in \left({h}\dots {l}\right)\to {i}\in ℝ$
356 355 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\in ℝ$
357 elfzole1 ${⊢}{h}\in \left(0..^{M}\right)\to 0\le {h}$
358 357 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to 0\le {h}$
359 elfzle1 ${⊢}{i}\in \left({h}\dots {l}\right)\to {h}\le {i}$
360 359 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {h}\le {i}$
361 353 354 356 358 360 letrd ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to 0\le {i}$
362 361 adantlr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to 0\le {i}$
363 355 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\in ℝ$
364 313 zred ${⊢}{l}\in \left(0..^{M}\right)\to {M}\in ℝ$
365 364 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {M}\in ℝ$
366 242 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {l}\in ℝ$
367 elfzle2 ${⊢}{i}\in \left({h}\dots {l}\right)\to {i}\le {l}$
368 367 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\le {l}$
369 elfzolt2 ${⊢}{l}\in \left(0..^{M}\right)\to {l}<{M}$
370 369 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {l}<{M}$
371 363 366 365 368 370 lelttrd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}<{M}$
372 363 365 371 ltled ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\le {M}$
373 372 adantll ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\le {M}$
374 352 362 373 jca32 ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to \left(\left(0\in ℤ\wedge {M}\in ℤ\wedge {i}\in ℤ\right)\wedge \left(0\le {i}\wedge {i}\le {M}\right)\right)$
375 374 290 sylibr ${⊢}\left(\left({h}\in \left(0..^{M}\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\in \left(0\dots {M}\right)$
376 375 adantlll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {i}\in \left(0\dots {M}\right)$
377 347 376 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {V}\left({i}\right)\in ℝ$
378 377 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}\right)\right)\to {V}\left({i}\right)\in ℝ$
379 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {\phi }$
380 0zd ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to 0\in ℤ$
381 elfzelz ${⊢}{i}\in \left({h}\dots {l}-1\right)\to {i}\in ℤ$
382 381 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in ℤ$
383 0red ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to 0\in ℝ$
384 246 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {h}\in ℝ$
385 382 zred ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in ℝ$
386 357 adantr ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to 0\le {h}$
387 elfzle1 ${⊢}{i}\in \left({h}\dots {l}-1\right)\to {h}\le {i}$
388 387 adantl ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {h}\le {i}$
389 383 384 385 386 388 letrd ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to 0\le {i}$
390 380 382 389 310 syl3anbrc ${⊢}\left({h}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in {ℤ}_{\ge 0}$
391 390 adantll ${⊢}\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in {ℤ}_{\ge 0}$
392 391 ad4ant14 ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in {ℤ}_{\ge 0}$
393 313 ad3antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {M}\in ℤ$
394 381 zred ${⊢}{i}\in \left({h}\dots {l}-1\right)\to {i}\in ℝ$
395 394 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in ℝ$
396 242 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {l}\in ℝ$
397 364 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {M}\in ℝ$
398 elfzle2 ${⊢}{i}\in \left({h}\dots {l}-1\right)\to {i}\le {l}-1$
399 398 adantl ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\le {l}-1$
400 zltlem1 ${⊢}\left({i}\in ℤ\wedge {l}\in ℤ\right)\to \left({i}<{l}↔{i}\le {l}-1\right)$
401 381 228 400 syl2anr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to \left({i}<{l}↔{i}\le {l}-1\right)$
402 399 401 mpbird ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}<{l}$
403 369 adantr ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {l}<{M}$
404 395 396 397 402 403 lttrd ${⊢}\left({l}\in \left(0..^{M}\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}<{M}$
405 404 adantll ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}<{M}$
406 405 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}<{M}$
407 392 393 406 329 syl3anbrc ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {i}\in \left(0..^{M}\right)$
408 379 407 334 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\wedge {i}\in \left({h}\dots {l}-1\right)\right)\to {V}\left({i}\right)\le {V}\left({i}+1\right)$
409 346 378 408 monoord ${⊢}\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {V}\left({h}\right)\le {V}\left({l}\right)$
410 225 409 chvarvv ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({l}+1\right)\right)\to {V}\left({k}\right)\le {V}\left({l}\right)$
411 217 410 chvarvv ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {V}\left({k}\right)<{V}\left({i}+1\right)\right)\to {V}\left({k}\right)\le {V}\left({i}\right)$
412 110 112 208 411 syl21anc ${⊢}{\chi }\to {V}\left({k}\right)\le {V}\left({i}\right)$
413 107 112 jca ${⊢}{\chi }\to \left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)$
414 110 149 syl ${⊢}{\chi }\to {Q}\left({k}+1\right)\in ℝ$
415 179 simpld ${⊢}{\chi }\to {Q}\left({i}\right)\le {S}\left({J}\right)$
416 176 143 138 415 164 lelttrd ${⊢}{\chi }\to {Q}\left({i}\right)<{S}\left({J}+1\right)$
417 166 simprd ${⊢}{\chi }\to {S}\left({J}+1\right)\le {Q}\left({k}+1\right)$
418 176 138 414 416 417 ltletrd ${⊢}{\chi }\to {Q}\left({i}\right)<{Q}\left({k}+1\right)$
419 176 414 118 418 ltadd2dd ${⊢}{\chi }\to {X}+{Q}\left({i}\right)<{X}+{Q}\left({k}+1\right)$
420 175 oveq2d ${⊢}{\chi }\to {X}+{Q}\left({i}\right)={X}+{V}\left({i}\right)-{X}$
421 107 172 26 syl2anc ${⊢}{\chi }\to {V}\left({i}\right)\in ℝ$
422 421 recnd ${⊢}{\chi }\to {V}\left({i}\right)\in ℂ$
423 184 422 pncan3d ${⊢}{\chi }\to {X}+{V}\left({i}\right)-{X}={V}\left({i}\right)$
424 420 423 eqtr2d ${⊢}{\chi }\to {V}\left({i}\right)={X}+{Q}\left({i}\right)$
425 9 a1i ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
426 fveq2 ${⊢}{i}={k}+1\to {V}\left({i}\right)={V}\left({k}+1\right)$
427 426 oveq1d ${⊢}{i}={k}+1\to {V}\left({i}\right)-{X}={V}\left({k}+1\right)-{X}$
428 427 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\wedge {i}={k}+1\right)\to {V}\left({i}\right)-{X}={V}\left({k}+1\right)-{X}$
429 25 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {V}:\left(0\dots {M}\right)⟶ℝ$
430 429 148 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {V}\left({k}+1\right)\in ℝ$
431 1 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {X}\in ℝ$
432 430 431 resubcld ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {V}\left({k}+1\right)-{X}\in ℝ$
433 425 428 148 432 fvmptd ${⊢}\left({\phi }\wedge {k}\in \left(0..^{M}\right)\right)\to {Q}\left({k}+1\right)={V}\left({k}+1\right)-{X}$
434 107 109 433 syl2anc ${⊢}{\chi }\to {Q}\left({k}+1\right)={V}\left({k}+1\right)-{X}$
435 434 oveq2d ${⊢}{\chi }\to {X}+{Q}\left({k}+1\right)={X}+{V}\left({k}+1\right)-{X}$
436 110 430 syl ${⊢}{\chi }\to {V}\left({k}+1\right)\in ℝ$
437 436 recnd ${⊢}{\chi }\to {V}\left({k}+1\right)\in ℂ$
438 184 437 pncan3d ${⊢}{\chi }\to {X}+{V}\left({k}+1\right)-{X}={V}\left({k}+1\right)$
439 435 438 eqtr2d ${⊢}{\chi }\to {V}\left({k}+1\right)={X}+{Q}\left({k}+1\right)$
440 419 424 439 3brtr4d ${⊢}{\chi }\to {V}\left({i}\right)<{V}\left({k}+1\right)$
441 eleq1w ${⊢}{l}={k}\to \left({l}\in \left(0..^{M}\right)↔{k}\in \left(0..^{M}\right)\right)$
442 441 anbi2d ${⊢}{l}={k}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)↔\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\right)$
443 oveq1 ${⊢}{l}={k}\to {l}+1={k}+1$
444 443 fveq2d ${⊢}{l}={k}\to {V}\left({l}+1\right)={V}\left({k}+1\right)$
445 444 breq2d ${⊢}{l}={k}\to \left({V}\left({i}\right)<{V}\left({l}+1\right)↔{V}\left({i}\right)<{V}\left({k}+1\right)\right)$
446 442 445 anbi12d ${⊢}{l}={k}\to \left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({l}+1\right)\right)↔\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({k}+1\right)\right)\right)$
447 fveq2 ${⊢}{l}={k}\to {V}\left({l}\right)={V}\left({k}\right)$
448 447 breq2d ${⊢}{l}={k}\to \left({V}\left({i}\right)\le {V}\left({l}\right)↔{V}\left({i}\right)\le {V}\left({k}\right)\right)$
449 446 448 imbi12d ${⊢}{l}={k}\to \left(\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({l}+1\right)\right)\to {V}\left({i}\right)\le {V}\left({l}\right)\right)↔\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({k}+1\right)\right)\to {V}\left({i}\right)\le {V}\left({k}\right)\right)\right)$
450 eleq1w ${⊢}{h}={i}\to \left({h}\in \left(0..^{M}\right)↔{i}\in \left(0..^{M}\right)\right)$
451 450 anbi2d ${⊢}{h}={i}\to \left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)↔\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\right)$
452 451 anbi1d ${⊢}{h}={i}\to \left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)↔\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\right)$
453 fveq2 ${⊢}{h}={i}\to {V}\left({h}\right)={V}\left({i}\right)$
454 453 breq1d ${⊢}{h}={i}\to \left({V}\left({h}\right)<{V}\left({l}+1\right)↔{V}\left({i}\right)<{V}\left({l}+1\right)\right)$
455 452 454 anbi12d ${⊢}{h}={i}\to \left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)↔\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({l}+1\right)\right)\right)$
456 453 breq1d ${⊢}{h}={i}\to \left({V}\left({h}\right)\le {V}\left({l}\right)↔{V}\left({i}\right)\le {V}\left({l}\right)\right)$
457 455 456 imbi12d ${⊢}{h}={i}\to \left(\left(\left(\left(\left({\phi }\wedge {h}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({h}\right)<{V}\left({l}+1\right)\right)\to {V}\left({h}\right)\le {V}\left({l}\right)\right)↔\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({l}+1\right)\right)\to {V}\left({i}\right)\le {V}\left({l}\right)\right)\right)$
458 457 409 chvarvv ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {l}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({l}+1\right)\right)\to {V}\left({i}\right)\le {V}\left({l}\right)$
459 449 458 chvarvv ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge {V}\left({i}\right)<{V}\left({k}+1\right)\right)\to {V}\left({i}\right)\le {V}\left({k}\right)$
460 413 109 440 459 syl21anc ${⊢}{\chi }\to {V}\left({i}\right)\le {V}\left({k}\right)$
461 117 421 letri3d ${⊢}{\chi }\to \left({V}\left({k}\right)={V}\left({i}\right)↔\left({V}\left({k}\right)\le {V}\left({i}\right)\wedge {V}\left({i}\right)\le {V}\left({k}\right)\right)\right)$
462 412 460 461 mpbir2and ${⊢}{\chi }\to {V}\left({k}\right)={V}\left({i}\right)$
463 2 3 4 fourierdlem34 ${⊢}{\phi }\to {V}:\left(0\dots {M}\right)\underset{1-1}{⟶}ℝ$
464 107 463 syl ${⊢}{\chi }\to {V}:\left(0\dots {M}\right)\underset{1-1}{⟶}ℝ$
465 f1fveq ${⊢}\left({V}:\left(0\dots {M}\right)\underset{1-1}{⟶}ℝ\wedge \left({k}\in \left(0\dots {M}\right)\wedge {i}\in \left(0\dots {M}\right)\right)\right)\to \left({V}\left({k}\right)={V}\left({i}\right)↔{k}={i}\right)$
466 464 115 172 465 syl12anc ${⊢}{\chi }\to \left({V}\left({k}\right)={V}\left({i}\right)↔{k}={i}\right)$
467 462 466 mpbid ${⊢}{\chi }\to {k}={i}$
468 15 467 sylbir ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)\to {k}={i}$
469 468 ex ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\to {k}={i}\right)$
470 simpl ${⊢}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\wedge {k}={i}\right)\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
471 fveq2 ${⊢}{k}={i}\to {Q}\left({k}\right)={Q}\left({i}\right)$
472 oveq1 ${⊢}{k}={i}\to {k}+1={i}+1$
473 472 fveq2d ${⊢}{k}={i}\to {Q}\left({k}+1\right)={Q}\left({i}+1\right)$
474 471 473 oveq12d ${⊢}{k}={i}\to \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)=\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
475 474 eqcomd ${⊢}{k}={i}\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
476 475 adantl ${⊢}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\wedge {k}={i}\right)\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
477 470 476 sseqtrd ${⊢}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\wedge {k}={i}\right)\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
478 477 ex ${⊢}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\to \left({k}={i}\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)$
479 478 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\to \left({k}={i}\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)$
480 469 479 impbid ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {k}\in \left(0..^{M}\right)\right)\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔{k}={i}\right)$
481 480 ralrimiva ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to \forall {k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔{k}={i}\right)$
482 481 ex ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\to \forall {k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔{k}={i}\right)\right)$
483 482 reximdva ${⊢}{\phi }\to \left(\exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔{k}={i}\right)\right)$
484 104 483 mpd ${⊢}{\phi }\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔{k}={i}\right)$
485 reu6 ${⊢}\exists !{k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔\exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)↔{k}={i}\right)$
486 484 485 sylibr ${⊢}{\phi }\to \exists !{k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
487 fveq2 ${⊢}{i}={k}\to {Q}\left({i}\right)={Q}\left({k}\right)$
488 oveq1 ${⊢}{i}={k}\to {i}+1={k}+1$
489 488 fveq2d ${⊢}{i}={k}\to {Q}\left({i}+1\right)={Q}\left({k}+1\right)$
490 487 489 oveq12d ${⊢}{i}={k}\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
491 490 sseq2d ${⊢}{i}={k}\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)↔\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)\right)$
492 491 cbvreuvw ${⊢}\exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)↔\exists !{k}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({k}\right),{Q}\left({k}+1\right)\right)$
493 486 492 sylibr ${⊢}{\phi }\to \exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
494 riotacl ${⊢}\exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\to \left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\in \left(0..^{M}\right)$
495 493 494 syl ${⊢}{\phi }\to \left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\in \left(0..^{M}\right)$
496 14 495 eqeltrid ${⊢}{\phi }\to {U}\in \left(0..^{M}\right)$
497 14 eqcomi ${⊢}\left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)={U}$
498 497 a1i ${⊢}{\phi }\to \left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)={U}$
499 fveq2 ${⊢}{i}={U}\to {Q}\left({i}\right)={Q}\left({U}\right)$
500 oveq1 ${⊢}{i}={U}\to {i}+1={U}+1$
501 500 fveq2d ${⊢}{i}={U}\to {Q}\left({i}+1\right)={Q}\left({U}+1\right)$
502 499 501 oveq12d ${⊢}{i}={U}\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)$
503 502 sseq2d ${⊢}{i}={U}\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)↔\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)\right)$
504 503 riota2 ${⊢}\left({U}\in \left(0..^{M}\right)\wedge \exists !{i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)↔\left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)={U}\right)$
505 496 493 504 syl2anc ${⊢}{\phi }\to \left(\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)↔\left(\iota {i}\in \left(0..^{M}\right)|\left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)={U}\right)$
506 498 505 mpbird ${⊢}{\phi }\to \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)$
507 496 506 jca ${⊢}{\phi }\to \left({U}\in \left(0..^{M}\right)\wedge \left({S}\left({J}\right),{S}\left({J}+1\right)\right)\subseteq \left({Q}\left({U}\right),{Q}\left({U}+1\right)\right)\right)$