Metamath Proof Explorer

Theorem icceuelpartlem

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

Ref Expression
Hypotheses iccpartiun.m 
|- ( ph -> M e. NN )
iccpartiun.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion icceuelpartlem 
|- ( ph -> ( ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) -> ( I < J -> ( P ` ( I + 1 ) ) <_ ( P ` J ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpartiun.m 
 |-  ( ph -> M e. NN )
2 iccpartiun.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 fveq2 
 |-  ( ( I + 1 ) = J -> ( P ` ( I + 1 ) ) = ( P ` J ) )
4 3 olcd 
 |-  ( ( I + 1 ) = J -> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) )
5 4 a1d 
 |-  ( ( I + 1 ) = J -> ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) ) )
6 elfzoelz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ZZ )
7 elfzoelz 
 |-  ( J e. ( 0 ..^ M ) -> J e. ZZ )
8 zltp1le 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( I < J <-> ( I + 1 ) <_ J ) )
9 8 biimpcd 
 |-  ( I < J -> ( ( I e. ZZ /\ J e. ZZ ) -> ( I + 1 ) <_ J ) )
10 9 adantr 
 |-  ( ( I < J /\ -. ( I + 1 ) = J ) -> ( ( I e. ZZ /\ J e. ZZ ) -> ( I + 1 ) <_ J ) )
11 10 impcom 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( I < J /\ -. ( I + 1 ) = J ) ) -> ( I + 1 ) <_ J )
12 df-ne 
 |-  ( ( I + 1 ) =/= J <-> -. ( I + 1 ) = J )
13 necom 
 |-  ( ( I + 1 ) =/= J <-> J =/= ( I + 1 ) )
14 12 13 sylbb1 
 |-  ( -. ( I + 1 ) = J -> J =/= ( I + 1 ) )
15 14 adantl 
 |-  ( ( I < J /\ -. ( I + 1 ) = J ) -> J =/= ( I + 1 ) )
16 15 adantl 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( I < J /\ -. ( I + 1 ) = J ) ) -> J =/= ( I + 1 ) )
17 11 16 jca 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( I < J /\ -. ( I + 1 ) = J ) ) -> ( ( I + 1 ) <_ J /\ J =/= ( I + 1 ) ) )
18 peano2z 
 |-  ( I e. ZZ -> ( I + 1 ) e. ZZ )
19 18 zred 
 |-  ( I e. ZZ -> ( I + 1 ) e. RR )
20 zre 
 |-  ( J e. ZZ -> J e. RR )
21 19 20 anim12i 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( ( I + 1 ) e. RR /\ J e. RR ) )
22 21 adantr 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( I < J /\ -. ( I + 1 ) = J ) ) -> ( ( I + 1 ) e. RR /\ J e. RR ) )
23 ltlen 
 |-  ( ( ( I + 1 ) e. RR /\ J e. RR ) -> ( ( I + 1 ) < J <-> ( ( I + 1 ) <_ J /\ J =/= ( I + 1 ) ) ) )
24 22 23 syl 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( I < J /\ -. ( I + 1 ) = J ) ) -> ( ( I + 1 ) < J <-> ( ( I + 1 ) <_ J /\ J =/= ( I + 1 ) ) ) )
25 17 24 mpbird 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( I < J /\ -. ( I + 1 ) = J ) ) -> ( I + 1 ) < J )
26 25 ex 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( ( I < J /\ -. ( I + 1 ) = J ) -> ( I + 1 ) < J ) )
27 6 7 26 syl2an 
 |-  ( ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) -> ( ( I < J /\ -. ( I + 1 ) = J ) -> ( I + 1 ) < J ) )
28 27 adantl 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( ( I < J /\ -. ( I + 1 ) = J ) -> ( I + 1 ) < J ) )
29 1 2 iccpartgt 
 |-  ( ph -> A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( i < j -> ( P ` i ) < ( P ` j ) ) )
30 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
31 elfzofz 
 |-  ( J e. ( 0 ..^ M ) -> J e. ( 0 ... M ) )
32 breq1 
 |-  ( i = ( I + 1 ) -> ( i < j <-> ( I + 1 ) < j ) )
33 fveq2 
 |-  ( i = ( I + 1 ) -> ( P ` i ) = ( P ` ( I + 1 ) ) )
34 33 breq1d 
 |-  ( i = ( I + 1 ) -> ( ( P ` i ) < ( P ` j ) <-> ( P ` ( I + 1 ) ) < ( P ` j ) ) )
35 32 34 imbi12d 
 |-  ( i = ( I + 1 ) -> ( ( i < j -> ( P ` i ) < ( P ` j ) ) <-> ( ( I + 1 ) < j -> ( P ` ( I + 1 ) ) < ( P ` j ) ) ) )
36 breq2 
 |-  ( j = J -> ( ( I + 1 ) < j <-> ( I + 1 ) < J ) )
37 fveq2 
 |-  ( j = J -> ( P ` j ) = ( P ` J ) )
38 37 breq2d 
 |-  ( j = J -> ( ( P ` ( I + 1 ) ) < ( P ` j ) <-> ( P ` ( I + 1 ) ) < ( P ` J ) ) )
39 36 38 imbi12d 
 |-  ( j = J -> ( ( ( I + 1 ) < j -> ( P ` ( I + 1 ) ) < ( P ` j ) ) <-> ( ( I + 1 ) < J -> ( P ` ( I + 1 ) ) < ( P ` J ) ) ) )
40 35 39 rspc2v 
 |-  ( ( ( I + 1 ) e. ( 0 ... M ) /\ J e. ( 0 ... M ) ) -> ( A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( i < j -> ( P ` i ) < ( P ` j ) ) -> ( ( I + 1 ) < J -> ( P ` ( I + 1 ) ) < ( P ` J ) ) ) )
41 30 31 40 syl2an 
 |-  ( ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) -> ( A. i e. ( 0 ... M ) A. j e. ( 0 ... M ) ( i < j -> ( P ` i ) < ( P ` j ) ) -> ( ( I + 1 ) < J -> ( P ` ( I + 1 ) ) < ( P ` J ) ) ) )
42 29 41 mpan9 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( ( I + 1 ) < J -> ( P ` ( I + 1 ) ) < ( P ` J ) ) )
43 28 42 syld 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( ( I < J /\ -. ( I + 1 ) = J ) -> ( P ` ( I + 1 ) ) < ( P ` J ) ) )
44 43 expdimp 
 |-  ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( -. ( I + 1 ) = J -> ( P ` ( I + 1 ) ) < ( P ` J ) ) )
45 44 impcom 
 |-  ( ( -. ( I + 1 ) = J /\ ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) ) -> ( P ` ( I + 1 ) ) < ( P ` J ) )
46 45 orcd 
 |-  ( ( -. ( I + 1 ) = J /\ ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) ) -> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) )
47 46 ex 
 |-  ( -. ( I + 1 ) = J -> ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) ) )
48 5 47 pm2.61i 
 |-  ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) )
49 1 adantr 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> M e. NN )
50 2 adantr 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> P e. ( RePart ` M ) )
51 30 adantr 
 |-  ( ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) -> ( I + 1 ) e. ( 0 ... M ) )
52 51 adantl 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( I + 1 ) e. ( 0 ... M ) )
53 49 50 52 iccpartxr 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( P ` ( I + 1 ) ) e. RR* )
54 31 adantl 
 |-  ( ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) -> J e. ( 0 ... M ) )
55 54 adantl 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> J e. ( 0 ... M ) )
56 49 50 55 iccpartxr 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( P ` J ) e. RR* )
57 53 56 jca 
 |-  ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) -> ( ( P ` ( I + 1 ) ) e. RR* /\ ( P ` J ) e. RR* ) )
58 57 adantr 
 |-  ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( ( P ` ( I + 1 ) ) e. RR* /\ ( P ` J ) e. RR* ) )
59 xrleloe 
 |-  ( ( ( P ` ( I + 1 ) ) e. RR* /\ ( P ` J ) e. RR* ) -> ( ( P ` ( I + 1 ) ) <_ ( P ` J ) <-> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) ) )
60 58 59 syl 
 |-  ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( ( P ` ( I + 1 ) ) <_ ( P ` J ) <-> ( ( P ` ( I + 1 ) ) < ( P ` J ) \/ ( P ` ( I + 1 ) ) = ( P ` J ) ) ) )
61 48 60 mpbird 
 |-  ( ( ( ph /\ ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) ) /\ I < J ) -> ( P ` ( I + 1 ) ) <_ ( P ` J ) )
62 61 exp31 
 |-  ( ph -> ( ( I e. ( 0 ..^ M ) /\ J e. ( 0 ..^ M ) ) -> ( I < J -> ( P ` ( I + 1 ) ) <_ ( P ` J ) ) ) )