# Metamath Proof Explorer

## Theorem iccelpart

Description: An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020)

Ref Expression
Assertion iccelpart ${⊢}{M}\in ℕ\to \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{x}=1\to \mathrm{RePart}\left({x}\right)=\mathrm{RePart}\left(1\right)$
2 fveq2 ${⊢}{x}=1\to {p}\left({x}\right)={p}\left(1\right)$
3 2 oveq2d ${⊢}{x}=1\to \left[{p}\left(0\right),{p}\left({x}\right)\right)=\left[{p}\left(0\right),{p}\left(1\right)\right)$
4 3 eleq2d ${⊢}{x}=1\to \left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\right)$
5 oveq2 ${⊢}{x}=1\to \left(0..^{x}\right)=\left(0..^1\right)$
6 fzo01 ${⊢}\left(0..^1\right)=\left\{0\right\}$
7 5 6 syl6eq ${⊢}{x}=1\to \left(0..^{x}\right)=\left\{0\right\}$
8 7 rexeqdv ${⊢}{x}=1\to \left(\exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔\exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
9 4 8 imbi12d ${⊢}{x}=1\to \left(\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\left({X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\to \exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
10 1 9 raleqbidv ${⊢}{x}=1\to \left(\forall {p}\in \mathrm{RePart}\left({x}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\forall {p}\in \mathrm{RePart}\left(1\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\to \exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
11 fveq2 ${⊢}{x}={y}\to \mathrm{RePart}\left({x}\right)=\mathrm{RePart}\left({y}\right)$
12 fveq2 ${⊢}{x}={y}\to {p}\left({x}\right)={p}\left({y}\right)$
13 12 oveq2d ${⊢}{x}={y}\to \left[{p}\left(0\right),{p}\left({x}\right)\right)=\left[{p}\left(0\right),{p}\left({y}\right)\right)$
14 13 eleq2d ${⊢}{x}={y}\to \left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)$
15 oveq2 ${⊢}{x}={y}\to \left(0..^{x}\right)=\left(0..^{y}\right)$
16 15 rexeqdv ${⊢}{x}={y}\to \left(\exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔\exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
17 14 16 imbi12d ${⊢}{x}={y}\to \left(\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
18 11 17 raleqbidv ${⊢}{x}={y}\to \left(\forall {p}\in \mathrm{RePart}\left({x}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
19 fveq2 ${⊢}{x}={y}+1\to \mathrm{RePart}\left({x}\right)=\mathrm{RePart}\left({y}+1\right)$
20 fveq2 ${⊢}{x}={y}+1\to {p}\left({x}\right)={p}\left({y}+1\right)$
21 20 oveq2d ${⊢}{x}={y}+1\to \left[{p}\left(0\right),{p}\left({x}\right)\right)=\left[{p}\left(0\right),{p}\left({y}+1\right)\right)$
22 21 eleq2d ${⊢}{x}={y}+1\to \left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)$
23 oveq2 ${⊢}{x}={y}+1\to \left(0..^{x}\right)=\left(0..^{y}+1\right)$
24 23 rexeqdv ${⊢}{x}={y}+1\to \left(\exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔\exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
25 22 24 imbi12d ${⊢}{x}={y}+1\to \left(\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
26 19 25 raleqbidv ${⊢}{x}={y}+1\to \left(\forall {p}\in \mathrm{RePart}\left({x}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\forall {p}\in \mathrm{RePart}\left({y}+1\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
27 fveq2 ${⊢}{x}={M}\to \mathrm{RePart}\left({x}\right)=\mathrm{RePart}\left({M}\right)$
28 fveq2 ${⊢}{x}={M}\to {p}\left({x}\right)={p}\left({M}\right)$
29 28 oveq2d ${⊢}{x}={M}\to \left[{p}\left(0\right),{p}\left({x}\right)\right)=\left[{p}\left(0\right),{p}\left({M}\right)\right)$
30 29 eleq2d ${⊢}{x}={M}\to \left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\right)$
31 oveq2 ${⊢}{x}={M}\to \left(0..^{x}\right)=\left(0..^{M}\right)$
32 31 rexeqdv ${⊢}{x}={M}\to \left(\exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔\exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
33 30 32 imbi12d ${⊢}{x}={M}\to \left(\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
34 27 33 raleqbidv ${⊢}{x}={M}\to \left(\forall {p}\in \mathrm{RePart}\left({x}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({x}\right)\right)\to \exists {i}\in \left(0..^{x}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)↔\forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
35 0nn0 ${⊢}0\in {ℕ}_{0}$
36 fveq2 ${⊢}{i}=0\to {p}\left({i}\right)={p}\left(0\right)$
37 fv0p1e1 ${⊢}{i}=0\to {p}\left({i}+1\right)={p}\left(1\right)$
38 36 37 oveq12d ${⊢}{i}=0\to \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)=\left[{p}\left(0\right),{p}\left(1\right)\right)$
39 38 eleq2d ${⊢}{i}=0\to \left({X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\right)$
40 39 rexsng ${⊢}0\in {ℕ}_{0}\to \left(\exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\right)$
41 35 40 ax-mp ${⊢}\exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔{X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)$
42 41 biimpri ${⊢}{X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\to \exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)$
43 42 rgenw ${⊢}\forall {p}\in \mathrm{RePart}\left(1\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left(1\right)\right)\to \exists {i}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
44 nfv ${⊢}Ⅎ{p}\phantom{\rule{.4em}{0ex}}{y}\in ℕ$
45 nfra1 ${⊢}Ⅎ{p}\phantom{\rule{.4em}{0ex}}\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
46 44 45 nfan ${⊢}Ⅎ{p}\phantom{\rule{.4em}{0ex}}\left({y}\in ℕ\wedge \forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
47 nnnn0 ${⊢}{y}\in ℕ\to {y}\in {ℕ}_{0}$
48 fzonn0p1 ${⊢}{y}\in {ℕ}_{0}\to {y}\in \left(0..^{y}+1\right)$
49 47 48 syl ${⊢}{y}\in ℕ\to {y}\in \left(0..^{y}+1\right)$
50 49 ad2antrr ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\to {y}\in \left(0..^{y}+1\right)$
51 fveq2 ${⊢}{i}={y}\to {p}\left({i}\right)={p}\left({y}\right)$
52 fvoveq1 ${⊢}{i}={y}\to {p}\left({i}+1\right)={p}\left({y}+1\right)$
53 51 52 oveq12d ${⊢}{i}={y}\to \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)=\left[{p}\left({y}\right),{p}\left({y}+1\right)\right)$
54 53 eleq2d ${⊢}{i}={y}\to \left({X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔{X}\in \left[{p}\left({y}\right),{p}\left({y}+1\right)\right)\right)$
55 54 adantl ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\wedge {i}={y}\right)\to \left({X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)↔{X}\in \left[{p}\left({y}\right),{p}\left({y}+1\right)\right)\right)$
56 peano2nn ${⊢}{y}\in ℕ\to {y}+1\in ℕ$
57 56 adantr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {y}+1\in ℕ$
58 simpr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {p}\in \mathrm{RePart}\left({y}+1\right)$
59 56 nnnn0d ${⊢}{y}\in ℕ\to {y}+1\in {ℕ}_{0}$
60 0elfz ${⊢}{y}+1\in {ℕ}_{0}\to 0\in \left(0\dots {y}+1\right)$
61 59 60 syl ${⊢}{y}\in ℕ\to 0\in \left(0\dots {y}+1\right)$
62 61 adantr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to 0\in \left(0\dots {y}+1\right)$
63 57 58 62 iccpartxr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {p}\left(0\right)\in {ℝ}^{*}$
64 nn0fz0 ${⊢}{y}+1\in {ℕ}_{0}↔{y}+1\in \left(0\dots {y}+1\right)$
65 59 64 sylib ${⊢}{y}\in ℕ\to {y}+1\in \left(0\dots {y}+1\right)$
66 65 adantr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {y}+1\in \left(0\dots {y}+1\right)$
67 57 58 66 iccpartxr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {p}\left({y}+1\right)\in {ℝ}^{*}$
68 63 67 jca ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({p}\left(0\right)\in {ℝ}^{*}\wedge {p}\left({y}+1\right)\in {ℝ}^{*}\right)$
69 68 adantlr ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({p}\left(0\right)\in {ℝ}^{*}\wedge {p}\left({y}+1\right)\in {ℝ}^{*}\right)$
70 elico1 ${⊢}\left({p}\left(0\right)\in {ℝ}^{*}\wedge {p}\left({y}+1\right)\in {ℝ}^{*}\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
71 69 70 syl ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
72 simp1 ${⊢}\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to {X}\in {ℝ}^{*}$
73 72 adantl ${⊢}\left({p}\left({y}\right)\le {X}\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {X}\in {ℝ}^{*}$
74 simpl ${⊢}\left({p}\left({y}\right)\le {X}\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {p}\left({y}\right)\le {X}$
75 simpr3 ${⊢}\left({p}\left({y}\right)\le {X}\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {X}<{p}\left({y}+1\right)$
76 73 74 75 3jca ${⊢}\left({p}\left({y}\right)\le {X}\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)$
77 76 ex ${⊢}{p}\left({y}\right)\le {X}\to \left(\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
78 77 adantl ${⊢}\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
79 78 adantr ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
80 71 79 sylbid ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
81 80 impr ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)$
82 nn0fz0 ${⊢}{y}\in {ℕ}_{0}↔{y}\in \left(0\dots {y}\right)$
83 47 82 sylib ${⊢}{y}\in ℕ\to {y}\in \left(0\dots {y}\right)$
84 fzelp1 ${⊢}{y}\in \left(0\dots {y}\right)\to {y}\in \left(0\dots {y}+1\right)$
85 83 84 syl ${⊢}{y}\in ℕ\to {y}\in \left(0\dots {y}+1\right)$
86 85 adantr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {y}\in \left(0\dots {y}+1\right)$
87 57 58 86 iccpartxr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {p}\left({y}\right)\in {ℝ}^{*}$
88 87 67 jca ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({p}\left({y}\right)\in {ℝ}^{*}\wedge {p}\left({y}+1\right)\in {ℝ}^{*}\right)$
89 88 ad2ant2r ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\to \left({p}\left({y}\right)\in {ℝ}^{*}\wedge {p}\left({y}+1\right)\in {ℝ}^{*}\right)$
90 elico1 ${⊢}\left({p}\left({y}\right)\in {ℝ}^{*}\wedge {p}\left({y}+1\right)\in {ℝ}^{*}\right)\to \left({X}\in \left[{p}\left({y}\right),{p}\left({y}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
91 89 90 syl ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\to \left({X}\in \left[{p}\left({y}\right),{p}\left({y}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
92 81 91 mpbird ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\to {X}\in \left[{p}\left({y}\right),{p}\left({y}+1\right)\right)$
93 50 55 92 rspcedvd ${⊢}\left(\left({y}\in ℕ\wedge {p}\left({y}\right)\le {X}\right)\wedge \left({p}\in \mathrm{RePart}\left({y}+1\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)$
94 93 exp43 ${⊢}{y}\in ℕ\to \left({p}\left({y}\right)\le {X}\to \left({p}\in \mathrm{RePart}\left({y}+1\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
95 94 adantr ${⊢}\left({y}\in ℕ\wedge \forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \left({p}\left({y}\right)\le {X}\to \left({p}\in \mathrm{RePart}\left({y}+1\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
96 iccpartres ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {{p}↾}_{\left(0\dots {y}\right)}\in \mathrm{RePart}\left({y}\right)$
97 rspsbca
98 vex ${⊢}{p}\in \mathrm{V}$
99 98 resex ${⊢}{{p}↾}_{\left(0\dots {y}\right)}\in \mathrm{V}$
100 sbcimg
101 sbcel2
102 csbov12g
103 csbfv12
104 csbvarg
105 csbconstg
106 104 105 fveq12d
107 103 106 syl5eq
108 csbfv12
109 csbconstg
110 104 109 fveq12d
111 108 110 syl5eq
112 107 111 oveq12d
113 102 112 eqtrd
114 113 eleq2d
115 101 114 syl5bb
116 sbcrex
117 sbcel2
118 csbov12g
119 csbfv12
120 csbconstg
121 104 120 fveq12d
122 119 121 syl5eq
123 csbfv12
124 csbconstg
125 104 124 fveq12d
126 123 125 syl5eq
127 122 126 oveq12d
128 118 127 eqtrd
129 128 eleq2d
130 117 129 syl5bb
131 130 rexbidv
132 116 131 syl5bb
133 115 132 imbi12d
134 100 133 bitrd
135 99 134 ax-mp
136 68 70 syl ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
137 136 adantr ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)$
138 72 adantl ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {X}\in {ℝ}^{*}$
139 simpr2 ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {p}\left(0\right)\le {X}$
140 xrltnle ${⊢}\left({X}\in {ℝ}^{*}\wedge {p}\left({y}\right)\in {ℝ}^{*}\right)\to \left({X}<{p}\left({y}\right)↔¬{p}\left({y}\right)\le {X}\right)$
141 72 87 140 syl2anr ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to \left({X}<{p}\left({y}\right)↔¬{p}\left({y}\right)\le {X}\right)$
142 141 exbiri ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to {X}<{p}\left({y}\right)\right)\right)$
143 142 com23 ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to {X}<{p}\left({y}\right)\right)\right)$
144 143 imp31 ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {X}<{p}\left({y}\right)$
145 138 139 144 3jca ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}\right)\right)$
146 63 87 jca ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({p}\left(0\right)\in {ℝ}^{*}\wedge {p}\left({y}\right)\in {ℝ}^{*}\right)$
147 146 ad2antrr ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to \left({p}\left(0\right)\in {ℝ}^{*}\wedge {p}\left({y}\right)\in {ℝ}^{*}\right)$
148 elico1 ${⊢}\left({p}\left(0\right)\in {ℝ}^{*}\wedge {p}\left({y}\right)\in {ℝ}^{*}\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}\right)\right)\right)$
149 147 148 syl ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)↔\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}\right)\right)\right)$
150 145 149 mpbird ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\wedge \left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\right)\to {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)$
151 150 ex ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\to \left(\left({X}\in {ℝ}^{*}\wedge {p}\left(0\right)\le {X}\wedge {X}<{p}\left({y}+1\right)\right)\to {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)$
152 137 151 sylbid ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)$
153 0elfz ${⊢}{y}\in {ℕ}_{0}\to 0\in \left(0\dots {y}\right)$
154 47 153 syl ${⊢}{y}\in ℕ\to 0\in \left(0\dots {y}\right)$
155 154 adantr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to 0\in \left(0\dots {y}\right)$
156 fvres ${⊢}0\in \left(0\dots {y}\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right)={p}\left(0\right)$
157 155 156 syl ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right)={p}\left(0\right)$
158 157 eqcomd ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {p}\left(0\right)=\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right)$
159 83 adantr ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {y}\in \left(0\dots {y}\right)$
160 fvres ${⊢}{y}\in \left(0\dots {y}\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)={p}\left({y}\right)$
161 159 160 syl ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)={p}\left({y}\right)$
162 161 eqcomd ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to {p}\left({y}\right)=\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)$
163 158 162 oveq12d ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left[{p}\left(0\right),{p}\left({y}\right)\right)=\left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)$
164 163 eleq2d ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)↔{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\right)$
165 164 biimpa ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\to {X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)$
166 elfzofz ${⊢}{i}\in \left(0..^{y}\right)\to {i}\in \left(0\dots {y}\right)$
167 166 adantl ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to {i}\in \left(0\dots {y}\right)$
168 fvres ${⊢}{i}\in \left(0\dots {y}\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right)={p}\left({i}\right)$
169 167 168 syl ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right)={p}\left({i}\right)$
170 fzofzp1 ${⊢}{i}\in \left(0..^{y}\right)\to {i}+1\in \left(0\dots {y}\right)$
171 170 adantl ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to {i}+1\in \left(0\dots {y}\right)$
172 fvres ${⊢}{i}+1\in \left(0\dots {y}\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)={p}\left({i}+1\right)$
173 171 172 syl ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)={p}\left({i}+1\right)$
174 173 adantlr ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to \left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)={p}\left({i}+1\right)$
175 169 174 oveq12d ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)=\left[{p}\left({i}\right),{p}\left({i}+1\right)\right)$
176 175 eleq2d ${⊢}\left(\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\wedge {i}\in \left(0..^{y}\right)\right)\to \left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)↔{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
177 176 rexbidva ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\to \left(\exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)↔\exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
178 nnz ${⊢}{y}\in ℕ\to {y}\in ℤ$
179 uzid ${⊢}{y}\in ℤ\to {y}\in {ℤ}_{\ge {y}}$
180 178 179 syl ${⊢}{y}\in ℕ\to {y}\in {ℤ}_{\ge {y}}$
181 peano2uz ${⊢}{y}\in {ℤ}_{\ge {y}}\to {y}+1\in {ℤ}_{\ge {y}}$
182 fzoss2 ${⊢}{y}+1\in {ℤ}_{\ge {y}}\to \left(0..^{y}\right)\subseteq \left(0..^{y}+1\right)$
183 180 181 182 3syl ${⊢}{y}\in ℕ\to \left(0..^{y}\right)\subseteq \left(0..^{y}+1\right)$
184 183 ad2antrr ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\to \left(0..^{y}\right)\subseteq \left(0..^{y}+1\right)$
185 ssrexv ${⊢}\left(0..^{y}\right)\subseteq \left(0..^{y}+1\right)\to \left(\exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
186 184 185 syl ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\to \left(\exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
187 177 186 sylbid ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\to \left(\exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
188 165 187 embantd ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge {X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\right)\to \left(\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
189 188 ex ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \left(\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
190 189 adantr ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \left(\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
191 152 190 syld ${⊢}\left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\wedge ¬{p}\left({y}\right)\le {X}\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \left(\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
192 191 ex ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \left(\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
193 192 com34 ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
194 193 com13 ${⊢}\left({X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left(0\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}\right),\left({{p}↾}_{\left(0\dots {y}\right)}\right)\left({i}+1\right)\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
195 135 194 sylbi
196 97 195 syl ${⊢}\left({{p}↾}_{\left(0\dots {y}\right)}\in \mathrm{RePart}\left({y}\right)\wedge \forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
197 196 ex ${⊢}{{p}↾}_{\left(0\dots {y}\right)}\in \mathrm{RePart}\left({y}\right)\to \left(\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)\right)$
198 197 com24 ${⊢}{{p}↾}_{\left(0\dots {y}\right)}\in \mathrm{RePart}\left({y}\right)\to \left(\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)\right)$
199 96 198 mpcom ${⊢}\left({y}\in ℕ\wedge {p}\in \mathrm{RePart}\left({y}+1\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
200 199 ex ${⊢}{y}\in ℕ\to \left({p}\in \mathrm{RePart}\left({y}+1\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left(\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)\right)$
201 200 com24 ${⊢}{y}\in ℕ\to \left(\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left({p}\in \mathrm{RePart}\left({y}+1\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)\right)$
202 201 imp ${⊢}\left({y}\in ℕ\wedge \forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \left(¬{p}\left({y}\right)\le {X}\to \left({p}\in \mathrm{RePart}\left({y}+1\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\right)$
203 95 202 pm2.61d ${⊢}\left({y}\in ℕ\wedge \forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \left({p}\in \mathrm{RePart}\left({y}+1\right)\to \left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
204 46 203 ralrimi ${⊢}\left({y}\in ℕ\wedge \forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)\to \forall {p}\in \mathrm{RePart}\left({y}+1\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$
205 204 ex ${⊢}{y}\in ℕ\to \left(\forall {p}\in \mathrm{RePart}\left({y}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}\right)\right)\to \exists {i}\in \left(0..^{y}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\to \forall {p}\in \mathrm{RePart}\left({y}+1\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({y}+1\right)\right)\to \exists {i}\in \left(0..^{y}+1\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)\right)$
206 10 18 26 34 43 205 nnind ${⊢}{M}\in ℕ\to \forall {p}\in \mathrm{RePart}\left({M}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in \left[{p}\left(0\right),{p}\left({M}\right)\right)\to \exists {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{X}\in \left[{p}\left({i}\right),{p}\left({i}+1\right)\right)\right)$