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