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 43143

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 12268	. . 3 ⊢ (𝜑 → (𝑀 + 1) ∈ ℤ)
3		iblspltprt.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
4		eluzelz 12431	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℤ)
6		eluzle 12434	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
7	3, 6	syl 17	. . 3 ⊢ (𝜑 → (𝑀 + 1) ≤ 𝑁)
8	5	zred 12265	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ)
9	8	leidd 11381	. . 3 ⊢ (𝜑 → 𝑁 ≤ 𝑁)
10	2, 5, 5, 7, 9	elfzd 13086	. 2 ⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁))
11		fveq2 6706	. . . . . . 7 ⊢ (𝑗 = (𝑀 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑀 + 1)))
12	11	oveq2d 7218	. . . . . 6 ⊢ (𝑗 = (𝑀 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
13	12	mpteq1d 5133	. . . . 5 ⊢ (𝑗 = (𝑀 + 1) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
14	13	eleq1d 2818	. . . 4 ⊢ (𝑗 = (𝑀 + 1) → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹ ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹))
15	14	imbi2d 344	. . 3 ⊢ (𝑗 = (𝑀 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹) ↔ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹)))
16		fveq2 6706	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘))
17	16	oveq2d 7218	. . . . . 6 ⊢ (𝑗 = 𝑘 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑘)))
18	17	mpteq1d 5133	. . . . 5 ⊢ (𝑗 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴))
19	18	eleq1d 2818	. . . 4 ⊢ (𝑗 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹ ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹))
20	19	imbi2d 344	. . 3 ⊢ (𝑗 = 𝑘 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹) ↔ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹)))
21		fveq2 6706	. . . . . . 7 ⊢ (𝑗 = (𝑘 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑘 + 1)))
22	21	oveq2d 7218	. . . . . 6 ⊢ (𝑗 = (𝑘 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
23	22	mpteq1d 5133	. . . . 5 ⊢ (𝑗 = (𝑘 + 1) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
24	23	eleq1d 2818	. . . 4 ⊢ (𝑗 = (𝑘 + 1) → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹ ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹))
25	24	imbi2d 344	. . 3 ⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹) ↔ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹)))
26		fveq2 6706	. . . . . . 7 ⊢ (𝑗 = 𝑁 → (𝑃‘𝑗) = (𝑃‘𝑁))
27	26	oveq2d 7218	. . . . . 6 ⊢ (𝑗 = 𝑁 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑁)))
28	27	mpteq1d 5133	. . . . 5 ⊢ (𝑗 = 𝑁 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴))
29	28	eleq1d 2818	. . . 4 ⊢ (𝑗 = 𝑁 → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹ ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈ 𝐿¹))
30	29	imbi2d 344	. . 3 ⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿¹) ↔ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈ 𝐿¹)))
31		uzid 12436	. . . . . . 7 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
32	1, 31	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
33	1	zred 12265	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℝ)
34		1red 10817	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
35	33, 34	readdcld 10845	. . . . . . 7 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
36	33	ltp1d 11745	. . . . . . 7 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
37	33, 35, 8, 36, 7	ltletrd 10975	. . . . . 6 ⊢ (𝜑 → 𝑀 < 𝑁)
38		elfzo2 13229	. . . . . 6 ⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ (ℤ_≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
39	32, 5, 37, 38	syl3anbrc 1345	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (𝑀..^𝑁))
40		fveq2 6706	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀))
41		fvoveq1 7225	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
42	40, 41	oveq12d 7220	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
43	42	mpteq1d 5133	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
44	43	eleq1d 2818	. . . . . . 7 ⊢ (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿¹ ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹))
45	44	imbi2d 344	. . . . . 6 ⊢ (𝑖 = 𝑀 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿¹) ↔ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹)))
46		iblspltprt.7	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿¹)
47	46	expcom 417	. . . . . 6 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿¹))
48	45, 47	vtoclga 3482	. . . . 5 ⊢ (𝑀 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹))
49	39, 48	mpcom 38	. . . 4 ⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹)
50	49	a1i 11	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿¹))
51		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑡 𝑘 ∈ ((𝑀 + 1)..^𝑁)
52		iblspltprt.1	. . . . . . 7 ⊢ Ⅎ𝑡𝜑
53		nfmpt1 5142	. . . . . . . 8 ⊢ Ⅎ𝑡(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴)
54	53	nfel1 2916	. . . . . . 7 ⊢ Ⅎ𝑡(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹
55	52, 54	nfim 1904	. . . . . 6 ⊢ Ⅎ𝑡(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹)
56	51, 55, 52	nf3an 1909	. . . . 5 ⊢ Ⅎ𝑡(𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑)
57		simp3 1140	. . . . . 6 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → 𝜑)
58		simp1 1138	. . . . . 6 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
59	33	leidd 11381	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
60	33, 8, 37	ltled 10963	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
61	1, 5, 1, 59, 60	elfzd 13086	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁))
62	61	ancli 552	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)))
63		eleq1 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑀 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁)))
64	63	anbi2d 632	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑀 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑀 ∈ (𝑀...𝑁))))
65	40	eleq1d 2818	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑀) ∈ ℝ))
66	64, 65	imbi12d 348	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑀 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝑃‘𝑀) ∈ ℝ)))
67		iblspltprt.4	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
68	66, 67	vtoclg 3474	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝑃‘𝑀) ∈ ℝ))
69	61, 62, 68	sylc 65	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃‘𝑀) ∈ ℝ)
70	69	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ)
71	70	rexrd 10866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ^*)
72		simpl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝜑)
73		elfzoelz 13226	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
74	73	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
75	33	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
76	74	zred 12265	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
77	35	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
78	36	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
79		elfzole1 13234	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
80	79	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
81	75, 77, 76, 78, 80	ltletrd 10975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
82	75, 76, 81	ltled 10963	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ 𝑘)
83	8	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
84		elfzolt2 13235	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
85	84	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
86	76, 83, 85	ltled 10963	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ≤ 𝑁)
87	1, 5	jca 515	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
88	87	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
89		elfz1 13083	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
90	88, 89	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
91	74, 82, 86, 90	mpbir3and 1344	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
92		eleq1 2821	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑘 ∈ (𝑀...𝑁)))
93	92	anbi2d 632	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀...𝑁))))
94		fveq2 6706	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑃‘𝑖) = (𝑃‘𝑘))
95	94	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑘) ∈ ℝ))
96	93, 95	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ)))
97	96, 67	chvarvv 2007	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ)
98	72, 91, 97	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ)
99	98	rexrd 10866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ^*)
100	74	peano2zd 12268	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
101	100	zred 12265	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
102		1red 10817	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 1 ∈ ℝ)
103	75, 76, 102, 81	ltadd1dd 11426	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) < (𝑘 + 1))
104	75, 77, 101, 78, 103	lttrd 10976	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
105	75, 101, 104	ltled 10963	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
106		zltp1le 12210	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
107	73, 5, 106	syl2anr 600	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
108	85, 107	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
109		elfz1 13083	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
110	88, 109	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
111	100, 105, 108, 110	mpbir3and 1344	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
112	72, 111	jca 515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))
113		eleq1 2821	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁)))
114	113	anbi2d 632	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))))
115		fveq2 6706	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑘 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑘 + 1)))
116	115	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑘 + 1) → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘(𝑘 + 1)) ∈ ℝ))
117	114, 116	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)))
118	117, 67	vtoclg 3474	. . . . . . . . . . 11 ⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ))
119	111, 112, 118	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
120	119	rexrd 10866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ^*)
121		eluz 12435	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑘))
122	1, 73, 121	syl2an 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑘))
123	82, 122	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ_≥‘𝑀))
124		simpll 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
125		elfzelz 13095	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
126	125	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
127		elfzle1 13098	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑀 ≤ 𝑖)
128	127	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖)
129	126	zred 12265	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
130	124, 8	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
131	76	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
132		elfzle2 13099	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ≤ 𝑘)
133	132	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑘)
134	85	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
135	129, 131, 130, 133, 134	lelttrd 10973	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
136	129, 130, 135	ltled 10963	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑁)
137		elfz1 13083	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
138	124, 87, 137	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
139	126, 128, 136, 138	mpbir3and 1344	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
140	124, 139, 67	syl2anc 587	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑖) ∈ ℝ)
141		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
142		elfzelz 13095	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
143	142	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
144		elfzle1 13098	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ 𝑖)
145	144	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ 𝑖)
146	143	zred 12265	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
147	141, 8	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
148	76	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
149		1red 10817	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
150	148, 149	resubcld 11243	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
151		elfzle2 13099	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
152	151	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
153	73	zred 12265	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
154		1red 10817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 1 ∈ ℝ)
155	153, 154	resubcld 11243	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) ∈ ℝ)
156		elfzoel2 13225	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℤ)
157	156	zred 12265	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℝ)
158	153	ltm1d 11747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑘)
159	155, 153, 157, 158, 84	lttrd 10976	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑁)
160	159	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑁)
161	146, 150, 147, 152, 160	lelttrd 10973	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
162	146, 147, 161	ltled 10963	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ 𝑁)
163	141, 87, 137	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
164	143, 145, 162, 163	mpbir3and 1344	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
165	141, 164, 67	syl2anc 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ∈ ℝ)
166	143	peano2zd 12268	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
167		elfzel1 13094	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℤ)
168	167	zred 12265	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℝ)
169	142	zred 12265	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℝ)
170		1red 10817	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 1 ∈ ℝ)
171	169, 170	readdcld 10845	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → (𝑖 + 1) ∈ ℝ)
172	169	ltp1d 11745	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 < (𝑖 + 1))
173	168, 169, 171, 144, 172	lelttrd 10973	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 < (𝑖 + 1))
174	168, 171, 173	ltled 10963	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ (𝑖 + 1))
175	174	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
176	141, 3, 4	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
177		zltp1le 12210	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
178	143, 176, 177	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
179	161, 178	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
180		elfz1 13083	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
181	141, 87, 180	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
182	166, 175, 179, 181	mpbir3and 1344	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
183	141, 182	jca 515	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)))
184		eleq1 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑖 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑖 + 1) ∈ (𝑀...𝑁)))
185	184	anbi2d 632	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑖 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁))))
186		fveq2 6706	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑖 + 1) → (𝑃‘𝑘) = (𝑃‘(𝑖 + 1)))
187	186	eleq1d 2818	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑖 + 1) → ((𝑃‘𝑘) ∈ ℝ ↔ (𝑃‘(𝑖 + 1)) ∈ ℝ))
188	185, 187	imbi12d 348	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑖 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ)))
189	188, 97	vtoclg 3474	. . . . . . . . . . . 12 ⊢ ((𝑖 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ))
190	182, 183, 189	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
191		elfzuz 13091	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ_≥‘𝑀))
192	191	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ_≥‘𝑀))
193		elfzo2 13229	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ_≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
194	192, 176, 161, 193	syl3anbrc 1345	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
195		iblspltprt.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
196	141, 194, 195	syl2anc 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
197	165, 190, 196	ltled 10963	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
198	123, 140, 197	monoord 13589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ≤ (𝑃‘𝑘))
199	156	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
200		elfzo2 13229	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ_≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
201	123, 199, 85, 200	syl3anbrc 1345	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
202		eleq1 2821	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
203	202	anbi2d 632	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁))))
204		fvoveq1 7225	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
205	94, 204	breq12d 5056	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))))
206	203, 205	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))))
207	206, 195	chvarvv 2007	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))
208	72, 201, 207	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))
209	98, 119, 208	ltled 10963	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))
210		iccintsng 42688	. . . . . . . . 9 ⊢ ((((𝑃‘𝑀) ∈ ℝ^* ∧ (𝑃‘𝑘) ∈ ℝ^* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ^*) ∧ ((𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))) → (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃‘𝑘)})
211	71, 99, 120, 198, 209, 210	syl32anc 1380	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃‘𝑘)})
212	211	fveq2d 6710	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = (vol‘{(𝑃‘𝑘)}))
213		ovolsn 24364	. . . . . . . 8 ⊢ ((𝑃‘𝑘) ∈ ℝ → (vol*‘{(𝑃‘𝑘)}) = 0)
214	98, 213	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘{(𝑃‘𝑘)}) = 0)
215	212, 214	eqtrd 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = 0)
216	57, 58, 215	syl2anc 587	. . . . 5 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = 0)
217	70, 119, 98, 198, 209	eliccd 42669	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
218	70, 119, 217	3jca 1130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))))
219	57, 58, 218	syl2anc 587	. . . . . 6 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))))
220		iccsplit 13056	. . . . . 6 ⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∪ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))))
221	219, 220	syl 17	. . . . 5 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∪ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))))
222		simpl3 1195	. . . . . 6 ⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
223		simpl1 1193	. . . . . 6 ⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
224		simpr 488	. . . . . 6 ⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
225		simp1 1138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
226		eliccxr 13006	. . . . . . . . 9 ⊢ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ^*)
227	226	3ad2ant3 1137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ^*)
228	69	rexrd 10866	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃‘𝑀) ∈ ℝ^*)
229	228	3ad2ant1 1135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈ ℝ^*)
230	120	3adant3 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ^*)
231		simp3 1140	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
232		iccgelb 12974	. . . . . . . . 9 ⊢ (((𝑃‘𝑀) ∈ ℝ^* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ^* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
233	229, 230, 231, 232	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
234	70, 119	jca 515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ))
235	234	3adant3 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ))
236		iccssre 13000	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ⊆ ℝ)
237	236	sseld 3890	. . . . . . . . . 10 ⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ))
238	235, 231, 237	sylc 65	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
239	119	3adant3 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
240	1, 5, 5, 60, 9	elfzd 13086	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
241	240	ancli 552	. . . . . . . . . . 11 ⊢ (𝜑 → (𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)))
242		eleq1 2821	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑁 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
243	242	anbi2d 632	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑁 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑁 ∈ (𝑀...𝑁))))
244		fveq2 6706	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑁 → (𝑃‘𝑖) = (𝑃‘𝑁))
245	244	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑁 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑁) ∈ ℝ))
246	243, 245	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑁 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)) → (𝑃‘𝑁) ∈ ℝ)))
247	246, 67	vtoclg 3474	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → ((𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)) → (𝑃‘𝑁) ∈ ℝ))
248	5, 241, 247	sylc 65	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃‘𝑁) ∈ ℝ)
249	248	3ad2ant1 1135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
250		elicc1 12962	. . . . . . . . . . . 12 ⊢ (((𝑃‘𝑀) ∈ ℝ^* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ^) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ^ ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1)))))
251	229, 230, 250	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ^* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1)))))
252	231, 251	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ℝ^* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1))))
253	252	simp3d 1146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
254		elfzop1le2 42453	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ≤ 𝑁)
255	73	peano2zd 12268	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ∈ ℤ)
256		eluz 12435	. . . . . . . . . . . . . 14 ⊢ (((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁))
257	255, 156, 256	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑁 ∈ (ℤ_≥‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁))
258	254, 257	mpbird 260	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ_≥‘(𝑘 + 1)))
259	258	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ_≥‘(𝑘 + 1)))
260		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝜑)
261		elfzelz 13095	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
262	261	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
263	260, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
264	262	zred 12265	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
265	76	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
266	81	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
267	153	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
268		1red 10817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
269	267, 268	readdcld 10845	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
270	261	zred 12265	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
271	270	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
272	267	ltp1d 11745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
273		elfzle1 13098	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
274	273	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
275	267, 269, 271, 272, 274	ltletrd 10975	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
276	275	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
277	263, 265, 264, 266, 276	lttrd 10976	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
278	263, 264, 277	ltled 10963	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
279		elfzle2 13099	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ≤ 𝑁)
280	279	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ≤ 𝑁)
281	260, 87, 137	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
282	262, 278, 280, 281	mpbir3and 1344	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
283	260, 282, 67	syl2anc 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
284		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
285		elfzelz 13095	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
286	285	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
287	284, 33	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
288	286	zred 12265	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
289	76	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
290	81	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
291	153	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
292		1red 10817	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
293	291, 292	readdcld 10845	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
294	285	zred 12265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
295	294	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
296	291	ltp1d 11745	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
297		elfzle1 13098	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
298	297	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
299	291, 293, 295, 296, 298	ltletrd 10975	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
300	299	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
301	287, 289, 288, 290, 300	lttrd 10976	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
302	287, 288, 301	ltled 10963	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
303	294	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
304	8	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
305		1red 10817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
306	304, 305	resubcld 11243	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
307		elfzle2 13099	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
308	307	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
309	304	ltm1d 11747	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
310	303, 306, 304, 308, 309	lelttrd 10973	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
311	303, 304, 310	ltled 10963	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
312	311	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
313	284, 87, 137	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
314	286, 302, 312, 313	mpbir3and 1344	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
315	284, 314, 67	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
316	286	peano2zd 12268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
317	316	zred 12265	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
318	295, 292	readdcld 10845	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
319	291, 295, 299	ltled 10963	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ≤ 𝑖)
320	291, 295, 292, 319	leadd1dd 11429	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ (𝑖 + 1))
321	291, 293, 318, 296, 320	ltletrd 10975	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
322	321	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
323	287, 289, 317, 290, 322	lttrd 10976	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
324	287, 317, 323	ltled 10963	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
325	285, 5, 177	syl2anr 600	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
326	310, 325	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
327	326	adantlr 715	. . . . . . . . . . . . . 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 1344	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
330	284, 329	jca 515	. . . . . . . . . . . . 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 12435	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑖))
334	332, 286, 333	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑖))
335	302, 334	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ_≥‘𝑀))
336	284, 3, 4	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
337	310	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
338	335, 336, 337, 193	syl3anbrc 1345	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
339	284, 338, 195	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
340	315, 331, 339	ltled 10963	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
341	259, 283, 340	monoord 13589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁))
342	341	3adant3 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁))
343	238, 239, 249, 253, 342	letrd 10972	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
344	249	rexrd 10866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ^*)
345		elicc1 12962	. . . . . . . . 9 ⊢ (((𝑃‘𝑀) ∈ ℝ^* ∧ (𝑃‘𝑁) ∈ ℝ^) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ^ ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
346	229, 344, 345	syl2anc 587	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ^* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
347	227, 233, 343, 346	mpbir3and 1344	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
348		iblspltprt.6	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ)
349	225, 347, 348	syl2anc 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
350	222, 223, 224, 349	syl3anc 1373	. . . . 5 ⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
351		simp2 1139	. . . . . 6 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹))
352	57, 351	mpd 15	. . . . 5 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹)
353	57, 58	jca 515	. . . . . 6 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → (𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)))
354	72, 201	jca 515	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)))
355	94, 204	oveq12d 7220	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))
356	355	mpteq1d 5133	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
357	356	eleq1d 2818	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿¹ ↔ (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹))
358	203, 357	imbi12d 348	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿¹) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹)))
359	358, 46	chvarvv 2007	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹)
360	353, 354, 359	3syl 18	. . . . 5 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹)
361	56, 216, 221, 350, 352, 360	iblsplitf 43140	. . . 4 ⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹)
362	361	3exp 1121	. . 3 ⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿¹) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿¹)))
363	15, 20, 25, 30, 50, 362	fzind2 13343	. 2 ⊢ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈ 𝐿¹))
364	10, 363	mpcom 38	1 ⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 Ⅎwnf 1791 ∈ wcel 2110 ∪ cun 3855 ∩ cin 3856 {csn 4531 class class class wbr 5043 ↦ cmpt 5124 ‘cfv 6369 (class class class)co 7202 ℂcc 10710 ℝcr 10711 0cc0 10712 1c1 10713 + caddc 10715 ℝ^*cxr 10849 < clt 10850 ≤ cle 10851 − cmin 11045 ℤcz 12159 ℤ_≥cuz 12421 [,]cicc 12921 ...cfz 13078 ..^cfzo 13221 vol*covol 24331 𝐿¹cibl 24486

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-inf2 9245 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-pre-sup 10790 ax-addf 10791

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-disj 5009 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-se 5499 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-isom 6378 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-of 7458 df-ofr 7459 df-om 7634 df-1st 7750 df-2nd 7751 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-2o 8192 df-er 8380 df-map 8499 df-pm 8500 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-fi 9016 df-sup 9047 df-inf 9048 df-oi 9115 df-dju 9500 df-card 9538 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-nn 11814 df-2 11876 df-3 11877 df-n0 12074 df-z 12160 df-uz 12422 df-q 12528 df-rp 12570 df-xneg 12687 df-xadd 12688 df-xmul 12689 df-ioo 12922 df-ico 12924 df-icc 12925 df-fz 13079 df-fzo 13222 df-fl 13350 df-seq 13558 df-exp 13619 df-hash 13880 df-cj 14645 df-re 14646 df-im 14647 df-sqrt 14781 df-abs 14782 df-clim 15032 df-sum 15233 df-rest 16899 df-topgen 16920 df-psmet 20327 df-xmet 20328 df-met 20329 df-bl 20330 df-mopn 20331 df-top 21763 df-topon 21780 df-bases 21815 df-cmp 22256 df-ovol 24333 df-vol 24334 df-mbf 24488 df-itg1 24489 df-itg2 24490 df-ibl 24491

This theorem is referenced by: itgspltprt 43149 fourierdlem69 43345

W3C validator