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 43514

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 Ⅎwnf 1786 ∈ wcel 2106 ∪ cun 3885 ∩ cin 3886 {csn 4561 class class class wbr 5074 ↦ cmpt 5157 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 ℤcz 12319 ℤ_≥cuz 12582 [,]cicc 13082 ...cfz 13239 ..^cfzo 13382 vol*covol 24626 𝐿¹cibl 24781

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-disj 5040 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-ofr 7534 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-z 12320 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-seq 13722 df-exp 13783 df-hash 14045 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-clim 15197 df-sum 15398 df-rest 17133 df-topgen 17154 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-top 22043 df-topon 22060 df-bases 22096 df-cmp 22538 df-ovol 24628 df-vol 24629 df-mbf 24783 df-itg1 24784 df-itg2 24785 df-ibl 24786

This theorem is referenced by: itgspltprt 43520 fourierdlem69 43716

W3C validator