# Metamath Proof Explorer

## Theorem iblspltprt

Description: If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iblspltprt.1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
iblspltprt.2 ${⊢}{\phi }\to {M}\in ℤ$
iblspltprt.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge \left({M}+1\right)}$
iblspltprt.4 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ$
iblspltprt.5 ${⊢}\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
iblspltprt.6 ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]\right)\to {A}\in ℂ$
iblspltprt.7 ${⊢}\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
Assertion iblspltprt ${⊢}{\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]⟼{A}\right)\in {𝐿}^{1}$

### Proof

Step Hyp Ref Expression
1 iblspltprt.1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{\phi }$
2 iblspltprt.2 ${⊢}{\phi }\to {M}\in ℤ$
3 iblspltprt.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge \left({M}+1\right)}$
4 iblspltprt.4 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ$
5 iblspltprt.5 ${⊢}\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
6 iblspltprt.6 ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]\right)\to {A}\in ℂ$
7 iblspltprt.7 ${⊢}\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
8 eluzelz ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}\in ℤ$
9 3 8 syl ${⊢}{\phi }\to {N}\in ℤ$
10 eluzle ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to {M}+1\le {N}$
11 3 10 syl ${⊢}{\phi }\to {M}+1\le {N}$
12 9 zred ${⊢}{\phi }\to {N}\in ℝ$
13 12 leidd ${⊢}{\phi }\to {N}\le {N}$
14 2 peano2zd ${⊢}{\phi }\to {M}+1\in ℤ$
15 elfz1 ${⊢}\left({M}+1\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in \left({M}+1\dots {N}\right)↔\left({N}\in ℤ\wedge {M}+1\le {N}\wedge {N}\le {N}\right)\right)$
16 14 9 15 syl2anc ${⊢}{\phi }\to \left({N}\in \left({M}+1\dots {N}\right)↔\left({N}\in ℤ\wedge {M}+1\le {N}\wedge {N}\le {N}\right)\right)$
17 9 11 13 16 mpbir3and ${⊢}{\phi }\to {N}\in \left({M}+1\dots {N}\right)$
18 fveq2 ${⊢}{j}={M}+1\to {P}\left({j}\right)={P}\left({M}+1\right)$
19 18 oveq2d ${⊢}{j}={M}+1\to \left[{P}\left({M}\right),{P}\left({j}\right)\right]=\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]$
20 19 mpteq1d ${⊢}{j}={M}+1\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)=\left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)$
21 20 eleq1d ${⊢}{j}={M}+1\to \left(\left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}↔\left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
22 21 imbi2d ${⊢}{j}={M}+1\to \left(\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)↔\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
23 fveq2 ${⊢}{j}={k}\to {P}\left({j}\right)={P}\left({k}\right)$
24 23 oveq2d ${⊢}{j}={k}\to \left[{P}\left({M}\right),{P}\left({j}\right)\right]=\left[{P}\left({M}\right),{P}\left({k}\right)\right]$
25 24 mpteq1d ${⊢}{j}={k}\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)=\left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)$
26 25 eleq1d ${⊢}{j}={k}\to \left(\left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}↔\left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
27 26 imbi2d ${⊢}{j}={k}\to \left(\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)↔\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
28 fveq2 ${⊢}{j}={k}+1\to {P}\left({j}\right)={P}\left({k}+1\right)$
29 28 oveq2d ${⊢}{j}={k}+1\to \left[{P}\left({M}\right),{P}\left({j}\right)\right]=\left[{P}\left({M}\right),{P}\left({k}+1\right)\right]$
30 29 mpteq1d ${⊢}{j}={k}+1\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)=\left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]⟼{A}\right)$
31 30 eleq1d ${⊢}{j}={k}+1\to \left(\left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}↔\left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
32 31 imbi2d ${⊢}{j}={k}+1\to \left(\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)↔\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
33 fveq2 ${⊢}{j}={N}\to {P}\left({j}\right)={P}\left({N}\right)$
34 33 oveq2d ${⊢}{j}={N}\to \left[{P}\left({M}\right),{P}\left({j}\right)\right]=\left[{P}\left({M}\right),{P}\left({N}\right)\right]$
35 34 mpteq1d ${⊢}{j}={N}\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)=\left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]⟼{A}\right)$
36 35 eleq1d ${⊢}{j}={N}\to \left(\left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}↔\left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
37 36 imbi2d ${⊢}{j}={N}\to \left(\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({j}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)↔\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
38 uzid ${⊢}{M}\in ℤ\to {M}\in {ℤ}_{\ge {M}}$
39 2 38 syl ${⊢}{\phi }\to {M}\in {ℤ}_{\ge {M}}$
40 2 zred ${⊢}{\phi }\to {M}\in ℝ$
41 1red ${⊢}{\phi }\to 1\in ℝ$
42 40 41 readdcld ${⊢}{\phi }\to {M}+1\in ℝ$
43 40 ltp1d ${⊢}{\phi }\to {M}<{M}+1$
44 40 42 12 43 11 ltletrd ${⊢}{\phi }\to {M}<{N}$
45 elfzo2 ${⊢}{M}\in \left({M}..^{N}\right)↔\left({M}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {M}<{N}\right)$
46 39 9 44 45 syl3anbrc ${⊢}{\phi }\to {M}\in \left({M}..^{N}\right)$
47 fveq2 ${⊢}{i}={M}\to {P}\left({i}\right)={P}\left({M}\right)$
48 fvoveq1 ${⊢}{i}={M}\to {P}\left({i}+1\right)={P}\left({M}+1\right)$
49 47 48 oveq12d ${⊢}{i}={M}\to \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]=\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]$
50 49 mpteq1d ${⊢}{i}={M}\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)=\left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)$
51 50 eleq1d ${⊢}{i}={M}\to \left(\left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}↔\left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
52 51 imbi2d ${⊢}{i}={M}\to \left(\left({\phi }\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)↔\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
53 7 expcom ${⊢}{i}\in \left({M}..^{N}\right)\to \left({\phi }\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
54 52 53 vtoclga ${⊢}{M}\in \left({M}..^{N}\right)\to \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
55 46 54 mpcom ${⊢}{\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
56 55 a1i ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
57 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}{k}\in \left({M}+1..^{N}\right)$
58 nfmpt1 ${⊢}\underset{_}{Ⅎ}{t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)$
59 58 nfel1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}$
60 1 59 nfim ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
61 57 60 1 nf3an ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)$
62 simp3 ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to {\phi }$
63 simp1 ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to {k}\in \left({M}+1..^{N}\right)$
64 40 leidd ${⊢}{\phi }\to {M}\le {M}$
65 40 12 44 ltled ${⊢}{\phi }\to {M}\le {N}$
66 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\in \left({M}\dots {N}\right)↔\left({M}\in ℤ\wedge {M}\le {M}\wedge {M}\le {N}\right)\right)$
67 2 9 66 syl2anc ${⊢}{\phi }\to \left({M}\in \left({M}\dots {N}\right)↔\left({M}\in ℤ\wedge {M}\le {M}\wedge {M}\le {N}\right)\right)$
68 2 64 65 67 mpbir3and ${⊢}{\phi }\to {M}\in \left({M}\dots {N}\right)$
69 68 ancli ${⊢}{\phi }\to \left({\phi }\wedge {M}\in \left({M}\dots {N}\right)\right)$
70 eleq1 ${⊢}{i}={M}\to \left({i}\in \left({M}\dots {N}\right)↔{M}\in \left({M}\dots {N}\right)\right)$
71 70 anbi2d ${⊢}{i}={M}\to \left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)↔\left({\phi }\wedge {M}\in \left({M}\dots {N}\right)\right)\right)$
72 47 eleq1d ${⊢}{i}={M}\to \left({P}\left({i}\right)\in ℝ↔{P}\left({M}\right)\in ℝ\right)$
73 71 72 imbi12d ${⊢}{i}={M}\to \left(\left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ\right)↔\left(\left({\phi }\wedge {M}\in \left({M}\dots {N}\right)\right)\to {P}\left({M}\right)\in ℝ\right)\right)$
74 73 4 vtoclg ${⊢}{M}\in \left({M}\dots {N}\right)\to \left(\left({\phi }\wedge {M}\in \left({M}\dots {N}\right)\right)\to {P}\left({M}\right)\in ℝ\right)$
75 68 69 74 sylc ${⊢}{\phi }\to {P}\left({M}\right)\in ℝ$
76 75 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({M}\right)\in ℝ$
77 76 rexrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({M}\right)\in {ℝ}^{*}$
78 simpl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {\phi }$
79 elfzoelz ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}\in ℤ$
80 79 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in ℤ$
81 40 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\in ℝ$
82 80 zred ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in ℝ$
83 42 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}+1\in ℝ$
84 43 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}<{M}+1$
85 elfzole1 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {M}+1\le {k}$
86 85 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}+1\le {k}$
87 81 83 82 84 86 ltletrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}<{k}$
88 81 82 87 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\le {k}$
89 12 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in ℝ$
90 elfzolt2 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}<{N}$
91 90 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}<{N}$
92 82 89 91 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\le {N}$
93 2 9 jca ${⊢}{\phi }\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
94 93 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
95 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({k}\in \left({M}\dots {N}\right)↔\left({k}\in ℤ\wedge {M}\le {k}\wedge {k}\le {N}\right)\right)$
96 94 95 syl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({k}\in \left({M}\dots {N}\right)↔\left({k}\in ℤ\wedge {M}\le {k}\wedge {k}\le {N}\right)\right)$
97 80 88 92 96 mpbir3and ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in \left({M}\dots {N}\right)$
98 eleq1 ${⊢}{i}={k}\to \left({i}\in \left({M}\dots {N}\right)↔{k}\in \left({M}\dots {N}\right)\right)$
99 98 anbi2d ${⊢}{i}={k}\to \left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)↔\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\right)$
100 fveq2 ${⊢}{i}={k}\to {P}\left({i}\right)={P}\left({k}\right)$
101 100 eleq1d ${⊢}{i}={k}\to \left({P}\left({i}\right)\in ℝ↔{P}\left({k}\right)\in ℝ\right)$
102 99 101 imbi12d ${⊢}{i}={k}\to \left(\left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ\right)↔\left(\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {P}\left({k}\right)\in ℝ\right)\right)$
103 102 4 chvarvv ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {P}\left({k}\right)\in ℝ$
104 78 97 103 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\in ℝ$
105 104 rexrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\in {ℝ}^{*}$
106 80 peano2zd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\in ℤ$
107 106 zred ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\in ℝ$
108 1red ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to 1\in ℝ$
109 81 82 108 87 ltadd1dd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}+1<{k}+1$
110 81 83 107 84 109 lttrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}<{k}+1$
111 81 107 110 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\le {k}+1$
112 zltp1le ${⊢}\left({k}\in ℤ\wedge {N}\in ℤ\right)\to \left({k}<{N}↔{k}+1\le {N}\right)$
113 79 9 112 syl2anr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({k}<{N}↔{k}+1\le {N}\right)$
114 91 113 mpbid ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\le {N}$
115 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({k}+1\in \left({M}\dots {N}\right)↔\left({k}+1\in ℤ\wedge {M}\le {k}+1\wedge {k}+1\le {N}\right)\right)$
116 94 115 syl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({k}+1\in \left({M}\dots {N}\right)↔\left({k}+1\in ℤ\wedge {M}\le {k}+1\wedge {k}+1\le {N}\right)\right)$
117 106 111 114 116 mpbir3and ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\in \left({M}\dots {N}\right)$
118 78 117 jca ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({\phi }\wedge {k}+1\in \left({M}\dots {N}\right)\right)$
119 eleq1 ${⊢}{i}={k}+1\to \left({i}\in \left({M}\dots {N}\right)↔{k}+1\in \left({M}\dots {N}\right)\right)$
120 119 anbi2d ${⊢}{i}={k}+1\to \left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)↔\left({\phi }\wedge {k}+1\in \left({M}\dots {N}\right)\right)\right)$
121 fveq2 ${⊢}{i}={k}+1\to {P}\left({i}\right)={P}\left({k}+1\right)$
122 121 eleq1d ${⊢}{i}={k}+1\to \left({P}\left({i}\right)\in ℝ↔{P}\left({k}+1\right)\in ℝ\right)$
123 120 122 imbi12d ${⊢}{i}={k}+1\to \left(\left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ\right)↔\left(\left({\phi }\wedge {k}+1\in \left({M}\dots {N}\right)\right)\to {P}\left({k}+1\right)\in ℝ\right)\right)$
124 123 4 vtoclg ${⊢}{k}+1\in \left({M}\dots {N}\right)\to \left(\left({\phi }\wedge {k}+1\in \left({M}\dots {N}\right)\right)\to {P}\left({k}+1\right)\in ℝ\right)$
125 117 118 124 sylc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}+1\right)\in ℝ$
126 125 rexrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}+1\right)\in {ℝ}^{*}$
127 eluz ${⊢}\left({M}\in ℤ\wedge {k}\in ℤ\right)\to \left({k}\in {ℤ}_{\ge {M}}↔{M}\le {k}\right)$
128 2 79 127 syl2an ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({k}\in {ℤ}_{\ge {M}}↔{M}\le {k}\right)$
129 88 128 mpbird ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in {ℤ}_{\ge {M}}$
130 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {\phi }$
131 elfzelz ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\in ℤ$
132 131 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\in ℤ$
133 elfzle1 ${⊢}{i}\in \left({M}\dots {k}\right)\to {M}\le {i}$
134 133 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {M}\le {i}$
135 132 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\in ℝ$
136 130 12 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {N}\in ℝ$
137 82 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {k}\in ℝ$
138 elfzle2 ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\le {k}$
139 138 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\le {k}$
140 91 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {k}<{N}$
141 135 137 136 139 140 lelttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}<{N}$
142 135 136 141 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\le {N}$
143 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({i}\in \left({M}\dots {N}\right)↔\left({i}\in ℤ\wedge {M}\le {i}\wedge {i}\le {N}\right)\right)$
144 130 93 143 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to \left({i}\in \left({M}\dots {N}\right)↔\left({i}\in ℤ\wedge {M}\le {i}\wedge {i}\le {N}\right)\right)$
145 132 134 142 144 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\in \left({M}\dots {N}\right)$
146 130 145 4 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {P}\left({i}\right)\in ℝ$
147 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {\phi }$
148 elfzelz ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\in ℤ$
149 148 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\in ℤ$
150 elfzle1 ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {M}\le {i}$
151 150 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {M}\le {i}$
152 149 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\in ℝ$
153 147 12 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {N}\in ℝ$
154 82 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {k}\in ℝ$
155 1red ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to 1\in ℝ$
156 154 155 resubcld ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {k}-1\in ℝ$
157 elfzle2 ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\le {k}-1$
158 157 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\le {k}-1$
159 79 zred ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}\in ℝ$
160 1red ${⊢}{k}\in \left({M}+1..^{N}\right)\to 1\in ℝ$
161 159 160 resubcld ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}-1\in ℝ$
162 elfzoel2 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {N}\in ℤ$
163 162 zred ${⊢}{k}\in \left({M}+1..^{N}\right)\to {N}\in ℝ$
164 159 ltm1d ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}-1<{k}$
165 161 159 163 164 90 lttrd ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}-1<{N}$
166 165 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {k}-1<{N}$
167 152 156 153 158 166 lelttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}<{N}$
168 152 153 167 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\le {N}$
169 147 93 143 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to \left({i}\in \left({M}\dots {N}\right)↔\left({i}\in ℤ\wedge {M}\le {i}\wedge {i}\le {N}\right)\right)$
170 149 151 168 169 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\in \left({M}\dots {N}\right)$
171 147 170 4 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {P}\left({i}\right)\in ℝ$
172 149 peano2zd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}+1\in ℤ$
173 elfzel1 ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {M}\in ℤ$
174 173 zred ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {M}\in ℝ$
175 148 zred ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\in ℝ$
176 1red ${⊢}{i}\in \left({M}\dots {k}-1\right)\to 1\in ℝ$
177 175 176 readdcld ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}+1\in ℝ$
178 175 ltp1d ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}<{i}+1$
179 174 175 177 150 178 lelttrd ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {M}<{i}+1$
180 174 177 179 ltled ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {M}\le {i}+1$
181 180 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {M}\le {i}+1$
182 147 3 8 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {N}\in ℤ$
183 zltp1le ${⊢}\left({i}\in ℤ\wedge {N}\in ℤ\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
184 149 182 183 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
185 167 184 mpbid ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}+1\le {N}$
186 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({i}+1\in \left({M}\dots {N}\right)↔\left({i}+1\in ℤ\wedge {M}\le {i}+1\wedge {i}+1\le {N}\right)\right)$
187 147 93 186 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to \left({i}+1\in \left({M}\dots {N}\right)↔\left({i}+1\in ℤ\wedge {M}\le {i}+1\wedge {i}+1\le {N}\right)\right)$
188 172 181 185 187 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}+1\in \left({M}\dots {N}\right)$
189 147 188 jca ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to \left({\phi }\wedge {i}+1\in \left({M}\dots {N}\right)\right)$
190 eleq1 ${⊢}{k}={i}+1\to \left({k}\in \left({M}\dots {N}\right)↔{i}+1\in \left({M}\dots {N}\right)\right)$
191 190 anbi2d ${⊢}{k}={i}+1\to \left(\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)↔\left({\phi }\wedge {i}+1\in \left({M}\dots {N}\right)\right)\right)$
192 fveq2 ${⊢}{k}={i}+1\to {P}\left({k}\right)={P}\left({i}+1\right)$
193 192 eleq1d ${⊢}{k}={i}+1\to \left({P}\left({k}\right)\in ℝ↔{P}\left({i}+1\right)\in ℝ\right)$
194 191 193 imbi12d ${⊢}{k}={i}+1\to \left(\left(\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {P}\left({k}\right)\in ℝ\right)↔\left(\left({\phi }\wedge {i}+1\in \left({M}\dots {N}\right)\right)\to {P}\left({i}+1\right)\in ℝ\right)\right)$
195 194 103 vtoclg ${⊢}{i}+1\in \left({M}\dots {N}\right)\to \left(\left({\phi }\wedge {i}+1\in \left({M}\dots {N}\right)\right)\to {P}\left({i}+1\right)\in ℝ\right)$
196 188 189 195 sylc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {P}\left({i}+1\right)\in ℝ$
197 elfzuz ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\in {ℤ}_{\ge {M}}$
198 197 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\in {ℤ}_{\ge {M}}$
199 elfzo2 ${⊢}{i}\in \left({M}..^{N}\right)↔\left({i}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {i}<{N}\right)$
200 198 182 167 199 syl3anbrc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}\in \left({M}..^{N}\right)$
201 147 200 5 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
202 171 196 201 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {P}\left({i}\right)\le {P}\left({i}+1\right)$
203 129 146 202 monoord ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({M}\right)\le {P}\left({k}\right)$
204 162 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in ℤ$
205 elfzo2 ${⊢}{k}\in \left({M}..^{N}\right)↔\left({k}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {k}<{N}\right)$
206 129 204 91 205 syl3anbrc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in \left({M}..^{N}\right)$
207 eleq1 ${⊢}{i}={k}\to \left({i}\in \left({M}..^{N}\right)↔{k}\in \left({M}..^{N}\right)\right)$
208 207 anbi2d ${⊢}{i}={k}\to \left(\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)↔\left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)\right)$
209 fvoveq1 ${⊢}{i}={k}\to {P}\left({i}+1\right)={P}\left({k}+1\right)$
210 100 209 breq12d ${⊢}{i}={k}\to \left({P}\left({i}\right)<{P}\left({i}+1\right)↔{P}\left({k}\right)<{P}\left({k}+1\right)\right)$
211 208 210 imbi12d ${⊢}{i}={k}\to \left(\left(\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)\right)↔\left(\left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)\to {P}\left({k}\right)<{P}\left({k}+1\right)\right)\right)$
212 211 5 chvarvv ${⊢}\left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)\to {P}\left({k}\right)<{P}\left({k}+1\right)$
213 78 206 212 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)<{P}\left({k}+1\right)$
214 104 125 213 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\le {P}\left({k}+1\right)$
215 iccintsng ${⊢}\left(\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({k}\right)\in {ℝ}^{*}\wedge {P}\left({k}+1\right)\in {ℝ}^{*}\right)\wedge \left({P}\left({M}\right)\le {P}\left({k}\right)\wedge {P}\left({k}\right)\le {P}\left({k}+1\right)\right)\right)\to \left[{P}\left({M}\right),{P}\left({k}\right)\right]\cap \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]=\left\{{P}\left({k}\right)\right\}$
216 77 105 126 203 214 215 syl32anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left[{P}\left({M}\right),{P}\left({k}\right)\right]\cap \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]=\left\{{P}\left({k}\right)\right\}$
217 216 fveq2d ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {vol}^{*}\left(\left[{P}\left({M}\right),{P}\left({k}\right)\right]\cap \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]\right)={vol}^{*}\left(\left\{{P}\left({k}\right)\right\}\right)$
218 ovolsn ${⊢}{P}\left({k}\right)\in ℝ\to {vol}^{*}\left(\left\{{P}\left({k}\right)\right\}\right)=0$
219 104 218 syl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {vol}^{*}\left(\left\{{P}\left({k}\right)\right\}\right)=0$
220 217 219 eqtrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {vol}^{*}\left(\left[{P}\left({M}\right),{P}\left({k}\right)\right]\cap \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]\right)=0$
221 62 63 220 syl2anc ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to {vol}^{*}\left(\left[{P}\left({M}\right),{P}\left({k}\right)\right]\cap \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]\right)=0$
222 76 125 104 203 214 eliccd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]$
223 76 125 222 3jca ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\wedge {P}\left({k}\right)\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)$
224 62 63 223 syl2anc ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\wedge {P}\left({k}\right)\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)$
225 iccsplit ${⊢}\left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\wedge {P}\left({k}\right)\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]=\left[{P}\left({M}\right),{P}\left({k}\right)\right]\cup \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]$
226 224 225 syl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]=\left[{P}\left({M}\right),{P}\left({k}\right)\right]\cup \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]$
227 simpl3 ${⊢}\left(\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {\phi }$
228 simpl1 ${⊢}\left(\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {k}\in \left({M}+1..^{N}\right)$
229 simpr ${⊢}\left(\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]$
230 simp1 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {\phi }$
231 eliccxr ${⊢}{t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\to {t}\in {ℝ}^{*}$
232 231 3ad2ant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in {ℝ}^{*}$
233 75 rexrd ${⊢}{\phi }\to {P}\left({M}\right)\in {ℝ}^{*}$
234 233 3ad2ant1 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({M}\right)\in {ℝ}^{*}$
235 126 3adant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({k}+1\right)\in {ℝ}^{*}$
236 simp3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]$
237 iccgelb ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({k}+1\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({M}\right)\le {t}$
238 234 235 236 237 syl3anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({M}\right)\le {t}$
239 76 125 jca ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\right)$
240 239 3adant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to \left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\right)$
241 iccssre ${⊢}\left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\right)\to \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\subseteq ℝ$
242 241 sseld ${⊢}\left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}+1\right)\in ℝ\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\to {t}\in ℝ\right)$
243 240 236 242 sylc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in ℝ$
244 125 3adant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({k}+1\right)\in ℝ$
245 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in \left({M}\dots {N}\right)↔\left({N}\in ℤ\wedge {M}\le {N}\wedge {N}\le {N}\right)\right)$
246 2 9 245 syl2anc ${⊢}{\phi }\to \left({N}\in \left({M}\dots {N}\right)↔\left({N}\in ℤ\wedge {M}\le {N}\wedge {N}\le {N}\right)\right)$
247 9 65 13 246 mpbir3and ${⊢}{\phi }\to {N}\in \left({M}\dots {N}\right)$
248 247 ancli ${⊢}{\phi }\to \left({\phi }\wedge {N}\in \left({M}\dots {N}\right)\right)$
249 eleq1 ${⊢}{i}={N}\to \left({i}\in \left({M}\dots {N}\right)↔{N}\in \left({M}\dots {N}\right)\right)$
250 249 anbi2d ${⊢}{i}={N}\to \left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)↔\left({\phi }\wedge {N}\in \left({M}\dots {N}\right)\right)\right)$
251 fveq2 ${⊢}{i}={N}\to {P}\left({i}\right)={P}\left({N}\right)$
252 251 eleq1d ${⊢}{i}={N}\to \left({P}\left({i}\right)\in ℝ↔{P}\left({N}\right)\in ℝ\right)$
253 250 252 imbi12d ${⊢}{i}={N}\to \left(\left(\left({\phi }\wedge {i}\in \left({M}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ\right)↔\left(\left({\phi }\wedge {N}\in \left({M}\dots {N}\right)\right)\to {P}\left({N}\right)\in ℝ\right)\right)$
254 253 4 vtoclg ${⊢}{N}\in ℤ\to \left(\left({\phi }\wedge {N}\in \left({M}\dots {N}\right)\right)\to {P}\left({N}\right)\in ℝ\right)$
255 9 248 254 sylc ${⊢}{\phi }\to {P}\left({N}\right)\in ℝ$
256 255 3ad2ant1 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({N}\right)\in ℝ$
257 elicc1 ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({k}+1\right)\in {ℝ}^{*}\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]↔\left({t}\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {t}\wedge {t}\le {P}\left({k}+1\right)\right)\right)$
258 234 235 257 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]↔\left({t}\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {t}\wedge {t}\le {P}\left({k}+1\right)\right)\right)$
259 236 258 mpbid ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to \left({t}\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {t}\wedge {t}\le {P}\left({k}+1\right)\right)$
260 259 simp3d ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\le {P}\left({k}+1\right)$
261 elfzop1le2 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}+1\le {N}$
262 79 peano2zd ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}+1\in ℤ$
263 eluz ${⊢}\left({k}+1\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge \left({k}+1\right)}↔{k}+1\le {N}\right)$
264 262 162 263 syl2anc ${⊢}{k}\in \left({M}+1..^{N}\right)\to \left({N}\in {ℤ}_{\ge \left({k}+1\right)}↔{k}+1\le {N}\right)$
265 261 264 mpbird ${⊢}{k}\in \left({M}+1..^{N}\right)\to {N}\in {ℤ}_{\ge \left({k}+1\right)}$
266 265 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in {ℤ}_{\ge \left({k}+1\right)}$
267 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {\phi }$
268 elfzelz ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {i}\in ℤ$
269 268 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {i}\in ℤ$
270 267 40 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {M}\in ℝ$
271 269 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {i}\in ℝ$
272 82 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}\in ℝ$
273 87 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {M}<{k}$
274 159 adantr ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}\in ℝ$
275 1red ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to 1\in ℝ$
276 274 275 readdcld ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}+1\in ℝ$
277 268 zred ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {i}\in ℝ$
278 277 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {i}\in ℝ$
279 274 ltp1d ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}<{k}+1$
280 elfzle1 ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {k}+1\le {i}$
281 280 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}+1\le {i}$
282 274 276 278 279 281 ltletrd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}<{i}$
283 282 adantll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}<{i}$
284 270 272 271 273 283 lttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {M}<{i}$
285 270 271 284 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {M}\le {i}$
286 elfzle2 ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {i}\le {N}$
287 286 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {i}\le {N}$
288 267 93 143 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to \left({i}\in \left({M}\dots {N}\right)↔\left({i}\in ℤ\wedge {M}\le {i}\wedge {i}\le {N}\right)\right)$
289 269 285 287 288 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {i}\in \left({M}\dots {N}\right)$
290 267 289 4 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ$
291 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {\phi }$
292 elfzelz ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {i}\in ℤ$
293 292 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in ℤ$
294 291 40 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}\in ℝ$
295 293 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
296 82 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}\in ℝ$
297 87 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}<{k}$
298 159 adantr ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}\in ℝ$
299 1red ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to 1\in ℝ$
300 298 299 readdcld ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}+1\in ℝ$
301 292 zred ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {i}\in ℝ$
302 301 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
303 298 ltp1d ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{k}+1$
304 elfzle1 ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {k}+1\le {i}$
305 304 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}+1\le {i}$
306 298 300 302 303 305 ltletrd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{i}$
307 306 adantll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{i}$
308 294 296 295 297 307 lttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}<{i}$
309 294 295 308 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}\le {i}$
310 301 adantl ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
311 12 adantr ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}\in ℝ$
312 1red ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to 1\in ℝ$
313 311 312 resubcld ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}-1\in ℝ$
314 elfzle2 ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {i}\le {N}-1$
315 314 adantl ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\le {N}-1$
316 311 ltm1d ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}-1<{N}$
317 310 313 311 315 316 lelttrd ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}<{N}$
318 310 311 317 ltled ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\le {N}$
319 318 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\le {N}$
320 291 93 143 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to \left({i}\in \left({M}\dots {N}\right)↔\left({i}\in ℤ\wedge {M}\le {i}\wedge {i}\le {N}\right)\right)$
321 293 309 319 320 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in \left({M}\dots {N}\right)$
322 291 321 4 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {P}\left({i}\right)\in ℝ$
323 293 peano2zd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}+1\in ℤ$
324 323 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}+1\in ℝ$
325 302 299 readdcld ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}+1\in ℝ$
326 298 302 306 ltled ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}\le {i}$
327 298 302 299 326 leadd1dd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}+1\le {i}+1$
328 298 300 325 303 327 ltletrd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{i}+1$
329 328 adantll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{i}+1$
330 294 296 324 297 329 lttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}<{i}+1$
331 294 324 330 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}\le {i}+1$
332 292 9 183 syl2anr ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
333 317 332 mpbid ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}+1\le {N}$
334 333 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}+1\le {N}$
335 291 93 186 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to \left({i}+1\in \left({M}\dots {N}\right)↔\left({i}+1\in ℤ\wedge {M}\le {i}+1\wedge {i}+1\le {N}\right)\right)$
336 323 331 334 335 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}+1\in \left({M}\dots {N}\right)$
337 291 336 jca ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to \left({\phi }\wedge {i}+1\in \left({M}\dots {N}\right)\right)$
338 336 337 195 sylc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {P}\left({i}+1\right)\in ℝ$
339 291 2 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {M}\in ℤ$
340 eluz ${⊢}\left({M}\in ℤ\wedge {i}\in ℤ\right)\to \left({i}\in {ℤ}_{\ge {M}}↔{M}\le {i}\right)$
341 339 293 340 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to \left({i}\in {ℤ}_{\ge {M}}↔{M}\le {i}\right)$
342 309 341 mpbird ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in {ℤ}_{\ge {M}}$
343 291 3 8 3syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}\in ℤ$
344 317 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}<{N}$
345 342 343 344 199 syl3anbrc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in \left({M}..^{N}\right)$
346 291 345 5 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
347 322 338 346 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {P}\left({i}\right)\le {P}\left({i}+1\right)$
348 266 290 347 monoord ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}+1\right)\le {P}\left({N}\right)$
349 348 3adant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({k}+1\right)\le {P}\left({N}\right)$
350 243 244 256 260 349 letrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\le {P}\left({N}\right)$
351 256 rexrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({N}\right)\in {ℝ}^{*}$
352 elicc1 ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({N}\right)\in {ℝ}^{*}\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]↔\left({t}\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {t}\wedge {t}\le {P}\left({N}\right)\right)\right)$
353 234 351 352 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]↔\left({t}\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {t}\wedge {t}\le {P}\left({N}\right)\right)\right)$
354 232 238 350 353 mpbir3and ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]$
355 230 354 6 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {A}\in ℂ$
356 227 228 229 355 syl3anc ${⊢}\left(\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {A}\in ℂ$
357 simp2 ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
358 62 357 mpd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}$
359 62 63 jca ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)$
360 78 206 jca ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)$
361 100 209 oveq12d ${⊢}{i}={k}\to \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]=\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]$
362 361 mpteq1d ${⊢}{i}={k}\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)=\left({t}\in \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]⟼{A}\right)$
363 362 eleq1d ${⊢}{i}={k}\to \left(\left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}↔\left({t}\in \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
364 208 363 imbi12d ${⊢}{i}={k}\to \left(\left(\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)↔\left(\left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
365 364 7 chvarvv ${⊢}\left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
366 359 360 365 3syl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left({t}\in \left[{P}\left({k}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
367 61 221 226 356 358 366 iblsplitf ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\wedge {\phi }\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
368 367 3exp ${⊢}{k}\in \left({M}+1..^{N}\right)\to \left(\left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\to \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
369 22 27 32 37 56 368 fzind2 ${⊢}{N}\in \left({M}+1\dots {N}\right)\to \left({\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
370 17 369 mpcom ${⊢}{\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]⟼{A}\right)\in {𝐿}^{1}$