Metamath Proof Explorer

Theorem iccpartgt

Description: If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartgt ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 elnn0uz ⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
5 3 4 sylib ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
6 fzpred ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) )
7 5 6 syl ⊢ ( 𝜑 → ( 0 ... 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) )
8 0p1e1 ⊢ ( 0 + 1 ) = 1
9 8 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
10 9 a1i ⊢ ( 𝜑 → ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 ) )
11 10 uneq2d ⊢ ( 𝜑 → ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) = ( { 0 } ∪ ( 1 ... 𝑀 ) ) )
12 7 11 eqtrd ⊢ ( 𝜑 → ( 0 ... 𝑀 ) = ( { 0 } ∪ ( 1 ... 𝑀 ) ) )
13 12 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) ↔ 𝑖 ∈ ( { 0 } ∪ ( 1 ... 𝑀 ) ) ) )
14 elun ⊢ ( 𝑖 ∈ ( { 0 } ∪ ( 1 ... 𝑀 ) ) ↔ ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) )
15 velsn ⊢ ( 𝑖 ∈ { 0 } ↔ 𝑖 = 0 )
16 15 orbi1i ⊢ ( ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) )
17 14 16 bitri ⊢ ( 𝑖 ∈ ( { 0 } ∪ ( 1 ... 𝑀 ) ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) )
18 fzisfzounsn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑀 ) = ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) )
19 5 18 syl ⊢ ( 𝜑 → ( 0 ... 𝑀 ) = ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) )
20 19 eleq2d ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑀 ) ↔ 𝑗 ∈ ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) ) )
21 elun ⊢ ( 𝑗 ∈ ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 ∈ { 𝑀 } ) )
22 velsn ⊢ ( 𝑗 ∈ { 𝑀 } ↔ 𝑗 = 𝑀 )
23 22 orbi2i ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 ∈ { 𝑀 } ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) )
24 21 23 bitri ⊢ ( 𝑗 ∈ ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) )
25 20 24 bitrdi ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑀 ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) ) )
26 simpl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 0 < 𝑗 ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
27 simpr ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 0 < 𝑗 ) → 0 < 𝑗 )
28 27 gt0ne0d ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 0 < 𝑗 ) → 𝑗 ≠ 0 )
29 fzo1fzo0n0 ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑗 ≠ 0 ) )
30 26 28 29 sylanbrc ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 0 < 𝑗 ) → 𝑗 ∈ ( 1 ..^ 𝑀 ) )
31 1 2 iccpartigtl ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) )
32 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑗 ) )
33 32 breq2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) )
34 33 rspcv ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑀 ) → ( ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) )
35 30 31 34 syl2imc ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 0 < 𝑗 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) )
36 35 expd ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 0 < 𝑗 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) ) )
37 36 impcom ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝜑 ) → ( 0 < 𝑗 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) )
38 breq1 ⊢ ( 𝑖 = 0 → ( 𝑖 < 𝑗 ↔ 0 < 𝑗 ) )
39 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
40 39 breq1d ⊢ ( 𝑖 = 0 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) )
41 38 40 imbi12d ⊢ ( 𝑖 = 0 → ( ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ↔ ( 0 < 𝑗 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑗 ) ) ) )
42 37 41 syl5ibr ⊢ ( 𝑖 = 0 → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝜑 ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) )
43 42 expd ⊢ ( 𝑖 = 0 → ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
44 43 com12 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 = 0 → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
45 1 2 iccpartlt ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
46 fveq2 ⊢ ( 𝑗 = 𝑀 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝑀 ) )
47 39 46 breqan12rd ⊢ ( ( 𝑗 = 𝑀 ∧ 𝑖 = 0 ) → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) ) )
48 45 47 syl5ibr ⊢ ( ( 𝑗 = 𝑀 ∧ 𝑖 = 0 ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) )
49 48 a1dd ⊢ ( ( 𝑗 = 𝑀 ∧ 𝑖 = 0 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) )
50 49 ex ⊢ ( 𝑗 = 𝑀 → ( 𝑖 = 0 → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
51 44 50 jaoi ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) → ( 𝑖 = 0 → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
52 51 com12 ⊢ ( 𝑖 = 0 → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
53 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℤ )
54 53 ad3antlr ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → 𝑖 ∈ ℤ )
55 53 peano2zd ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝑖 + 1 ) ∈ ℤ )
56 55 ad2antlr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 + 1 ) ∈ ℤ )
57 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℤ )
58 57 ad2antrr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ℤ )
59 simpr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 )
60 57 53 anim12ci ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) )
61 60 adantr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) )
62 zltp1le ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑖 < 𝑗 ↔ ( 𝑖 + 1 ) ≤ 𝑗 ) )
63 61 62 syl ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 < 𝑗 ↔ ( 𝑖 + 1 ) ≤ 𝑗 ) )
64 59 63 mpbid ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 + 1 ) ≤ 𝑗 )
65 56 58 64 3jca ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ( 𝑖 + 1 ) ≤ 𝑗 ) )
66 65 adantr ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ( 𝑖 + 1 ) ≤ 𝑗 ) )
67 eluz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ( 𝑖 + 1 ) ≤ 𝑗 ) )
68 66 67 sylibr ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
69 1 ad2antlr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑀 ∈ ℕ )
70 2 ad2antlr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
71 1zzd ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 1 ∈ ℤ )
72 elfzelz ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 𝑘 ∈ ℤ )
73 72 adantl ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑘 ∈ ℤ )
74 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 1 ≤ 𝑖 )
75 elfzle1 ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 𝑖 ≤ 𝑘 )
76 1red ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 1 ∈ ℝ )
77 elfzel1 ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 𝑖 ∈ ℤ )
78 77 zred ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 𝑖 ∈ ℝ )
79 72 zred ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 𝑘 ∈ ℝ )
80 letr ⊢ ( ( 1 ∈ ℝ ∧ 𝑖 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑘 ) → 1 ≤ 𝑘 ) )
81 76 78 79 80 syl3anc ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → ( ( 1 ≤ 𝑖 ∧ 𝑖 ≤ 𝑘 ) → 1 ≤ 𝑘 ) )
82 75 81 mpan2d ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → ( 1 ≤ 𝑖 → 1 ≤ 𝑘 ) )
83 74 82 syl5com ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 1 ≤ 𝑘 ) )
84 83 ad3antlr ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 1 ≤ 𝑘 ) )
85 84 imp ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 1 ≤ 𝑘 )
86 eluz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
87 71 73 85 86 syl3anbrc ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
88 elfzel2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ℤ )
89 88 ad2antlr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → 𝑀 ∈ ℤ )
90 89 ad2antrr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑀 ∈ ℤ )
91 79 adantl ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑘 ∈ ℝ )
92 57 zred ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℝ )
93 92 ad4antr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑗 ∈ ℝ )
94 69 nnred ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑀 ∈ ℝ )
95 elfzle2 ⊢ ( 𝑘 ∈ ( 𝑖 ... 𝑗 ) → 𝑘 ≤ 𝑗 )
96 95 adantl ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑘 ≤ 𝑗 )
97 elfzolt2 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 < 𝑀 )
98 97 ad4antr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑗 < 𝑀 )
99 91 93 94 96 98 lelttrd ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑘 < 𝑀 )
100 elfzo2 ⊢ ( 𝑘 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑘 < 𝑀 ) )
101 87 90 99 100 syl3anbrc ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) )
102 69 70 101 iccpartipre ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... 𝑗 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
103 1 ad2antlr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℕ )
104 2 ad2antlr ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑗 − 1 ) ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
105 57 ad3antrrr ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → 𝑗 ∈ ℤ )
106 fzoval ⊢ ( 𝑗 ∈ ℤ → ( 𝑖 ..^ 𝑗 ) = ( 𝑖 ... ( 𝑗 − 1 ) ) )
107 105 106 syl ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → ( 𝑖 ..^ 𝑗 ) = ( 𝑖 ... ( 𝑗 − 1 ) ) )
108 elfzo0le ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ≤ 𝑀 )
109 0le1 ⊢ 0 ≤ 1
110 0red ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
111 1red ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
112 53 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℝ )
113 letr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑖 ∈ ℝ ) → ( ( 0 ≤ 1 ∧ 1 ≤ 𝑖 ) → 0 ≤ 𝑖 ) )
114 110 111 112 113 syl3anc ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( ( 0 ≤ 1 ∧ 1 ≤ 𝑖 ) → 0 ≤ 𝑖 ) )
115 109 114 mpani ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 1 ≤ 𝑖 → 0 ≤ 𝑖 ) )
116 74 115 mpd ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 ≤ 𝑖 )
117 108 116 anim12ci ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 0 ≤ 𝑖 ∧ 𝑗 ≤ 𝑀 ) )
118 117 adantr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 0 ≤ 𝑖 ∧ 𝑗 ≤ 𝑀 ) )
119 0zd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 0 ∈ ℤ )
120 elfzoel2 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
121 119 120 jca ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
122 121 ad2antrr ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
123 ssfzo12bi ⊢ ( ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ∧ ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑖 < 𝑗 ) → ( ( 𝑖 ..^ 𝑗 ) ⊆ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑖 ∧ 𝑗 ≤ 𝑀 ) ) )
124 61 122 59 123 syl3anc ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( ( 𝑖 ..^ 𝑗 ) ⊆ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑖 ∧ 𝑗 ≤ 𝑀 ) ) )
125 118 124 mpbird ⊢ ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) → ( 𝑖 ..^ 𝑗 ) ⊆ ( 0 ..^ 𝑀 ) )
126 125 adantr ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → ( 𝑖 ..^ 𝑗 ) ⊆ ( 0 ..^ 𝑀 ) )
127 107 126 eqsstrrd ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → ( 𝑖 ... ( 𝑗 − 1 ) ) ⊆ ( 0 ..^ 𝑀 ) )
128 127 sselda ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑗 − 1 ) ) ) → 𝑘 ∈ ( 0 ..^ 𝑀 ) )
129 iccpartimp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
130 103 104 128 129 syl3anc ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑗 − 1 ) ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
131 130 simprd ⊢ ( ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝑖 ... ( 𝑗 − 1 ) ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
132 54 68 102 131 smonoord ⊢ ( ( ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑖 < 𝑗 ) ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) )
133 132 exp31 ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑖 < 𝑗 → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) )
134 133 com23 ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) )
135 134 ex ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
136 elfzuz ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
137 136 adantr ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑖 < 𝑀 ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
138 88 adantr ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑖 < 𝑀 ) → 𝑀 ∈ ℤ )
139 simpr ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑖 < 𝑀 ) → 𝑖 < 𝑀 )
140 elfzo2 ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ↔ ( 𝑖 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀 ) )
141 137 138 139 140 syl3anbrc ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑖 < 𝑀 ) → 𝑖 ∈ ( 1 ..^ 𝑀 ) )
142 1 2 iccpartiltu ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) )
143 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
144 143 breq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
145 144 rspcv ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
146 141 142 145 syl2imc ⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑖 < 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
147 146 expd ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝑖 < 𝑀 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) ) )
148 147 impcom ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝜑 ) → ( 𝑖 < 𝑀 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
149 148 imp ⊢ ( ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝜑 ) ∧ 𝑖 < 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
150 149 a1i ⊢ ( 𝑗 = 𝑀 → ( ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝜑 ) ∧ 𝑖 < 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
151 breq2 ⊢ ( 𝑗 = 𝑀 → ( 𝑖 < 𝑗 ↔ 𝑖 < 𝑀 ) )
152 151 anbi2d ⊢ ( 𝑗 = 𝑀 → ( ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝜑 ) ∧ 𝑖 < 𝑗 ) ↔ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝜑 ) ∧ 𝑖 < 𝑀 ) ) )
153 46 breq2d ⊢ ( 𝑗 = 𝑀 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
154 150 152 153 3imtr4d ⊢ ( 𝑗 = 𝑀 → ( ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝜑 ) ∧ 𝑖 < 𝑗 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) )
155 154 exp4c ⊢ ( 𝑗 = 𝑀 → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
156 135 155 jaoi ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
157 156 com12 ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
158 52 157 jaoi ⊢ ( ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) → ( 𝜑 → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
159 158 com13 ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑗 = 𝑀 ) → ( ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
160 25 159 sylbid ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
161 160 com3r ⊢ ( ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
162 17 161 sylbi ⊢ ( 𝑖 ∈ ( { 0 } ∪ ( 1 ... 𝑀 ) ) → ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
163 162 com12 ⊢ ( 𝜑 → ( 𝑖 ∈ ( { 0 } ∪ ( 1 ... 𝑀 ) ) → ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
164 13 163 sylbid ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) ) ) )
165 164 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ) → ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) )
166 165 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ∀ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑖 < 𝑗 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑗 ) ) )