# Metamath Proof Explorer

## Theorem itgspltprt

Description: The S. integral splits on a given partition P . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgspltprt.1 ${⊢}{\phi }\to {M}\in ℤ$
itgspltprt.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge \left({M}+1\right)}$
itgspltprt.3 ${⊢}{\phi }\to {P}:\left({M}\dots {N}\right)⟶ℝ$
itgspltprt.4 ${⊢}\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
itgspltprt.5 ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]\right)\to {A}\in ℂ$
itgspltprt.6 ${⊢}\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 itgspltprt ${⊢}{\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({N}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{N}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$

### Proof

Step Hyp Ref Expression
1 itgspltprt.1 ${⊢}{\phi }\to {M}\in ℤ$
2 itgspltprt.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge \left({M}+1\right)}$
3 itgspltprt.3 ${⊢}{\phi }\to {P}:\left({M}\dots {N}\right)⟶ℝ$
4 itgspltprt.4 ${⊢}\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
5 itgspltprt.5 ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]\right)\to {A}\in ℂ$
6 itgspltprt.6 ${⊢}\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}$
7 1 peano2zd ${⊢}{\phi }\to {M}+1\in ℤ$
8 eluzelz ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}\in ℤ$
9 2 8 syl ${⊢}{\phi }\to {N}\in ℤ$
10 7 9 9 3jca ${⊢}{\phi }\to \left({M}+1\in ℤ\wedge {N}\in ℤ\wedge {N}\in ℤ\right)$
11 eluzle ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to {M}+1\le {N}$
12 2 11 syl ${⊢}{\phi }\to {M}+1\le {N}$
13 eluzelre ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}\in ℝ$
14 2 13 syl ${⊢}{\phi }\to {N}\in ℝ$
15 14 leidd ${⊢}{\phi }\to {N}\le {N}$
16 10 12 15 jca32 ${⊢}{\phi }\to \left(\left({M}+1\in ℤ\wedge {N}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}+1\le {N}\wedge {N}\le {N}\right)\right)$
17 elfz2 ${⊢}{N}\in \left({M}+1\dots {N}\right)↔\left(\left({M}+1\in ℤ\wedge {N}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}+1\le {N}\wedge {N}\le {N}\right)\right)$
18 16 17 sylibr ${⊢}{\phi }\to {N}\in \left({M}+1\dots {N}\right)$
19 fveq2 ${⊢}{j}={M}+1\to {P}\left({j}\right)={P}\left({M}+1\right)$
20 19 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]$
21 20 itgeq1d ${⊢}{j}={M}+1\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}$
22 oveq2 ${⊢}{j}={M}+1\to \left({M}..^{j}\right)=\left({M}..^{M}+1\right)$
23 22 sumeq1d ${⊢}{j}={M}+1\to \sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{M}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
24 21 23 eqeq12d ${⊢}{j}={M}+1\to \left({\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}↔{\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{M}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)$
25 24 imbi2d ${⊢}{j}={M}+1\to \left(\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)↔\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{M}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\right)$
26 fveq2 ${⊢}{j}={k}\to {P}\left({j}\right)={P}\left({k}\right)$
27 26 oveq2d ${⊢}{j}={k}\to \left[{P}\left({M}\right),{P}\left({j}\right)\right]=\left[{P}\left({M}\right),{P}\left({k}\right)\right]$
28 27 itgeq1d ${⊢}{j}={k}\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}$
29 oveq2 ${⊢}{j}={k}\to \left({M}..^{j}\right)=\left({M}..^{k}\right)$
30 29 sumeq1d ${⊢}{j}={k}\to \sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
31 28 30 eqeq12d ${⊢}{j}={k}\to \left({\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}↔{\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)$
32 31 imbi2d ${⊢}{j}={k}\to \left(\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)↔\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\right)$
33 fveq2 ${⊢}{j}={k}+1\to {P}\left({j}\right)={P}\left({k}+1\right)$
34 33 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]$
35 34 itgeq1d ${⊢}{j}={k}+1\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
36 oveq2 ${⊢}{j}={k}+1\to \left({M}..^{j}\right)=\left({M}..^{k}+1\right)$
37 36 sumeq1d ${⊢}{j}={k}+1\to \sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
38 35 37 eqeq12d ${⊢}{j}={k}+1\to \left({\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}↔{\int }_{\left[{P}\left({M}\right),{P}\left({k}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)$
39 38 imbi2d ${⊢}{j}={k}+1\to \left(\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)↔\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\right)$
40 fveq2 ${⊢}{j}={N}\to {P}\left({j}\right)={P}\left({N}\right)$
41 40 oveq2d ${⊢}{j}={N}\to \left[{P}\left({M}\right),{P}\left({j}\right)\right]=\left[{P}\left({M}\right),{P}\left({N}\right)\right]$
42 41 itgeq1d ${⊢}{j}={N}\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({N}\right)\right]}{A}d{t}$
43 oveq2 ${⊢}{j}={N}\to \left({M}..^{j}\right)=\left({M}..^{N}\right)$
44 43 sumeq1d ${⊢}{j}={N}\to \sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{N}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
45 42 44 eqeq12d ${⊢}{j}={N}\to \left({\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}↔{\int }_{\left[{P}\left({M}\right),{P}\left({N}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{N}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)$
46 45 imbi2d ${⊢}{j}={N}\to \left(\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({j}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{j}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)↔\left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({N}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{N}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\right)$
47 1 adantl ${⊢}\left({N}\in {ℤ}_{\ge \left({M}+1\right)}\wedge {\phi }\right)\to {M}\in ℤ$
48 fzval3 ${⊢}{M}\in ℤ\to \left({M}\dots {M}\right)=\left({M}..^{M}+1\right)$
49 47 48 syl ${⊢}\left({N}\in {ℤ}_{\ge \left({M}+1\right)}\wedge {\phi }\right)\to \left({M}\dots {M}\right)=\left({M}..^{M}+1\right)$
50 49 eqcomd ${⊢}\left({N}\in {ℤ}_{\ge \left({M}+1\right)}\wedge {\phi }\right)\to \left({M}..^{M}+1\right)=\left({M}\dots {M}\right)$
51 50 sumeq1d ${⊢}\left({N}\in {ℤ}_{\ge \left({M}+1\right)}\wedge {\phi }\right)\to \sum _{{i}\in \left({M}..^{M}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}={M}}^{{M}}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
52 3 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
53 1 zred ${⊢}{\phi }\to {M}\in ℝ$
54 1red ${⊢}{\phi }\to 1\in ℝ$
55 53 54 readdcld ${⊢}{\phi }\to {M}+1\in ℝ$
56 53 ltp1d ${⊢}{\phi }\to {M}<{M}+1$
57 53 55 14 56 12 ltletrd ${⊢}{\phi }\to {M}<{N}$
58 53 14 57 ltled ${⊢}{\phi }\to {M}\le {N}$
59 eluz ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge {M}}↔{M}\le {N}\right)$
60 1 9 59 syl2anc ${⊢}{\phi }\to \left({N}\in {ℤ}_{\ge {M}}↔{M}\le {N}\right)$
61 58 60 mpbird ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
62 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in \left({M}\dots {N}\right)$
63 61 62 syl ${⊢}{\phi }\to {M}\in \left({M}\dots {N}\right)$
64 63 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {M}\in \left({M}\dots {N}\right)$
65 52 64 ffvelrnd ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}\right)\in ℝ$
66 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)$
67 1 9 66 syl2anc ${⊢}{\phi }\to \left({N}\in \left({M}\dots {N}\right)↔\left({N}\in ℤ\wedge {M}\le {N}\wedge {N}\le {N}\right)\right)$
68 9 58 15 67 mpbir3and ${⊢}{\phi }\to {N}\in \left({M}\dots {N}\right)$
69 3 68 ffvelrnd ${⊢}{\phi }\to {P}\left({N}\right)\in ℝ$
70 69 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({N}\right)\in ℝ$
71 53 lep1d ${⊢}{\phi }\to {M}\le {M}+1$
72 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}+1\in \left({M}\dots {N}\right)↔\left({M}+1\in ℤ\wedge {M}\le {M}+1\wedge {M}+1\le {N}\right)\right)$
73 1 9 72 syl2anc ${⊢}{\phi }\to \left({M}+1\in \left({M}\dots {N}\right)↔\left({M}+1\in ℤ\wedge {M}\le {M}+1\wedge {M}+1\le {N}\right)\right)$
74 7 71 12 73 mpbir3and ${⊢}{\phi }\to {M}+1\in \left({M}\dots {N}\right)$
75 3 74 ffvelrnd ${⊢}{\phi }\to {P}\left({M}+1\right)\in ℝ$
76 75 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}+1\right)\in ℝ$
77 simpr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]$
78 eliccre ${⊢}\left({P}\left({M}\right)\in ℝ\wedge {P}\left({M}+1\right)\in ℝ\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\in ℝ$
79 65 76 77 78 syl3anc ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\in ℝ$
80 3 63 ffvelrnd ${⊢}{\phi }\to {P}\left({M}\right)\in ℝ$
81 80 rexrd ${⊢}{\phi }\to {P}\left({M}\right)\in {ℝ}^{*}$
82 81 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}\right)\in {ℝ}^{*}$
83 76 rexrd ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}+1\right)\in {ℝ}^{*}$
84 iccgelb ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({M}+1\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}\right)\le {t}$
85 82 83 77 84 syl3anc ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}\right)\le {t}$
86 iccleub ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({M}+1\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\le {P}\left({M}+1\right)$
87 82 83 77 86 syl3anc ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\le {P}\left({M}+1\right)$
88 3 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
89 elfzelz ${⊢}{i}\in \left({M}+1\dots {N}\right)\to {i}\in ℤ$
90 89 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {i}\in ℤ$
91 53 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {M}\in ℝ$
92 90 zred ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {i}\in ℝ$
93 55 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {M}+1\in ℝ$
94 56 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {M}<{M}+1$
95 elfzle1 ${⊢}{i}\in \left({M}+1\dots {N}\right)\to {M}+1\le {i}$
96 95 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {M}+1\le {i}$
97 91 93 92 94 96 ltletrd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {M}<{i}$
98 91 92 97 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {M}\le {i}$
99 elfzle2 ${⊢}{i}\in \left({M}+1\dots {N}\right)\to {i}\le {N}$
100 99 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {i}\le {N}$
101 1 9 jca ${⊢}{\phi }\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
102 101 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
103 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)$
104 102 103 syl ${⊢}\left({\phi }\wedge {i}\in \left({M}+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)$
105 90 98 100 104 mpbir3and ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {i}\in \left({M}\dots {N}\right)$
106 88 105 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ$
107 3 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
108 elfzelz ${⊢}{i}\in \left({M}+1\dots {N}-1\right)\to {i}\in ℤ$
109 108 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\in ℤ$
110 53 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}\in ℝ$
111 109 zred ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
112 55 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}+1\in ℝ$
113 56 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}<{M}+1$
114 elfzle1 ${⊢}{i}\in \left({M}+1\dots {N}-1\right)\to {M}+1\le {i}$
115 114 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}+1\le {i}$
116 110 112 111 113 115 ltletrd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}<{i}$
117 110 111 116 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}\le {i}$
118 14 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {N}\in ℝ$
119 1red ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to 1\in ℝ$
120 118 119 resubcld ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {N}-1\in ℝ$
121 elfzle2 ${⊢}{i}\in \left({M}+1\dots {N}-1\right)\to {i}\le {N}-1$
122 121 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\le {N}-1$
123 118 ltm1d ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {N}-1<{N}$
124 111 120 118 122 123 lelttrd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}<{N}$
125 111 118 124 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\le {N}$
126 101 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
127 126 103 syl ${⊢}\left({\phi }\wedge {i}\in \left({M}+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)$
128 109 117 125 127 mpbir3and ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\in \left({M}\dots {N}\right)$
129 107 128 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {P}\left({i}\right)\in ℝ$
130 109 peano2zd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}+1\in ℤ$
131 111 119 readdcld ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}+1\in ℝ$
132 110 111 119 116 ltadd1dd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}+1<{i}+1$
133 110 112 131 113 132 lttrd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}<{i}+1$
134 110 131 133 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {M}\le {i}+1$
135 zltp1le ${⊢}\left({i}\in ℤ\wedge {N}\in ℤ\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
136 108 9 135 syl2anr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
137 124 136 mpbid ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}+1\le {N}$
138 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)$
139 126 138 syl ${⊢}\left({\phi }\wedge {i}\in \left({M}+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)$
140 130 134 137 139 mpbir3and ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}+1\in \left({M}\dots {N}\right)$
141 107 140 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {P}\left({i}+1\right)\in ℝ$
142 eluz ${⊢}\left({M}\in ℤ\wedge {i}\in ℤ\right)\to \left({i}\in {ℤ}_{\ge {M}}↔{M}\le {i}\right)$
143 1 108 142 syl2an ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to \left({i}\in {ℤ}_{\ge {M}}↔{M}\le {i}\right)$
144 117 143 mpbird ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\in {ℤ}_{\ge {M}}$
145 9 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {N}\in ℤ$
146 elfzo2 ${⊢}{i}\in \left({M}..^{N}\right)↔\left({i}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {i}<{N}\right)$
147 144 145 124 146 syl3anbrc ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {i}\in \left({M}..^{N}\right)$
148 147 4 syldan ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
149 129 141 148 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}+1\dots {N}-1\right)\right)\to {P}\left({i}\right)\le {P}\left({i}+1\right)$
150 2 106 149 monoord ${⊢}{\phi }\to {P}\left({M}+1\right)\le {P}\left({N}\right)$
151 150 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {P}\left({M}+1\right)\le {P}\left({N}\right)$
152 79 76 70 87 151 letrd ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\le {P}\left({N}\right)$
153 65 70 79 85 152 eliccd ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]$
154 153 5 syldan ${⊢}\left({\phi }\wedge {t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]\right)\to {A}\in ℂ$
155 id ${⊢}{\phi }\to {\phi }$
156 fzolb ${⊢}{M}\in \left({M}..^{N}\right)↔\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}<{N}\right)$
157 1 9 57 156 syl3anbrc ${⊢}{\phi }\to {M}\in \left({M}..^{N}\right)$
158 155 157 jca ${⊢}{\phi }\to \left({\phi }\wedge {M}\in \left({M}..^{N}\right)\right)$
159 eleq1 ${⊢}{i}={M}\to \left({i}\in \left({M}..^{N}\right)↔{M}\in \left({M}..^{N}\right)\right)$
160 159 anbi2d ${⊢}{i}={M}\to \left(\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)↔\left({\phi }\wedge {M}\in \left({M}..^{N}\right)\right)\right)$
161 fveq2 ${⊢}{i}={M}\to {P}\left({i}\right)={P}\left({M}\right)$
162 fvoveq1 ${⊢}{i}={M}\to {P}\left({i}+1\right)={P}\left({M}+1\right)$
163 161 162 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]$
164 163 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)$
165 164 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)$
166 160 165 imbi12d ${⊢}{i}={M}\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 {M}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)\right)$
167 166 6 vtoclg ${⊢}{M}\in ℤ\to \left(\left({\phi }\wedge {M}\in \left({M}..^{N}\right)\right)\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}\right)$
168 1 158 167 sylc ${⊢}{\phi }\to \left({t}\in \left[{P}\left({M}\right),{P}\left({M}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
169 154 168 itgcl ${⊢}{\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}\in ℂ$
170 163 itgeq1d ${⊢}{i}={M}\to {\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}$
171 170 fsum1 ${⊢}\left({M}\in ℤ\wedge {\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}\in ℂ\right)\to \sum _{{i}={M}}^{{M}}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}$
172 1 169 171 syl2anc ${⊢}{\phi }\to \sum _{{i}={M}}^{{M}}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}$
173 172 adantl ${⊢}\left({N}\in {ℤ}_{\ge \left({M}+1\right)}\wedge {\phi }\right)\to \sum _{{i}={M}}^{{M}}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}$
174 51 173 eqtr2d ${⊢}\left({N}\in {ℤ}_{\ge \left({M}+1\right)}\wedge {\phi }\right)\to {\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{M}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
175 174 ex ${⊢}{N}\in {ℤ}_{\ge \left({M}+1\right)}\to \left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({M}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{M}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)$
176 simp3 ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\wedge {\phi }\right)\to {\phi }$
177 simp1 ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\wedge {\phi }\right)\to {k}\in \left({M}+1..^{N}\right)$
178 simp2 ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\wedge {\phi }\right)\to \left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)$
179 176 178 mpd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge \left({\phi }\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\wedge {\phi }\right)\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}$
180 53 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\in ℝ$
181 elfzoelz ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}\in ℤ$
182 181 zred ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}\in ℝ$
183 182 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in ℝ$
184 55 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}+1\in ℝ$
185 56 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}<{M}+1$
186 elfzole1 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {M}+1\le {k}$
187 186 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}+1\le {k}$
188 180 184 183 185 187 ltletrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}<{k}$
189 180 183 188 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\le {k}$
190 eluz ${⊢}\left({M}\in ℤ\wedge {k}\in ℤ\right)\to \left({k}\in {ℤ}_{\ge {M}}↔{M}\le {k}\right)$
191 1 181 190 syl2an ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({k}\in {ℤ}_{\ge {M}}↔{M}\le {k}\right)$
192 189 191 mpbird ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in {ℤ}_{\ge {M}}$
193 simplll ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {\phi }$
194 eliccxr ${⊢}{t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\to {t}\in {ℝ}^{*}$
195 194 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\in {ℝ}^{*}$
196 193 80 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({M}\right)\in ℝ$
197 193 3 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
198 elfzelz ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\in ℤ$
199 198 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 ℤ$
200 elfzle1 ${⊢}{i}\in \left({M}\dots {k}\right)\to {M}\le {i}$
201 200 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}$
202 199 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 ℝ$
203 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {N}\in ℝ$
204 183 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 ℝ$
205 elfzle2 ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\le {k}$
206 205 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}$
207 elfzolt2 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}<{N}$
208 207 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {k}<{N}$
209 202 204 203 206 208 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}$
210 202 203 209 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}$
211 101 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
212 211 103 syl ${⊢}\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)$
213 199 201 210 212 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)$
214 213 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {i}\in \left({M}\dots {N}\right)$
215 197 214 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}\right)\in ℝ$
216 199 peano2zd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}+1\in ℤ$
217 53 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {M}\in ℝ$
218 216 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}+1\in ℝ$
219 53 adantr ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {M}\in ℝ$
220 198 zred ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\in ℝ$
221 220 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}\in ℝ$
222 1red ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to 1\in ℝ$
223 221 222 readdcld ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}+1\in ℝ$
224 200 adantl ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {M}\le {i}$
225 221 ltp1d ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}<{i}+1$
226 219 221 223 224 225 lelttrd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to {M}<{i}+1$
227 226 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {M}<{i}+1$
228 217 218 227 ltled ${⊢}\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}+1$
229 9 198 anim12ci ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\right)\to \left({i}\in ℤ\wedge {N}\in ℤ\right)$
230 229 adantlr ${⊢}\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 ℤ\wedge {N}\in ℤ\right)$
231 230 135 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
232 209 231 mpbid ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}+1\le {N}$
233 211 138 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\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)$
234 216 228 232 233 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {i}+1\in \left({M}\dots {N}\right)$
235 234 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {i}+1\in \left({M}\dots {N}\right)$
236 197 235 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}+1\right)\in ℝ$
237 simpr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]$
238 eliccre ${⊢}\left({P}\left({i}\right)\in ℝ\wedge {P}\left({i}+1\right)\in ℝ\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\in ℝ$
239 215 236 237 238 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\in ℝ$
240 elfzuz ${⊢}{i}\in \left({M}\dots {k}\right)\to {i}\in {ℤ}_{\ge {M}}$
241 240 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 {ℤ}_{\ge {M}}$
242 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
243 elfzelz ${⊢}{j}\in \left({M}\dots {i}\right)\to {j}\in ℤ$
244 243 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {j}\in ℤ$
245 elfzle1 ${⊢}{j}\in \left({M}\dots {i}\right)\to {M}\le {j}$
246 245 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {M}\le {j}$
247 244 zred ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {j}\in ℝ$
248 203 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {N}\in ℝ$
249 202 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {i}\in ℝ$
250 elfzle2 ${⊢}{j}\in \left({M}\dots {i}\right)\to {j}\le {i}$
251 250 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {j}\le {i}$
252 209 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {i}<{N}$
253 247 249 248 251 252 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {j}<{N}$
254 247 248 253 ltled ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {j}\le {N}$
255 211 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
256 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({j}\in \left({M}\dots {N}\right)↔\left({j}\in ℤ\wedge {M}\le {j}\wedge {j}\le {N}\right)\right)$
257 255 256 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to \left({j}\in \left({M}\dots {N}\right)↔\left({j}\in ℤ\wedge {M}\le {j}\wedge {j}\le {N}\right)\right)$
258 244 246 254 257 mpbir3and ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {j}\in \left({M}\dots {N}\right)$
259 242 258 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}\right)\right)\to {P}\left({j}\right)\in ℝ$
260 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
261 elfzelz ${⊢}{j}\in \left({M}\dots {i}-1\right)\to {j}\in ℤ$
262 261 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\in ℤ$
263 elfzle1 ${⊢}{j}\in \left({M}\dots {i}-1\right)\to {M}\le {j}$
264 263 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}\le {j}$
265 262 zred ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\in ℝ$
266 203 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {N}\in ℝ$
267 202 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {i}\in ℝ$
268 1red ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to 1\in ℝ$
269 267 268 resubcld ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {i}-1\in ℝ$
270 elfzle2 ${⊢}{j}\in \left({M}\dots {i}-1\right)\to {j}\le {i}-1$
271 270 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\le {i}-1$
272 267 ltm1d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {i}-1<{i}$
273 265 269 267 271 272 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}<{i}$
274 209 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {i}<{N}$
275 265 267 266 273 274 lttrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}<{N}$
276 265 266 275 ltled ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\le {N}$
277 211 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
278 277 256 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to \left({j}\in \left({M}\dots {N}\right)↔\left({j}\in ℤ\wedge {M}\le {j}\wedge {j}\le {N}\right)\right)$
279 262 264 276 278 mpbir3and ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\in \left({M}\dots {N}\right)$
280 260 279 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {P}\left({j}\right)\in ℝ$
281 262 peano2zd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1\in ℤ$
282 180 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}\in ℝ$
283 265 268 readdcld ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1\in ℝ$
284 53 adantr ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}\in ℝ$
285 261 zred ${⊢}{j}\in \left({M}\dots {i}-1\right)\to {j}\in ℝ$
286 285 adantl ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\in ℝ$
287 1red ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to 1\in ℝ$
288 286 287 readdcld ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1\in ℝ$
289 263 adantl ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}\le {j}$
290 286 ltp1d ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}<{j}+1$
291 284 286 288 289 290 lelttrd ${⊢}\left({\phi }\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}<{j}+1$
292 291 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}<{j}+1$
293 282 283 292 ltled ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {M}\le {j}+1$
294 zltp1le ${⊢}\left({j}\in ℤ\wedge {i}\in ℤ\right)\to \left({j}<{i}↔{j}+1\le {i}\right)$
295 261 199 294 syl2anr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to \left({j}<{i}↔{j}+1\le {i}\right)$
296 273 295 mpbid ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1\le {i}$
297 283 267 266 296 274 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1<{N}$
298 283 266 297 ltled ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1\le {N}$
299 elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({j}+1\in \left({M}\dots {N}\right)↔\left({j}+1\in ℤ\wedge {M}\le {j}+1\wedge {j}+1\le {N}\right)\right)$
300 277 299 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to \left({j}+1\in \left({M}\dots {N}\right)↔\left({j}+1\in ℤ\wedge {M}\le {j}+1\wedge {j}+1\le {N}\right)\right)$
301 281 293 298 300 mpbir3and ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}+1\in \left({M}\dots {N}\right)$
302 260 301 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {P}\left({j}+1\right)\in ℝ$
303 simplll ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {\phi }$
304 elfzuz ${⊢}{j}\in \left({M}\dots {i}-1\right)\to {j}\in {ℤ}_{\ge {M}}$
305 304 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\in {ℤ}_{\ge {M}}$
306 303 9 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {N}\in ℤ$
307 elfzo2 ${⊢}{j}\in \left({M}..^{N}\right)↔\left({j}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {j}<{N}\right)$
308 305 306 275 307 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {j}\in \left({M}..^{N}\right)$
309 eleq1 ${⊢}{i}={j}\to \left({i}\in \left({M}..^{N}\right)↔{j}\in \left({M}..^{N}\right)\right)$
310 309 anbi2d ${⊢}{i}={j}\to \left(\left({\phi }\wedge {i}\in \left({M}..^{N}\right)\right)↔\left({\phi }\wedge {j}\in \left({M}..^{N}\right)\right)\right)$
311 fveq2 ${⊢}{i}={j}\to {P}\left({i}\right)={P}\left({j}\right)$
312 fvoveq1 ${⊢}{i}={j}\to {P}\left({i}+1\right)={P}\left({j}+1\right)$
313 311 312 breq12d ${⊢}{i}={j}\to \left({P}\left({i}\right)<{P}\left({i}+1\right)↔{P}\left({j}\right)<{P}\left({j}+1\right)\right)$
314 310 313 imbi12d ${⊢}{i}={j}\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 {j}\in \left({M}..^{N}\right)\right)\to {P}\left({j}\right)<{P}\left({j}+1\right)\right)\right)$
315 314 4 chvarvv ${⊢}\left({\phi }\wedge {j}\in \left({M}..^{N}\right)\right)\to {P}\left({j}\right)<{P}\left({j}+1\right)$
316 303 308 315 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {P}\left({j}\right)<{P}\left({j}+1\right)$
317 280 302 316 ltled ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({M}\dots {i}-1\right)\right)\to {P}\left({j}\right)\le {P}\left({j}+1\right)$
318 241 259 317 monoord ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {P}\left({M}\right)\le {P}\left({i}\right)$
319 318 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({M}\right)\le {P}\left({i}\right)$
320 215 rexrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}\right)\in {ℝ}^{*}$
321 236 rexrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}+1\right)\in {ℝ}^{*}$
322 iccgelb ${⊢}\left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left({i}+1\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}\right)\le {t}$
323 320 321 237 322 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}\right)\le {t}$
324 196 215 239 319 323 letrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({M}\right)\le {t}$
325 193 69 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({N}\right)\in ℝ$
326 iccleub ${⊢}\left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left({i}+1\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\le {P}\left({i}+1\right)$
327 320 321 237 326 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\le {P}\left({i}+1\right)$
328 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {N}\in ℤ$
329 eluz ${⊢}\left({i}+1\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge \left({i}+1\right)}↔{i}+1\le {N}\right)$
330 216 328 329 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to \left({N}\in {ℤ}_{\ge \left({i}+1\right)}↔{i}+1\le {N}\right)$
331 232 330 mpbird ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {N}\in {ℤ}_{\ge \left({i}+1\right)}$
332 331 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {N}\in {ℤ}_{\ge \left({i}+1\right)}$
333 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
334 elfzelz ${⊢}{j}\in \left({i}+1\dots {N}\right)\to {j}\in ℤ$
335 334 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {j}\in ℤ$
336 elfzel1 ${⊢}{i}\in \left({M}\dots {k}\right)\to {M}\in ℤ$
337 336 zred ${⊢}{i}\in \left({M}\dots {k}\right)\to {M}\in ℝ$
338 337 adantr ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {M}\in ℝ$
339 334 zred ${⊢}{j}\in \left({i}+1\dots {N}\right)\to {j}\in ℝ$
340 339 adantl ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {j}\in ℝ$
341 220 adantr ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {i}\in ℝ$
342 1red ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to 1\in ℝ$
343 341 342 readdcld ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {i}+1\in ℝ$
344 200 adantr ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {M}\le {i}$
345 341 ltp1d ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {i}<{i}+1$
346 338 341 343 344 345 lelttrd ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {M}<{i}+1$
347 elfzle1 ${⊢}{j}\in \left({i}+1\dots {N}\right)\to {i}+1\le {j}$
348 347 adantl ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {i}+1\le {j}$
349 338 343 340 346 348 ltletrd ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {M}<{j}$
350 338 340 349 ltled ${⊢}\left({i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {M}\le {j}$
351 350 adantll ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {M}\le {j}$
352 elfzle2 ${⊢}{j}\in \left({i}+1\dots {N}\right)\to {j}\le {N}$
353 352 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {j}\le {N}$
354 211 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
355 354 256 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to \left({j}\in \left({M}\dots {N}\right)↔\left({j}\in ℤ\wedge {M}\le {j}\wedge {j}\le {N}\right)\right)$
356 335 351 353 355 mpbir3and ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {j}\in \left({M}\dots {N}\right)$
357 333 356 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {P}\left({j}\right)\in ℝ$
358 357 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\wedge {j}\in \left({i}+1\dots {N}\right)\right)\to {P}\left({j}\right)\in ℝ$
359 simplll ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {\phi }$
360 simplr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}\in \left({M}\dots {k}\right)$
361 simpr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in \left({i}+1\dots {N}-1\right)$
362 3 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
363 elfzelz ${⊢}{j}\in \left({i}+1\dots {N}-1\right)\to {j}\in ℤ$
364 363 3ad2ant3 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in ℤ$
365 53 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}\in ℝ$
366 364 zred ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in ℝ$
367 223 3adant3 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}+1\in ℝ$
368 226 3adant3 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}<{i}+1$
369 elfzle1 ${⊢}{j}\in \left({i}+1\dots {N}-1\right)\to {i}+1\le {j}$
370 369 3ad2ant3 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}+1\le {j}$
371 365 367 366 368 370 ltletrd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}<{j}$
372 365 366 371 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}\le {j}$
373 363 adantl ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in ℤ$
374 373 zred ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in ℝ$
375 14 adantr ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {N}\in ℝ$
376 1red ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to 1\in ℝ$
377 375 376 resubcld ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {N}-1\in ℝ$
378 elfzle2 ${⊢}{j}\in \left({i}+1\dots {N}-1\right)\to {j}\le {N}-1$
379 378 adantl ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\le {N}-1$
380 375 ltm1d ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {N}-1<{N}$
381 374 377 375 379 380 lelttrd ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}<{N}$
382 374 375 381 ltled ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\le {N}$
383 382 3adant2 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\le {N}$
384 101 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
385 384 256 syl ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to \left({j}\in \left({M}\dots {N}\right)↔\left({j}\in ℤ\wedge {M}\le {j}\wedge {j}\le {N}\right)\right)$
386 364 372 383 385 mpbir3and ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in \left({M}\dots {N}\right)$
387 362 386 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}\left({j}\right)\in ℝ$
388 364 peano2zd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}+1\in ℤ$
389 388 zred ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}+1\in ℝ$
390 220 3ad2ant2 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
391 1red ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to 1\in ℝ$
392 225 3adant3 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}<{i}+1$
393 390 367 366 392 370 ltletrd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}<{j}$
394 390 366 393 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}\le {j}$
395 390 366 391 394 leadd1dd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {i}+1\le {j}+1$
396 365 367 389 368 395 ltletrd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}<{j}+1$
397 365 389 396 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}\le {j}+1$
398 zltp1le ${⊢}\left({j}\in ℤ\wedge {N}\in ℤ\right)\to \left({j}<{N}↔{j}+1\le {N}\right)$
399 363 9 398 syl2anr ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to \left({j}<{N}↔{j}+1\le {N}\right)$
400 381 399 mpbid ${⊢}\left({\phi }\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}+1\le {N}$
401 400 3adant2 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}+1\le {N}$
402 384 299 syl ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to \left({j}+1\in \left({M}\dots {N}\right)↔\left({j}+1\in ℤ\wedge {M}\le {j}+1\wedge {j}+1\le {N}\right)\right)$
403 388 397 401 402 mpbir3and ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}+1\in \left({M}\dots {N}\right)$
404 362 403 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}\left({j}+1\right)\in ℝ$
405 simp1 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {\phi }$
406 1 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {M}\in ℤ$
407 eluz ${⊢}\left({M}\in ℤ\wedge {j}\in ℤ\right)\to \left({j}\in {ℤ}_{\ge {M}}↔{M}\le {j}\right)$
408 406 364 407 syl2anc ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to \left({j}\in {ℤ}_{\ge {M}}↔{M}\le {j}\right)$
409 372 408 mpbird ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in {ℤ}_{\ge {M}}$
410 9 3ad2ant1 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {N}\in ℤ$
411 381 3adant2 ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}<{N}$
412 409 410 411 307 syl3anbrc ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {j}\in \left({M}..^{N}\right)$
413 405 412 315 syl2anc ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}\left({j}\right)<{P}\left({j}+1\right)$
414 387 404 413 ltled ${⊢}\left({\phi }\wedge {i}\in \left({M}\dots {k}\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}\left({j}\right)\le {P}\left({j}+1\right)$
415 359 360 361 414 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}\left({j}\right)\le {P}\left({j}+1\right)$
416 415 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\wedge {j}\in \left({i}+1\dots {N}-1\right)\right)\to {P}\left({j}\right)\le {P}\left({j}+1\right)$
417 332 358 416 monoord ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {P}\left({i}+1\right)\le {P}\left({N}\right)$
418 239 236 325 327 417 letrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\le {P}\left({N}\right)$
419 69 rexrd ${⊢}{\phi }\to {P}\left({N}\right)\in {ℝ}^{*}$
420 81 419 jca ${⊢}{\phi }\to \left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({N}\right)\in {ℝ}^{*}\right)$
421 193 420 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to \left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({N}\right)\in {ℝ}^{*}\right)$
422 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)$
423 421 422 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+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)$
424 195 324 418 423 mpbir3and ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({N}\right)\right]$
425 193 424 5 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\wedge {t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]\right)\to {A}\in ℂ$
426 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {\phi }$
427 241 328 209 146 syl3anbrc ${⊢}\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}..^{N}\right)$
428 426 427 6 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to \left({t}\in \left[{P}\left({i}\right),{P}\left({i}+1\right)\right]⟼{A}\right)\in {𝐿}^{1}$
429 425 428 itgcl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\in ℂ$
430 fveq2 ${⊢}{i}={k}\to {P}\left({i}\right)={P}\left({k}\right)$
431 fvoveq1 ${⊢}{i}={k}\to {P}\left({i}+1\right)={P}\left({k}+1\right)$
432 430 431 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]$
433 432 itgeq1d ${⊢}{i}={k}\to {\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
434 192 429 433 fzosump1 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \sum _{{i}\in \left({M}..^{k}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
435 434 3adant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\to \sum _{{i}\in \left({M}..^{k}+1\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
436 oveq1 ${⊢}{\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\to {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
437 436 eqcomd ${⊢}{\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\to \sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
438 437 3ad2ant3 ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\wedge {\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}=\sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}\right)\to \sum _{{i}\in \left({M}..^{k}\right)}{\int }_{\left[{P}\left({i}\right),{P}\left({i}+1\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}={\int }_{\left[{P}\left({M}\right),{P}\left({k}\right)\right]}{A}d{t}+{\int }_{\left[{P}\left({k}\right),{P}\left({k}+1\right)\right]}{A}d{t}$
439 80 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({M}\right)\in ℝ$
440 3 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
441 181 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in ℤ$
442 441 peano2zd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\in ℤ$
443 442 zred ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\in ℝ$
444 183 ltp1d ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}<{k}+1$
445 180 183 443 188 444 lttrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}<{k}+1$
446 180 443 445 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\le {k}+1$
447 207 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}<{N}$
448 zltp1le ${⊢}\left({k}\in ℤ\wedge {N}\in ℤ\right)\to \left({k}<{N}↔{k}+1\le {N}\right)$
449 181 9 448 syl2anr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({k}<{N}↔{k}+1\le {N}\right)$
450 447 449 mpbid ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\le {N}$
451 101 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
452 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)$
453 451 452 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)$
454 442 446 450 453 mpbir3and ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}+1\in \left({M}\dots {N}\right)$
455 440 454 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}+1\right)\in ℝ$
456 14 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in ℝ$
457 183 456 447 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\le {N}$
458 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)$
459 451 458 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)$
460 441 189 457 459 mpbir3and ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in \left({M}\dots {N}\right)$
461 440 460 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\in ℝ$
462 461 rexrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\in {ℝ}^{*}$
463 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
464 463 213 ffvelrnd ${⊢}\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 ℝ$
465 3 ad2antrr ${⊢}\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({M}\dots {N}\right)⟶ℝ$
466 elfzelz ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\in ℤ$
467 466 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 ℤ$
468 elfzle1 ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {M}\le {i}$
469 468 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}$
470 467 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 ℝ$
471 14 ad2antrr ${⊢}\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 ℝ$
472 183 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 ℝ$
473 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 ℝ$
474 472 473 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 ℝ$
475 elfzle2 ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\le {k}-1$
476 475 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$
477 472 ltm1d ${⊢}\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<{k}$
478 470 474 472 476 477 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}<{k}$
479 447 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}<{N}$
480 470 472 471 478 479 lttrd ${⊢}\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}$
481 470 471 480 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}$
482 101 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
483 482 103 syl ${⊢}\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)$
484 467 469 481 483 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)$
485 465 484 ffvelrnd ${⊢}\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 ℝ$
486 467 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 ℤ$
487 53 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {M}\in ℝ$
488 470 473 readdcld ${⊢}\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 ℝ$
489 470 ltp1d ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {i}<{i}+1$
490 487 470 488 469 489 lelttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}\dots {k}-1\right)\right)\to {M}<{i}+1$
491 487 488 490 ltled ${⊢}\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$
492 zltp1le ${⊢}\left({i}\in ℤ\wedge {k}\in ℤ\right)\to \left({i}<{k}↔{i}+1\le {k}\right)$
493 466 441 492 syl2anr ${⊢}\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}<{k}↔{i}+1\le {k}\right)$
494 478 493 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 {k}$
495 488 472 471 494 479 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}+1<{N}$
496 488 471 495 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}+1\le {N}$
497 482 138 syl ${⊢}\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)$
498 486 491 496 497 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)$
499 465 498 ffvelrnd ${⊢}\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 ℝ$
500 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 }$
501 elfzuz ${⊢}{i}\in \left({M}\dots {k}-1\right)\to {i}\in {ℤ}_{\ge {M}}$
502 501 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}}$
503 9 ad2antrr ${⊢}\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 ℤ$
504 502 503 480 146 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)$
505 500 504 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)<{P}\left({i}+1\right)$
506 485 499 505 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)$
507 192 464 506 monoord ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({M}\right)\le {P}\left({k}\right)$
508 9 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in ℤ$
509 elfzo2 ${⊢}{k}\in \left({M}..^{N}\right)↔\left({k}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {k}<{N}\right)$
510 192 508 447 509 syl3anbrc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in \left({M}..^{N}\right)$
511 eleq1 ${⊢}{i}={k}\to \left({i}\in \left({M}..^{N}\right)↔{k}\in \left({M}..^{N}\right)\right)$
512 511 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)$
513 430 431 breq12d ${⊢}{i}={k}\to \left({P}\left({i}\right)<{P}\left({i}+1\right)↔{P}\left({k}\right)<{P}\left({k}+1\right)\right)$
514 512 513 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)$
515 514 4 chvarvv ${⊢}\left({\phi }\wedge {k}\in \left({M}..^{N}\right)\right)\to {P}\left({k}\right)<{P}\left({k}+1\right)$
516 510 515 syldan ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)<{P}\left({k}+1\right)$
517 461 455 516 ltled ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\le {P}\left({k}+1\right)$
518 81 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({M}\right)\in {ℝ}^{*}$
519 455 rexrd ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}+1\right)\in {ℝ}^{*}$
520 elicc1 ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({k}+1\right)\in {ℝ}^{*}\right)\to \left({P}\left({k}\right)\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]↔\left({P}\left({k}\right)\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {P}\left({k}\right)\wedge {P}\left({k}\right)\le {P}\left({k}+1\right)\right)\right)$
521 518 519 520 syl2anc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to \left({P}\left({k}\right)\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]↔\left({P}\left({k}\right)\in {ℝ}^{*}\wedge {P}\left({M}\right)\le {P}\left({k}\right)\wedge {P}\left({k}\right)\le {P}\left({k}+1\right)\right)\right)$
522 462 507 517 521 mpbir3and ${⊢}\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]$
523 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {\phi }$
524 eliccxr ${⊢}{t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\to {t}\in {ℝ}^{*}$
525 524 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in {ℝ}^{*}$
526 81 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({M}\right)\in {ℝ}^{*}$
527 519 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({k}+1\right)\in {ℝ}^{*}$
528 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\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]$
529 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}$
530 526 527 528 529 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({M}\right)\le {t}$
531 80 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({M}\right)\in ℝ$
532 455 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({k}+1\right)\in ℝ$
533 eliccre ${⊢}\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 {t}\in ℝ$
534 531 532 528 533 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\in ℝ$
535 69 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {P}\left({N}\right)\in ℝ$
536 iccleub ${⊢}\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 {t}\le {P}\left({k}+1\right)$
537 526 527 528 536 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\le {P}\left({k}+1\right)$
538 eluz2 ${⊢}{N}\in {ℤ}_{\ge \left({k}+1\right)}↔\left({k}+1\in ℤ\wedge {N}\in ℤ\wedge {k}+1\le {N}\right)$
539 442 508 450 538 syl3anbrc ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in {ℤ}_{\ge \left({k}+1\right)}$
540 3 ad2antrr ${⊢}\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({M}\dots {N}\right)⟶ℝ$
541 1 ad2antrr ${⊢}\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 ℤ$
542 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {N}\in ℤ$
543 elfzelz ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {i}\in ℤ$
544 543 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 ℤ$
545 541 542 544 3jca ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)$
546 53 ad2antrr ${⊢}\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 ℝ$
547 544 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 ℝ$
548 183 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 ℝ$
549 188 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}$
550 182 adantr ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}\in ℝ$
551 1red ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to 1\in ℝ$
552 550 551 readdcld ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}+1\in ℝ$
553 543 zred ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {i}\in ℝ$
554 553 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {i}\in ℝ$
555 550 ltp1d ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}<{k}+1$
556 elfzle1 ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {k}+1\le {i}$
557 556 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}+1\le {i}$
558 550 552 554 555 557 ltletrd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to {k}<{i}$
559 558 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}$
560 546 548 547 549 559 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}$
561 546 547 560 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}$
562 elfzle2 ${⊢}{i}\in \left({k}+1\dots {N}\right)\to {i}\le {N}$
563 562 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}$
564 545 561 563 jca32 ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}+1\dots {N}\right)\right)\to \left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({M}\le {i}\wedge {i}\le {N}\right)\right)$
565 elfz2 ${⊢}{i}\in \left({M}\dots {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({M}\le {i}\wedge {i}\le {N}\right)\right)$
566 564 565 sylibr ${⊢}\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)$
567 540 566 ffvelrnd ${⊢}\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 ℝ$
568 3 ad2antrr ${⊢}\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({M}\dots {N}\right)⟶ℝ$
569 1 ad2antrr ${⊢}\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 ℤ$
570 9 ad2antrr ${⊢}\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 ℤ$
571 elfzelz ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {i}\in ℤ$
572 571 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 ℤ$
573 569 570 572 3jca ${⊢}\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({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)$
574 53 ad2antrr ${⊢}\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 ℝ$
575 572 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 ℝ$
576 183 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 ℝ$
577 188 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}$
578 182 adantr ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}\in ℝ$
579 1red ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to 1\in ℝ$
580 578 579 readdcld ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}+1\in ℝ$
581 571 zred ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {i}\in ℝ$
582 581 adantl ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
583 578 ltp1d ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{k}+1$
584 elfzle1 ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {k}+1\le {i}$
585 584 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}$
586 578 580 582 583 585 ltletrd ${⊢}\left({k}\in \left({M}+1..^{N}\right)\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {k}<{i}$
587 586 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}$
588 574 576 575 577 587 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}$
589 574 575 588 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}$
590 581 adantl ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\in ℝ$
591 14 adantr ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}\in ℝ$
592 1red ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to 1\in ℝ$
593 591 592 resubcld ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}-1\in ℝ$
594 elfzle2 ${⊢}{i}\in \left({k}+1\dots {N}-1\right)\to {i}\le {N}-1$
595 594 adantl ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\le {N}-1$
596 591 ltm1d ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {N}-1<{N}$
597 590 593 591 595 596 lelttrd ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}<{N}$
598 590 591 597 ltled ${⊢}\left({\phi }\wedge {i}\in \left({k}+1\dots {N}-1\right)\right)\to {i}\le {N}$
599 598 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}$
600 573 589 599 jca32 ${⊢}\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(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({M}\le {i}\wedge {i}\le {N}\right)\right)$
601 600 565 sylibr ${⊢}\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)$
602 568 601 ffvelrnd ${⊢}\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 ℝ$
603 572 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 ℤ$
604 569 570 603 3jca ${⊢}\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({M}\in ℤ\wedge {N}\in ℤ\wedge {i}+1\in ℤ\right)$
605 603 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 ℝ$
606 575 ltp1d ${⊢}\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}<{i}+1$
607 576 575 605 587 606 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 {k}<{i}+1$
608 574 576 605 577 607 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$
609 574 605 608 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$
610 597 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}$
611 571 508 135 syl2anr ${⊢}\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}<{N}↔{i}+1\le {N}\right)$
612 610 611 mpbid ${⊢}\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}$
613 604 609 612 jca32 ${⊢}\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(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}+1\in ℤ\right)\wedge \left({M}\le {i}+1\wedge {i}+1\le {N}\right)\right)$
614 elfz2 ${⊢}{i}+1\in \left({M}\dots {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}+1\in ℤ\right)\wedge \left({M}\le {i}+1\wedge {i}+1\le {N}\right)\right)$
615 613 614 sylibr ${⊢}\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)$
616 568 615 ffvelrnd ${⊢}\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 ℝ$
617 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 }$
618 eluz2 ${⊢}{i}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {i}\in ℤ\wedge {M}\le {i}\right)$
619 569 572 589 618 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 {ℤ}_{\ge {M}}$
620 619 570 610 146 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)$
621 617 620 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)<{P}\left({i}+1\right)$
622 602 616 621 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)$
623 539 567 622 monoord ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}+1\right)\le {P}\left({N}\right)$
624 623 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\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)$
625 534 532 535 537 624 letrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {t}\le {P}\left({N}\right)$
626 420 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\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({N}\right)\in {ℝ}^{*}\right)$
627 626 422 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\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)$
628 525 530 625 627 mpbir3and ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\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]$
629 523 628 5 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}+1\right)\right]\right)\to {A}\in ℂ$
630 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)$
631 1 adantr ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {M}\in ℤ$
632 elfzouz ${⊢}{k}\in \left({M}+1..^{N}\right)\to {k}\in {ℤ}_{\ge \left({M}+1\right)}$
633 632 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {k}\in {ℤ}_{\ge \left({M}+1\right)}$
634 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {\phi }$
635 elfzouz ${⊢}{i}\in \left({M}..^{k}\right)\to {i}\in {ℤ}_{\ge {M}}$
636 635 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {i}\in {ℤ}_{\ge {M}}$
637 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {N}\in ℤ$
638 elfzoelz ${⊢}{i}\in \left({M}..^{k}\right)\to {i}\in ℤ$
639 638 zred ${⊢}{i}\in \left({M}..^{k}\right)\to {i}\in ℝ$
640 639 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {i}\in ℝ$
641 183 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {k}\in ℝ$
642 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {N}\in ℝ$
643 elfzolt2 ${⊢}{i}\in \left({M}..^{k}\right)\to {i}<{k}$
644 643 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {i}<{k}$
645 447 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {k}<{N}$
646 640 641 642 644 645 lttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {i}<{N}$
647 636 637 646 146 syl3anbrc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {i}\in \left({M}..^{N}\right)$
648 634 647 4 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({M}..^{k}\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
649 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {\phi }$
650 80 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({M}\right)\in ℝ$
651 69 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({N}\right)\in ℝ$
652 461 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({k}\right)\in ℝ$
653 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]$
654 eliccre ${⊢}\left({P}\left({M}\right)\in ℝ\wedge {P}\left({k}\right)\in ℝ\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {t}\in ℝ$
655 650 652 653 654 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {t}\in ℝ$
656 81 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({M}\right)\in {ℝ}^{*}$
657 462 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({k}\right)\in {ℝ}^{*}$
658 iccgelb ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({k}\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({M}\right)\le {t}$
659 656 657 653 658 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {P}\left({M}\right)\le {t}$
660 iccleub ${⊢}\left({P}\left({M}\right)\in {ℝ}^{*}\wedge {P}\left({k}\right)\in {ℝ}^{*}\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {t}\le {P}\left({k}\right)$
661 656 657 653 660 syl3anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\left({k}\right)\right]\right)\to {t}\le {P}\left({k}\right)$
662 elfzouz2 ${⊢}{k}\in \left({M}+1..^{N}\right)\to {N}\in {ℤ}_{\ge {k}}$
663 662 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {N}\in {ℤ}_{\ge {k}}$
664 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
665 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {M}\in ℤ$
666 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {N}\in ℤ$
667 elfzelz ${⊢}{i}\in \left({k}\dots {N}\right)\to {i}\in ℤ$
668 667 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {i}\in ℤ$
669 665 666 668 3jca ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)$
670 53 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {M}\in ℝ$
671 668 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {i}\in ℝ$
672 183 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {k}\in ℝ$
673 188 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {M}<{k}$
674 elfzle1 ${⊢}{i}\in \left({k}\dots {N}\right)\to {k}\le {i}$
675 674 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {k}\le {i}$
676 670 672 671 673 675 ltletrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {M}<{i}$
677 670 671 676 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {M}\le {i}$
678 elfzle2 ${⊢}{i}\in \left({k}\dots {N}\right)\to {i}\le {N}$
679 678 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {i}\le {N}$
680 669 677 679 jca32 ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to \left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({M}\le {i}\wedge {i}\le {N}\right)\right)$
681 680 565 sylibr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {i}\in \left({M}\dots {N}\right)$
682 664 681 ffvelrnd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}\right)\right)\to {P}\left({i}\right)\in ℝ$
683 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {P}:\left({M}\dots {N}\right)⟶ℝ$
684 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}\in ℤ$
685 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {N}\in ℤ$
686 elfzelz ${⊢}{i}\in \left({k}\dots {N}-1\right)\to {i}\in ℤ$
687 686 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\in ℤ$
688 684 685 687 3jca ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)$
689 53 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}\in ℝ$
690 687 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\in ℝ$
691 183 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {k}\in ℝ$
692 188 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}<{k}$
693 elfzle1 ${⊢}{i}\in \left({k}\dots {N}-1\right)\to {k}\le {i}$
694 693 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {k}\le {i}$
695 689 691 690 692 694 ltletrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}<{i}$
696 689 690 695 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}\le {i}$
697 686 zred ${⊢}{i}\in \left({k}\dots {N}-1\right)\to {i}\in ℝ$
698 697 adantl ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\in ℝ$
699 14 adantr ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {N}\in ℝ$
700 1red ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to 1\in ℝ$
701 699 700 resubcld ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {N}-1\in ℝ$
702 elfzle2 ${⊢}{i}\in \left({k}\dots {N}-1\right)\to {i}\le {N}-1$
703 702 adantl ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\le {N}-1$
704 699 ltm1d ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {N}-1<{N}$
705 698 701 699 703 704 lelttrd ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}<{N}$
706 698 699 705 ltled ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\le {N}$
707 706 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\le {N}$
708 688 696 707 jca32 ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to \left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({M}\le {i}\wedge {i}\le {N}\right)\right)$
709 708 565 sylibr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\in \left({M}\dots {N}\right)$
710 683 709 ffvelrnd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {P}\left({i}\right)\in ℝ$
711 687 peano2zd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}+1\in ℤ$
712 684 685 711 3jca ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}+1\in ℤ\right)$
713 711 zred ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}+1\in ℝ$
714 690 ltp1d ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}<{i}+1$
715 689 690 713 696 714 lelttrd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}<{i}+1$
716 689 713 715 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {M}\le {i}+1$
717 686 9 135 syl2anr ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to \left({i}<{N}↔{i}+1\le {N}\right)$
718 705 717 mpbid ${⊢}\left({\phi }\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}+1\le {N}$
719 718 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}+1\le {N}$
720 712 716 719 jca32 ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to \left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {i}+1\in ℤ\right)\wedge \left({M}\le {i}+1\wedge {i}+1\le {N}\right)\right)$
721 720 614 sylibr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}+1\in \left({M}\dots {N}\right)$
722 683 721 ffvelrnd ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {P}\left({i}+1\right)\in ℝ$
723 simpll ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {\phi }$
724 684 687 696 618 syl3anbrc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\in {ℤ}_{\ge {M}}$
725 705 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}<{N}$
726 724 685 725 146 syl3anbrc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {i}\in \left({M}..^{N}\right)$
727 723 726 4 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {P}\left({i}\right)<{P}\left({i}+1\right)$
728 710 722 727 ltled ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {i}\in \left({k}\dots {N}-1\right)\right)\to {P}\left({i}\right)\le {P}\left({i}+1\right)$
729 663 682 728 monoord ${⊢}\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\to {P}\left({k}\right)\le {P}\left({N}\right)$
730 729 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left({M}+1..^{N}\right)\right)\wedge {t}\in \left[{P}\left({M}\right),{P}\right]\right)$