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

Metamath Proof Explorer

Theorem iblspltprt

Proof