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 ) < ( 𝑃 ‘ 𝑖 ) )