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 φ M
iccpartgtprec.p φ P RePart M
Assertion iccpartlt φ P 0 < P M

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m φ M
2 iccpartgtprec.p φ P RePart M
3 lbfzo0 0 0 ..^ M M
4 1 3 sylibr φ 0 0 ..^ M
5 iccpartimp M P RePart M 0 0 ..^ M P * 0 M P 0 < P 0 + 1
6 1 2 4 5 syl3anc φ P * 0 M P 0 < P 0 + 1
7 6 simprd φ P 0 < P 0 + 1
8 7 adantl M = 1 φ 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 φ P M = P 0 + 1
14 8 13 breqtrrd M = 1 φ P 0 < P M
15 14 ex M = 1 φ P 0 < P M
16 1 2 iccpartiltu φ i 1 ..^ M P i < P M
17 1 2 iccpartigtl φ i 1 ..^ M P 0 < P i
18 1nn 1
19 18 a1i φ ¬ M = 1 1
20 1 adantr φ ¬ M = 1 M
21 df-ne M 1 ¬ M = 1
22 1 nnge1d φ 1 M
23 1red φ 1
24 1 nnred φ M
25 23 24 ltlend φ 1 < M 1 M M 1
26 25 biimprd φ 1 M M 1 1 < M
27 22 26 mpand φ M 1 1 < M
28 21 27 syl5bir φ ¬ M = 1 1 < M
29 28 imp φ ¬ M = 1 1 < M
30 elfzo1 1 1 ..^ M 1 M 1 < M
31 19 20 29 30 syl3anbrc φ ¬ M = 1 1 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 1 ..^ M i 1 ..^ M P 0 < P i P 0 < P 1
35 31 34 syl φ ¬ M = 1 i 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 1 ..^ M i 1 ..^ M P i < P M P 1 < P M
38 31 37 syl φ ¬ M = 1 i 1 ..^ M P i < P M P 1 < P M
39 nnnn0 M M 0
40 0elfz M 0 0 0 M
41 1 39 40 3syl φ 0 0 M
42 1 2 41 iccpartxr φ P 0 *
43 42 adantr φ ¬ M = 1 P 0 *
44 2 adantr φ ¬ M = 1 P RePart M
45 1nn0 1 0
46 45 a1i φ ¬ M = 1 1 0
47 1 39 syl φ M 0
48 47 adantr φ ¬ M = 1 M 0
49 22 adantr φ ¬ M = 1 1 M
50 elfz2nn0 1 0 M 1 0 M 0 1 M
51 46 48 49 50 syl3anbrc φ ¬ M = 1 1 0 M
52 20 44 51 iccpartxr φ ¬ M = 1 P 1 *
53 nn0fz0 M 0 M 0 M
54 39 53 sylib M M 0 M
55 1 54 syl φ M 0 M
56 1 2 55 iccpartxr φ P M *
57 56 adantr φ ¬ M = 1 P M *
58 xrlttr P 0 * P 1 * P M * P 0 < P 1 P 1 < P M P 0 < P M
59 43 52 57 58 syl3anc φ ¬ M = 1 P 0 < P 1 P 1 < P M P 0 < P M
60 59 expcomd φ ¬ M = 1 P 1 < P M P 0 < P 1 P 0 < P M
61 38 60 syld φ ¬ M = 1 i 1 ..^ M P i < P M P 0 < P 1 P 0 < P M
62 61 com23 φ ¬ M = 1 P 0 < P 1 i 1 ..^ M P i < P M P 0 < P M
63 35 62 syld φ ¬ M = 1 i 1 ..^ M P 0 < P i i 1 ..^ M P i < P M P 0 < P M
64 63 ex φ ¬ M = 1 i 1 ..^ M P 0 < P i i 1 ..^ M P i < P M P 0 < P M
65 64 com24 φ i 1 ..^ M P i < P M i 1 ..^ M P 0 < P i ¬ M = 1 P 0 < P M
66 16 17 65 mp2d φ ¬ M = 1 P 0 < P M
67 66 com12 ¬ M = 1 φ P 0 < P M
68 15 67 pm2.61i φ P 0 < P M