Metamath Proof Explorer

Theorem iccpartlt

Description: If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 in GS's mathbox. (Contributed by AV, 12-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartlt 
|- ( ph -> ( P ` 0 ) < ( P ` M ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m 
 |-  ( ph -> M e. NN )
2 iccpartgtprec.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 lbfzo0 
 |-  ( 0 e. ( 0 ..^ M ) <-> M e. NN )
4 1 3 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
5 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ 0 e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` 0 ) < ( P ` ( 0 + 1 ) ) ) )
6 1 2 4 5 syl3anc 
 |-  ( ph -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` 0 ) < ( P ` ( 0 + 1 ) ) ) )
7 6 simprd 
 |-  ( ph -> ( P ` 0 ) < ( P ` ( 0 + 1 ) ) )
8 7 adantl 
 |-  ( ( M = 1 /\ ph ) -> ( P ` 0 ) < ( P ` ( 0 + 1 ) ) )
9 fveq2 
 |-  ( M = 1 -> ( P ` M ) = ( P ` 1 ) )
10 1e0p1 
 |-  1 = ( 0 + 1 )
11 10 fveq2i 
 |-  ( P ` 1 ) = ( P ` ( 0 + 1 ) )
12 9 11 eqtrdi 
 |-  ( M = 1 -> ( P ` M ) = ( P ` ( 0 + 1 ) ) )
13 12 adantr 
 |-  ( ( M = 1 /\ ph ) -> ( P ` M ) = ( P ` ( 0 + 1 ) ) )
14 8 13 breqtrrd 
 |-  ( ( M = 1 /\ ph ) -> ( P ` 0 ) < ( P ` M ) )
15 14 ex 
 |-  ( M = 1 -> ( ph -> ( P ` 0 ) < ( P ` M ) ) )
16 1 2 iccpartiltu 
 |-  ( ph -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) )
17 1 2 iccpartigtl 
 |-  ( ph -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )
18 1nn 
 |-  1 e. NN
19 18 a1i 
 |-  ( ( ph /\ -. M = 1 ) -> 1 e. NN )
20 1 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> M e. NN )
21 df-ne 
 |-  ( M =/= 1 <-> -. M = 1 )
22 1 nnge1d 
 |-  ( ph -> 1 <_ M )
23 1red 
 |-  ( ph -> 1 e. RR )
24 1 nnred 
 |-  ( ph -> M e. RR )
25 23 24 ltlend 
 |-  ( ph -> ( 1 < M <-> ( 1 <_ M /\ M =/= 1 ) ) )
26 25 biimprd 
 |-  ( ph -> ( ( 1 <_ M /\ M =/= 1 ) -> 1 < M ) )
27 22 26 mpand 
 |-  ( ph -> ( M =/= 1 -> 1 < M ) )
28 21 27 syl5bir 
 |-  ( ph -> ( -. M = 1 -> 1 < M ) )
29 28 imp 
 |-  ( ( ph /\ -. M = 1 ) -> 1 < M )
30 elfzo1 
 |-  ( 1 e. ( 1 ..^ M ) <-> ( 1 e. NN /\ M e. NN /\ 1 < M ) )
31 19 20 29 30 syl3anbrc 
 |-  ( ( ph /\ -. M = 1 ) -> 1 e. ( 1 ..^ M ) )
32 fveq2 
 |-  ( i = 1 -> ( P ` i ) = ( P ` 1 ) )
33 32 breq2d 
 |-  ( i = 1 -> ( ( P ` 0 ) < ( P ` i ) <-> ( P ` 0 ) < ( P ` 1 ) ) )
34 33 rspcv 
 |-  ( 1 e. ( 1 ..^ M ) -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) -> ( P ` 0 ) < ( P ` 1 ) ) )
35 31 34 syl 
 |-  ( ( ph /\ -. M = 1 ) -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) -> ( P ` 0 ) < ( P ` 1 ) ) )
36 32 breq1d 
 |-  ( i = 1 -> ( ( P ` i ) < ( P ` M ) <-> ( P ` 1 ) < ( P ` M ) ) )
37 36 rspcv 
 |-  ( 1 e. ( 1 ..^ M ) -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( P ` 1 ) < ( P ` M ) ) )
38 31 37 syl 
 |-  ( ( ph /\ -. M = 1 ) -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( P ` 1 ) < ( P ` M ) ) )
39 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
40 0elfz 
 |-  ( M e. NN0 -> 0 e. ( 0 ... M ) )
41 1 39 40 3syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
42 1 2 41 iccpartxr 
 |-  ( ph -> ( P ` 0 ) e. RR* )
43 42 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> ( P ` 0 ) e. RR* )
44 2 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> P e. ( RePart ` M ) )
45 1nn0 
 |-  1 e. NN0
46 45 a1i 
 |-  ( ( ph /\ -. M = 1 ) -> 1 e. NN0 )
47 1 39 syl 
 |-  ( ph -> M e. NN0 )
48 47 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> M e. NN0 )
49 22 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> 1 <_ M )
50 elfz2nn0 
 |-  ( 1 e. ( 0 ... M ) <-> ( 1 e. NN0 /\ M e. NN0 /\ 1 <_ M ) )
51 46 48 49 50 syl3anbrc 
 |-  ( ( ph /\ -. M = 1 ) -> 1 e. ( 0 ... M ) )
52 20 44 51 iccpartxr 
 |-  ( ( ph /\ -. M = 1 ) -> ( P ` 1 ) e. RR* )
53 nn0fz0 
 |-  ( M e. NN0 <-> M e. ( 0 ... M ) )
54 39 53 sylib 
 |-  ( M e. NN -> M e. ( 0 ... M ) )
55 1 54 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
56 1 2 55 iccpartxr 
 |-  ( ph -> ( P ` M ) e. RR* )
57 56 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> ( P ` M ) e. RR* )
58 xrlttr 
 |-  ( ( ( P ` 0 ) e. RR* /\ ( P ` 1 ) e. RR* /\ ( P ` M ) e. RR* ) -> ( ( ( P ` 0 ) < ( P ` 1 ) /\ ( P ` 1 ) < ( P ` M ) ) -> ( P ` 0 ) < ( P ` M ) ) )
59 43 52 57 58 syl3anc 
 |-  ( ( ph /\ -. M = 1 ) -> ( ( ( P ` 0 ) < ( P ` 1 ) /\ ( P ` 1 ) < ( P ` M ) ) -> ( P ` 0 ) < ( P ` M ) ) )
60 59 expcomd 
 |-  ( ( ph /\ -. M = 1 ) -> ( ( P ` 1 ) < ( P ` M ) -> ( ( P ` 0 ) < ( P ` 1 ) -> ( P ` 0 ) < ( P ` M ) ) ) )
61 38 60 syld 
 |-  ( ( ph /\ -. M = 1 ) -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( ( P ` 0 ) < ( P ` 1 ) -> ( P ` 0 ) < ( P ` M ) ) ) )
62 61 com23 
 |-  ( ( ph /\ -. M = 1 ) -> ( ( P ` 0 ) < ( P ` 1 ) -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( P ` 0 ) < ( P ` M ) ) ) )
63 35 62 syld 
 |-  ( ( ph /\ -. M = 1 ) -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( P ` 0 ) < ( P ` M ) ) ) )
64 63 ex 
 |-  ( ph -> ( -. M = 1 -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( P ` 0 ) < ( P ` M ) ) ) ) )
65 64 com24 
 |-  ( ph -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) -> ( -. M = 1 -> ( P ` 0 ) < ( P ` M ) ) ) ) )
66 16 17 65 mp2d 
 |-  ( ph -> ( -. M = 1 -> ( P ` 0 ) < ( P ` M ) ) )
67 66 com12 
 |-  ( -. M = 1 -> ( ph -> ( P ` 0 ) < ( P ` M ) ) )
68 15 67 pm2.61i 
 |-  ( ph -> ( P ` 0 ) < ( P ` M ) )