iblspltprt

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)

	Ref	Expression
Hypotheses	iblspltprt.1	$⊢ Ⅎ t φ$
	iblspltprt.2	$⊢ φ \to M \in ℤ$
	iblspltprt.3	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
	iblspltprt.4	$⊢ (φ \land i \in (M \dots N)) \to P (i) \in ℝ$
	iblspltprt.5	$⊢ (φ \land i \in (M ..^N)) \to P (i) < P (i + 1)$
	iblspltprt.6	$⊢ (φ \land t \in [P (M), P (N)]) \to A \in ℂ$
	iblspltprt.7	$⊢ (φ \land i \in (M ..^N)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}$
Assertion	iblspltprt	$⊢ φ \to (t \in [P (M), P (N)] ⟼ A) \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		iblspltprt.1	$⊢ Ⅎ t φ$
2		iblspltprt.2	$⊢ φ \to M \in ℤ$
3		iblspltprt.3	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
4		iblspltprt.4	$⊢ (φ \land i \in (M \dots N)) \to P (i) \in ℝ$
5		iblspltprt.5	$⊢ (φ \land i \in (M ..^N)) \to P (i) < P (i + 1)$
6		iblspltprt.6	$⊢ (φ \land t \in [P (M), P (N)]) \to A \in ℂ$
7		iblspltprt.7	$⊢ (φ \land i \in (M ..^N)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}$
8		eluzelz	$⊢ N \in ℤ_{\geq (M + 1)} \to N \in ℤ$
9	3 8	syl	$⊢ φ \to N \in ℤ$
10		eluzle	$⊢ N \in ℤ_{\geq (M + 1)} \to M + 1 \leq N$
11	3 10	syl	$⊢ φ \to M + 1 \leq N$
12	9	zred	$⊢ φ \to N \in ℝ$
13	12	leidd	$⊢ φ \to N \leq N$
14	2	peano2zd	$⊢ φ \to M + 1 \in ℤ$
15		elfz1	$⊢ (M + 1 \in ℤ \land N \in ℤ) \to (N \in (M + 1 \dots N) \leftrightarrow (N \in ℤ \land M + 1 \leq N \land N \leq N))$
16	14 9 15	syl2anc	$⊢ φ \to (N \in (M + 1 \dots N) \leftrightarrow (N \in ℤ \land M + 1 \leq N \land N \leq N))$
17	9 11 13 16	mpbir3and	$⊢ φ \to N \in (M + 1 \dots N)$
18		fveq2	$⊢ j = M + 1 \to P (j) = P (M + 1)$
19	18	oveq2d	$⊢ j = M + 1 \to [P (M), P (j)] = [P (M), P (M + 1)]$
20	19	mpteq1d	$⊢ j = M + 1 \to (t \in [P (M), P (j)] ⟼ A) = (t \in [P (M), P (M + 1)] ⟼ A)$
21	20	eleq1d	$⊢ j = M + 1 \to ((t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1} \leftrightarrow (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1})$
22	21	imbi2d	$⊢ j = M + 1 \to ((φ \to (t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1}) \leftrightarrow (φ \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1}))$
23		fveq2	$⊢ j = k \to P (j) = P (k)$
24	23	oveq2d	$⊢ j = k \to [P (M), P (j)] = [P (M), P (k)]$
25	24	mpteq1d	$⊢ j = k \to (t \in [P (M), P (j)] ⟼ A) = (t \in [P (M), P (k)] ⟼ A)$
26	25	eleq1d	$⊢ j = k \to ((t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1} \leftrightarrow (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1})$
27	26	imbi2d	$⊢ j = k \to ((φ \to (t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1}) \leftrightarrow (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}))$
28		fveq2	$⊢ j = k + 1 \to P (j) = P (k + 1)$
29	28	oveq2d	$⊢ j = k + 1 \to [P (M), P (j)] = [P (M), P (k + 1)]$
30	29	mpteq1d	$⊢ j = k + 1 \to (t \in [P (M), P (j)] ⟼ A) = (t \in [P (M), P (k + 1)] ⟼ A)$
31	30	eleq1d	$⊢ j = k + 1 \to ((t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1} \leftrightarrow (t \in [P (M), P (k + 1)] ⟼ A) \in 𝐿^{1})$
32	31	imbi2d	$⊢ j = k + 1 \to ((φ \to (t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1}) \leftrightarrow (φ \to (t \in [P (M), P (k + 1)] ⟼ A) \in 𝐿^{1}))$
33		fveq2	$⊢ j = N \to P (j) = P (N)$
34	33	oveq2d	$⊢ j = N \to [P (M), P (j)] = [P (M), P (N)]$
35	34	mpteq1d	$⊢ j = N \to (t \in [P (M), P (j)] ⟼ A) = (t \in [P (M), P (N)] ⟼ A)$
36	35	eleq1d	$⊢ j = N \to ((t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1} \leftrightarrow (t \in [P (M), P (N)] ⟼ A) \in 𝐿^{1})$
37	36	imbi2d	$⊢ j = N \to ((φ \to (t \in [P (M), P (j)] ⟼ A) \in 𝐿^{1}) \leftrightarrow (φ \to (t \in [P (M), P (N)] ⟼ A) \in 𝐿^{1}))$
38		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
39	2 38	syl	$⊢ φ \to M \in ℤ_{\geq M}$
40	2	zred	$⊢ φ \to M \in ℝ$
41		1red	$⊢ φ \to 1 \in ℝ$
42	40 41	readdcld	$⊢ φ \to M + 1 \in ℝ$
43	40	ltp1d	$⊢ φ \to M < M + 1$
44	40 42 12 43 11	ltletrd	$⊢ φ \to M < N$
45		elfzo2	$⊢ M \in (M ..^N) \leftrightarrow (M \in ℤ_{\geq M} \land N \in ℤ \land M < N)$
46	39 9 44 45	syl3anbrc	$⊢ φ \to M \in (M ..^N)$
47		fveq2	$⊢ i = M \to P (i) = P (M)$
48		fvoveq1	$⊢ i = M \to P (i + 1) = P (M + 1)$
49	47 48	oveq12d	$⊢ i = M \to [P (i), P (i + 1)] = [P (M), P (M + 1)]$
50	49	mpteq1d	$⊢ i = M \to (t \in [P (i), P (i + 1)] ⟼ A) = (t \in [P (M), P (M + 1)] ⟼ A)$
51	50	eleq1d	$⊢ i = M \to ((t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1} \leftrightarrow (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1})$
52	51	imbi2d	$⊢ i = M \to ((φ \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}) \leftrightarrow (φ \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1}))$
53	7	expcom	$⊢ i \in (M ..^N) \to (φ \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1})$
54	52 53	vtoclga	$⊢ M \in (M ..^N) \to (φ \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1})$
55	46 54	mpcom	$⊢ φ \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1}$
56	55	a1i	$⊢ N \in ℤ_{\geq (M + 1)} \to (φ \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1})$
57		nfv	$⊢ Ⅎ t k \in (M + 1 ..^N)$
58		nfmpt1	$⊢ \underline{Ⅎ} t (t \in [P (M), P (k)] ⟼ A)$
59	58	nfel1	$⊢ Ⅎ t (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}$
60	1 59	nfim	$⊢ Ⅎ t (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1})$
61	57 60 1	nf3an	$⊢ Ⅎ t (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ)$
62		simp3	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to φ$
63		simp1	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to k \in (M + 1 ..^N)$
64	40	leidd	$⊢ φ \to M \leq M$
65	40 12 44	ltled	$⊢ φ \to M \leq N$
66		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (M \in (M \dots N) \leftrightarrow (M \in ℤ \land M \leq M \land M \leq N))$
67	2 9 66	syl2anc	$⊢ φ \to (M \in (M \dots N) \leftrightarrow (M \in ℤ \land M \leq M \land M \leq N))$
68	2 64 65 67	mpbir3and	$⊢ φ \to M \in (M \dots N)$
69	68	ancli	$⊢ φ \to (φ \land M \in (M \dots N))$
70		eleq1	$⊢ i = M \to (i \in (M \dots N) \leftrightarrow M \in (M \dots N))$
71	70	anbi2d	$⊢ i = M \to ((φ \land i \in (M \dots N)) \leftrightarrow (φ \land M \in (M \dots N)))$
72	47	eleq1d	$⊢ i = M \to (P (i) \in ℝ \leftrightarrow P (M) \in ℝ)$
73	71 72	imbi12d	$⊢ i = M \to (((φ \land i \in (M \dots N)) \to P (i) \in ℝ) \leftrightarrow ((φ \land M \in (M \dots N)) \to P (M) \in ℝ))$
74	73 4	vtoclg	$⊢ M \in (M \dots N) \to ((φ \land M \in (M \dots N)) \to P (M) \in ℝ)$
75	68 69 74	sylc	$⊢ φ \to P (M) \in ℝ$
76	75	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (M) \in ℝ$
77	76	rexrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (M) \in ℝ^{*}$
78		simpl	$⊢ (φ \land k \in (M + 1 ..^N)) \to φ$
79		elfzoelz	$⊢ k \in (M + 1 ..^N) \to k \in ℤ$
80	79	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℤ$
81	40	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \in ℝ$
82	80	zred	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℝ$
83	42	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M + 1 \in ℝ$
84	43	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M < M + 1$
85		elfzole1	$⊢ k \in (M + 1 ..^N) \to M + 1 \leq k$
86	85	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to M + 1 \leq k$
87	81 83 82 84 86	ltletrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to M < k$
88	81 82 87	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \leq k$
89	12	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℝ$
90		elfzolt2	$⊢ k \in (M + 1 ..^N) \to k < N$
91	90	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to k < N$
92	82 89 91	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \leq N$
93	2 9	jca	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
94	93	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to (M \in ℤ \land N \in ℤ)$
95		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (k \in (M \dots N) \leftrightarrow (k \in ℤ \land M \leq k \land k \leq N))$
96	94 95	syl	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k \in (M \dots N) \leftrightarrow (k \in ℤ \land M \leq k \land k \leq N))$
97	80 88 92 96	mpbir3and	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in (M \dots N)$
98		eleq1	$⊢ i = k \to (i \in (M \dots N) \leftrightarrow k \in (M \dots N))$
99	98	anbi2d	$⊢ i = k \to ((φ \land i \in (M \dots N)) \leftrightarrow (φ \land k \in (M \dots N)))$
100		fveq2	$⊢ i = k \to P (i) = P (k)$
101	100	eleq1d	$⊢ i = k \to (P (i) \in ℝ \leftrightarrow P (k) \in ℝ)$
102	99 101	imbi12d	$⊢ i = k \to (((φ \land i \in (M \dots N)) \to P (i) \in ℝ) \leftrightarrow ((φ \land k \in (M \dots N)) \to P (k) \in ℝ))$
103	102 4	chvarvv	$⊢ (φ \land k \in (M \dots N)) \to P (k) \in ℝ$
104	78 97 103	syl2anc	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \in ℝ$
105	104	rexrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \in ℝ^{*}$
106	80	peano2zd	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \in ℤ$
107	106	zred	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \in ℝ$
108		1red	$⊢ (φ \land k \in (M + 1 ..^N)) \to 1 \in ℝ$
109	81 82 108 87	ltadd1dd	$⊢ (φ \land k \in (M + 1 ..^N)) \to M + 1 < k + 1$
110	81 83 107 84 109	lttrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to M < k + 1$
111	81 107 110	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \leq k + 1$
112		zltp1le	$⊢ (k \in ℤ \land N \in ℤ) \to (k < N \leftrightarrow k + 1 \leq N)$
113	79 9 112	syl2anr	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k < N \leftrightarrow k + 1 \leq N)$
114	91 113	mpbid	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \leq N$
115		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (k + 1 \in (M \dots N) \leftrightarrow (k + 1 \in ℤ \land M \leq k + 1 \land k + 1 \leq N))$
116	94 115	syl	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k + 1 \in (M \dots N) \leftrightarrow (k + 1 \in ℤ \land M \leq k + 1 \land k + 1 \leq N))$
117	106 111 114 116	mpbir3and	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \in (M \dots N)$
118	78 117	jca	$⊢ (φ \land k \in (M + 1 ..^N)) \to (φ \land k + 1 \in (M \dots N))$
119		eleq1	$⊢ i = k + 1 \to (i \in (M \dots N) \leftrightarrow k + 1 \in (M \dots N))$
120	119	anbi2d	$⊢ i = k + 1 \to ((φ \land i \in (M \dots N)) \leftrightarrow (φ \land k + 1 \in (M \dots N)))$
121		fveq2	$⊢ i = k + 1 \to P (i) = P (k + 1)$
122	121	eleq1d	$⊢ i = k + 1 \to (P (i) \in ℝ \leftrightarrow P (k + 1) \in ℝ)$
123	120 122	imbi12d	$⊢ i = k + 1 \to (((φ \land i \in (M \dots N)) \to P (i) \in ℝ) \leftrightarrow ((φ \land k + 1 \in (M \dots N)) \to P (k + 1) \in ℝ))$
124	123 4	vtoclg	$⊢ k + 1 \in (M \dots N) \to ((φ \land k + 1 \in (M \dots N)) \to P (k + 1) \in ℝ)$
125	117 118 124	sylc	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k + 1) \in ℝ$
126	125	rexrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k + 1) \in ℝ^{*}$
127		eluz	$⊢ (M \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq M} \leftrightarrow M \leq k)$
128	2 79 127	syl2an	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k \in ℤ_{\geq M} \leftrightarrow M \leq k)$
129	88 128	mpbird	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℤ_{\geq M}$
130		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to φ$
131		elfzelz	$⊢ i \in (M \dots k) \to i \in ℤ$
132	131	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in ℤ$
133		elfzle1	$⊢ i \in (M \dots k) \to M \leq i$
134	133	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to M \leq i$
135	132	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in ℝ$
136	130 12	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to N \in ℝ$
137	82	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to k \in ℝ$
138		elfzle2	$⊢ i \in (M \dots k) \to i \leq k$
139	138	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \leq k$
140	91	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to k < N$
141	135 137 136 139 140	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i < N$
142	135 136 141	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \leq N$
143		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
144	130 93 143	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
145	132 134 142 144	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in (M \dots N)$
146	130 145 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to P (i) \in ℝ$
147		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to φ$
148		elfzelz	$⊢ i \in (M \dots k - 1) \to i \in ℤ$
149	148	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in ℤ$
150		elfzle1	$⊢ i \in (M \dots k - 1) \to M \leq i$
151	150	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to M \leq i$
152	149	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in ℝ$
153	147 12	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to N \in ℝ$
154	82	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k \in ℝ$
155		1red	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to 1 \in ℝ$
156	154 155	resubcld	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k - 1 \in ℝ$
157		elfzle2	$⊢ i \in (M \dots k - 1) \to i \leq k - 1$
158	157	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \leq k - 1$
159	79	zred	$⊢ k \in (M + 1 ..^N) \to k \in ℝ$
160		1red	$⊢ k \in (M + 1 ..^N) \to 1 \in ℝ$
161	159 160	resubcld	$⊢ k \in (M + 1 ..^N) \to k - 1 \in ℝ$
162		elfzoel2	$⊢ k \in (M + 1 ..^N) \to N \in ℤ$
163	162	zred	$⊢ k \in (M + 1 ..^N) \to N \in ℝ$
164	159	ltm1d	$⊢ k \in (M + 1 ..^N) \to k - 1 < k$
165	161 159 163 164 90	lttrd	$⊢ k \in (M + 1 ..^N) \to k - 1 < N$
166	165	ad2antlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k - 1 < N$
167	152 156 153 158 166	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i < N$
168	152 153 167	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \leq N$
169	147 93 143	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
170	149 151 168 169	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in (M \dots N)$
171	147 170 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i) \in ℝ$
172	149	peano2zd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \in ℤ$
173		elfzel1	$⊢ i \in (M \dots k - 1) \to M \in ℤ$
174	173	zred	$⊢ i \in (M \dots k - 1) \to M \in ℝ$
175	148	zred	$⊢ i \in (M \dots k - 1) \to i \in ℝ$
176		1red	$⊢ i \in (M \dots k - 1) \to 1 \in ℝ$
177	175 176	readdcld	$⊢ i \in (M \dots k - 1) \to i + 1 \in ℝ$
178	175	ltp1d	$⊢ i \in (M \dots k - 1) \to i < i + 1$
179	174 175 177 150 178	lelttrd	$⊢ i \in (M \dots k - 1) \to M < i + 1$
180	174 177 179	ltled	$⊢ i \in (M \dots k - 1) \to M \leq i + 1$
181	180	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to M \leq i + 1$
182	147 3 8	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to N \in ℤ$
183		zltp1le	$⊢ (i \in ℤ \land N \in ℤ) \to (i < N \leftrightarrow i + 1 \leq N)$
184	149 182 183	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to (i < N \leftrightarrow i + 1 \leq N)$
185	167 184	mpbid	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \leq N$
186		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (i + 1 \in (M \dots N) \leftrightarrow (i + 1 \in ℤ \land M \leq i + 1 \land i + 1 \leq N))$
187	147 93 186	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to (i + 1 \in (M \dots N) \leftrightarrow (i + 1 \in ℤ \land M \leq i + 1 \land i + 1 \leq N))$
188	172 181 185 187	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \in (M \dots N)$
189	147 188	jca	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to (φ \land i + 1 \in (M \dots N))$
190		eleq1	$⊢ k = i + 1 \to (k \in (M \dots N) \leftrightarrow i + 1 \in (M \dots N))$
191	190	anbi2d	$⊢ k = i + 1 \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land i + 1 \in (M \dots N)))$
192		fveq2	$⊢ k = i + 1 \to P (k) = P (i + 1)$
193	192	eleq1d	$⊢ k = i + 1 \to (P (k) \in ℝ \leftrightarrow P (i + 1) \in ℝ)$
194	191 193	imbi12d	$⊢ k = i + 1 \to (((φ \land k \in (M \dots N)) \to P (k) \in ℝ) \leftrightarrow ((φ \land i + 1 \in (M \dots N)) \to P (i + 1) \in ℝ))$
195	194 103	vtoclg	$⊢ i + 1 \in (M \dots N) \to ((φ \land i + 1 \in (M \dots N)) \to P (i + 1) \in ℝ)$
196	188 189 195	sylc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i + 1) \in ℝ$
197		elfzuz	$⊢ i \in (M \dots k - 1) \to i \in ℤ_{\geq M}$
198	197	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in ℤ_{\geq M}$
199		elfzo2	$⊢ i \in (M ..^N) \leftrightarrow (i \in ℤ_{\geq M} \land N \in ℤ \land i < N)$
200	198 182 167 199	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in (M ..^N)$
201	147 200 5	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i) < P (i + 1)$
202	171 196 201	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i) \leq P (i + 1)$
203	129 146 202	monoord	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (M) \leq P (k)$
204	162	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℤ$
205		elfzo2	$⊢ k \in (M ..^N) \leftrightarrow (k \in ℤ_{\geq M} \land N \in ℤ \land k < N)$
206	129 204 91 205	syl3anbrc	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in (M ..^N)$
207		eleq1	$⊢ i = k \to (i \in (M ..^N) \leftrightarrow k \in (M ..^N))$
208	207	anbi2d	$⊢ i = k \to ((φ \land i \in (M ..^N)) \leftrightarrow (φ \land k \in (M ..^N)))$
209		fvoveq1	$⊢ i = k \to P (i + 1) = P (k + 1)$
210	100 209	breq12d	$⊢ i = k \to (P (i) < P (i + 1) \leftrightarrow P (k) < P (k + 1))$
211	208 210	imbi12d	$⊢ i = k \to (((φ \land i \in (M ..^N)) \to P (i) < P (i + 1)) \leftrightarrow ((φ \land k \in (M ..^N)) \to P (k) < P (k + 1)))$
212	211 5	chvarvv	$⊢ (φ \land k \in (M ..^N)) \to P (k) < P (k + 1)$
213	78 206 212	syl2anc	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) < P (k + 1)$
214	104 125 213	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \leq P (k + 1)$
215		iccintsng	$⊢ ((P (M) \in ℝ^{} \land P (k) \in ℝ^{} \land P (k + 1) \in ℝ^{*}) \land (P (M) \leq P (k) \land P (k) \leq P (k + 1))) \to [P (M), P (k)] \cap [P (k), P (k + 1)] = \{P (k)\}$
216	77 105 126 203 214 215	syl32anc	$⊢ (φ \land k \in (M + 1 ..^N)) \to [P (M), P (k)] \cap [P (k), P (k + 1)] = \{P (k)\}$
217	216	fveq2d	$⊢ (φ \land k \in (M + 1 ..^N)) \to {vol}^{} ([P (M), P (k)] \cap [P (k), P (k + 1)]) = {vol}^{} (\{P (k)\})$
218		ovolsn	$⊢ P (k) \in ℝ \to {vol}^{*} (\{P (k)\}) = 0$
219	104 218	syl	$⊢ (φ \land k \in (M + 1 ..^N)) \to {vol}^{*} (\{P (k)\}) = 0$
220	217 219	eqtrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to {vol}^{*} ([P (M), P (k)] \cap [P (k), P (k + 1)]) = 0$
221	62 63 220	syl2anc	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to {vol}^{*} ([P (M), P (k)] \cap [P (k), P (k + 1)]) = 0$
222	76 125 104 203 214	eliccd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \in [P (M), P (k + 1)]$
223	76 125 222	3jca	$⊢ (φ \land k \in (M + 1 ..^N)) \to (P (M) \in ℝ \land P (k + 1) \in ℝ \land P (k) \in [P (M), P (k + 1)])$
224	62 63 223	syl2anc	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to (P (M) \in ℝ \land P (k + 1) \in ℝ \land P (k) \in [P (M), P (k + 1)])$
225		iccsplit	$⊢ (P (M) \in ℝ \land P (k + 1) \in ℝ \land P (k) \in [P (M), P (k + 1)]) \to [P (M), P (k + 1)] = [P (M), P (k)] \cup [P (k), P (k + 1)]$
226	224 225	syl	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to [P (M), P (k + 1)] = [P (M), P (k)] \cup [P (k), P (k + 1)]$
227		simpl3	$⊢ ((k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \land t \in [P (M), P (k + 1)]) \to φ$
228		simpl1	$⊢ ((k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \land t \in [P (M), P (k + 1)]) \to k \in (M + 1 ..^N)$
229		simpr	$⊢ ((k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \land t \in [P (M), P (k + 1)]) \to t \in [P (M), P (k + 1)]$
230		simp1	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to φ$
231		eliccxr	$⊢ t \in [P (M), P (k + 1)] \to t \in ℝ^{*}$
232	231	3ad2ant3	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to t \in ℝ^{*}$
233	75	rexrd	$⊢ φ \to P (M) \in ℝ^{*}$
234	233	3ad2ant1	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (M) \in ℝ^{*}$
235	126	3adant3	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (k + 1) \in ℝ^{*}$
236		simp3	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to t \in [P (M), P (k + 1)]$
237		iccgelb	$⊢ (P (M) \in ℝ^{} \land P (k + 1) \in ℝ^{} \land t \in [P (M), P (k + 1)]) \to P (M) \leq t$
238	234 235 236 237	syl3anc	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (M) \leq t$
239	76 125	jca	$⊢ (φ \land k \in (M + 1 ..^N)) \to (P (M) \in ℝ \land P (k + 1) \in ℝ)$
240	239	3adant3	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to (P (M) \in ℝ \land P (k + 1) \in ℝ)$
241		iccssre	$⊢ (P (M) \in ℝ \land P (k + 1) \in ℝ) \to [P (M), P (k + 1)] \subseteq ℝ$
242	241	sseld	$⊢ (P (M) \in ℝ \land P (k + 1) \in ℝ) \to (t \in [P (M), P (k + 1)] \to t \in ℝ)$
243	240 236 242	sylc	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to t \in ℝ$
244	125	3adant3	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (k + 1) \in ℝ$
245		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in (M \dots N) \leftrightarrow (N \in ℤ \land M \leq N \land N \leq N))$
246	2 9 245	syl2anc	$⊢ φ \to (N \in (M \dots N) \leftrightarrow (N \in ℤ \land M \leq N \land N \leq N))$
247	9 65 13 246	mpbir3and	$⊢ φ \to N \in (M \dots N)$
248	247	ancli	$⊢ φ \to (φ \land N \in (M \dots N))$
249		eleq1	$⊢ i = N \to (i \in (M \dots N) \leftrightarrow N \in (M \dots N))$
250	249	anbi2d	$⊢ i = N \to ((φ \land i \in (M \dots N)) \leftrightarrow (φ \land N \in (M \dots N)))$
251		fveq2	$⊢ i = N \to P (i) = P (N)$
252	251	eleq1d	$⊢ i = N \to (P (i) \in ℝ \leftrightarrow P (N) \in ℝ)$
253	250 252	imbi12d	$⊢ i = N \to (((φ \land i \in (M \dots N)) \to P (i) \in ℝ) \leftrightarrow ((φ \land N \in (M \dots N)) \to P (N) \in ℝ))$
254	253 4	vtoclg	$⊢ N \in ℤ \to ((φ \land N \in (M \dots N)) \to P (N) \in ℝ)$
255	9 248 254	sylc	$⊢ φ \to P (N) \in ℝ$
256	255	3ad2ant1	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (N) \in ℝ$
257		elicc1	$⊢ (P (M) \in ℝ^{} \land P (k + 1) \in ℝ^{}) \to (t \in [P (M), P (k + 1)] \leftrightarrow (t \in ℝ^{*} \land P (M) \leq t \land t \leq P (k + 1)))$
258	234 235 257	syl2anc	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to (t \in [P (M), P (k + 1)] \leftrightarrow (t \in ℝ^{*} \land P (M) \leq t \land t \leq P (k + 1)))$
259	236 258	mpbid	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to (t \in ℝ^{*} \land P (M) \leq t \land t \leq P (k + 1))$
260	259	simp3d	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to t \leq P (k + 1)$
261		elfzop1le2	$⊢ k \in (M + 1 ..^N) \to k + 1 \leq N$
262	79	peano2zd	$⊢ k \in (M + 1 ..^N) \to k + 1 \in ℤ$
263		eluz	$⊢ (k + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (k + 1)} \leftrightarrow k + 1 \leq N)$
264	262 162 263	syl2anc	$⊢ k \in (M + 1 ..^N) \to (N \in ℤ_{\geq (k + 1)} \leftrightarrow k + 1 \leq N)$
265	261 264	mpbird	$⊢ k \in (M + 1 ..^N) \to N \in ℤ_{\geq (k + 1)}$
266	265	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℤ_{\geq (k + 1)}$
267		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to φ$
268		elfzelz	$⊢ i \in (k + 1 \dots N) \to i \in ℤ$
269	268	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \in ℤ$
270	267 40	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M \in ℝ$
271	269	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \in ℝ$
272	82	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to k \in ℝ$
273	87	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M < k$
274	159	adantr	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k \in ℝ$
275		1red	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to 1 \in ℝ$
276	274 275	readdcld	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k + 1 \in ℝ$
277	268	zred	$⊢ i \in (k + 1 \dots N) \to i \in ℝ$
278	277	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to i \in ℝ$
279	274	ltp1d	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k < k + 1$
280		elfzle1	$⊢ i \in (k + 1 \dots N) \to k + 1 \leq i$
281	280	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k + 1 \leq i$
282	274 276 278 279 281	ltletrd	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k < i$
283	282	adantll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to k < i$
284	270 272 271 273 283	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M < i$
285	270 271 284	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M \leq i$
286		elfzle2	$⊢ i \in (k + 1 \dots N) \to i \leq N$
287	286	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \leq N$
288	267 93 143	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
289	269 285 287 288	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \in (M \dots N)$
290	267 289 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to P (i) \in ℝ$
291		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to φ$
292		elfzelz	$⊢ i \in (k + 1 \dots N - 1) \to i \in ℤ$
293	292	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in ℤ$
294	291 40	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \in ℝ$
295	293	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in ℝ$
296	82	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to k \in ℝ$
297	87	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M < k$
298	159	adantr	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k \in ℝ$
299		1red	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to 1 \in ℝ$
300	298 299	readdcld	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k + 1 \in ℝ$
301	292	zred	$⊢ i \in (k + 1 \dots N - 1) \to i \in ℝ$
302	301	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to i \in ℝ$
303	298	ltp1d	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k < k + 1$
304		elfzle1	$⊢ i \in (k + 1 \dots N - 1) \to k + 1 \leq i$
305	304	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k + 1 \leq i$
306	298 300 302 303 305	ltletrd	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k < i$
307	306	adantll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to k < i$
308	294 296 295 297 307	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M < i$
309	294 295 308	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \leq i$
310	301	adantl	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i \in ℝ$
311	12	adantr	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to N \in ℝ$
312		1red	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to 1 \in ℝ$
313	311 312	resubcld	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to N - 1 \in ℝ$
314		elfzle2	$⊢ i \in (k + 1 \dots N - 1) \to i \leq N - 1$
315	314	adantl	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i \leq N - 1$
316	311	ltm1d	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to N - 1 < N$
317	310 313 311 315 316	lelttrd	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i < N$
318	310 311 317	ltled	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i \leq N$
319	318	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \leq N$
320	291 93 143	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
321	293 309 319 320	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in (M \dots N)$
322	291 321 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i) \in ℝ$
323	293	peano2zd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in ℤ$
324	323	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in ℝ$
325	302 299	readdcld	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in ℝ$
326	298 302 306	ltled	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k \leq i$
327	298 302 299 326	leadd1dd	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k + 1 \leq i + 1$
328	298 300 325 303 327	ltletrd	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k < i + 1$
329	328	adantll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to k < i + 1$
330	294 296 324 297 329	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M < i + 1$
331	294 324 330	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \leq i + 1$
332	292 9 183	syl2anr	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to (i < N \leftrightarrow i + 1 \leq N)$
333	317 332	mpbid	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i + 1 \leq N$
334	333	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \leq N$
335	291 93 186	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to (i + 1 \in (M \dots N) \leftrightarrow (i + 1 \in ℤ \land M \leq i + 1 \land i + 1 \leq N))$
336	323 331 334 335	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in (M \dots N)$
337	291 336	jca	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to (φ \land i + 1 \in (M \dots N))$
338	336 337 195	sylc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i + 1) \in ℝ$
339	291 2	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \in ℤ$
340		eluz	$⊢ (M \in ℤ \land i \in ℤ) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
341	339 293 340	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
342	309 341	mpbird	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in ℤ_{\geq M}$
343	291 3 8	3syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to N \in ℤ$
344	317	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i < N$
345	342 343 344 199	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in (M ..^N)$
346	291 345 5	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i) < P (i + 1)$
347	322 338 346	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i) \leq P (i + 1)$
348	266 290 347	monoord	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k + 1) \leq P (N)$
349	348	3adant3	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (k + 1) \leq P (N)$
350	243 244 256 260 349	letrd	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to t \leq P (N)$
351	256	rexrd	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to P (N) \in ℝ^{*}$
352		elicc1	$⊢ (P (M) \in ℝ^{} \land P (N) \in ℝ^{}) \to (t \in [P (M), P (N)] \leftrightarrow (t \in ℝ^{*} \land P (M) \leq t \land t \leq P (N)))$
353	234 351 352	syl2anc	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to (t \in [P (M), P (N)] \leftrightarrow (t \in ℝ^{*} \land P (M) \leq t \land t \leq P (N)))$
354	232 238 350 353	mpbir3and	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to t \in [P (M), P (N)]$
355	230 354 6	syl2anc	$⊢ (φ \land k \in (M + 1 ..^N) \land t \in [P (M), P (k + 1)]) \to A \in ℂ$
356	227 228 229 355	syl3anc	$⊢ ((k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \land t \in [P (M), P (k + 1)]) \to A \in ℂ$
357		simp2	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1})$
358	62 357	mpd	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}$
359	62 63	jca	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to (φ \land k \in (M + 1 ..^N))$
360	78 206	jca	$⊢ (φ \land k \in (M + 1 ..^N)) \to (φ \land k \in (M ..^N))$
361	100 209	oveq12d	$⊢ i = k \to [P (i), P (i + 1)] = [P (k), P (k + 1)]$
362	361	mpteq1d	$⊢ i = k \to (t \in [P (i), P (i + 1)] ⟼ A) = (t \in [P (k), P (k + 1)] ⟼ A)$
363	362	eleq1d	$⊢ i = k \to ((t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1} \leftrightarrow (t \in [P (k), P (k + 1)] ⟼ A) \in 𝐿^{1})$
364	208 363	imbi12d	$⊢ i = k \to (((φ \land i \in (M ..^N)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}) \leftrightarrow ((φ \land k \in (M ..^N)) \to (t \in [P (k), P (k + 1)] ⟼ A) \in 𝐿^{1}))$
365	364 7	chvarvv	$⊢ (φ \land k \in (M ..^N)) \to (t \in [P (k), P (k + 1)] ⟼ A) \in 𝐿^{1}$
366	359 360 365	3syl	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to (t \in [P (k), P (k + 1)] ⟼ A) \in 𝐿^{1}$
367	61 221 226 356 358 366	iblsplitf	$⊢ (k \in (M + 1 ..^N) \land (φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \land φ) \to (t \in [P (M), P (k + 1)] ⟼ A) \in 𝐿^{1}$
368	367	3exp	$⊢ k \in (M + 1 ..^N) \to ((φ \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}) \to (φ \to (t \in [P (M), P (k + 1)] ⟼ A) \in 𝐿^{1}))$
369	22 27 32 37 56 368	fzind2	$⊢ N \in (M + 1 \dots N) \to (φ \to (t \in [P (M), P (N)] ⟼ A) \in 𝐿^{1})$
370	17 369	mpcom	$⊢ φ \to (t \in [P (M), P (N)] ⟼ A) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem iblspltprt

Proof