itgspltprt - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > itgspltprt		Structured version Visualization version GIF version

Theorem itgspltprt 45429

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

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

**Assertion**
Ref	Expression
itgspltprt	⊢ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)

Distinct variable groups: 𝐴,𝑖 𝑖,𝑀,𝑡 𝑖,𝑁,𝑡 𝑃,𝑖,𝑡 𝜑,𝑖,𝑡 Allowed substitution hint: 𝐴(𝑡)

Proof of Theorem itgspltprt Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 class class class wbr 5143 ↦ cmpt 5226 ⟶wf 6538 ‘cfv 6542 (class class class)co 7415 ℂcc 11134 ℝcr 11135 1c1 11137 + caddc 11139 ℝ^*cxr 11275 < clt 11276 ≤ cle 11277 − cmin 11472 ℤcz 12586 ℤ_≥cuz 12850 [,]cicc 13357 ...cfz 13514 ..^cfzo 13657 Σcsu 15662 𝐿¹cibl 25562 ∫citg 25563

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7737 ax-inf2 9662 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213 ax-pre-sup 11214 ax-addf 11215

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3960 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-disj 5109 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7371 df-ov 7418 df-oprab 7419 df-mpo 7420 df-of 7681 df-ofr 7682 df-om 7868 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8388 df-rdg 8427 df-1o 8483 df-2o 8484 df-er 8721 df-map 8843 df-pm 8844 df-en 8961 df-dom 8962 df-sdom 8963 df-fin 8964 df-fi 9432 df-sup 9463 df-inf 9464 df-oi 9531 df-dju 9922 df-card 9960 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11474 df-neg 11475 df-div 11900 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-n0 12501 df-z 12587 df-uz 12851 df-q 12961 df-rp 13005 df-xneg 13122 df-xadd 13123 df-xmul 13124 df-ioo 13358 df-ico 13360 df-icc 13361 df-fz 13515 df-fzo 13658 df-fl 13787 df-mod 13865 df-seq 13997 df-exp 14057 df-hash 14320 df-cj 15076 df-re 15077 df-im 15078 df-sqrt 15212 df-abs 15213 df-clim 15462 df-sum 15663 df-rest 17401 df-topgen 17422 df-psmet 21273 df-xmet 21274 df-met 21275 df-bl 21276 df-mopn 21277 df-top 22812 df-topon 22829 df-bases 22865 df-cmp 23307 df-ovol 25409 df-vol 25410 df-mbf 25564 df-itg1 25565 df-itg2 25566 df-ibl 25567 df-itg 25568

This theorem is referenced by: fourierdlem73 45629 fourierdlem81 45637 fourierdlem93 45649

W3C validator