Metamath Proof Explorer

Theorem itgspltprt

Description: The S. integral splits on a given partition P . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgspltprt.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
itgspltprt.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
itgspltprt.3 ⊢ ( 𝜑 → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
itgspltprt.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
itgspltprt.5 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ) → 𝐴 ∈ ℂ )
itgspltprt.6 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
Assertion itgspltprt ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )

Proof

Step Hyp Ref Expression
1 itgspltprt.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 itgspltprt.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
3 itgspltprt.3 ⊢ ( 𝜑 → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
4 itgspltprt.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
5 itgspltprt.5 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ) → 𝐴 ∈ ℂ )
6 itgspltprt.6 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
7 1 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
8 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ℤ )
9 2 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑀 + 1 ) ≤ 𝑁 )
11 2 10 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ 𝑁 )
12 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ℝ )
13 2 12 syl ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
14 13 leidd ⊢ ( 𝜑 → 𝑁 ≤ 𝑁 )
15 7 9 9 11 14 elfzd ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
16 fveq2 ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ ( 𝑀 + 1 ) ) )
17 16 oveq2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) )
18 17 itgeq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 )
19 oveq2 ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑀 ..^ 𝑗 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
20 19 sumeq1d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
21 18 20 eqeq12d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ↔ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
22 21 imbi2d ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ↔ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ) )
23 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝑘 ) )
24 23 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) )
25 24 itgeq1d ⊢ ( 𝑗 = 𝑘 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 )
26 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑀 ..^ 𝑗 ) = ( 𝑀 ..^ 𝑘 ) )
27 26 sumeq1d ⊢ ( 𝑗 = 𝑘 → Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
28 25 27 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ↔ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
29 28 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ↔ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ) )
30 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
31 30 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
32 31 itgeq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 )
33 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 ..^ 𝑗 ) = ( 𝑀 ..^ ( 𝑘 + 1 ) ) )
34 33 sumeq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
35 32 34 eqeq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ↔ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
36 35 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ↔ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ) )
37 fveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝑃 ‘ 𝑗 ) = ( 𝑃 ‘ 𝑁 ) )
38 37 oveq2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
39 38 itgeq1d ⊢ ( 𝑗 = 𝑁 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) 𝐴 d 𝑡 )
40 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝑀 ..^ 𝑗 ) = ( 𝑀 ..^ 𝑁 ) )
41 40 sumeq1d ⊢ ( 𝑗 = 𝑁 → Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
42 39 41 eqeq12d ⊢ ( 𝑗 = 𝑁 → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ↔ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
43 42 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑗 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑗 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ↔ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ) )
44 1 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝜑 ) → 𝑀 ∈ ℤ )
45 fzval3 ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
46 44 45 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝜑 ) → ( 𝑀 ... 𝑀 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
47 46 eqcomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝜑 ) → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = ( 𝑀 ... 𝑀 ) )
48 47 sumeq1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝜑 ) → Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
49 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
50 1 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
51 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
52 50 51 readdcld ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
53 50 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
54 50 52 13 53 11 ltletrd ⊢ ( 𝜑 → 𝑀 < 𝑁 )
55 50 13 54 ltled ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
56 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
57 1 9 56 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
58 55 57 mpbird ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
59 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
60 58 59 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
62 49 61 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
63 1 9 9 55 14 elfzd ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
64 3 63 ffvelrnd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
66 50 lep1d ⊢ ( 𝜑 → 𝑀 ≤ ( 𝑀 + 1 ) )
67 1 9 7 66 11 elfzd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
68 3 67 ffvelrnd ⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑀 + 1 ) ) ∈ ℝ )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑀 + 1 ) ) ∈ ℝ )
70 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) )
71 eliccre ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑀 + 1 ) ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
72 62 69 70 71 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
73 3 60 ffvelrnd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
74 73 rexrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
76 69 rexrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑀 + 1 ) ) ∈ ℝ* )
77 iccgelb ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑀 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
78 75 76 70 77 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
79 iccleub ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑀 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑀 + 1 ) ) )
80 75 76 70 79 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑀 + 1 ) ) )
81 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
82 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑖 ∈ ℤ )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℤ )
84 50 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑀 ∈ ℝ )
85 83 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
86 52 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑀 + 1 ) ∈ ℝ )
87 53 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑀 < ( 𝑀 + 1 ) )
88 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑀 + 1 ) ≤ 𝑖 )
89 88 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑀 + 1 ) ≤ 𝑖 )
90 84 86 85 87 89 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑀 < 𝑖 )
91 84 85 90 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑀 ≤ 𝑖 )
92 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑖 ≤ 𝑁 )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑖 ≤ 𝑁 )
94 1 9 jca ⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
96 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
97 95 96 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
98 83 91 93 97 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
99 81 98 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
100 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
101 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℤ )
102 101 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℤ )
103 50 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℝ )
104 102 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
105 52 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑀 + 1 ) ∈ ℝ )
106 53 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑀 + 1 ) )
107 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝑀 + 1 ) ≤ 𝑖 )
108 107 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑀 + 1 ) ≤ 𝑖 )
109 103 105 104 106 108 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑖 )
110 103 104 109 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ 𝑖 )
111 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
112 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
113 111 112 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
114 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
115 114 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
116 111 ltm1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
117 104 113 111 115 116 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
118 104 111 117 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
119 94 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
120 119 96 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
121 102 110 118 120 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
122 100 121 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
123 102 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
124 104 112 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
125 103 104 112 109 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑀 + 1 ) < ( 𝑖 + 1 ) )
126 103 105 124 106 125 lttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑖 + 1 ) )
127 103 124 126 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
128 zltp1le ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
129 101 9 128 syl2anr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
130 117 129 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
131 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
132 119 131 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
133 123 127 130 132 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
134 100 133 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
135 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑖 ) )
136 1 101 135 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑖 ) )
137 110 136 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
138 9 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
139 elfzo2 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁 ) )
140 137 138 117 139 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
141 140 4 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
142 122 134 141 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
143 2 99 142 monoord ⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑀 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
144 143 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑀 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
145 72 69 65 80 144 letrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) )
146 62 65 72 78 145 eliccd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
147 146 5 syldan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ) → 𝐴 ∈ ℂ )
148 id ⊢ ( 𝜑 → 𝜑 )
149 fzolb ⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
150 1 9 54 149 syl3anbrc ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
151 148 150 jca ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) )
152 eleq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) )
153 152 anbi2d ⊢ ( 𝑖 = 𝑀 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
154 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑀 ) )
155 fvoveq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑀 + 1 ) ) )
156 154 155 oveq12d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) )
157 156 mpteq1d ⊢ ( 𝑖 = 𝑀 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) )
158 157 eleq1d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
159 153 158 imbi12d ⊢ ( 𝑖 = 𝑀 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
160 159 6 vtoclg ⊢ ( 𝑀 ∈ ℤ → ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
161 1 151 160 sylc ⊢ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
162 147 161 itgcl ⊢ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 ∈ ℂ )
163 156 itgeq1d ⊢ ( 𝑖 = 𝑀 → ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 )
164 163 fsum1 ⊢ ( ( 𝑀 ∈ ℤ ∧ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 ∈ ℂ ) → Σ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 )
165 1 162 164 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 )
166 165 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝜑 ) → Σ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 )
167 48 166 eqtr2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝜑 ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
168 167 ex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑀 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
169 simp3 ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ∧ 𝜑 ) → 𝜑 )
170 simp1 ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ∧ 𝜑 ) → 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
171 simp2 ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ∧ 𝜑 ) → ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
172 169 171 mpd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ∧ 𝜑 ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
173 50 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
174 elfzoelz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 ∈ ℤ )
175 174 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 ∈ ℝ )
176 175 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ℝ )
177 52 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 + 1 ) ∈ ℝ )
178 53 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 < ( 𝑀 + 1 ) )
179 elfzole1 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( 𝑀 + 1 ) ≤ 𝑘 )
180 179 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 + 1 ) ≤ 𝑘 )
181 173 177 176 178 180 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 < 𝑘 )
182 173 176 181 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ≤ 𝑘 )
183 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑘 ) )
184 1 174 183 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑘 ) )
185 182 184 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
186 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
187 eliccxr ⊢ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ* )
188 187 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ℝ* )
189 186 73 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
190 186 3 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
191 elfzelz ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ∈ ℤ )
192 191 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ℤ )
193 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑀 ≤ 𝑖 )
194 193 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 ≤ 𝑖 )
195 192 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ℝ )
196 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑁 ∈ ℝ )
197 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑘 ∈ ℝ )
198 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ≤ 𝑘 )
199 198 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ≤ 𝑘 )
200 elfzolt2 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 < 𝑁 )
201 200 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑘 < 𝑁 )
202 195 197 196 199 201 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 < 𝑁 )
203 195 196 202 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ≤ 𝑁 )
204 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
205 204 96 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
206 192 194 203 205 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
207 206 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
208 190 207 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
209 192 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 + 1 ) ∈ ℤ )
210 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 ∈ ℝ )
211 209 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
212 50 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 ∈ ℝ )
213 191 zred ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ∈ ℝ )
214 213 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ℝ )
215 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 1 ∈ ℝ )
216 214 215 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
217 193 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 ≤ 𝑖 )
218 214 ltp1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 < ( 𝑖 + 1 ) )
219 212 214 216 217 218 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 < ( 𝑖 + 1 ) )
220 219 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 < ( 𝑖 + 1 ) )
221 210 211 220 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
222 9 191 anim12ci ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
223 222 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
224 223 128 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
225 202 224 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
226 204 131 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
227 209 221 225 226 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
228 227 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
229 190 228 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
230 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
231 eliccre ⊢ ( ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
232 208 229 230 231 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
233 elfzuz ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
234 233 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
235 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
236 elfzelz ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) → 𝑗 ∈ ℤ )
237 236 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ∈ ℤ )
238 elfzle1 ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) → 𝑀 ≤ 𝑗 )
239 238 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑀 ≤ 𝑗 )
240 237 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ∈ ℝ )
241 196 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑁 ∈ ℝ )
242 195 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑖 ∈ ℝ )
243 elfzle2 ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) → 𝑗 ≤ 𝑖 )
244 243 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ≤ 𝑖 )
245 202 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑖 < 𝑁 )
246 240 242 241 244 245 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 < 𝑁 )
247 240 241 246 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ≤ 𝑁 )
248 204 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
249 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
250 248 249 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
251 237 239 247 250 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
252 235 251 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ )
253 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
254 elfzelz ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) → 𝑗 ∈ ℤ )
255 254 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℤ )
256 elfzle1 ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) → 𝑀 ≤ 𝑗 )
257 256 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 ≤ 𝑗 )
258 255 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℝ )
259 196 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑁 ∈ ℝ )
260 195 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑖 ∈ ℝ )
261 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 1 ∈ ℝ )
262 260 261 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) ∈ ℝ )
263 elfzle2 ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) → 𝑗 ≤ ( 𝑖 − 1 ) )
264 263 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ≤ ( 𝑖 − 1 ) )
265 260 ltm1d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) < 𝑖 )
266 258 262 260 264 265 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 < 𝑖 )
267 202 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑖 < 𝑁 )
268 258 260 259 266 267 lttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 < 𝑁 )
269 258 259 268 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ≤ 𝑁 )
270 204 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
271 270 249 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
272 255 257 269 271 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
273 253 272 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ )
274 255 peano2zd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℤ )
275 173 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℝ )
276 258 261 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℝ )
277 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℝ )
278 254 zred ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) → 𝑗 ∈ ℝ )
279 278 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℝ )
280 1red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 1 ∈ ℝ )
281 279 280 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℝ )
282 256 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 ≤ 𝑗 )
283 279 ltp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 < ( 𝑗 + 1 ) )
284 277 279 281 282 283 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 < ( 𝑗 + 1 ) )
285 284 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 < ( 𝑗 + 1 ) )
286 275 276 285 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑀 ≤ ( 𝑗 + 1 ) )
287 zltp1le ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑗 < 𝑖 ↔ ( 𝑗 + 1 ) ≤ 𝑖 ) )
288 254 192 287 syl2anr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 < 𝑖 ↔ ( 𝑗 + 1 ) ≤ 𝑖 ) )
289 266 288 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑖 )
290 276 260 259 289 267 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) < 𝑁 )
291 276 259 290 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑁 )
292 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑗 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑗 + 1 ) ∧ ( 𝑗 + 1 ) ≤ 𝑁 ) ) )
293 270 292 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑗 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑗 + 1 ) ∧ ( 𝑗 + 1 ) ≤ 𝑁 ) ) )
294 274 286 291 293 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
295 253 294 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
296 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝜑 )
297 elfzuz ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
298 297 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
299 296 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑁 ∈ ℤ )
300 elfzo2 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁 ) )
301 298 299 268 300 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) )
302 eleq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) )
303 302 anbi2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
304 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑗 ) )
305 fvoveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
306 304 305 breq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑃 ‘ 𝑗 ) < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) )
307 303 306 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑗 ) < ( 𝑃 ‘ ( 𝑗 + 1 ) ) ) ) )
308 307 4 chvarvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑗 ) < ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
309 296 301 308 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) < ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
310 273 295 309 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) ≤ ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
311 234 252 310 monoord ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑖 ) )
312 311 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑖 ) )
313 208 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ* )
314 229 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
315 iccgelb ⊢ ( ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ 𝑡 )
316 313 314 230 315 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ 𝑡 )
317 189 208 232 312 316 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
318 186 64 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
319 iccleub ⊢ ( ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
320 313 314 230 319 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
321 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑁 ∈ ℤ )
322 eluz ⊢ ( ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
323 209 321 322 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
324 225 323 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
325 324 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) )
326 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
327 elfzelz ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) → 𝑗 ∈ ℤ )
328 327 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑗 ∈ ℤ )
329 elfzel1 ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑀 ∈ ℤ )
330 329 zred ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑀 ∈ ℝ )
331 330 adantr ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑀 ∈ ℝ )
332 327 zred ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) → 𝑗 ∈ ℝ )
333 332 adantl ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑗 ∈ ℝ )
334 213 adantr ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
335 1red ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 1 ∈ ℝ )
336 334 335 readdcld ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
337 193 adantr ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑀 ≤ 𝑖 )
338 334 ltp1d ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑖 < ( 𝑖 + 1 ) )
339 331 334 336 337 338 lelttrd ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑀 < ( 𝑖 + 1 ) )
340 elfzle1 ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) → ( 𝑖 + 1 ) ≤ 𝑗 )
341 340 adantl ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → ( 𝑖 + 1 ) ≤ 𝑗 )
342 331 336 333 339 341 ltletrd ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑀 < 𝑗 )
343 331 333 342 ltled ⊢ ( ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑀 ≤ 𝑗 )
344 343 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑀 ≤ 𝑗 )
345 elfzle2 ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) → 𝑗 ≤ 𝑁 )
346 345 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑗 ≤ 𝑁 )
347 204 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
348 347 249 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
349 328 344 346 348 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
350 326 349 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ )
351 350 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... 𝑁 ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ )
352 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝜑 )
353 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑘 ) )
354 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) )
355 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
356 elfzelz ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℤ )
357 356 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℤ )
358 50 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℝ )
359 357 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℝ )
360 216 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
361 219 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑖 + 1 ) )
362 elfzle1 ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝑖 + 1 ) ≤ 𝑗 )
363 362 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑗 )
364 358 360 359 361 363 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑗 )
365 358 359 364 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ 𝑗 )
366 356 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℤ )
367 366 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℝ )
368 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
369 1red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
370 368 369 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
371 elfzle2 ⊢ ( 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑗 ≤ ( 𝑁 − 1 ) )
372 371 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ≤ ( 𝑁 − 1 ) )
373 368 ltm1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
374 367 370 368 372 373 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 < 𝑁 )
375 367 368 374 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ≤ 𝑁 )
376 375 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ≤ 𝑁 )
377 94 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
378 377 249 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
379 357 365 376 378 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
380 355 379 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) ∈ ℝ )
381 357 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℤ )
382 381 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℝ )
383 213 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
384 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
385 218 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < ( 𝑖 + 1 ) )
386 383 360 359 385 363 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑗 )
387 383 359 386 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑗 )
388 383 359 384 387 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ ( 𝑗 + 1 ) )
389 358 360 382 361 388 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑗 + 1 ) )
390 358 382 389 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ ( 𝑗 + 1 ) )
391 zltp1le ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 < 𝑁 ↔ ( 𝑗 + 1 ) ≤ 𝑁 ) )
392 356 9 391 syl2anr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 < 𝑁 ↔ ( 𝑗 + 1 ) ≤ 𝑁 ) )
393 374 392 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑁 )
394 393 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑁 )
395 377 292 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑗 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑗 + 1 ) ∧ ( 𝑗 + 1 ) ≤ 𝑁 ) ) )
396 381 390 394 395 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
397 355 396 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
398 simp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝜑 )
399 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℤ )
400 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑗 ) )
401 399 357 400 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑗 ) )
402 365 401 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
403 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
404 374 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 < 𝑁 )
405 402 403 404 300 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) )
406 398 405 308 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) < ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
407 380 397 406 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) ≤ ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
408 352 353 354 407 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) ≤ ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
409 408 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑗 ∈ ( ( 𝑖 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑗 ) ≤ ( 𝑃 ‘ ( 𝑗 + 1 ) ) )
410 325 351 409 monoord ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
411 232 229 318 320 410 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) )
412 64 rexrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) ∈ ℝ* )
413 74 412 jca ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑁 ) ∈ ℝ* ) )
414 186 413 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑁 ) ∈ ℝ* ) )
415 elicc1 ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑁 ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) ) ) )
416 414 415 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) ) ) )
417 188 317 411 416 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
418 186 417 5 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐴 ∈ ℂ )
419 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝜑 )
420 234 321 202 139 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
421 419 420 6 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
422 418 421 itgcl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ∈ ℂ )
423 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑘 ) )
424 fvoveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
425 423 424 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
426 425 itgeq1d ⊢ ( 𝑖 = 𝑘 → ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 )
427 185 422 426 fzosump1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ( Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) )
428 427 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) → Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 = ( Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) )
429 oveq1 ⊢ ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) = ( Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) )
430 429 eqcomd ⊢ ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 → ( Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) = ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) )
431 430 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) → ( Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) = ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) )
432 73 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
433 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
434 174 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ℤ )
435 434 peano2zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℤ )
436 435 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
437 176 ltp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 < ( 𝑘 + 1 ) )
438 173 176 436 181 437 lttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 < ( 𝑘 + 1 ) )
439 173 436 438 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ≤ ( 𝑘 + 1 ) )
440 200 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 < 𝑁 )
441 zltp1le ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
442 174 9 441 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 < 𝑁 ↔ ( 𝑘 + 1 ) ≤ 𝑁 ) )
443 440 442 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
444 94 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
445 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) )
446 444 445 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑘 + 1 ) ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) )
447 435 439 443 446 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
448 433 447 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
449 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
450 176 449 440 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ≤ 𝑁 )
451 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
452 444 451 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
453 434 182 450 452 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
454 433 453 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
455 454 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ* )
456 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
457 456 206 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
458 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
459 elfzelz ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ∈ ℤ )
460 459 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ℤ )
461 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑀 ≤ 𝑖 )
462 461 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑀 ≤ 𝑖 )
463 460 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ℝ )
464 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑁 ∈ ℝ )
465 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑘 ∈ ℝ )
466 1red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 1 ∈ ℝ )
467 465 466 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℝ )
468 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ≤ ( 𝑘 − 1 ) )
469 468 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ≤ ( 𝑘 − 1 ) )
470 465 ltm1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑘 − 1 ) < 𝑘 )
471 463 467 465 469 470 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 < 𝑘 )
472 440 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑘 < 𝑁 )
473 463 465 464 471 472 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 < 𝑁 )
474 463 464 473 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
475 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
476 475 96 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
477 460 462 474 476 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
478 458 477 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
479 460 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
480 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑀 ∈ ℝ )
481 463 466 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
482 463 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 < ( 𝑖 + 1 ) )
483 480 463 481 462 482 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑀 < ( 𝑖 + 1 ) )
484 480 481 483 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
485 zltp1le ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑖 < 𝑘 ↔ ( 𝑖 + 1 ) ≤ 𝑘 ) )
486 459 434 485 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 < 𝑘 ↔ ( 𝑖 + 1 ) ≤ 𝑘 ) )
487 471 486 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑘 )
488 481 465 464 487 472 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) < 𝑁 )
489 481 464 488 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
490 475 131 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ 𝑁 ) ) )
491 479 484 489 490 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
492 458 491 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
493 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝜑 )
494 elfzuz ⊢ ( 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
495 494 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
496 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑁 ∈ ℤ )
497 495 496 473 139 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
498 493 497 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
499 478 492 498 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ... ( 𝑘 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
500 185 457 499 monoord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑘 ) )
501 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
502 elfzo2 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁 ) )
503 185 501 440 502 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
504 eleq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) )
505 504 anbi2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
506 423 424 breq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
507 505 506 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
508 507 4 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
509 503 508 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
510 454 448 509 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
511 74 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
512 448 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* )
513 elicc1 ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝑃 ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
514 511 512 513 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝑃 ‘ 𝑘 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑘 ) ∧ ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
515 455 500 510 514 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
516 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝜑 )
517 eliccxr ⊢ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) → 𝑡 ∈ ℝ* )
518 517 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ℝ* )
519 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
520 512 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* )
521 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
522 iccgelb ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
523 519 520 521 522 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
524 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
525 448 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
526 eliccre ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
527 524 525 521 526 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
528 64 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
529 iccleub ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
530 519 520 521 529 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
531 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) )
532 435 501 443 531 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
533 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
534 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 ∈ ℤ )
535 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ℤ )
536 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → 𝑖 ∈ ℤ )
537 536 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℤ )
538 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 ∈ ℝ )
539 537 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
540 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℝ )
541 181 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 < 𝑘 )
542 175 adantr ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℝ )
543 1red ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 1 ∈ ℝ )
544 542 543 readdcld ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
545 536 zred ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → 𝑖 ∈ ℝ )
546 545 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
547 542 ltp1d ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 < ( 𝑘 + 1 ) )
548 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑖 )
549 548 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑖 )
550 542 544 546 547 549 ltletrd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 < 𝑖 )
551 550 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑘 < 𝑖 )
552 538 540 539 541 551 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 < 𝑖 )
553 538 539 552 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑀 ≤ 𝑖 )
554 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) → 𝑖 ≤ 𝑁 )
555 554 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ≤ 𝑁 )
556 534 535 537 553 555 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
557 533 556 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
558 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
559 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℤ )
560 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
561 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℤ )
562 561 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℤ )
563 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℝ )
564 562 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
565 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℝ )
566 181 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑘 )
567 175 adantr ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℝ )
568 1red ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
569 567 568 readdcld ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℝ )
570 561 zred ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℝ )
571 570 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
572 567 ltp1d ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < ( 𝑘 + 1 ) )
573 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → ( 𝑘 + 1 ) ≤ 𝑖 )
574 573 adantl ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ≤ 𝑖 )
575 567 569 571 572 574 ltletrd ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < 𝑖 )
576 575 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < 𝑖 )
577 563 565 564 566 576 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑖 )
578 563 564 577 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ 𝑖 )
579 570 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
580 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
581 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
582 580 581 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
583 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
584 583 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
585 580 ltm1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
586 579 582 580 584 585 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
587 579 580 586 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
588 587 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
589 559 560 562 578 588 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
590 558 589 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
591 562 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
592 591 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
593 564 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < ( 𝑖 + 1 ) )
594 565 564 592 576 593 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑘 < ( 𝑖 + 1 ) )
595 563 565 592 566 594 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑖 + 1 ) )
596 563 592 595 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
597 586 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
598 561 501 128 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
599 597 598 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
600 559 560 591 596 599 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
601 558 600 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
602 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝜑 )
603 eluz2 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ) )
604 559 562 578 603 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
605 604 560 597 139 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
606 602 605 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
607 590 601 606 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( ( 𝑘 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
608 532 557 607 monoord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
609 608 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝑃 ‘ 𝑁 ) )
610 527 525 528 530 609 letrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) )
611 413 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑁 ) ∈ ℝ* ) )
612 611 415 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝑡 ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 ∧ 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) ) ) )
613 518 523 610 612 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
614 516 613 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → 𝐴 ∈ ℂ )
615 nfv ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
616 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑀 ∈ ℤ )
617 elfzouz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
618 617 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
619 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝜑 )
620 elfzouz ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
621 620 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
622 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑁 ∈ ℤ )
623 elfzoelz ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) → 𝑖 ∈ ℤ )
624 623 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) → 𝑖 ∈ ℝ )
625 624 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑖 ∈ ℝ )
626 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑘 ∈ ℝ )
627 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑁 ∈ ℝ )
628 elfzolt2 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) → 𝑖 < 𝑘 )
629 628 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑖 < 𝑘 )
630 440 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑘 < 𝑁 )
631 625 626 627 629 630 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑖 < 𝑁 )
632 621 622 631 139 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
633 619 632 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
634 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝜑 )
635 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ )
636 64 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ ℝ )
637 454 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ )
638 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) )
639 eliccre ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝑃 ‘ 𝑘 ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ∈ ℝ )
640 635 637 638 639 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ∈ ℝ )
641 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
642 455 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ℝ* )
643 iccgelb ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑘 ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
644 641 642 638 643 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑀 ) ≤ 𝑡 )
645 iccleub ⊢ ( ( ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑘 ) ∈ ℝ* ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑘 ) )
646 641 642 638 645 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑘 ) )
647 elfzouz2 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
648 647 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
649 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
650 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
651 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
652 elfzelz ⊢ ( 𝑖 ∈ ( 𝑘 ... 𝑁 ) → 𝑖 ∈ ℤ )
653 652 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑖 ∈ ℤ )
654 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
655 653 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑖 ∈ ℝ )
656 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
657 181 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑀 < 𝑘 )
658 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑘 ... 𝑁 ) → 𝑘 ≤ 𝑖 )
659 658 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑘 ≤ 𝑖 )
660 654 656 655 657 659 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑀 < 𝑖 )
661 654 655 660 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑀 ≤ 𝑖 )
662 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑘 ... 𝑁 ) → 𝑖 ≤ 𝑁 )
663 662 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑖 ≤ 𝑁 )
664 650 651 653 661 663 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
665 649 664 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
666 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑃 : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
667 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℤ )
668 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℤ )
669 elfzelz ⊢ ( 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℤ )
670 669 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℤ )
671 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 ∈ ℝ )
672 670 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
673 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℝ )
674 181 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑘 )
675 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) → 𝑘 ≤ 𝑖 )
676 675 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑘 ≤ 𝑖 )
677 671 673 672 674 676 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 < 𝑖 )
678 671 672 677 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ 𝑖 )
679 669 zred ⊢ ( 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) → 𝑖 ∈ ℝ )
680 679 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ℝ )
681 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℝ )
682 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℝ )
683 681 682 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
684 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
685 684 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ ( 𝑁 − 1 ) )
686 681 ltm1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 1 ) < 𝑁 )
687 680 683 681 685 686 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
688 680 681 687 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
689 688 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ≤ 𝑁 )
690 667 668 670 678 689 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ... 𝑁 ) )
691 666 690 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ )
692 670 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
693 692 zred ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
694 672 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 < ( 𝑖 + 1 ) )
695 671 672 693 678 694 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 < ( 𝑖 + 1 ) )
696 671 693 695 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
697 669 9 128 syl2anr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 < 𝑁 ↔ ( 𝑖 + 1 ) ≤ 𝑁 ) )
698 687 697 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
699 698 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑁 )
700 667 668 692 696 699 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
701 666 700 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
702 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝜑 )
703 667 670 678 603 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
704 687 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 < 𝑁 )
705 703 668 704 139 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
706 702 705 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
707 691 701 706 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑘 ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
708 648 665 707 monoord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ 𝑁 ) )
709 708 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ 𝑁 ) )
710 640 637 636 646 709 letrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ≤ ( 𝑃 ‘ 𝑁 ) )
711 635 636 640 644 710 eliccd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) )
712 634 711 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ) → 𝐴 ∈ ℂ )
713 619 632 6 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
714 615 616 618 457 633 712 713 iblspltprt ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) ↦ 𝐴 ) ∈ 𝐿1 )
715 425 mpteq1d ⊢ ( 𝑖 = 𝑘 → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) )
716 715 eleq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ↔ ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) )
717 505 716 imbi12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 ) ) )
718 717 6 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
719 503 718 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝑡 ∈ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↦ 𝐴 ) ∈ 𝐿1 )
720 432 448 515 614 714 719 itgspliticc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 = ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) )
721 720 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 )
722 721 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) → ( ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 + ∫ ( ( 𝑃 ‘ 𝑘 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 ) = ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 )
723 428 431 722 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
724 169 170 172 723 syl3anc ⊢ ( ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∧ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ∧ 𝜑 ) → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )
725 724 3exp ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) → ( ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑘 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑘 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) → ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ ( 𝑘 + 1 ) ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) ) )
726 22 29 36 43 168 725 fzind2 ⊢ ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 ) )
727 15 726 mpcom ⊢ ( 𝜑 → ∫ ( ( 𝑃 ‘ 𝑀 ) [,] ( 𝑃 ‘ 𝑁 ) ) 𝐴 d 𝑡 = Σ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∫ ( ( 𝑃 ‘ 𝑖 ) [,] ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) 𝐴 d 𝑡 )