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