iblspltprt - Mathbox for Glauco Siliprandi

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

Theorem iblspltprt 38865

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

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

**Assertion**
Ref	Expression
iblspltprt	⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈ 𝐿¹)

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

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

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 Ⅎwnf 1699 ∈ wcel 1977 ∪ cun 3538 ∩ cin 3539 {csn 4125 class class class wbr 4583 ↦ cmpt 4643 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 ℤcz 11254 ℤ_≥cuz 11563 [,]cicc 12049 ...cfz 12197 ..^cfzo 12334 vol*covol 23038 𝐿¹cibl 23192

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-disj 4554 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-ofr 6796 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-sum 14265 df-rest 15906 df-topgen 15927 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-top 20521 df-bases 20522 df-topon 20523 df-cmp 21000 df-ovol 23040 df-vol 23041 df-mbf 23194 df-itg1 23195 df-itg2 23196 df-ibl 23197

This theorem is referenced by: itgspltprt 38871 fourierdlem69 39068

W3C validator