Metamath Proof Explorer

Theorem iccpartiltu

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

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

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 ral0 ⊢ ∀ 𝑖 ∈ ∅ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 1 )
4 oveq2 ⊢ ( 𝑀 = 1 → ( 1 ..^ 𝑀 ) = ( 1 ..^ 1 ) )
5 fzo0 ⊢ ( 1 ..^ 1 ) = ∅
6 4 5 eqtrdi ⊢ ( 𝑀 = 1 → ( 1 ..^ 𝑀 ) = ∅ )
7 fveq2 ⊢ ( 𝑀 = 1 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 1 ) )
8 7 breq2d ⊢ ( 𝑀 = 1 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 1 ) ) )
9 6 8 raleqbidv ⊢ ( 𝑀 = 1 → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ↔ ∀ 𝑖 ∈ ∅ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 1 ) ) )
10 3 9 mpbiri ⊢ ( 𝑀 = 1 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
11 10 2a1d ⊢ ( 𝑀 = 1 → ( 𝜑 → ( 𝑀 ∈ ℕ → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
12 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
13 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
14 13 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
15 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
16 nn0fz0 ⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( 0 ... 𝑀 ) )
17 15 16 sylib ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( 0 ... 𝑀 ) )
18 17 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
19 12 14 18 iccpartxr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
20 elxr ⊢ ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ↔ ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∨ ( 𝑃 ‘ 𝑀 ) = +∞ ∨ ( 𝑃 ‘ 𝑀 ) = -∞ ) )
21 elfzoelz ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑖 ∈ ℤ )
22 21 ad2antll ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑖 ∈ ℤ )
23 elfzo2 ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) )
24 eluzelz ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → 𝑖 ∈ ℤ )
25 24 peano2zd ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑖 + 1 ) ∈ ℤ )
26 25 3ad2ant1 ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → ( 𝑖 + 1 ) ∈ ℤ )
27 simp2 ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → 𝑀 ∈ ℤ )
28 zltp1le ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑖 < 𝑀 ↔ ( 𝑖 + 1 ) ≤ 𝑀 ) )
29 24 28 sylan ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑖 < 𝑀 ↔ ( 𝑖 + 1 ) ≤ 𝑀 ) )
30 29 biimp3a ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → ( 𝑖 + 1 ) ≤ 𝑀 )
31 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ≤ 𝑀 ) )
32 26 27 30 31 syl3anbrc ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
33 23 32 sylbi ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
34 33 ad2antll ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
35 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑀 ) )
36 35 eqcomd ⊢ ( 𝑘 = 𝑀 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑘 ) )
37 36 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ↔ ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
38 37 biimpcd ⊢ ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ → ( 𝑘 = 𝑀 → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
39 38 adantr ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑘 = 𝑀 → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
40 39 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → ( 𝑘 = 𝑀 → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
41 40 com12 ⊢ ( 𝑘 = 𝑀 → ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
42 12 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ )
43 42 adantl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑀 ∈ ℕ )
44 43 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
45 44 adantl ⊢ ( ( ¬ 𝑘 = 𝑀 ∧ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) ) → 𝑀 ∈ ℕ )
46 14 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
47 46 adantl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
48 47 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
49 48 adantl ⊢ ( ( ¬ 𝑘 = 𝑀 ∧ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
50 elfz2 ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) ↔ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) )
51 eluz2 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ) )
52 1red ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 1 ∈ ℝ )
53 zre ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℝ )
54 53 adantr ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 𝑖 ∈ ℝ )
55 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
56 55 adantl ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
57 letr ⊢ ( ( 1 ∈ ℝ ∧ 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑘 ) → 1 ≤ 𝑘 ) )
58 52 54 56 57 syl3anc ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑘 ) → 1 ≤ 𝑘 ) )
59 58 expcomd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑖 ≤ 𝑘 → ( 1 ≤ 𝑖 → 1 ≤ 𝑘 ) ) )
60 59 adantrd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) → ( 1 ≤ 𝑖 → 1 ≤ 𝑘 ) ) )
61 60 3adant2 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) → ( 1 ≤ 𝑖 → 1 ≤ 𝑘 ) ) )
62 61 imp ⊢ ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → ( 1 ≤ 𝑖 → 1 ≤ 𝑘 ) )
63 62 com12 ⊢ ( 1 ≤ 𝑖 → ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → 1 ≤ 𝑘 ) )
64 63 3ad2ant3 ⊢ ( ( 1 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ) → ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → 1 ≤ 𝑘 ) )
65 51 64 sylbi ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → 1 ≤ 𝑘 ) )
66 65 3ad2ant1 ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) → ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → 1 ≤ 𝑘 ) )
67 23 66 sylbi ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → 1 ≤ 𝑘 ) )
68 50 67 syl5bi ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → 1 ≤ 𝑘 ) )
69 68 imp ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → 1 ≤ 𝑘 )
70 69 3adant3 ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → 1 ≤ 𝑘 )
71 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
72 71 55 anim12ci ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
73 72 3adant1 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
74 ltlen ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑘 < 𝑀 ↔ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≠ 𝑘 ) ) )
75 73 74 syl ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 < 𝑀 ↔ ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≠ 𝑘 ) ) )
76 nesym ⊢ ( 𝑀 ≠ 𝑘 ↔ ¬ 𝑘 = 𝑀 )
77 76 anbi2i ⊢ ( ( 𝑘 ≤ 𝑀 ∧ 𝑀 ≠ 𝑘 ) ↔ ( 𝑘 ≤ 𝑀 ∧ ¬ 𝑘 = 𝑀 ) )
78 75 77 bitr2di ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 ≤ 𝑀 ∧ ¬ 𝑘 = 𝑀 ) ↔ 𝑘 < 𝑀 ) )
79 78 biimpd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 ≤ 𝑀 ∧ ¬ 𝑘 = 𝑀 ) → 𝑘 < 𝑀 ) )
80 79 expd ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ≤ 𝑀 → ( ¬ 𝑘 = 𝑀 → 𝑘 < 𝑀 ) ) )
81 80 adantld ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) → ( ¬ 𝑘 = 𝑀 → 𝑘 < 𝑀 ) ) )
82 81 imp ⊢ ( ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑖 ≤ 𝑘 ∧ 𝑘 ≤ 𝑀 ) ) → ( ¬ 𝑘 = 𝑀 → 𝑘 < 𝑀 ) )
83 50 82 sylbi ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → ( ¬ 𝑘 = 𝑀 → 𝑘 < 𝑀 ) )
84 83 imp ⊢ ( ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → 𝑘 < 𝑀 )
85 84 3adant1 ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → 𝑘 < 𝑀 )
86 70 85 jca ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → ( 1 ≤ 𝑘 ∧ 𝑘 < 𝑀 ) )
87 elfzelz ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → 𝑘 ∈ ℤ )
88 1zzd ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → 1 ∈ ℤ )
89 elfzel2 ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → 𝑀 ∈ ℤ )
90 87 88 89 3jca ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
91 90 3ad2ant2 ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
92 elfzo ⊢ ( ( 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑘 ∈ ( 1 ..^ 𝑀 ) ↔ ( 1 ≤ 𝑘 ∧ 𝑘 < 𝑀 ) ) )
93 91 92 syl ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → ( 𝑘 ∈ ( 1 ..^ 𝑀 ) ↔ ( 1 ≤ 𝑘 ∧ 𝑘 < 𝑀 ) ) )
94 86 93 mpbird ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ∧ ¬ 𝑘 = 𝑀 ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) )
95 94 3exp ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → ( ¬ 𝑘 = 𝑀 → 𝑘 ∈ ( 1 ..^ 𝑀 ) ) ) )
96 95 ad2antll ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑘 ∈ ( 𝑖 ... 𝑀 ) → ( ¬ 𝑘 = 𝑀 → 𝑘 ∈ ( 1 ..^ 𝑀 ) ) ) )
97 96 imp ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → ( ¬ 𝑘 = 𝑀 → 𝑘 ∈ ( 1 ..^ 𝑀 ) ) )
98 97 impcom ⊢ ( ( ¬ 𝑘 = 𝑀 ∧ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) )
99 45 49 98 iccpartipre ⊢ ( ( ¬ 𝑘 = 𝑀 ∧ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
100 99 ex ⊢ ( ¬ 𝑘 = 𝑀 → ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
101 41 100 pm2.61i ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
102 43 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℕ )
103 47 adantr ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
104 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
105 fzoss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ..^ 𝑀 ) ⊆ ( 0 ..^ 𝑀 ) )
106 104 105 mp1i ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 1 ..^ 𝑀 ) ⊆ ( 0 ..^ 𝑀 ) )
107 elfzoel2 ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
108 fzoval ⊢ ( 𝑀 ∈ ℤ → ( 𝑖 ..^ 𝑀 ) = ( 𝑖 ... ( 𝑀 − 1 ) ) )
109 107 108 syl ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑖 ..^ 𝑀 ) = ( 𝑖 ... ( 𝑀 − 1 ) ) )
110 109 eqcomd ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑖 ... ( 𝑀 − 1 ) ) = ( 𝑖 ..^ 𝑀 ) )
111 110 eleq2d ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ↔ 𝑘 ∈ ( 𝑖 ..^ 𝑀 ) ) )
112 elfzouz ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
113 fzoss1 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑖 ..^ 𝑀 ) ⊆ ( 1 ..^ 𝑀 ) )
114 112 113 syl ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑖 ..^ 𝑀 ) ⊆ ( 1 ..^ 𝑀 ) )
115 114 sseld ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ..^ 𝑀 ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) ) )
116 111 115 sylbid ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) ) )
117 116 imp ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) )
118 106 117 sseldd ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
119 118 ex ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
120 119 ad2antll ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) ) )
121 120 imp ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
122 iccpartimp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
123 102 103 121 122 syl3anc ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
124 123 simprd ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
125 22 34 101 124 smonoord ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
126 125 ex ⊢ ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ → ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
127 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑖 ∈ ( 1 ..^ 𝑀 ) )
128 42 46 127 iccpartipre ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
129 ltpnf ⊢ ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ → ( 𝑃 ‘ 𝑖 ) < +∞ )
130 128 129 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < +∞ )
131 breq2 ⊢ ( ( 𝑃 ‘ 𝑀 ) = +∞ → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) < +∞ ) )
132 130 131 syl5ibr ⊢ ( ( 𝑃 ‘ 𝑀 ) = +∞ → ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
133 42 adantl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑀 ∈ ℕ )
134 46 adantl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
135 elfzofz ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
136 135 ad2antll ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
137 elfzubelfz ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ( 1 ... 𝑀 ) )
138 136 137 syl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → 𝑀 ∈ ( 1 ... 𝑀 ) )
139 133 134 138 iccpartgtprec ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ ( 𝑀 − 1 ) ) < ( 𝑃 ‘ 𝑀 ) )
140 breq2 ⊢ ( -∞ = ( 𝑃 ‘ 𝑀 ) → ( ( 𝑃 ‘ ( 𝑀 − 1 ) ) < -∞ ↔ ( 𝑃 ‘ ( 𝑀 − 1 ) ) < ( 𝑃 ‘ 𝑀 ) ) )
141 140 eqcoms ⊢ ( ( 𝑃 ‘ 𝑀 ) = -∞ → ( ( 𝑃 ‘ ( 𝑀 − 1 ) ) < -∞ ↔ ( 𝑃 ‘ ( 𝑀 − 1 ) ) < ( 𝑃 ‘ 𝑀 ) ) )
142 141 adantr ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( ( 𝑃 ‘ ( 𝑀 − 1 ) ) < -∞ ↔ ( 𝑃 ‘ ( 𝑀 − 1 ) ) < ( 𝑃 ‘ 𝑀 ) ) )
143 139 142 mpbird ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ ( 𝑀 − 1 ) ) < -∞ )
144 15 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ0 )
145 144 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ0 )
146 nnne0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
147 146 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ≠ 0 )
148 df-ne ⊢ ( 𝑀 ≠ 1 ↔ ¬ 𝑀 = 1 )
149 148 biimpri ⊢ ( ¬ 𝑀 = 1 → 𝑀 ≠ 1 )
150 149 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → 𝑀 ≠ 1 )
151 150 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ≠ 1 )
152 144 147 151 3jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≠ 0 ∧ 𝑀 ≠ 1 ) )
153 152 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≠ 0 ∧ 𝑀 ≠ 1 ) )
154 nn0n0n1ge2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≠ 0 ∧ 𝑀 ≠ 1 ) → 2 ≤ 𝑀 )
155 153 154 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → 2 ≤ 𝑀 )
156 145 155 jca ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑀 ∈ ℕ0 ∧ 2 ≤ 𝑀 ) )
157 156 adantl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑀 ∈ ℕ0 ∧ 2 ≤ 𝑀 ) )
158 ige2m1fz ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 2 ≤ 𝑀 ) → ( 𝑀 − 1 ) ∈ ( 0 ... 𝑀 ) )
159 157 158 syl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑀 − 1 ) ∈ ( 0 ... 𝑀 ) )
160 133 134 159 iccpartxr ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ ( 𝑀 − 1 ) ) ∈ ℝ* )
161 nltmnf ⊢ ( ( 𝑃 ‘ ( 𝑀 − 1 ) ) ∈ ℝ* → ¬ ( 𝑃 ‘ ( 𝑀 − 1 ) ) < -∞ )
162 160 161 syl ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ¬ ( 𝑃 ‘ ( 𝑀 − 1 ) ) < -∞ )
163 143 162 pm2.21dd ⊢ ( ( ( 𝑃 ‘ 𝑀 ) = -∞ ∧ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
164 163 ex ⊢ ( ( 𝑃 ‘ 𝑀 ) = -∞ → ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
165 126 132 164 3jaoi ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∨ ( 𝑃 ‘ 𝑀 ) = +∞ ∨ ( 𝑃 ‘ 𝑀 ) = -∞ ) → ( ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
166 165 impl ⊢ ( ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∨ ( 𝑃 ‘ 𝑀 ) = +∞ ∨ ( 𝑃 ‘ 𝑀 ) = -∞ ) ∧ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
167 166 ralrimiva ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∨ ( 𝑃 ‘ 𝑀 ) = +∞ ∨ ( 𝑃 ‘ 𝑀 ) = -∞ ) ∧ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
168 167 ex ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∨ ( 𝑃 ‘ 𝑀 ) = +∞ ∨ ( 𝑃 ‘ 𝑀 ) = -∞ ) → ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
169 20 168 sylbi ⊢ ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* → ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
170 19 169 mpcom ⊢ ( ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) ∧ 𝑀 ∈ ℕ ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
171 170 ex ⊢ ( ( 𝜑 ∧ ¬ 𝑀 = 1 ) → ( 𝑀 ∈ ℕ → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
172 171 expcom ⊢ ( ¬ 𝑀 = 1 → ( 𝜑 → ( 𝑀 ∈ ℕ → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
173 11 172 pm2.61i ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
174 1 173 mpd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )