Metamath Proof Explorer


Theorem iccpartigtl

Description: If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ( 𝜑𝑀 ∈ ℕ )
iccpartgtprec.p ( 𝜑𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartigtl ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ( 𝜑𝑀 ∈ ℕ )
2 iccpartgtprec.p ( 𝜑𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 ral0 𝑖 ∈ ∅ ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 )
4 oveq2 ( 𝑀 = 1 → ( 1 ..^ 𝑀 ) = ( 1 ..^ 1 ) )
5 fzo0 ( 1 ..^ 1 ) = ∅
6 4 5 eqtrdi ( 𝑀 = 1 → ( 1 ..^ 𝑀 ) = ∅ )
7 6 raleqdv ( 𝑀 = 1 → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ↔ ∀ 𝑖 ∈ ∅ ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
8 3 7 mpbiri ( 𝑀 = 1 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
9 8 a1d ( 𝑀 = 1 → ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
10 1 nnnn0d ( 𝜑𝑀 ∈ ℕ0 )
11 0elfz ( 𝑀 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑀 ) )
12 10 11 syl ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
13 1 2 12 iccpartxr ( 𝜑 → ( 𝑃 ‘ 0 ) ∈ ℝ* )
14 13 adantr ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( 𝑃 ‘ 0 ) ∈ ℝ* )
15 elxr ( ( 𝑃 ‘ 0 ) ∈ ℝ* ↔ ( ( 𝑃 ‘ 0 ) ∈ ℝ ∨ ( 𝑃 ‘ 0 ) = +∞ ∨ ( 𝑃 ‘ 0 ) = -∞ ) )
16 0zd ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 0 ∈ ℤ )
17 elfzouz ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑖 ∈ ( ℤ ‘ 1 ) )
18 0p1e1 ( 0 + 1 ) = 1
19 18 fveq2i ( ℤ ‘ ( 0 + 1 ) ) = ( ℤ ‘ 1 )
20 17 19 eleqtrrdi ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑖 ∈ ( ℤ ‘ ( 0 + 1 ) ) )
21 20 adantl ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑖 ∈ ( ℤ ‘ ( 0 + 1 ) ) )
22 fveq2 ( 𝑘 = 0 → ( 𝑃𝑘 ) = ( 𝑃 ‘ 0 ) )
23 22 eqcomd ( 𝑘 = 0 → ( 𝑃 ‘ 0 ) = ( 𝑃𝑘 ) )
24 23 eleq1d ( 𝑘 = 0 → ( ( 𝑃 ‘ 0 ) ∈ ℝ ↔ ( 𝑃𝑘 ) ∈ ℝ ) )
25 24 biimpcd ( ( 𝑃 ‘ 0 ) ∈ ℝ → ( 𝑘 = 0 → ( 𝑃𝑘 ) ∈ ℝ ) )
26 25 ad3antrrr ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑘 = 0 → ( 𝑃𝑘 ) ∈ ℝ ) )
27 1 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) ) → 𝑀 ∈ ℕ )
28 2 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
29 elfz2nn0 ( 𝑘 ∈ ( 0 ... 𝑖 ) ↔ ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) )
30 elfzo2 ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) )
31 simpl1 ( ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) ∧ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) ) → 𝑘 ∈ ℕ0 )
32 simpr2 ( ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) ∧ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) ) → 𝑀 ∈ ℤ )
33 nn0ge0 ( 𝑖 ∈ ℕ0 → 0 ≤ 𝑖 )
34 0red ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → 0 ∈ ℝ )
35 eluzelre ( 𝑖 ∈ ( ℤ ‘ 1 ) → 𝑖 ∈ ℝ )
36 35 adantr ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → 𝑖 ∈ ℝ )
37 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
38 37 adantl ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℝ )
39 lelttr ( ( 0 ∈ ℝ ∧ 𝑖 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 ≤ 𝑖𝑖 < 𝑀 ) → 0 < 𝑀 ) )
40 34 36 38 39 syl3anc ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → ( ( 0 ≤ 𝑖𝑖 < 𝑀 ) → 0 < 𝑀 ) )
41 40 expcomd ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑖 < 𝑀 → ( 0 ≤ 𝑖 → 0 < 𝑀 ) ) )
42 41 3impia ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → ( 0 ≤ 𝑖 → 0 < 𝑀 ) )
43 33 42 syl5com ( 𝑖 ∈ ℕ0 → ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → 0 < 𝑀 ) )
44 43 3ad2ant2 ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) → ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → 0 < 𝑀 ) )
45 44 imp ( ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) ∧ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) ) → 0 < 𝑀 )
46 elnnz ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
47 32 45 46 sylanbrc ( ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) ∧ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) ) → 𝑀 ∈ ℕ )
48 nn0re ( 𝑘 ∈ ℕ0𝑘 ∈ ℝ )
49 48 ad2antrl ( ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) ) → 𝑘 ∈ ℝ )
50 nn0re ( 𝑖 ∈ ℕ0𝑖 ∈ ℝ )
51 50 adantl ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℝ )
52 51 adantl ( ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) ) → 𝑖 ∈ ℝ )
53 38 adantr ( ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) ) → 𝑀 ∈ ℝ )
54 lelttr ( ( 𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 𝑘𝑖𝑖 < 𝑀 ) → 𝑘 < 𝑀 ) )
55 54 expd ( ( 𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑘𝑖 → ( 𝑖 < 𝑀𝑘 < 𝑀 ) ) )
56 49 52 53 55 syl3anc ( ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) ) → ( 𝑘𝑖 → ( 𝑖 < 𝑀𝑘 < 𝑀 ) ) )
57 56 exp31 ( 𝑖 ∈ ( ℤ ‘ 1 ) → ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) → ( 𝑘𝑖 → ( 𝑖 < 𝑀𝑘 < 𝑀 ) ) ) ) )
58 57 com34 ( 𝑖 ∈ ( ℤ ‘ 1 ) → ( 𝑀 ∈ ℤ → ( 𝑘𝑖 → ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) → ( 𝑖 < 𝑀𝑘 < 𝑀 ) ) ) ) )
59 58 com35 ( 𝑖 ∈ ( ℤ ‘ 1 ) → ( 𝑀 ∈ ℤ → ( 𝑖 < 𝑀 → ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) → ( 𝑘𝑖𝑘 < 𝑀 ) ) ) ) )
60 59 3imp ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ) → ( 𝑘𝑖𝑘 < 𝑀 ) ) )
61 60 expdcom ( 𝑘 ∈ ℕ0 → ( 𝑖 ∈ ℕ0 → ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → ( 𝑘𝑖𝑘 < 𝑀 ) ) ) )
62 61 com34 ( 𝑘 ∈ ℕ0 → ( 𝑖 ∈ ℕ0 → ( 𝑘𝑖 → ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → 𝑘 < 𝑀 ) ) ) )
63 62 3imp1 ( ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) ∧ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) ) → 𝑘 < 𝑀 )
64 elfzo0 ( 𝑘 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑘 ∈ ℕ0𝑀 ∈ ℕ ∧ 𝑘 < 𝑀 ) )
65 31 47 63 64 syl3anbrc ( ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) ∧ ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
66 65 ex ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) → ( ( 𝑖 ∈ ( ℤ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
67 30 66 syl5bi ( ( 𝑘 ∈ ℕ0𝑖 ∈ ℕ0𝑘𝑖 ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
68 29 67 sylbi ( 𝑘 ∈ ( 0 ... 𝑖 ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
69 68 adantr ( ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
70 69 impcom ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
71 simpr ( ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) → 𝑘 ≠ 0 )
72 71 adantl ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) → 𝑘 ≠ 0 )
73 fzo1fzo0n0 ( 𝑘 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑘 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ≠ 0 ) )
74 70 72 73 sylanbrc ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) )
75 74 adantl ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) )
76 27 28 75 iccpartipre ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) ) ) → ( 𝑃𝑘 ) ∈ ℝ )
77 76 exp32 ( 𝜑 → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) → ( 𝑃𝑘 ) ∈ ℝ ) ) )
78 77 ad2antrl ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) → ( 𝑃𝑘 ) ∈ ℝ ) ) )
79 78 imp ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑖 ) ∧ 𝑘 ≠ 0 ) → ( 𝑃𝑘 ) ∈ ℝ ) )
80 79 expdimp ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑘 ≠ 0 → ( 𝑃𝑘 ) ∈ ℝ ) )
81 26 80 pm2.61dne ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑃𝑘 ) ∈ ℝ )
82 1 adantr ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑀 ∈ ℕ )
83 82 ad3antlr ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℕ )
84 2 adantr ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
85 84 ad3antlr ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
86 elfzoelz ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑖 ∈ ℤ )
87 86 adantl ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑖 ∈ ℤ )
88 fzoval ( 𝑖 ∈ ℤ → ( 0 ..^ 𝑖 ) = ( 0 ... ( 𝑖 − 1 ) ) )
89 88 eqcomd ( 𝑖 ∈ ℤ → ( 0 ... ( 𝑖 − 1 ) ) = ( 0 ..^ 𝑖 ) )
90 87 89 syl ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 0 ... ( 𝑖 − 1 ) ) = ( 0 ..^ 𝑖 ) )
91 90 eleq2d ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) ↔ 𝑘 ∈ ( 0 ..^ 𝑖 ) ) )
92 elfzouz2 ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑀 ∈ ( ℤ𝑖 ) )
93 92 adantl ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑀 ∈ ( ℤ𝑖 ) )
94 fzoss2 ( 𝑀 ∈ ( ℤ𝑖 ) → ( 0 ..^ 𝑖 ) ⊆ ( 0 ..^ 𝑀 ) )
95 93 94 syl ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 0 ..^ 𝑖 ) ⊆ ( 0 ..^ 𝑀 ) )
96 95 sseld ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑘 ∈ ( 0 ..^ 𝑖 ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
97 91 96 sylbid ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
98 97 imp ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
99 iccpartimp ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
100 83 85 98 99 syl3anc ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
101 100 simprd ( ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝑃𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
102 16 21 81 101 smonoord ( ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
103 102 ralrimiva ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
104 103 ex ( ( 𝑃 ‘ 0 ) ∈ ℝ → ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
105 lbfzo0 ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑀 ∈ ℕ )
106 1 105 sylibr ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
107 1 2 106 3jca ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) )
108 107 ad2antrl ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) )
109 108 adantr ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) )
110 iccpartimp ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
111 109 110 syl ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ*m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
112 111 simprd ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) )
113 breq1 ( ( 𝑃 ‘ 0 ) = +∞ → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ↔ +∞ < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
114 113 adantr ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ↔ +∞ < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
115 114 adantr ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ ( 0 + 1 ) ) ↔ +∞ < ( 𝑃 ‘ ( 0 + 1 ) ) ) )
116 112 115 mpbid ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → +∞ < ( 𝑃 ‘ ( 0 + 1 ) ) )
117 1 ad2antrl ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → 𝑀 ∈ ℕ )
118 117 adantr ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ )
119 2 ad2antrl ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
120 119 adantr ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
121 1nn0 1 ∈ ℕ0
122 121 a1i ( 𝑀 ∈ ℕ → 1 ∈ ℕ0 )
123 nnnn0 ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
124 nnge1 ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
125 122 123 124 3jca ( 𝑀 ∈ ℕ → ( 1 ∈ ℕ0𝑀 ∈ ℕ0 ∧ 1 ≤ 𝑀 ) )
126 1 125 syl ( 𝜑 → ( 1 ∈ ℕ0𝑀 ∈ ℕ0 ∧ 1 ≤ 𝑀 ) )
127 elfz2nn0 ( 1 ∈ ( 0 ... 𝑀 ) ↔ ( 1 ∈ ℕ0𝑀 ∈ ℕ0 ∧ 1 ≤ 𝑀 ) )
128 126 127 sylibr ( 𝜑 → 1 ∈ ( 0 ... 𝑀 ) )
129 18 128 eqeltrid ( 𝜑 → ( 0 + 1 ) ∈ ( 0 ... 𝑀 ) )
130 129 ad2antrl ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ( 0 + 1 ) ∈ ( 0 ... 𝑀 ) )
131 130 adantr ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 0 + 1 ) ∈ ( 0 ... 𝑀 ) )
132 118 120 131 iccpartxr ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ ( 0 + 1 ) ) ∈ ℝ* )
133 pnfnlt ( ( 𝑃 ‘ ( 0 + 1 ) ) ∈ ℝ* → ¬ +∞ < ( 𝑃 ‘ ( 0 + 1 ) ) )
134 132 133 syl ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ¬ +∞ < ( 𝑃 ‘ ( 0 + 1 ) ) )
135 116 134 pm2.21dd ( ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
136 135 ralrimiva ( ( ( 𝑃 ‘ 0 ) = +∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
137 136 ex ( ( 𝑃 ‘ 0 ) = +∞ → ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
138 1 adantr ( ( 𝜑𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ )
139 2 adantr ( ( 𝜑𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
140 simpr ( ( 𝜑𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑖 ∈ ( 1 ..^ 𝑀 ) )
141 138 139 140 iccpartipre ( ( 𝜑𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃𝑖 ) ∈ ℝ )
142 mnflt ( ( 𝑃𝑖 ) ∈ ℝ → -∞ < ( 𝑃𝑖 ) )
143 141 142 syl ( ( 𝜑𝑖 ∈ ( 1 ..^ 𝑀 ) ) → -∞ < ( 𝑃𝑖 ) )
144 143 ralrimiva ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) -∞ < ( 𝑃𝑖 ) )
145 144 ad2antrl ( ( ( 𝑃 ‘ 0 ) = -∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) -∞ < ( 𝑃𝑖 ) )
146 breq1 ( ( 𝑃 ‘ 0 ) = -∞ → ( ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ↔ -∞ < ( 𝑃𝑖 ) ) )
147 146 adantr ( ( ( 𝑃 ‘ 0 ) = -∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ( ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ↔ -∞ < ( 𝑃𝑖 ) ) )
148 147 ralbidv ( ( ( 𝑃 ‘ 0 ) = -∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) -∞ < ( 𝑃𝑖 ) ) )
149 145 148 mpbird ( ( ( 𝑃 ‘ 0 ) = -∞ ∧ ( 𝜑 ∧ ¬ 𝑀 = 1 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
150 149 ex ( ( 𝑃 ‘ 0 ) = -∞ → ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
151 104 137 150 3jaoi ( ( ( 𝑃 ‘ 0 ) ∈ ℝ ∨ ( 𝑃 ‘ 0 ) = +∞ ∨ ( 𝑃 ‘ 0 ) = -∞ ) → ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
152 15 151 sylbi ( ( 𝑃 ‘ 0 ) ∈ ℝ* → ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
153 14 152 mpcom ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )
154 153 expcom ( ¬ 𝑀 = 1 → ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) ) )
155 9 154 pm2.61i ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃𝑖 ) )