itgspltprt

Description: The S. integral splits on a given partition P . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		itgspltprt.1	$⊢ φ \to M \in ℤ$
2		itgspltprt.2	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
3		itgspltprt.3	$⊢ φ \to P : (M \dots N) ⟶ ℝ$
4		itgspltprt.4	$⊢ (φ \land i \in (M ..^N)) \to P (i) < P (i + 1)$
5		itgspltprt.5	$⊢ (φ \land t \in [P (M), P (N)]) \to A \in ℂ$
6		itgspltprt.6	$⊢ (φ \land i \in (M ..^N)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}$
7	1	peano2zd	$⊢ φ \to M + 1 \in ℤ$
8		eluzelz	$⊢ N \in ℤ_{\geq (M + 1)} \to N \in ℤ$
9	2 8	syl	$⊢ φ \to N \in ℤ$
10		eluzle	$⊢ N \in ℤ_{\geq (M + 1)} \to M + 1 \leq N$
11	2 10	syl	$⊢ φ \to M + 1 \leq N$
12		eluzelre	$⊢ N \in ℤ_{\geq (M + 1)} \to N \in ℝ$
13	2 12	syl	$⊢ φ \to N \in ℝ$
14	13	leidd	$⊢ φ \to N \leq N$
15	7 9 9 11 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	itgeq1d	$⊢ j = M + 1 \to \int_{[P (M), P (j)]} A d t = \int_{[P (M), P (M + 1)]} A d t$
19		oveq2	$⊢ j = M + 1 \to (M ..^j) = (M ..^M + 1)$
20	19	sumeq1d	$⊢ j = M + 1 \to \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i \in (M ..^M + 1)} \int_{[P (i), P (i + 1)]} A d t$
21	18 20	eqeq12d	$⊢ j = M + 1 \to (\int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t \leftrightarrow \int_{[P (M), P (M + 1)]} A d t = \sum_{i \in (M ..^M + 1)} \int_{[P (i), P (i + 1)]} A d t)$
22	21	imbi2d	$⊢ j = M + 1 \to ((φ \to \int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t) \leftrightarrow (φ \to \int_{[P (M), P (M + 1)]} A d t = \sum_{i \in (M ..^M + 1)} \int_{[P (i), P (i + 1)]} A d t))$
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	itgeq1d	$⊢ j = k \to \int_{[P (M), P (j)]} A d t = \int_{[P (M), P (k)]} A d t$
26		oveq2	$⊢ j = k \to (M ..^j) = (M ..^k)$
27	26	sumeq1d	$⊢ j = k \to \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t$
28	25 27	eqeq12d	$⊢ j = k \to (\int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t \leftrightarrow \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t)$
29	28	imbi2d	$⊢ j = k \to ((φ \to \int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t) \leftrightarrow (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t))$
30		fveq2	$⊢ j = k + 1 \to P (j) = P (k + 1)$
31	30	oveq2d	$⊢ j = k + 1 \to [P (M), P (j)] = [P (M), P (k + 1)]$
32	31	itgeq1d	$⊢ j = k + 1 \to \int_{[P (M), P (j)]} A d t = \int_{[P (M), P (k + 1)]} A d t$
33		oveq2	$⊢ j = k + 1 \to (M ..^j) = (M ..^k + 1)$
34	33	sumeq1d	$⊢ j = k + 1 \to \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t$
35	32 34	eqeq12d	$⊢ j = k + 1 \to (\int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t \leftrightarrow \int_{[P (M), P (k + 1)]} A d t = \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t)$
36	35	imbi2d	$⊢ j = k + 1 \to ((φ \to \int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t) \leftrightarrow (φ \to \int_{[P (M), P (k + 1)]} A d t = \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t))$
37		fveq2	$⊢ j = N \to P (j) = P (N)$
38	37	oveq2d	$⊢ j = N \to [P (M), P (j)] = [P (M), P (N)]$
39	38	itgeq1d	$⊢ j = N \to \int_{[P (M), P (j)]} A d t = \int_{[P (M), P (N)]} A d t$
40		oveq2	$⊢ j = N \to (M ..^j) = (M ..^N)$
41	40	sumeq1d	$⊢ j = N \to \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i \in (M ..^N)} \int_{[P (i), P (i + 1)]} A d t$
42	39 41	eqeq12d	$⊢ j = N \to (\int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t \leftrightarrow \int_{[P (M), P (N)]} A d t = \sum_{i \in (M ..^N)} \int_{[P (i), P (i + 1)]} A d t)$
43	42	imbi2d	$⊢ j = N \to ((φ \to \int_{[P (M), P (j)]} A d t = \sum_{i \in (M ..^j)} \int_{[P (i), P (i + 1)]} A d t) \leftrightarrow (φ \to \int_{[P (M), P (N)]} A d t = \sum_{i \in (M ..^N)} \int_{[P (i), P (i + 1)]} A d t))$
44	1	adantl	$⊢ (N \in ℤ_{\geq (M + 1)} \land φ) \to M \in ℤ$
45		fzval3	$⊢ M \in ℤ \to (M \dots M) = (M ..^M + 1)$
46	44 45	syl	$⊢ (N \in ℤ_{\geq (M + 1)} \land φ) \to (M \dots M) = (M ..^M + 1)$
47	46	eqcomd	$⊢ (N \in ℤ_{\geq (M + 1)} \land φ) \to (M ..^M + 1) = (M \dots M)$
48	47	sumeq1d	$⊢ (N \in ℤ_{\geq (M + 1)} \land φ) \to \sum_{i \in (M ..^M + 1)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i = M}^{M} \int_{[P (i), P (i + 1)]} A d t$
49	3	adantr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P : (M \dots N) ⟶ ℝ$
50	1	zred	$⊢ φ \to M \in ℝ$
51		1red	$⊢ φ \to 1 \in ℝ$
52	50 51	readdcld	$⊢ φ \to M + 1 \in ℝ$
53	50	ltp1d	$⊢ φ \to M < M + 1$
54	50 52 13 53 11	ltletrd	$⊢ φ \to M < N$
55	50 13 54	ltled	$⊢ φ \to M \leq N$
56		eluz	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
57	1 9 56	syl2anc	$⊢ φ \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
58	55 57	mpbird	$⊢ φ \to N \in ℤ_{\geq M}$
59		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
60	58 59	syl	$⊢ φ \to M \in (M \dots N)$
61	60	adantr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to M \in (M \dots N)$
62	49 61	ffvelrnd	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (M) \in ℝ$
63	1 9 9 55 14	elfzd	$⊢ φ \to N \in (M \dots N)$
64	3 63	ffvelrnd	$⊢ φ \to P (N) \in ℝ$
65	64	adantr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (N) \in ℝ$
66	50	lep1d	$⊢ φ \to M \leq M + 1$
67	1 9 7 66 11	elfzd	$⊢ φ \to M + 1 \in (M \dots N)$
68	3 67	ffvelrnd	$⊢ φ \to P (M + 1) \in ℝ$
69	68	adantr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (M + 1) \in ℝ$
70		simpr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to t \in [P (M), P (M + 1)]$
71		eliccre	$⊢ (P (M) \in ℝ \land P (M + 1) \in ℝ \land t \in [P (M), P (M + 1)]) \to t \in ℝ$
72	62 69 70 71	syl3anc	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to t \in ℝ$
73	3 60	ffvelrnd	$⊢ φ \to P (M) \in ℝ$
74	73	rexrd	$⊢ φ \to P (M) \in ℝ^{*}$
75	74	adantr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (M) \in ℝ^{*}$
76	69	rexrd	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (M + 1) \in ℝ^{*}$
77		iccgelb	$⊢ (P (M) \in ℝ^{} \land P (M + 1) \in ℝ^{} \land t \in [P (M), P (M + 1)]) \to P (M) \leq t$
78	75 76 70 77	syl3anc	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (M) \leq t$
79		iccleub	$⊢ (P (M) \in ℝ^{} \land P (M + 1) \in ℝ^{} \land t \in [P (M), P (M + 1)]) \to t \leq P (M + 1)$
80	75 76 70 79	syl3anc	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to t \leq P (M + 1)$
81	3	adantr	$⊢ (φ \land i \in (M + 1 \dots N)) \to P : (M \dots N) ⟶ ℝ$
82		elfzelz	$⊢ i \in (M + 1 \dots N) \to i \in ℤ$
83	82	adantl	$⊢ (φ \land i \in (M + 1 \dots N)) \to i \in ℤ$
84	50	adantr	$⊢ (φ \land i \in (M + 1 \dots N)) \to M \in ℝ$
85	83	zred	$⊢ (φ \land i \in (M + 1 \dots N)) \to i \in ℝ$
86	52	adantr	$⊢ (φ \land i \in (M + 1 \dots N)) \to M + 1 \in ℝ$
87	53	adantr	$⊢ (φ \land i \in (M + 1 \dots N)) \to M < M + 1$
88		elfzle1	$⊢ i \in (M + 1 \dots N) \to M + 1 \leq i$
89	88	adantl	$⊢ (φ \land i \in (M + 1 \dots N)) \to M + 1 \leq i$
90	84 86 85 87 89	ltletrd	$⊢ (φ \land i \in (M + 1 \dots N)) \to M < i$
91	84 85 90	ltled	$⊢ (φ \land i \in (M + 1 \dots N)) \to M \leq i$
92		elfzle2	$⊢ i \in (M + 1 \dots N) \to i \leq N$
93	92	adantl	$⊢ (φ \land i \in (M + 1 \dots N)) \to i \leq N$
94	1 9	jca	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
95	94	adantr	$⊢ (φ \land i \in (M + 1 \dots N)) \to (M \in ℤ \land N \in ℤ)$
96		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
97	95 96	syl	$⊢ (φ \land i \in (M + 1 \dots N)) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
98	83 91 93 97	mpbir3and	$⊢ (φ \land i \in (M + 1 \dots N)) \to i \in (M \dots N)$
99	81 98	ffvelrnd	$⊢ (φ \land i \in (M + 1 \dots N)) \to P (i) \in ℝ$
100	3	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to P : (M \dots N) ⟶ ℝ$
101		elfzelz	$⊢ i \in (M + 1 \dots N - 1) \to i \in ℤ$
102	101	adantl	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \in ℤ$
103	50	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M \in ℝ$
104	102	zred	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \in ℝ$
105	52	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M + 1 \in ℝ$
106	53	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M < M + 1$
107		elfzle1	$⊢ i \in (M + 1 \dots N - 1) \to M + 1 \leq i$
108	107	adantl	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M + 1 \leq i$
109	103 105 104 106 108	ltletrd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M < i$
110	103 104 109	ltled	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M \leq i$
111	13	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to N \in ℝ$
112		1red	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to 1 \in ℝ$
113	111 112	resubcld	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to N - 1 \in ℝ$
114		elfzle2	$⊢ i \in (M + 1 \dots N - 1) \to i \leq N - 1$
115	114	adantl	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \leq N - 1$
116	111	ltm1d	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to N - 1 < N$
117	104 113 111 115 116	lelttrd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i < N$
118	104 111 117	ltled	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \leq N$
119	94	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to (M \in ℤ \land N \in ℤ)$
120	119 96	syl	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to (i \in (M \dots N) \leftrightarrow (i \in ℤ \land M \leq i \land i \leq N))$
121	102 110 118 120	mpbir3and	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \in (M \dots N)$
122	100 121	ffvelrnd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to P (i) \in ℝ$
123	102	peano2zd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i + 1 \in ℤ$
124	104 112	readdcld	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i + 1 \in ℝ$
125	103 104 112 109	ltadd1dd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M + 1 < i + 1$
126	103 105 124 106 125	lttrd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M < i + 1$
127	103 124 126	ltled	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to M \leq i + 1$
128		zltp1le	$⊢ (i \in ℤ \land N \in ℤ) \to (i < N \leftrightarrow i + 1 \leq N)$
129	101 9 128	syl2anr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to (i < N \leftrightarrow i + 1 \leq N)$
130	117 129	mpbid	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i + 1 \leq N$
131		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))$
132	119 131	syl	$⊢ (φ \land i \in (M + 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))$
133	123 127 130 132	mpbir3and	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i + 1 \in (M \dots N)$
134	100 133	ffvelrnd	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to P (i + 1) \in ℝ$
135		eluz	$⊢ (M \in ℤ \land i \in ℤ) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
136	1 101 135	syl2an	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
137	110 136	mpbird	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \in ℤ_{\geq M}$
138	9	adantr	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to N \in ℤ$
139		elfzo2	$⊢ i \in (M ..^N) \leftrightarrow (i \in ℤ_{\geq M} \land N \in ℤ \land i < N)$
140	137 138 117 139	syl3anbrc	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to i \in (M ..^N)$
141	140 4	syldan	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to P (i) < P (i + 1)$
142	122 134 141	ltled	$⊢ (φ \land i \in (M + 1 \dots N - 1)) \to P (i) \leq P (i + 1)$
143	2 99 142	monoord	$⊢ φ \to P (M + 1) \leq P (N)$
144	143	adantr	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to P (M + 1) \leq P (N)$
145	72 69 65 80 144	letrd	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to t \leq P (N)$
146	62 65 72 78 145	eliccd	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to t \in [P (M), P (N)]$
147	146 5	syldan	$⊢ (φ \land t \in [P (M), P (M + 1)]) \to A \in ℂ$
148		id	$⊢ φ \to φ$
149		fzolb	$⊢ M \in (M ..^N) \leftrightarrow (M \in ℤ \land N \in ℤ \land M < N)$
150	1 9 54 149	syl3anbrc	$⊢ φ \to M \in (M ..^N)$
151	148 150	jca	$⊢ φ \to (φ \land M \in (M ..^N))$
152		eleq1	$⊢ i = M \to (i \in (M ..^N) \leftrightarrow M \in (M ..^N))$
153	152	anbi2d	$⊢ i = M \to ((φ \land i \in (M ..^N)) \leftrightarrow (φ \land M \in (M ..^N)))$
154		fveq2	$⊢ i = M \to P (i) = P (M)$
155		fvoveq1	$⊢ i = M \to P (i + 1) = P (M + 1)$
156	154 155	oveq12d	$⊢ i = M \to [P (i), P (i + 1)] = [P (M), P (M + 1)]$
157	156	mpteq1d	$⊢ i = M \to (t \in [P (i), P (i + 1)] ⟼ A) = (t \in [P (M), P (M + 1)] ⟼ A)$
158	157	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})$
159	153 158	imbi12d	$⊢ i = M \to (((φ \land i \in (M ..^N)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}) \leftrightarrow ((φ \land M \in (M ..^N)) \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1}))$
160	159 6	vtoclg	$⊢ M \in ℤ \to ((φ \land M \in (M ..^N)) \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1})$
161	1 151 160	sylc	$⊢ φ \to (t \in [P (M), P (M + 1)] ⟼ A) \in 𝐿^{1}$
162	147 161	itgcl	$⊢ φ \to \int_{[P (M), P (M + 1)]} A d t \in ℂ$
163	156	itgeq1d	$⊢ i = M \to \int_{[P (i), P (i + 1)]} A d t = \int_{[P (M), P (M + 1)]} A d t$
164	163	fsum1	$⊢ (M \in ℤ \land \int_{[P (M), P (M + 1)]} A d t \in ℂ) \to \sum_{i = M}^{M} \int_{[P (i), P (i + 1)]} A d t = \int_{[P (M), P (M + 1)]} A d t$
165	1 162 164	syl2anc	$⊢ φ \to \sum_{i = M}^{M} \int_{[P (i), P (i + 1)]} A d t = \int_{[P (M), P (M + 1)]} A d t$
166	165	adantl	$⊢ (N \in ℤ_{\geq (M + 1)} \land φ) \to \sum_{i = M}^{M} \int_{[P (i), P (i + 1)]} A d t = \int_{[P (M), P (M + 1)]} A d t$
167	48 166	eqtr2d	$⊢ (N \in ℤ_{\geq (M + 1)} \land φ) \to \int_{[P (M), P (M + 1)]} A d t = \sum_{i \in (M ..^M + 1)} \int_{[P (i), P (i + 1)]} A d t$
168	167	ex	$⊢ N \in ℤ_{\geq (M + 1)} \to (φ \to \int_{[P (M), P (M + 1)]} A d t = \sum_{i \in (M ..^M + 1)} \int_{[P (i), P (i + 1)]} A d t)$
169		simp3	$⊢ (k \in (M + 1 ..^N) \land (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \land φ) \to φ$
170		simp1	$⊢ (k \in (M + 1 ..^N) \land (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \land φ) \to k \in (M + 1 ..^N)$
171		simp2	$⊢ (k \in (M + 1 ..^N) \land (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \land φ) \to (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t)$
172	169 171	mpd	$⊢ (k \in (M + 1 ..^N) \land (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \land φ) \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t$
173	50	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \in ℝ$
174		elfzoelz	$⊢ k \in (M + 1 ..^N) \to k \in ℤ$
175	174	zred	$⊢ k \in (M + 1 ..^N) \to k \in ℝ$
176	175	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℝ$
177	52	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M + 1 \in ℝ$
178	53	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M < M + 1$
179		elfzole1	$⊢ k \in (M + 1 ..^N) \to M + 1 \leq k$
180	179	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to M + 1 \leq k$
181	173 177 176 178 180	ltletrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to M < k$
182	173 176 181	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \leq k$
183		eluz	$⊢ (M \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq M} \leftrightarrow M \leq k)$
184	1 174 183	syl2an	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k \in ℤ_{\geq M} \leftrightarrow M \leq k)$
185	182 184	mpbird	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℤ_{\geq M}$
186		simplll	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to φ$
187		eliccxr	$⊢ t \in [P (i), P (i + 1)] \to t \in ℝ^{*}$
188	187	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to t \in ℝ^{*}$
189	186 73	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (M) \in ℝ$
190	186 3	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P : (M \dots N) ⟶ ℝ$
191		elfzelz	$⊢ i \in (M \dots k) \to i \in ℤ$
192	191	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in ℤ$
193		elfzle1	$⊢ i \in (M \dots k) \to M \leq i$
194	193	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to M \leq i$
195	192	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in ℝ$
196	13	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to N \in ℝ$
197	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to k \in ℝ$
198		elfzle2	$⊢ i \in (M \dots k) \to i \leq k$
199	198	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \leq k$
200		elfzolt2	$⊢ k \in (M + 1 ..^N) \to k < N$
201	200	ad2antlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to k < N$
202	195 197 196 199 201	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i < N$
203	195 196 202	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \leq N$
204	94	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (M \in ℤ \land N \in ℤ)$
205	204 96	syl	$⊢ ((φ \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))$
206	192 194 203 205	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in (M \dots N)$
207	206	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to i \in (M \dots N)$
208	190 207	ffvelrnd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (i) \in ℝ$
209	192	peano2zd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i + 1 \in ℤ$
210	50	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to M \in ℝ$
211	209	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i + 1 \in ℝ$
212	50	adantr	$⊢ (φ \land i \in (M \dots k)) \to M \in ℝ$
213	191	zred	$⊢ i \in (M \dots k) \to i \in ℝ$
214	213	adantl	$⊢ (φ \land i \in (M \dots k)) \to i \in ℝ$
215		1red	$⊢ (φ \land i \in (M \dots k)) \to 1 \in ℝ$
216	214 215	readdcld	$⊢ (φ \land i \in (M \dots k)) \to i + 1 \in ℝ$
217	193	adantl	$⊢ (φ \land i \in (M \dots k)) \to M \leq i$
218	214	ltp1d	$⊢ (φ \land i \in (M \dots k)) \to i < i + 1$
219	212 214 216 217 218	lelttrd	$⊢ (φ \land i \in (M \dots k)) \to M < i + 1$
220	219	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to M < i + 1$
221	210 211 220	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to M \leq i + 1$
222	9 191	anim12ci	$⊢ (φ \land i \in (M \dots k)) \to (i \in ℤ \land N \in ℤ)$
223	222	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (i \in ℤ \land N \in ℤ)$
224	223 128	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (i < N \leftrightarrow i + 1 \leq N)$
225	202 224	mpbid	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i + 1 \leq N$
226	204 131	syl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (i + 1 \in (M \dots N) \leftrightarrow (i + 1 \in ℤ \land M \leq i + 1 \land i + 1 \leq N))$
227	209 221 225 226	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i + 1 \in (M \dots N)$
228	227	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to i + 1 \in (M \dots N)$
229	190 228	ffvelrnd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (i + 1) \in ℝ$
230		simpr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to t \in [P (i), P (i + 1)]$
231		eliccre	$⊢ (P (i) \in ℝ \land P (i + 1) \in ℝ \land t \in [P (i), P (i + 1)]) \to t \in ℝ$
232	208 229 230 231	syl3anc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to t \in ℝ$
233		elfzuz	$⊢ i \in (M \dots k) \to i \in ℤ_{\geq M}$
234	233	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in ℤ_{\geq M}$
235	3	ad3antrrr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to P : (M \dots N) ⟶ ℝ$
236		elfzelz	$⊢ j \in (M \dots i) \to j \in ℤ$
237	236	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to j \in ℤ$
238		elfzle1	$⊢ j \in (M \dots i) \to M \leq j$
239	238	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to M \leq j$
240	237	zred	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to j \in ℝ$
241	196	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to N \in ℝ$
242	195	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to i \in ℝ$
243		elfzle2	$⊢ j \in (M \dots i) \to j \leq i$
244	243	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to j \leq i$
245	202	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to i < N$
246	240 242 241 244 245	lelttrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to j < N$
247	240 241 246	ltled	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to j \leq N$
248	204	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to (M \in ℤ \land N \in ℤ)$
249		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
250	248 249	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
251	237 239 247 250	mpbir3and	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to j \in (M \dots N)$
252	235 251	ffvelrnd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i)) \to P (j) \in ℝ$
253	3	ad3antrrr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to P : (M \dots N) ⟶ ℝ$
254		elfzelz	$⊢ j \in (M \dots i - 1) \to j \in ℤ$
255	254	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \in ℤ$
256		elfzle1	$⊢ j \in (M \dots i - 1) \to M \leq j$
257	256	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to M \leq j$
258	255	zred	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \in ℝ$
259	196	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to N \in ℝ$
260	195	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to i \in ℝ$
261		1red	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to 1 \in ℝ$
262	260 261	resubcld	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to i - 1 \in ℝ$
263		elfzle2	$⊢ j \in (M \dots i - 1) \to j \leq i - 1$
264	263	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \leq i - 1$
265	260	ltm1d	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to i - 1 < i$
266	258 262 260 264 265	lelttrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j < i$
267	202	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to i < N$
268	258 260 259 266 267	lttrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j < N$
269	258 259 268	ltled	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \leq N$
270	204	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to (M \in ℤ \land N \in ℤ)$
271	270 249	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
272	255 257 269 271	mpbir3and	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \in (M \dots N)$
273	253 272	ffvelrnd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to P (j) \in ℝ$
274	255	peano2zd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j + 1 \in ℤ$
275	173	ad2antrr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to M \in ℝ$
276	258 261	readdcld	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j + 1 \in ℝ$
277	50	adantr	$⊢ (φ \land j \in (M \dots i - 1)) \to M \in ℝ$
278	254	zred	$⊢ j \in (M \dots i - 1) \to j \in ℝ$
279	278	adantl	$⊢ (φ \land j \in (M \dots i - 1)) \to j \in ℝ$
280		1red	$⊢ (φ \land j \in (M \dots i - 1)) \to 1 \in ℝ$
281	279 280	readdcld	$⊢ (φ \land j \in (M \dots i - 1)) \to j + 1 \in ℝ$
282	256	adantl	$⊢ (φ \land j \in (M \dots i - 1)) \to M \leq j$
283	279	ltp1d	$⊢ (φ \land j \in (M \dots i - 1)) \to j < j + 1$
284	277 279 281 282 283	lelttrd	$⊢ (φ \land j \in (M \dots i - 1)) \to M < j + 1$
285	284	ad4ant14	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to M < j + 1$
286	275 276 285	ltled	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to M \leq j + 1$
287		zltp1le	$⊢ (j \in ℤ \land i \in ℤ) \to (j < i \leftrightarrow j + 1 \leq i)$
288	254 192 287	syl2anr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to (j < i \leftrightarrow j + 1 \leq i)$
289	266 288	mpbid	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j + 1 \leq i$
290	276 260 259 289 267	lelttrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j + 1 < N$
291	276 259 290	ltled	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j + 1 \leq N$
292		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (j + 1 \in (M \dots N) \leftrightarrow (j + 1 \in ℤ \land M \leq j + 1 \land j + 1 \leq N))$
293	270 292	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to (j + 1 \in (M \dots N) \leftrightarrow (j + 1 \in ℤ \land M \leq j + 1 \land j + 1 \leq N))$
294	274 286 291 293	mpbir3and	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j + 1 \in (M \dots N)$
295	253 294	ffvelrnd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to P (j + 1) \in ℝ$
296		simplll	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to φ$
297		elfzuz	$⊢ j \in (M \dots i - 1) \to j \in ℤ_{\geq M}$
298	297	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \in ℤ_{\geq M}$
299	296 9	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to N \in ℤ$
300		elfzo2	$⊢ j \in (M ..^N) \leftrightarrow (j \in ℤ_{\geq M} \land N \in ℤ \land j < N)$
301	298 299 268 300	syl3anbrc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to j \in (M ..^N)$
302		eleq1	$⊢ i = j \to (i \in (M ..^N) \leftrightarrow j \in (M ..^N))$
303	302	anbi2d	$⊢ i = j \to ((φ \land i \in (M ..^N)) \leftrightarrow (φ \land j \in (M ..^N)))$
304		fveq2	$⊢ i = j \to P (i) = P (j)$
305		fvoveq1	$⊢ i = j \to P (i + 1) = P (j + 1)$
306	304 305	breq12d	$⊢ i = j \to (P (i) < P (i + 1) \leftrightarrow P (j) < P (j + 1))$
307	303 306	imbi12d	$⊢ i = j \to (((φ \land i \in (M ..^N)) \to P (i) < P (i + 1)) \leftrightarrow ((φ \land j \in (M ..^N)) \to P (j) < P (j + 1)))$
308	307 4	chvarvv	$⊢ (φ \land j \in (M ..^N)) \to P (j) < P (j + 1)$
309	296 301 308	syl2anc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to P (j) < P (j + 1)$
310	273 295 309	ltled	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (M \dots i - 1)) \to P (j) \leq P (j + 1)$
311	234 252 310	monoord	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to P (M) \leq P (i)$
312	311	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (M) \leq P (i)$
313	208	rexrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (i) \in ℝ^{*}$
314	229	rexrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (i + 1) \in ℝ^{*}$
315		iccgelb	$⊢ (P (i) \in ℝ^{} \land P (i + 1) \in ℝ^{} \land t \in [P (i), P (i + 1)]) \to P (i) \leq t$
316	313 314 230 315	syl3anc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (i) \leq t$
317	189 208 232 312 316	letrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (M) \leq t$
318	186 64	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (N) \in ℝ$
319		iccleub	$⊢ (P (i) \in ℝ^{} \land P (i + 1) \in ℝ^{} \land t \in [P (i), P (i + 1)]) \to t \leq P (i + 1)$
320	313 314 230 319	syl3anc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to t \leq P (i + 1)$
321	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to N \in ℤ$
322		eluz	$⊢ (i + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (i + 1)} \leftrightarrow i + 1 \leq N)$
323	209 321 322	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (N \in ℤ_{\geq (i + 1)} \leftrightarrow i + 1 \leq N)$
324	225 323	mpbird	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to N \in ℤ_{\geq (i + 1)}$
325	324	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to N \in ℤ_{\geq (i + 1)}$
326	3	ad3antrrr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to P : (M \dots N) ⟶ ℝ$
327		elfzelz	$⊢ j \in (i + 1 \dots N) \to j \in ℤ$
328	327	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to j \in ℤ$
329		elfzel1	$⊢ i \in (M \dots k) \to M \in ℤ$
330	329	zred	$⊢ i \in (M \dots k) \to M \in ℝ$
331	330	adantr	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to M \in ℝ$
332	327	zred	$⊢ j \in (i + 1 \dots N) \to j \in ℝ$
333	332	adantl	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to j \in ℝ$
334	213	adantr	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to i \in ℝ$
335		1red	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to 1 \in ℝ$
336	334 335	readdcld	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to i + 1 \in ℝ$
337	193	adantr	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to M \leq i$
338	334	ltp1d	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to i < i + 1$
339	331 334 336 337 338	lelttrd	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to M < i + 1$
340		elfzle1	$⊢ j \in (i + 1 \dots N) \to i + 1 \leq j$
341	340	adantl	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to i + 1 \leq j$
342	331 336 333 339 341	ltletrd	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to M < j$
343	331 333 342	ltled	$⊢ (i \in (M \dots k) \land j \in (i + 1 \dots N)) \to M \leq j$
344	343	adantll	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to M \leq j$
345		elfzle2	$⊢ j \in (i + 1 \dots N) \to j \leq N$
346	345	adantl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to j \leq N$
347	204	adantr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to (M \in ℤ \land N \in ℤ)$
348	347 249	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
349	328 344 346 348	mpbir3and	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to j \in (M \dots N)$
350	326 349	ffvelrnd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N)) \to P (j) \in ℝ$
351	350	adantlr	$⊢ ((((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \land j \in (i + 1 \dots N)) \to P (j) \in ℝ$
352		simplll	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N - 1)) \to φ$
353		simplr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N - 1)) \to i \in (M \dots k)$
354		simpr	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N - 1)) \to j \in (i + 1 \dots N - 1)$
355	3	3ad2ant1	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to P : (M \dots N) ⟶ ℝ$
356		elfzelz	$⊢ j \in (i + 1 \dots N - 1) \to j \in ℤ$
357	356	3ad2ant3	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j \in ℤ$
358	50	3ad2ant1	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M \in ℝ$
359	357	zred	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j \in ℝ$
360	216	3adant3	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i + 1 \in ℝ$
361	219	3adant3	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M < i + 1$
362		elfzle1	$⊢ j \in (i + 1 \dots N - 1) \to i + 1 \leq j$
363	362	3ad2ant3	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i + 1 \leq j$
364	358 360 359 361 363	ltletrd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M < j$
365	358 359 364	ltled	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M \leq j$
366	356	adantl	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to j \in ℤ$
367	366	zred	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to j \in ℝ$
368	13	adantr	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to N \in ℝ$
369		1red	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to 1 \in ℝ$
370	368 369	resubcld	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to N - 1 \in ℝ$
371		elfzle2	$⊢ j \in (i + 1 \dots N - 1) \to j \leq N - 1$
372	371	adantl	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to j \leq N - 1$
373	368	ltm1d	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to N - 1 < N$
374	367 370 368 372 373	lelttrd	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to j < N$
375	367 368 374	ltled	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to j \leq N$
376	375	3adant2	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j \leq N$
377	94	3ad2ant1	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to (M \in ℤ \land N \in ℤ)$
378	377 249	syl	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
379	357 365 376 378	mpbir3and	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j \in (M \dots N)$
380	355 379	ffvelrnd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to P (j) \in ℝ$
381	357	peano2zd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j + 1 \in ℤ$
382	381	zred	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j + 1 \in ℝ$
383	213	3ad2ant2	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i \in ℝ$
384		1red	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to 1 \in ℝ$
385	218	3adant3	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i < i + 1$
386	383 360 359 385 363	ltletrd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i < j$
387	383 359 386	ltled	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i \leq j$
388	383 359 384 387	leadd1dd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to i + 1 \leq j + 1$
389	358 360 382 361 388	ltletrd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M < j + 1$
390	358 382 389	ltled	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M \leq j + 1$
391		zltp1le	$⊢ (j \in ℤ \land N \in ℤ) \to (j < N \leftrightarrow j + 1 \leq N)$
392	356 9 391	syl2anr	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to (j < N \leftrightarrow j + 1 \leq N)$
393	374 392	mpbid	$⊢ (φ \land j \in (i + 1 \dots N - 1)) \to j + 1 \leq N$
394	393	3adant2	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j + 1 \leq N$
395	377 292	syl	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to (j + 1 \in (M \dots N) \leftrightarrow (j + 1 \in ℤ \land M \leq j + 1 \land j + 1 \leq N))$
396	381 390 394 395	mpbir3and	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j + 1 \in (M \dots N)$
397	355 396	ffvelrnd	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to P (j + 1) \in ℝ$
398		simp1	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to φ$
399	1	3ad2ant1	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to M \in ℤ$
400		eluz	$⊢ (M \in ℤ \land j \in ℤ) \to (j \in ℤ_{\geq M} \leftrightarrow M \leq j)$
401	399 357 400	syl2anc	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to (j \in ℤ_{\geq M} \leftrightarrow M \leq j)$
402	365 401	mpbird	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j \in ℤ_{\geq M}$
403	9	3ad2ant1	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to N \in ℤ$
404	374	3adant2	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j < N$
405	402 403 404 300	syl3anbrc	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to j \in (M ..^N)$
406	398 405 308	syl2anc	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to P (j) < P (j + 1)$
407	380 397 406	ltled	$⊢ (φ \land i \in (M \dots k) \land j \in (i + 1 \dots N - 1)) \to P (j) \leq P (j + 1)$
408	352 353 354 407	syl3anc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land j \in (i + 1 \dots N - 1)) \to P (j) \leq P (j + 1)$
409	408	adantlr	$⊢ ((((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \land j \in (i + 1 \dots N - 1)) \to P (j) \leq P (j + 1)$
410	325 351 409	monoord	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to P (i + 1) \leq P (N)$
411	232 229 318 320 410	letrd	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to t \leq P (N)$
412	64	rexrd	$⊢ φ \to P (N) \in ℝ^{*}$
413	74 412	jca	$⊢ φ \to (P (M) \in ℝ^{} \land P (N) \in ℝ^{})$
414	186 413	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to (P (M) \in ℝ^{} \land P (N) \in ℝ^{})$
415		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)))$
416	414 415	syl	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to (t \in [P (M), P (N)] \leftrightarrow (t \in ℝ^{*} \land P (M) \leq t \land t \leq P (N)))$
417	188 317 411 416	mpbir3and	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to t \in [P (M), P (N)]$
418	186 417 5	syl2anc	$⊢ (((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \land t \in [P (i), P (i + 1)]) \to A \in ℂ$
419		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to φ$
420	234 321 202 139	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to i \in (M ..^N)$
421	419 420 6	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}$
422	418 421	itgcl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to \int_{[P (i), P (i + 1)]} A d t \in ℂ$
423		fveq2	$⊢ i = k \to P (i) = P (k)$
424		fvoveq1	$⊢ i = k \to P (i + 1) = P (k + 1)$
425	423 424	oveq12d	$⊢ i = k \to [P (i), P (i + 1)] = [P (k), P (k + 1)]$
426	425	itgeq1d	$⊢ i = k \to \int_{[P (i), P (i + 1)]} A d t = \int_{[P (k), P (k + 1)]} A d t$
427	185 422 426	fzosump1	$⊢ (φ \land k \in (M + 1 ..^N)) \to \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t + \int_{[P (k), P (k + 1)]} A d t$
428	427	3adant3	$⊢ (φ \land k \in (M + 1 ..^N) \land \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \to \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t + \int_{[P (k), P (k + 1)]} A d t$
429		oveq1	$⊢ \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t \to \int_{[P (M), P (k)]} A d t + \int_{[P (k), P (k + 1)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t + \int_{[P (k), P (k + 1)]} A d t$
430	429	eqcomd	$⊢ \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t \to \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t + \int_{[P (k), P (k + 1)]} A d t = \int_{[P (M), P (k)]} A d t + \int_{[P (k), P (k + 1)]} A d t$
431	430	3ad2ant3	$⊢ (φ \land k \in (M + 1 ..^N) \land \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \to \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t + \int_{[P (k), P (k + 1)]} A d t = \int_{[P (M), P (k)]} A d t + \int_{[P (k), P (k + 1)]} A d t$
432	73	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (M) \in ℝ$
433	3	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to P : (M \dots N) ⟶ ℝ$
434	174	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℤ$
435	434	peano2zd	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \in ℤ$
436	435	zred	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \in ℝ$
437	176	ltp1d	$⊢ (φ \land k \in (M + 1 ..^N)) \to k < k + 1$
438	173 176 436 181 437	lttrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to M < k + 1$
439	173 436 438	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \leq k + 1$
440	200	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to k < N$
441		zltp1le	$⊢ (k \in ℤ \land N \in ℤ) \to (k < N \leftrightarrow k + 1 \leq N)$
442	174 9 441	syl2anr	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k < N \leftrightarrow k + 1 \leq N)$
443	440 442	mpbid	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \leq N$
444	94	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to (M \in ℤ \land N \in ℤ)$
445		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))$
446	444 445	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))$
447	435 439 443 446	mpbir3and	$⊢ (φ \land k \in (M + 1 ..^N)) \to k + 1 \in (M \dots N)$
448	433 447	ffvelrnd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k + 1) \in ℝ$
449	13	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℝ$
450	176 449 440	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \leq N$
451		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (k \in (M \dots N) \leftrightarrow (k \in ℤ \land M \leq k \land k \leq N))$
452	444 451	syl	$⊢ (φ \land k \in (M + 1 ..^N)) \to (k \in (M \dots N) \leftrightarrow (k \in ℤ \land M \leq k \land k \leq N))$
453	434 182 450 452	mpbir3and	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in (M \dots N)$
454	433 453	ffvelrnd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \in ℝ$
455	454	rexrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \in ℝ^{*}$
456	3	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to P : (M \dots N) ⟶ ℝ$
457	456 206	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k)) \to P (i) \in ℝ$
458	3	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P : (M \dots N) ⟶ ℝ$
459		elfzelz	$⊢ i \in (M \dots k - 1) \to i \in ℤ$
460	459	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in ℤ$
461		elfzle1	$⊢ i \in (M \dots k - 1) \to M \leq i$
462	461	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to M \leq i$
463	460	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in ℝ$
464	13	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to N \in ℝ$
465	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k \in ℝ$
466		1red	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to 1 \in ℝ$
467	465 466	resubcld	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k - 1 \in ℝ$
468		elfzle2	$⊢ i \in (M \dots k - 1) \to i \leq k - 1$
469	468	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \leq k - 1$
470	465	ltm1d	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k - 1 < k$
471	463 467 465 469 470	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i < k$
472	440	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to k < N$
473	463 465 464 471 472	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i < N$
474	463 464 473	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \leq N$
475	94	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to (M \in ℤ \land N \in ℤ)$
476	475 96	syl	$⊢ ((φ \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))$
477	460 462 474 476	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in (M \dots N)$
478	458 477	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i) \in ℝ$
479	460	peano2zd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \in ℤ$
480	50	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to M \in ℝ$
481	463 466	readdcld	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \in ℝ$
482	463	ltp1d	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i < i + 1$
483	480 463 481 462 482	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to M < i + 1$
484	480 481 483	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to M \leq i + 1$
485		zltp1le	$⊢ (i \in ℤ \land k \in ℤ) \to (i < k \leftrightarrow i + 1 \leq k)$
486	459 434 485	syl2anr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to (i < k \leftrightarrow i + 1 \leq k)$
487	471 486	mpbid	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \leq k$
488	481 465 464 487 472	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 < N$
489	481 464 488	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \leq N$
490	475 131	syl	$⊢ ((φ \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))$
491	479 484 489 490	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i + 1 \in (M \dots N)$
492	458 491	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i + 1) \in ℝ$
493		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to φ$
494		elfzuz	$⊢ i \in (M \dots k - 1) \to i \in ℤ_{\geq M}$
495	494	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in ℤ_{\geq M}$
496	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to N \in ℤ$
497	495 496 473 139	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to i \in (M ..^N)$
498	493 497 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i) < P (i + 1)$
499	478 492 498	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M \dots k - 1)) \to P (i) \leq P (i + 1)$
500	185 457 499	monoord	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (M) \leq P (k)$
501	9	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℤ$
502		elfzo2	$⊢ k \in (M ..^N) \leftrightarrow (k \in ℤ_{\geq M} \land N \in ℤ \land k < N)$
503	185 501 440 502	syl3anbrc	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in (M ..^N)$
504		eleq1	$⊢ i = k \to (i \in (M ..^N) \leftrightarrow k \in (M ..^N))$
505	504	anbi2d	$⊢ i = k \to ((φ \land i \in (M ..^N)) \leftrightarrow (φ \land k \in (M ..^N)))$
506	423 424	breq12d	$⊢ i = k \to (P (i) < P (i + 1) \leftrightarrow P (k) < P (k + 1))$
507	505 506	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)))$
508	507 4	chvarvv	$⊢ (φ \land k \in (M ..^N)) \to P (k) < P (k + 1)$
509	503 508	syldan	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) < P (k + 1)$
510	454 448 509	ltled	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \leq P (k + 1)$
511	74	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (M) \in ℝ^{*}$
512	448	rexrd	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k + 1) \in ℝ^{*}$
513		elicc1	$⊢ (P (M) \in ℝ^{} \land P (k + 1) \in ℝ^{}) \to (P (k) \in [P (M), P (k + 1)] \leftrightarrow (P (k) \in ℝ^{*} \land P (M) \leq P (k) \land P (k) \leq P (k + 1)))$
514	511 512 513	syl2anc	$⊢ (φ \land k \in (M + 1 ..^N)) \to (P (k) \in [P (M), P (k + 1)] \leftrightarrow (P (k) \in ℝ^{*} \land P (M) \leq P (k) \land P (k) \leq P (k + 1)))$
515	455 500 510 514	mpbir3and	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \in [P (M), P (k + 1)]$
516		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to φ$
517		eliccxr	$⊢ t \in [P (M), P (k + 1)] \to t \in ℝ^{*}$
518	517	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to t \in ℝ^{*}$
519	74	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (M) \in ℝ^{*}$
520	512	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (k + 1) \in ℝ^{*}$
521		simpr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to t \in [P (M), P (k + 1)]$
522		iccgelb	$⊢ (P (M) \in ℝ^{} \land P (k + 1) \in ℝ^{} \land t \in [P (M), P (k + 1)]) \to P (M) \leq t$
523	519 520 521 522	syl3anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (M) \leq t$
524	73	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (M) \in ℝ$
525	448	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (k + 1) \in ℝ$
526		eliccre	$⊢ (P (M) \in ℝ \land P (k + 1) \in ℝ \land t \in [P (M), P (k + 1)]) \to t \in ℝ$
527	524 525 521 526	syl3anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to t \in ℝ$
528	64	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (N) \in ℝ$
529		iccleub	$⊢ (P (M) \in ℝ^{} \land P (k + 1) \in ℝ^{} \land t \in [P (M), P (k + 1)]) \to t \leq P (k + 1)$
530	519 520 521 529	syl3anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to t \leq P (k + 1)$
531		eluz2	$⊢ N \in ℤ_{\geq (k + 1)} \leftrightarrow (k + 1 \in ℤ \land N \in ℤ \land k + 1 \leq N)$
532	435 501 443 531	syl3anbrc	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℤ_{\geq (k + 1)}$
533	3	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to P : (M \dots N) ⟶ ℝ$
534	1	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M \in ℤ$
535	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to N \in ℤ$
536		elfzelz	$⊢ i \in (k + 1 \dots N) \to i \in ℤ$
537	536	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \in ℤ$
538	50	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M \in ℝ$
539	537	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \in ℝ$
540	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to k \in ℝ$
541	181	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M < k$
542	175	adantr	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k \in ℝ$
543		1red	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to 1 \in ℝ$
544	542 543	readdcld	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k + 1 \in ℝ$
545	536	zred	$⊢ i \in (k + 1 \dots N) \to i \in ℝ$
546	545	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to i \in ℝ$
547	542	ltp1d	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k < k + 1$
548		elfzle1	$⊢ i \in (k + 1 \dots N) \to k + 1 \leq i$
549	548	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k + 1 \leq i$
550	542 544 546 547 549	ltletrd	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N)) \to k < i$
551	550	adantll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to k < i$
552	538 540 539 541 551	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M < i$
553	538 539 552	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to M \leq i$
554		elfzle2	$⊢ i \in (k + 1 \dots N) \to i \leq N$
555	554	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \leq N$
556	534 535 537 553 555	elfzd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to i \in (M \dots N)$
557	533 556	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N)) \to P (i) \in ℝ$
558	3	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P : (M \dots N) ⟶ ℝ$
559	1	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \in ℤ$
560	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to N \in ℤ$
561		elfzelz	$⊢ i \in (k + 1 \dots N - 1) \to i \in ℤ$
562	561	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in ℤ$
563	50	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \in ℝ$
564	562	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in ℝ$
565	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to k \in ℝ$
566	181	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M < k$
567	175	adantr	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k \in ℝ$
568		1red	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to 1 \in ℝ$
569	567 568	readdcld	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k + 1 \in ℝ$
570	561	zred	$⊢ i \in (k + 1 \dots N - 1) \to i \in ℝ$
571	570	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to i \in ℝ$
572	567	ltp1d	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k < k + 1$
573		elfzle1	$⊢ i \in (k + 1 \dots N - 1) \to k + 1 \leq i$
574	573	adantl	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k + 1 \leq i$
575	567 569 571 572 574	ltletrd	$⊢ (k \in (M + 1 ..^N) \land i \in (k + 1 \dots N - 1)) \to k < i$
576	575	adantll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to k < i$
577	563 565 564 566 576	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M < i$
578	563 564 577	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \leq i$
579	570	adantl	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i \in ℝ$
580	13	adantr	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to N \in ℝ$
581		1red	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to 1 \in ℝ$
582	580 581	resubcld	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to N - 1 \in ℝ$
583		elfzle2	$⊢ i \in (k + 1 \dots N - 1) \to i \leq N - 1$
584	583	adantl	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i \leq N - 1$
585	580	ltm1d	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to N - 1 < N$
586	579 582 580 584 585	lelttrd	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i < N$
587	579 580 586	ltled	$⊢ (φ \land i \in (k + 1 \dots N - 1)) \to i \leq N$
588	587	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \leq N$
589	559 560 562 578 588	elfzd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in (M \dots N)$
590	558 589	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i) \in ℝ$
591	562	peano2zd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in ℤ$
592	591	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in ℝ$
593	564	ltp1d	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i < i + 1$
594	565 564 592 576 593	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to k < i + 1$
595	563 565 592 566 594	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M < i + 1$
596	563 592 595	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to M \leq i + 1$
597	586	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i < N$
598	561 501 128	syl2anr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to (i < N \leftrightarrow i + 1 \leq N)$
599	597 598	mpbid	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \leq N$
600	559 560 591 596 599	elfzd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i + 1 \in (M \dots N)$
601	558 600	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i + 1) \in ℝ$
602		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to φ$
603		eluz2	$⊢ i \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land i \in ℤ \land M \leq i)$
604	559 562 578 603	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in ℤ_{\geq M}$
605	604 560 597 139	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to i \in (M ..^N)$
606	602 605 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i) < P (i + 1)$
607	590 601 606	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k + 1 \dots N - 1)) \to P (i) \leq P (i + 1)$
608	532 557 607	monoord	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k + 1) \leq P (N)$
609	608	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to P (k + 1) \leq P (N)$
610	527 525 528 530 609	letrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to t \leq P (N)$
611	413	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to (P (M) \in ℝ^{} \land P (N) \in ℝ^{})$
612	611 415	syl	$⊢ ((φ \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)))$
613	518 523 610 612	mpbir3and	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to t \in [P (M), P (N)]$
614	516 613 5	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k + 1)]) \to A \in ℂ$
615		nfv	$⊢ Ⅎ t (φ \land k \in (M + 1 ..^N))$
616	1	adantr	$⊢ (φ \land k \in (M + 1 ..^N)) \to M \in ℤ$
617		elfzouz	$⊢ k \in (M + 1 ..^N) \to k \in ℤ_{\geq (M + 1)}$
618	617	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to k \in ℤ_{\geq (M + 1)}$
619		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to φ$
620		elfzouz	$⊢ i \in (M ..^k) \to i \in ℤ_{\geq M}$
621	620	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to i \in ℤ_{\geq M}$
622	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to N \in ℤ$
623		elfzoelz	$⊢ i \in (M ..^k) \to i \in ℤ$
624	623	zred	$⊢ i \in (M ..^k) \to i \in ℝ$
625	624	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to i \in ℝ$
626	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to k \in ℝ$
627	13	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to N \in ℝ$
628		elfzolt2	$⊢ i \in (M ..^k) \to i < k$
629	628	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to i < k$
630	440	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to k < N$
631	625 626 627 629 630	lttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to i < N$
632	621 622 631 139	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to i \in (M ..^N)$
633	619 632 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to P (i) < P (i + 1)$
634		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to φ$
635	73	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (M) \in ℝ$
636	64	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (N) \in ℝ$
637	454	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (k) \in ℝ$
638		simpr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to t \in [P (M), P (k)]$
639		eliccre	$⊢ (P (M) \in ℝ \land P (k) \in ℝ \land t \in [P (M), P (k)]) \to t \in ℝ$
640	635 637 638 639	syl3anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to t \in ℝ$
641	74	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (M) \in ℝ^{*}$
642	455	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (k) \in ℝ^{*}$
643		iccgelb	$⊢ (P (M) \in ℝ^{} \land P (k) \in ℝ^{} \land t \in [P (M), P (k)]) \to P (M) \leq t$
644	641 642 638 643	syl3anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (M) \leq t$
645		iccleub	$⊢ (P (M) \in ℝ^{} \land P (k) \in ℝ^{} \land t \in [P (M), P (k)]) \to t \leq P (k)$
646	641 642 638 645	syl3anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to t \leq P (k)$
647		elfzouz2	$⊢ k \in (M + 1 ..^N) \to N \in ℤ_{\geq k}$
648	647	adantl	$⊢ (φ \land k \in (M + 1 ..^N)) \to N \in ℤ_{\geq k}$
649	3	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to P : (M \dots N) ⟶ ℝ$
650	1	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to M \in ℤ$
651	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to N \in ℤ$
652		elfzelz	$⊢ i \in (k \dots N) \to i \in ℤ$
653	652	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to i \in ℤ$
654	50	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to M \in ℝ$
655	653	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to i \in ℝ$
656	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to k \in ℝ$
657	181	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to M < k$
658		elfzle1	$⊢ i \in (k \dots N) \to k \leq i$
659	658	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to k \leq i$
660	654 656 655 657 659	ltletrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to M < i$
661	654 655 660	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to M \leq i$
662		elfzle2	$⊢ i \in (k \dots N) \to i \leq N$
663	662	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to i \leq N$
664	650 651 653 661 663	elfzd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to i \in (M \dots N)$
665	649 664	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N)) \to P (i) \in ℝ$
666	3	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to P : (M \dots N) ⟶ ℝ$
667	1	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M \in ℤ$
668	9	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to N \in ℤ$
669		elfzelz	$⊢ i \in (k \dots N - 1) \to i \in ℤ$
670	669	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i \in ℤ$
671	50	ad2antrr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M \in ℝ$
672	670	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i \in ℝ$
673	176	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to k \in ℝ$
674	181	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M < k$
675		elfzle1	$⊢ i \in (k \dots N - 1) \to k \leq i$
676	675	adantl	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to k \leq i$
677	671 673 672 674 676	ltletrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M < i$
678	671 672 677	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M \leq i$
679	669	zred	$⊢ i \in (k \dots N - 1) \to i \in ℝ$
680	679	adantl	$⊢ (φ \land i \in (k \dots N - 1)) \to i \in ℝ$
681	13	adantr	$⊢ (φ \land i \in (k \dots N - 1)) \to N \in ℝ$
682		1red	$⊢ (φ \land i \in (k \dots N - 1)) \to 1 \in ℝ$
683	681 682	resubcld	$⊢ (φ \land i \in (k \dots N - 1)) \to N - 1 \in ℝ$
684		elfzle2	$⊢ i \in (k \dots N - 1) \to i \leq N - 1$
685	684	adantl	$⊢ (φ \land i \in (k \dots N - 1)) \to i \leq N - 1$
686	681	ltm1d	$⊢ (φ \land i \in (k \dots N - 1)) \to N - 1 < N$
687	680 683 681 685 686	lelttrd	$⊢ (φ \land i \in (k \dots N - 1)) \to i < N$
688	680 681 687	ltled	$⊢ (φ \land i \in (k \dots N - 1)) \to i \leq N$
689	688	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i \leq N$
690	667 668 670 678 689	elfzd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i \in (M \dots N)$
691	666 690	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to P (i) \in ℝ$
692	670	peano2zd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i + 1 \in ℤ$
693	692	zred	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i + 1 \in ℝ$
694	672	ltp1d	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i < i + 1$
695	671 672 693 678 694	lelttrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M < i + 1$
696	671 693 695	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to M \leq i + 1$
697	669 9 128	syl2anr	$⊢ (φ \land i \in (k \dots N - 1)) \to (i < N \leftrightarrow i + 1 \leq N)$
698	687 697	mpbid	$⊢ (φ \land i \in (k \dots N - 1)) \to i + 1 \leq N$
699	698	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i + 1 \leq N$
700	667 668 692 696 699	elfzd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i + 1 \in (M \dots N)$
701	666 700	ffvelrnd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to P (i + 1) \in ℝ$
702		simpll	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to φ$
703	667 670 678 603	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i \in ℤ_{\geq M}$
704	687	adantlr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i < N$
705	703 668 704 139	syl3anbrc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to i \in (M ..^N)$
706	702 705 4	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to P (i) < P (i + 1)$
707	691 701 706	ltled	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (k \dots N - 1)) \to P (i) \leq P (i + 1)$
708	648 665 707	monoord	$⊢ (φ \land k \in (M + 1 ..^N)) \to P (k) \leq P (N)$
709	708	adantr	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to P (k) \leq P (N)$
710	640 637 636 646 709	letrd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to t \leq P (N)$
711	635 636 640 644 710	eliccd	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to t \in [P (M), P (N)]$
712	634 711 5	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land t \in [P (M), P (k)]) \to A \in ℂ$
713	619 632 6	syl2anc	$⊢ ((φ \land k \in (M + 1 ..^N)) \land i \in (M ..^k)) \to (t \in [P (i), P (i + 1)] ⟼ A) \in 𝐿^{1}$
714	615 616 618 457 633 712 713	iblspltprt	$⊢ (φ \land k \in (M + 1 ..^N)) \to (t \in [P (M), P (k)] ⟼ A) \in 𝐿^{1}$
715	425	mpteq1d	$⊢ i = k \to (t \in [P (i), P (i + 1)] ⟼ A) = (t \in [P (k), P (k + 1)] ⟼ A)$
716	715	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})$
717	505 716	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}))$
718	717 6	chvarvv	$⊢ (φ \land k \in (M ..^N)) \to (t \in [P (k), P (k + 1)] ⟼ A) \in 𝐿^{1}$
719	503 718	syldan	$⊢ (φ \land k \in (M + 1 ..^N)) \to (t \in [P (k), P (k + 1)] ⟼ A) \in 𝐿^{1}$
720	432 448 515 614 714 719	itgspliticc	$⊢ (φ \land k \in (M + 1 ..^N)) \to \int_{[P (M), P (k + 1)]} A d t = \int_{[P (M), P (k)]} A d t + \int_{[P (k), P (k + 1)]} A d t$
721	720	eqcomd	$⊢ (φ \land k \in (M + 1 ..^N)) \to \int_{[P (M), P (k)]} A d t + \int_{[P (k), P (k + 1)]} A d t = \int_{[P (M), P (k + 1)]} A d t$
722	721	3adant3	$⊢ (φ \land k \in (M + 1 ..^N) \land \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \to \int_{[P (M), P (k)]} A d t + \int_{[P (k), P (k + 1)]} A d t = \int_{[P (M), P (k + 1)]} A d t$
723	428 431 722	3eqtrrd	$⊢ (φ \land k \in (M + 1 ..^N) \land \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \to \int_{[P (M), P (k + 1)]} A d t = \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t$
724	169 170 172 723	syl3anc	$⊢ (k \in (M + 1 ..^N) \land (φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \land φ) \to \int_{[P (M), P (k + 1)]} A d t = \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t$
725	724	3exp	$⊢ k \in (M + 1 ..^N) \to ((φ \to \int_{[P (M), P (k)]} A d t = \sum_{i \in (M ..^k)} \int_{[P (i), P (i + 1)]} A d t) \to (φ \to \int_{[P (M), P (k + 1)]} A d t = \sum_{i \in (M ..^k + 1)} \int_{[P (i), P (i + 1)]} A d t))$
726	22 29 36 43 168 725	fzind2	$⊢ N \in (M + 1 \dots N) \to (φ \to \int_{[P (M), P (N)]} A d t = \sum_{i \in (M ..^N)} \int_{[P (i), P (i + 1)]} A d t)$
727	15 726	mpcom	$⊢ φ \to \int_{[P (M), P (N)]} A d t = \sum_{i \in (M ..^N)} \int_{[P (i), P (i + 1)]} A d t$

Metamath Proof Explorer

Theorem itgspltprt

Proof