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