Metamath Proof Explorer

Theorem icceuelpartlem

Description: Lemma for icceuelpart . (Contributed by AV, 19-Jul-2020)

Ref Expression
Hypotheses iccpartiun.m ${⊢}{\phi }\to {M}\in ℕ$
iccpartiun.p ${⊢}{\phi }\to {P}\in \mathrm{RePart}\left({M}\right)$
Assertion icceuelpartlem ${⊢}{\phi }\to \left(\left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\to \left({I}<{J}\to {P}\left({I}+1\right)\le {P}\left({J}\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 iccpartiun.m ${⊢}{\phi }\to {M}\in ℕ$
2 iccpartiun.p ${⊢}{\phi }\to {P}\in \mathrm{RePart}\left({M}\right)$
3 fveq2 ${⊢}{I}+1={J}\to {P}\left({I}+1\right)={P}\left({J}\right)$
4 3 olcd ${⊢}{I}+1={J}\to \left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)$
5 4 a1d ${⊢}{I}+1={J}\to \left(\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to \left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)\right)$
6 elfzoelz ${⊢}{I}\in \left(0..^{M}\right)\to {I}\in ℤ$
7 elfzoelz ${⊢}{J}\in \left(0..^{M}\right)\to {J}\in ℤ$
8 zltp1le ${⊢}\left({I}\in ℤ\wedge {J}\in ℤ\right)\to \left({I}<{J}↔{I}+1\le {J}\right)$
9 8 biimpcd ${⊢}{I}<{J}\to \left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\to {I}+1\le {J}\right)$
10 9 adantr ${⊢}\left({I}<{J}\wedge ¬{I}+1={J}\right)\to \left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\to {I}+1\le {J}\right)$
11 10 impcom ${⊢}\left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}<{J}\wedge ¬{I}+1={J}\right)\right)\to {I}+1\le {J}$
12 df-ne ${⊢}{I}+1\ne {J}↔¬{I}+1={J}$
13 necom ${⊢}{I}+1\ne {J}↔{J}\ne {I}+1$
14 12 13 sylbb1 ${⊢}¬{I}+1={J}\to {J}\ne {I}+1$
15 14 adantl ${⊢}\left({I}<{J}\wedge ¬{I}+1={J}\right)\to {J}\ne {I}+1$
16 15 adantl ${⊢}\left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}<{J}\wedge ¬{I}+1={J}\right)\right)\to {J}\ne {I}+1$
17 11 16 jca ${⊢}\left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}<{J}\wedge ¬{I}+1={J}\right)\right)\to \left({I}+1\le {J}\wedge {J}\ne {I}+1\right)$
18 peano2z ${⊢}{I}\in ℤ\to {I}+1\in ℤ$
19 18 zred ${⊢}{I}\in ℤ\to {I}+1\in ℝ$
20 zre ${⊢}{J}\in ℤ\to {J}\in ℝ$
21 19 20 anim12i ${⊢}\left({I}\in ℤ\wedge {J}\in ℤ\right)\to \left({I}+1\in ℝ\wedge {J}\in ℝ\right)$
22 21 adantr ${⊢}\left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}<{J}\wedge ¬{I}+1={J}\right)\right)\to \left({I}+1\in ℝ\wedge {J}\in ℝ\right)$
23 ltlen ${⊢}\left({I}+1\in ℝ\wedge {J}\in ℝ\right)\to \left({I}+1<{J}↔\left({I}+1\le {J}\wedge {J}\ne {I}+1\right)\right)$
24 22 23 syl ${⊢}\left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}<{J}\wedge ¬{I}+1={J}\right)\right)\to \left({I}+1<{J}↔\left({I}+1\le {J}\wedge {J}\ne {I}+1\right)\right)$
25 17 24 mpbird ${⊢}\left(\left({I}\in ℤ\wedge {J}\in ℤ\right)\wedge \left({I}<{J}\wedge ¬{I}+1={J}\right)\right)\to {I}+1<{J}$
26 25 ex ${⊢}\left({I}\in ℤ\wedge {J}\in ℤ\right)\to \left(\left({I}<{J}\wedge ¬{I}+1={J}\right)\to {I}+1<{J}\right)$
27 6 7 26 syl2an ${⊢}\left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\to \left(\left({I}<{J}\wedge ¬{I}+1={J}\right)\to {I}+1<{J}\right)$
28 27 adantl ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to \left(\left({I}<{J}\wedge ¬{I}+1={J}\right)\to {I}+1<{J}\right)$
29 1 2 iccpartgt ${⊢}{\phi }\to \forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}\left({i}<{j}\to {P}\left({i}\right)<{P}\left({j}\right)\right)$
30 fzofzp1 ${⊢}{I}\in \left(0..^{M}\right)\to {I}+1\in \left(0\dots {M}\right)$
31 elfzofz ${⊢}{J}\in \left(0..^{M}\right)\to {J}\in \left(0\dots {M}\right)$
32 breq1 ${⊢}{i}={I}+1\to \left({i}<{j}↔{I}+1<{j}\right)$
33 fveq2 ${⊢}{i}={I}+1\to {P}\left({i}\right)={P}\left({I}+1\right)$
34 33 breq1d ${⊢}{i}={I}+1\to \left({P}\left({i}\right)<{P}\left({j}\right)↔{P}\left({I}+1\right)<{P}\left({j}\right)\right)$
35 32 34 imbi12d ${⊢}{i}={I}+1\to \left(\left({i}<{j}\to {P}\left({i}\right)<{P}\left({j}\right)\right)↔\left({I}+1<{j}\to {P}\left({I}+1\right)<{P}\left({j}\right)\right)\right)$
36 breq2 ${⊢}{j}={J}\to \left({I}+1<{j}↔{I}+1<{J}\right)$
37 fveq2 ${⊢}{j}={J}\to {P}\left({j}\right)={P}\left({J}\right)$
38 37 breq2d ${⊢}{j}={J}\to \left({P}\left({I}+1\right)<{P}\left({j}\right)↔{P}\left({I}+1\right)<{P}\left({J}\right)\right)$
39 36 38 imbi12d ${⊢}{j}={J}\to \left(\left({I}+1<{j}\to {P}\left({I}+1\right)<{P}\left({j}\right)\right)↔\left({I}+1<{J}\to {P}\left({I}+1\right)<{P}\left({J}\right)\right)\right)$
40 35 39 rspc2v ${⊢}\left({I}+1\in \left(0\dots {M}\right)\wedge {J}\in \left(0\dots {M}\right)\right)\to \left(\forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}\left({i}<{j}\to {P}\left({i}\right)<{P}\left({j}\right)\right)\to \left({I}+1<{J}\to {P}\left({I}+1\right)<{P}\left({J}\right)\right)\right)$
41 30 31 40 syl2an ${⊢}\left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\to \left(\forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}\left({i}<{j}\to {P}\left({i}\right)<{P}\left({j}\right)\right)\to \left({I}+1<{J}\to {P}\left({I}+1\right)<{P}\left({J}\right)\right)\right)$
42 29 41 mpan9 ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to \left({I}+1<{J}\to {P}\left({I}+1\right)<{P}\left({J}\right)\right)$
43 28 42 syld ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to \left(\left({I}<{J}\wedge ¬{I}+1={J}\right)\to {P}\left({I}+1\right)<{P}\left({J}\right)\right)$
44 43 expdimp ${⊢}\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to \left(¬{I}+1={J}\to {P}\left({I}+1\right)<{P}\left({J}\right)\right)$
45 44 impcom ${⊢}\left(¬{I}+1={J}\wedge \left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\right)\to {P}\left({I}+1\right)<{P}\left({J}\right)$
46 45 orcd ${⊢}\left(¬{I}+1={J}\wedge \left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\right)\to \left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)$
47 46 ex ${⊢}¬{I}+1={J}\to \left(\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to \left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)\right)$
48 5 47 pm2.61i ${⊢}\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to \left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)$
49 1 adantr ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to {M}\in ℕ$
50 2 adantr ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to {P}\in \mathrm{RePart}\left({M}\right)$
51 30 adantr ${⊢}\left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\to {I}+1\in \left(0\dots {M}\right)$
52 51 adantl ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to {I}+1\in \left(0\dots {M}\right)$
53 49 50 52 iccpartxr ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to {P}\left({I}+1\right)\in {ℝ}^{*}$
54 31 adantl ${⊢}\left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\to {J}\in \left(0\dots {M}\right)$
55 54 adantl ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to {J}\in \left(0\dots {M}\right)$
56 49 50 55 iccpartxr ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to {P}\left({J}\right)\in {ℝ}^{*}$
57 53 56 jca ${⊢}\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\to \left({P}\left({I}+1\right)\in {ℝ}^{*}\wedge {P}\left({J}\right)\in {ℝ}^{*}\right)$
58 57 adantr ${⊢}\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to \left({P}\left({I}+1\right)\in {ℝ}^{*}\wedge {P}\left({J}\right)\in {ℝ}^{*}\right)$
59 xrleloe ${⊢}\left({P}\left({I}+1\right)\in {ℝ}^{*}\wedge {P}\left({J}\right)\in {ℝ}^{*}\right)\to \left({P}\left({I}+1\right)\le {P}\left({J}\right)↔\left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)\right)$
60 58 59 syl ${⊢}\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to \left({P}\left({I}+1\right)\le {P}\left({J}\right)↔\left({P}\left({I}+1\right)<{P}\left({J}\right)\vee {P}\left({I}+1\right)={P}\left({J}\right)\right)\right)$
61 48 60 mpbird ${⊢}\left(\left({\phi }\wedge \left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\right)\wedge {I}<{J}\right)\to {P}\left({I}+1\right)\le {P}\left({J}\right)$
62 61 exp31 ${⊢}{\phi }\to \left(\left({I}\in \left(0..^{M}\right)\wedge {J}\in \left(0..^{M}\right)\right)\to \left({I}<{J}\to {P}\left({I}+1\right)\le {P}\left({J}\right)\right)\right)$