Metamath Proof Explorer

Theorem iblspltprt

Description: If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iblspltprt.1 ⊢ Ⅎ 𝑡 𝜑
iblspltprt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iblspltprt.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
iblspltprt.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
iblspltprt.5 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
iblspltprt.6 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ) → 𝐴 ∈ ℂ )
iblspltprt.7 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
Assertion iblspltprt ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↦ 𝐴 ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 iblspltprt.1 ⊢ Ⅎ 𝑡 𝜑
2 iblspltprt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iblspltprt.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
4 iblspltprt.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
5 iblspltprt.5 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
6 iblspltprt.6 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ) → 𝐴 ∈ ℂ )
7 iblspltprt.7 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
8 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ℤ )
9 3 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑀 + 1 ) ≤ 𝑁 )
11 3 10 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ 𝑁 )
12 9 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
13 12 leidd ⊢ ( 𝜑 → 𝑁 ≤ 𝑁 )
14 2 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
15 elfz1 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ∧ 𝑁 ≤ 𝑁 ) ) )
16 14 9 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ∧ 𝑁 ≤ 𝑁 ) ) )
17 9 11 13 16 mpbir3and ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
18 fveq2 ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ ( 𝑀 + 1 ) ) )
19 18 oveq2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) )
20 19 mpteq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) )
21 20 eleq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
22 21 imbi2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
23 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝑘 ) )
24 23 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) )
25 24 mpteq1d ⊢ ( 𝑗 = 𝑘 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) )
26 25 eleq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
27 26 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
28 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
29 28 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
30 29 mpteq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) )
31 30 eleq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
32 31 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
33 fveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝑁 ) )
34 33 oveq2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
35 34 mpteq1d ⊢ ( 𝑗 = 𝑁 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↦ 𝐴 ) )
36 35 eleq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
37 36 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
38 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
39 2 38 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
40 2 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
41 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
42 40 41 readdcld ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
43 40 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
44 40 42 12 43 11 ltletrd ⊢ ( 𝜑 → 𝑀 < 𝑁 )
45 elfzo2 ⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
46 39 9 44 45 syl3anbrc ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
47 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑀 ) )
48 fvoveq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑀 + 1 ) ) )
49 47 48 oveq12d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) )
50 49 mpteq1d ⊢ ( 𝑖 = 𝑀 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) )
51 50 eleq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
52 51 imbi2d ⊢ ( 𝑖 = 𝑀 → ( ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
53 7 expcom ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
54 52 53 vtoclga ⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
55 46 54 mpcom ⊢ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
56 55 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
57 nfv ⊢ Ⅎ 𝑡 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 )
58 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 )
59 58 nfel1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1
60 1 59 nfim ⊢ Ⅎ 𝑡 ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 )
61 57 60 1 nf3an ⊢ Ⅎ 𝑡 ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 )
62 simp3 ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → 𝜑 )
63 simp1 ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
64 40 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
65 40 12 44 ltled ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
66 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
67 2 9 66 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
68 2 64 65 67 mpbir3and ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
69 68 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
70 eleq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
71 70 anbi2d ⊢ ( 𝑖 = 𝑀 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) ) )
72 47 eleq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝑃 ‘ 𝑀 ) ∈ ℝ ) )
73 71 72 imbi12d ⊢ ( 𝑖 = 𝑀 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ ) ) )
74 73 4 vtoclg ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ ) )
75 68 69 74 sylc ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
77 76 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
78 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝜑 )
79 elfzoelz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 ∈ ℤ )
80 79 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ℤ )
81 40 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
82 80 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ℝ )
83 42 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 + 1 ) ∈ ℝ )
84 43 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 < ( 𝑀 + 1 ) )
85 elfzole1 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑀 + 1 ) ≤ 𝑘 )
86 85 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 + 1 ) ≤ 𝑘 )
87 81 83 82 84 86 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 < 𝑘 )
88 81 82 87 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ≤ 𝑘 )
89 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
90 elfzolt2 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 < 𝑁 )
91 90 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 < 𝑁 )
92 82 89 91 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ≤ 𝑁 )
93 2 9 jca ⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
95 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
96 94 95 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
97 80 88 92 96 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
98 eleq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) )
99 98 anbi2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ) )
100 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑘 ) )
101 100 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) )
102 99 101 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) ) )
103 102 4 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
104 78 97 103 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
105 104 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ* )
106 80 peano2zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
107 106 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
108 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 1 ∈ ℝ )
109 81 82 108 87 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 + 1 ) < ( 𝑘 + 1 ) )
110 81 83 107 84 109 lttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 < ( 𝑘 + 1 ) )
111 81 107 110 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ≤ ( 𝑘 + 1 ) )
112 zltp1le ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
113 79 9 112 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
114 91 113 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
115 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) )
116 94 115 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) )
117 106 111 114 116 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
118 78 117 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
119 eleq1 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
120 119 anbi2d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) )
121 fveq2 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
122 121 eleq1d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
123 120 122 imbi12d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) ) )
124 123 4 vtoclg ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
125 117 118 124 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
126 125 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* )
127 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑘 ) )
128 2 79 127 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑘 ) )
129 88 128 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
130 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝜑 )
131 elfzelz ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ∈ ℤ )
132 131 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ℤ )
133 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑀 ≤ 𝑖 )
134 133 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 ≤ 𝑖 )
135 132 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ℝ )
136 130 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑁 ∈ ℝ )
137 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑘 ∈ ℝ )
138 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ≤ 𝑘 )
139 138 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ≤ 𝑘 )
140 91 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑘 < 𝑁 )
141 135 137 136 139 140 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 < 𝑁 )
142 135 136 141 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ≤ 𝑁 )
143 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
144 130 93 143 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
145 132 134 142 144 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
146 130 145 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
147 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝜑 )
148 elfzelz ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ∈ ℤ )
149 148 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ℤ )
150 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑀 ≤ 𝑖 )
151 150 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑀 ≤ 𝑖 )
152 149 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ℝ )
153 147 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑁 ∈ ℝ )
154 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑘 ∈ ℝ )
155 1red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 1 ∈ ℝ )
156 154 155 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℝ )
157 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ≤ ( 𝑘 − 1 ) )
158 157 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ≤ ( 𝑘 − 1 ) )
159 79 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 ∈ ℝ )
160 1red ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 1 ∈ ℝ )
161 159 160 resubcld ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑘 − 1 ) ∈ ℝ )
162 elfzoel2 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑁 ∈ ℤ )
163 162 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑁 ∈ ℝ )
164 159 ltm1d ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑘 − 1 ) < 𝑘 )
165 161 159 163 164 90 lttrd ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑘 − 1 ) < 𝑁 )
166 165 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑘 − 1 ) < 𝑁 )
167 152 156 153 158 166 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 < 𝑁 )
168 152 153 167 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
169 147 93 143 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
170 149 151 168 169 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
171 147 170 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
172 149 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
173 elfzel1 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑀 ∈ ℤ )
174 173 zred ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑀 ∈ ℝ )
175 148 zred ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ∈ ℝ )
176 1red ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 1 ∈ ℝ )
177 175 176 readdcld ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
178 175 ltp1d ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 < ( 𝑖 + 1 ) )
179 174 175 177 150 178 lelttrd ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑀 < ( 𝑖 + 1 ) )
180 174 177 179 ltled ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
181 180 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
182 147 3 8 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑁 ∈ ℤ )
183 zltp1le ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
184 149 182 183 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
185 167 184 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
186 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
187 147 93 186 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
188 172 181 185 187 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
189 147 188 jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
190 eleq1 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
191 190 anbi2d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) )
192 fveq2 ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
193 192 eleq1d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) )
194 191 193 imbi12d ⊢ ( 𝑘 = ( 𝑖 + 1 ) → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) ) )
195 194 103 vtoclg ⊢ ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) )
196 188 189 195 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
197 elfzuz ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
198 197 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
199 elfzo2 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁 ) )
200 198 182 167 199 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
201 147 200 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
202 171 196 201 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
203 129 146 202 monoord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑘 ) )
204 162 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
205 elfzo2 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁 ) )
206 129 204 91 205 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
207 eleq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) )
208 207 anbi2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
209 fvoveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
210 100 209 breq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
211 208 210 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
212 211 5 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
213 78 206 212 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
214 104 125 213 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
215 iccintsng ⊢ ( ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* ) ∧ ( ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∩ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) = { ( 𝑃 ‘ 𝑘 ) } )
216 77 105 126 203 214 215 syl32anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∩ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) = { ( 𝑃 ‘ 𝑘 ) } )
217 216 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( vol* ‘ ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∩ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) ) = ( vol* ‘ { ( 𝑃 ‘ 𝑘 ) } ) )
218 ovolsn ⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ℝ → ( vol* ‘ { ( 𝑃 ‘ 𝑘 ) } ) = 0 )
219 104 218 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( vol* ‘ { ( 𝑃 ‘ 𝑘 ) } ) = 0 )
220 217 219 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( vol* ‘ ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∩ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) ) = 0 )
221 62 63 220 syl2anc ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( vol* ‘ ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∩ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) ) = 0 )
222 76 125 104 203 214 eliccd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
223 76 125 222 3jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
224 62 63 223 syl2anc ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
225 iccsplit ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∪ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
226 224 225 syl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ∪ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
227 simpl3 ⊢ ( ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝜑 )
228 simpl1 ⊢ ( ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
229 simpr ⊢ ( ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
230 simp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝜑 )
231 eliccxr ⊢ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) → 𝑡 ∈ ℝ* )
232 231 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ℝ* )
233 75 rexrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
234 233 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
235 126 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* )
236 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
237 iccgelb ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
238 234 235 236 237 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
239 76 125 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
240 239 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
241 iccssre ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ⊆ ℝ )
242 241 sseld ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) → 𝑡 ∈ ℝ ) )
243 240 236 242 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
244 125 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
245 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁 ) ) )
246 2 9 245 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁 ) ) )
247 9 65 13 246 mpbir3and ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
248 247 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
249 eleq1 ⊢ ( 𝑖 = 𝑁 → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
250 249 anbi2d ⊢ ( 𝑖 = 𝑁 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) ) )
251 fveq2 ⊢ ( 𝑖 = 𝑁 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑁 ) )
252 251 eleq1d ⊢ ( 𝑖 = 𝑁 → ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝑃 ‘ 𝑁 ) ∈ ℝ ) )
253 250 252 imbi12d ⊢ ( 𝑖 = 𝑁 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ ) ) )
254 253 4 vtoclg ⊢ ( 𝑁 ∈ ℤ → ( ( 𝜑 ∧ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ ) )
255 9 248 254 sylc ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
256 255 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
257 elicc1 ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
258 234 235 257 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
259 236 258 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
260 259 simp3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
261 elfzop1le2 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑁 )
262 79 peano2zd ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ℤ )
263 eluz ⊢ ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
264 262 162 263 syl2anc ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
265 261 264 mpbird ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
266 265 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
267 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝜑 )
268 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → 𝑖 ∈ ℤ )
269 268 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℤ )
270 267 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 ∈ ℝ )
271 269 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
272 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℝ )
273 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 < 𝑘 )
274 159 adantr ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℝ )
275 1red ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 1 ∈ ℝ )
276 274 275 readdcld ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
277 268 zred ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → 𝑖 ∈ ℝ )
278 277 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
279 274 ltp1d ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 < ( 𝑘 + 1 ) )
280 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑖 )
281 280 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑖 )
282 274 276 278 279 281 ltletrd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 < 𝑖 )
283 282 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 < 𝑖 )
284 270 272 271 273 283 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 < 𝑖 )
285 270 271 284 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 ≤ 𝑖 )
286 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → 𝑖 ≤ 𝑁 )
287 286 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ≤ 𝑁 )
288 267 93 143 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
289 269 285 287 288 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
290 267 289 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
291 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝜑 )
292 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℤ )
293 292 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℤ )
294 291 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℝ )
295 293 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
296 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℝ )
297 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑘 )
298 159 adantr ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℝ )
299 1red ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
300 298 299 readdcld ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℝ )
301 292 zred ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℝ )
302 301 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
303 298 ltp1d ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < ( 𝑘 + 1 ) )
304 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝑘 + 1 ) ≤ 𝑖 )
305 304 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ≤ 𝑖 )
306 298 300 302 303 305 ltletrd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < 𝑖 )
307 306 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < 𝑖 )
308 294 296 295 297 307 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑖 )
309 294 295 308 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ 𝑖 )
310 301 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
311 12 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
312 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
313 311 312 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
314 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
315 314 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
316 311 ltm1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
317 310 313 311 315 316 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
318 310 311 317 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
319 318 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
320 291 93 143 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
321 293 309 319 320 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
322 291 321 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
323 293 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
324 323 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
325 302 299 readdcld ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
326 298 302 306 ltled ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 ≤ 𝑖 )
327 298 302 299 326 leadd1dd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ≤ ( 𝑖 + 1 ) )
328 298 300 325 303 327 ltletrd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < ( 𝑖 + 1 ) )
329 328 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < ( 𝑖 + 1 ) )
330 294 296 324 297 329 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑖 + 1 ) )
331 294 324 330 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
332 292 9 183 syl2anr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
333 317 332 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
334 333 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
335 291 93 186 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
336 323 331 334 335 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
337 291 336 jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
338 336 337 195 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
339 291 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℤ )
340 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑖 ) )
341 339 293 340 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑖 ) )
342 309 341 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
343 291 3 8 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
344 317 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
345 342 343 344 199 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
346 291 345 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
347 322 338 346 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
348 266 290 347 monoord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
349 348 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
350 243 244 256 260 349 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) )
351 256 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ* )
352 elicc1 ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑁 ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) ) ) )
353 234 351 352 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) ) ) )
354 232 238 350 353 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
355 230 354 6 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝐴 ∈ ℂ )
356 227 228 229 355 syl3anc ⊢ ( ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝐴 ∈ ℂ )
357 simp2 ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
358 62 357 mpd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 )
359 62 63 jca ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
360 78 206 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) )
361 100 209 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
362 361 mpteq1d ⊢ ( 𝑖 = 𝑘 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) )
363 362 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
364 208 363 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
365 364 7 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
366 359 360 365 3syl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
367 61 221 226 356 358 366 iblsplitf ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ∧ 𝜑 ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
368 367 3exp ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) → ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
369 22 27 32 37 56 368 fzind2 ⊢ ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
370 17 369 mpcom ⊢ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↦ 𝐴 ) ∈ 𝐿1 )