ovolicc2lem4

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014) (Revised by AV, 17-Sep-2020)

	Ref	Expression
Hypotheses	ovolicc.1	$⊢ φ \to A \in ℝ$
	ovolicc.2	$⊢ φ \to B \in ℝ$
	ovolicc.3	$⊢ φ \to A \leq B$
	ovolicc2.4	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ovolicc2.5	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	ovolicc2.6	$⊢ φ \to U \in (𝒫 ran ((.) \circ F) \cap Fin)$
	ovolicc2.7	$⊢ φ \to [A, B] \subseteq ⋃ U$
	ovolicc2.8	$⊢ φ \to G : U ⟶ ℕ$
	ovolicc2.9	$⊢ (φ \land t \in U) \to ((.) \circ F) (G (t)) = t$
	ovolicc2.10	$⊢ T = \{u \in U \| u \cap [A, B] \neq \emptyset\}$
	ovolicc2.11	$⊢ φ \to H : T ⟶ T$
	ovolicc2.12	$⊢ (φ \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in H (t)$
	ovolicc2.13	$⊢ φ \to A \in C$
	ovolicc2.14	$⊢ φ \to C \in T$
	ovolicc2.15	$⊢ K = seq 1 ((H \circ 1^{st}), (ℕ \times \{C\}))$
	ovolicc2.16	$⊢ W = \{n \in ℕ \| B \in K (n)\}$
	ovolicc2.17	$⊢ M = sup (W ℝ <)$
Assertion	ovolicc2lem4	$⊢ φ \to B - A \leq sup (ran S ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolicc.1	$⊢ φ \to A \in ℝ$
2		ovolicc.2	$⊢ φ \to B \in ℝ$
3		ovolicc.3	$⊢ φ \to A \leq B$
4		ovolicc2.4	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
5		ovolicc2.5	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
6		ovolicc2.6	$⊢ φ \to U \in (𝒫 ran ((.) \circ F) \cap Fin)$
7		ovolicc2.7	$⊢ φ \to [A, B] \subseteq ⋃ U$
8		ovolicc2.8	$⊢ φ \to G : U ⟶ ℕ$
9		ovolicc2.9	$⊢ (φ \land t \in U) \to ((.) \circ F) (G (t)) = t$
10		ovolicc2.10	$⊢ T = \{u \in U \| u \cap [A, B] \neq \emptyset\}$
11		ovolicc2.11	$⊢ φ \to H : T ⟶ T$
12		ovolicc2.12	$⊢ (φ \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in H (t)$
13		ovolicc2.13	$⊢ φ \to A \in C$
14		ovolicc2.14	$⊢ φ \to C \in T$
15		ovolicc2.15	$⊢ K = seq 1 ((H \circ 1^{st}), (ℕ \times \{C\}))$
16		ovolicc2.16	$⊢ W = \{n \in ℕ \| B \in K (n)\}$
17		ovolicc2.17	$⊢ M = sup (W ℝ <)$
18		arch	$⊢ x \in ℝ \to \exists z \in ℕ x < z$
19	18	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \forall y \in (G \circ K) [(1 \dots M)] y \leq x) \to \exists z \in ℕ x < z$
20		df-ima	$⊢ (G \circ K) [(1 \dots M)] = ran ({(G \circ K) ↾}_{(1 \dots M)})$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22		1zzd	$⊢ φ \to 1 \in ℤ$
23	21 15 22 14 11	algrf	$⊢ φ \to K : ℕ ⟶ T$
24	10	ssrab3	$⊢ T \subseteq U$
25		fss	$⊢ (K : ℕ ⟶ T \land T \subseteq U) \to K : ℕ ⟶ U$
26	23 24 25	sylancl	$⊢ φ \to K : ℕ ⟶ U$
27		fco	$⊢ (G : U ⟶ ℕ \land K : ℕ ⟶ U) \to (G \circ K) : ℕ ⟶ ℕ$
28	8 26 27	syl2anc	$⊢ φ \to (G \circ K) : ℕ ⟶ ℕ$
29		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
30		fssres	$⊢ ((G \circ K) : ℕ ⟶ ℕ \land (1 \dots M) \subseteq ℕ) \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) ⟶ ℕ$
31	28 29 30	sylancl	$⊢ φ \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) ⟶ ℕ$
32	31	frnd	$⊢ φ \to ran ({(G \circ K) ↾}_{(1 \dots M)}) \subseteq ℕ$
33	20 32	eqsstrid	$⊢ φ \to (G \circ K) [(1 \dots M)] \subseteq ℕ$
34		nnssre	$⊢ ℕ \subseteq ℝ$
35	33 34	sstrdi	$⊢ φ \to (G \circ K) [(1 \dots M)] \subseteq ℝ$
36	35	ad3antrrr	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to (G \circ K) [(1 \dots M)] \subseteq ℝ$
37		simpr	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to y \in (G \circ K) [(1 \dots M)]$
38	36 37	sseldd	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to y \in ℝ$
39		simpllr	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to x \in ℝ$
40		nnre	$⊢ z \in ℕ \to z \in ℝ$
41	40	ad2antlr	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to z \in ℝ$
42		lelttr	$⊢ (y \in ℝ \land x \in ℝ \land z \in ℝ) \to ((y \leq x \land x < z) \to y < z)$
43	38 39 41 42	syl3anc	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to ((y \leq x \land x < z) \to y < z)$
44	43	ancomsd	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to ((x < z \land y \leq x) \to y < z)$
45	44	expdimp	$⊢ ((((φ \land x \in ℝ) \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \land x < z) \to (y \leq x \to y < z)$
46	45	an32s	$⊢ ((((φ \land x \in ℝ) \land z \in ℕ) \land x < z) \land y \in (G \circ K) [(1 \dots M)]) \to (y \leq x \to y < z)$
47	46	ralimdva	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land x < z) \to (\forall y \in (G \circ K) [(1 \dots M)] y \leq x \to \forall y \in (G \circ K) [(1 \dots M)] y < z)$
48	47	impancom	$⊢ (((φ \land x \in ℝ) \land z \in ℕ) \land \forall y \in (G \circ K) [(1 \dots M)] y \leq x) \to (x < z \to \forall y \in (G \circ K) [(1 \dots M)] y < z)$
49	48	an32s	$⊢ (((φ \land x \in ℝ) \land \forall y \in (G \circ K) [(1 \dots M)] y \leq x) \land z \in ℕ) \to (x < z \to \forall y \in (G \circ K) [(1 \dots M)] y < z)$
50	49	reximdva	$⊢ ((φ \land x \in ℝ) \land \forall y \in (G \circ K) [(1 \dots M)] y \leq x) \to (\exists z \in ℕ x < z \to \exists z \in ℕ \forall y \in (G \circ K) [(1 \dots M)] y < z)$
51	19 50	mpd	$⊢ ((φ \land x \in ℝ) \land \forall y \in (G \circ K) [(1 \dots M)] y \leq x) \to \exists z \in ℕ \forall y \in (G \circ K) [(1 \dots M)] y < z$
52		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
53		fvres	$⊢ i \in (1 \dots M) \to ({(G \circ K) ↾}_{(1 \dots M)}) (i) = (G \circ K) (i)$
54	53	adantl	$⊢ (φ \land i \in (1 \dots M)) \to ({(G \circ K) ↾}_{(1 \dots M)}) (i) = (G \circ K) (i)$
55		elfznn	$⊢ i \in (1 \dots M) \to i \in ℕ$
56		fvco3	$⊢ (K : ℕ ⟶ T \land i \in ℕ) \to (G \circ K) (i) = G (K (i))$
57	23 55 56	syl2an	$⊢ (φ \land i \in (1 \dots M)) \to (G \circ K) (i) = G (K (i))$
58	54 57	eqtrd	$⊢ (φ \land i \in (1 \dots M)) \to ({(G \circ K) ↾}_{(1 \dots M)}) (i) = G (K (i))$
59	58	adantrr	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to ({(G \circ K) ↾}_{(1 \dots M)}) (i) = G (K (i))$
60		fvres	$⊢ j \in (1 \dots M) \to ({(G \circ K) ↾}_{(1 \dots M)}) (j) = (G \circ K) (j)$
61	60	ad2antll	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to ({(G \circ K) ↾}_{(1 \dots M)}) (j) = (G \circ K) (j)$
62		elfznn	$⊢ j \in (1 \dots M) \to j \in ℕ$
63	62	adantl	$⊢ (i \in (1 \dots M) \land j \in (1 \dots M)) \to j \in ℕ$
64		fvco3	$⊢ (K : ℕ ⟶ T \land j \in ℕ) \to (G \circ K) (j) = G (K (j))$
65	23 63 64	syl2an	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (G \circ K) (j) = G (K (j))$
66	61 65	eqtrd	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to ({(G \circ K) ↾}_{(1 \dots M)}) (j) = G (K (j))$
67	59 66	eqeq12d	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (({(G \circ K) ↾}_{(1 \dots M)}) (i) = ({(G \circ K) ↾}_{(1 \dots M)}) (j) \leftrightarrow G (K (i)) = G (K (j)))$
68		2fveq3	$⊢ G (K (i)) = G (K (j)) \to 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (j))))$
69	29	a1i	$⊢ φ \to (1 \dots M) \subseteq ℕ$
70		elfznn	$⊢ n \in (1 \dots M) \to n \in ℕ$
71	70	ad2antlr	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to n \in ℕ$
72	71	nnred	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to n \in ℝ$
73	16	ssrab3	$⊢ W \subseteq ℕ$
74	73 34	sstri	$⊢ W \subseteq ℝ$
75	73 21	sseqtri	$⊢ W \subseteq ℤ_{\geq 1}$
76		nnnfi	$⊢ \neg ℕ \in Fin$
77	6	elin2d	$⊢ φ \to U \in Fin$
78		ssfi	$⊢ (U \in Fin \land T \subseteq U) \to T \in Fin$
79	77 24 78	sylancl	$⊢ φ \to T \in Fin$
80	79	adantr	$⊢ (φ \land W = \emptyset) \to T \in Fin$
81	23	adantr	$⊢ (φ \land W = \emptyset) \to K : ℕ ⟶ T$
82		2fveq3	$⊢ K (i) = K (j) \to F (G (K (i))) = F (G (K (j)))$
83	82	fveq2d	$⊢ K (i) = K (j) \to 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (j))))$
84		simpll	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to φ$
85		simprl	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to i \in ℕ$
86		ral0	$⊢ \forall m \in \emptyset n \leq m$
87		simplr	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to W = \emptyset$
88	87	raleqdv	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to (\forall m \in W n \leq m \leftrightarrow \forall m \in \emptyset n \leq m)$
89	86 88	mpbiri	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to \forall m \in W n \leq m$
90	89	ralrimivw	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to \forall n \in ℕ \forall m \in W n \leq m$
91		rabid2	$⊢ ℕ = \{n \in ℕ \| \forall m \in W n \leq m\} \leftrightarrow \forall n \in ℕ \forall m \in W n \leq m$
92	90 91	sylibr	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to ℕ = \{n \in ℕ \| \forall m \in W n \leq m\}$
93	85 92	eleqtrd	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to i \in \{n \in ℕ \| \forall m \in W n \leq m\}$
94		simprr	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to j \in ℕ$
95	94 92	eleqtrd	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to j \in \{n \in ℕ \| \forall m \in W n \leq m\}$
96	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	ovolicc2lem3	$⊢ (φ \land (i \in \{n \in ℕ \| \forall m \in W n \leq m\} \land j \in \{n \in ℕ \| \forall m \in W n \leq m\})) \to (i = j \leftrightarrow 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (j)))))$
97	84 93 95 96	syl12anc	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to (i = j \leftrightarrow 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (j)))))$
98	83 97	syl5ibr	$⊢ ((φ \land W = \emptyset) \land (i \in ℕ \land j \in ℕ)) \to (K (i) = K (j) \to i = j)$
99	98	ralrimivva	$⊢ (φ \land W = \emptyset) \to \forall i \in ℕ \forall j \in ℕ (K (i) = K (j) \to i = j)$
100		dff13	$⊢ K : ℕ \underset{1-1}{⟶} T \leftrightarrow (K : ℕ ⟶ T \land \forall i \in ℕ \forall j \in ℕ (K (i) = K (j) \to i = j))$
101	81 99 100	sylanbrc	$⊢ (φ \land W = \emptyset) \to K : ℕ \underset{1-1}{⟶} T$
102		f1domg	$⊢ T \in Fin \to (K : ℕ \underset{1-1}{⟶} T \to ℕ ≼ T)$
103	80 101 102	sylc	$⊢ (φ \land W = \emptyset) \to ℕ ≼ T$
104		domfi	$⊢ (T \in Fin \land ℕ ≼ T) \to ℕ \in Fin$
105	79 103 104	syl2an2r	$⊢ (φ \land W = \emptyset) \to ℕ \in Fin$
106	105	ex	$⊢ φ \to (W = \emptyset \to ℕ \in Fin)$
107	106	necon3bd	$⊢ φ \to (\neg ℕ \in Fin \to W \neq \emptyset)$
108	76 107	mpi	$⊢ φ \to W \neq \emptyset$
109		infssuzcl	$⊢ (W \subseteq ℤ_{\geq 1} \land W \neq \emptyset) \to sup (W ℝ <) \in W$
110	75 108 109	sylancr	$⊢ φ \to sup (W ℝ <) \in W$
111	17 110	eqeltrid	$⊢ φ \to M \in W$
112	74 111	sselid	$⊢ φ \to M \in ℝ$
113	112	ad2antrr	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to M \in ℝ$
114	74	sseli	$⊢ m \in W \to m \in ℝ$
115	114	adantl	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to m \in ℝ$
116		elfzle2	$⊢ n \in (1 \dots M) \to n \leq M$
117	116	ad2antlr	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to n \leq M$
118		infssuzle	$⊢ (W \subseteq ℤ_{\geq 1} \land m \in W) \to sup (W ℝ <) \leq m$
119	75 118	mpan	$⊢ m \in W \to sup (W ℝ <) \leq m$
120	17 119	eqbrtrid	$⊢ m \in W \to M \leq m$
121	120	adantl	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to M \leq m$
122	72 113 115 117 121	letrd	$⊢ ((φ \land n \in (1 \dots M)) \land m \in W) \to n \leq m$
123	122	ralrimiva	$⊢ (φ \land n \in (1 \dots M)) \to \forall m \in W n \leq m$
124	69 123	ssrabdv	$⊢ φ \to (1 \dots M) \subseteq \{n \in ℕ \| \forall m \in W n \leq m\}$
125	124	adantr	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (1 \dots M) \subseteq \{n \in ℕ \| \forall m \in W n \leq m\}$
126		simprl	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to i \in (1 \dots M)$
127	125 126	sseldd	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to i \in \{n \in ℕ \| \forall m \in W n \leq m\}$
128		simprr	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to j \in (1 \dots M)$
129	125 128	sseldd	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to j \in \{n \in ℕ \| \forall m \in W n \leq m\}$
130	127 129	jca	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (i \in \{n \in ℕ \| \forall m \in W n \leq m\} \land j \in \{n \in ℕ \| \forall m \in W n \leq m\})$
131	130 96	syldan	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (i = j \leftrightarrow 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (j)))))$
132	68 131	syl5ibr	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (G (K (i)) = G (K (j)) \to i = j)$
133	67 132	sylbid	$⊢ (φ \land (i \in (1 \dots M) \land j \in (1 \dots M))) \to (({(G \circ K) ↾}_{(1 \dots M)}) (i) = ({(G \circ K) ↾}_{(1 \dots M)}) (j) \to i = j)$
134	133	ralrimivva	$⊢ φ \to \forall i \in (1 \dots M) \forall j \in (1 \dots M) (({(G \circ K) ↾}_{(1 \dots M)}) (i) = ({(G \circ K) ↾}_{(1 \dots M)}) (j) \to i = j)$
135		dff13	$⊢ ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1}{⟶} ℕ \leftrightarrow (({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) ⟶ ℕ \land \forall i \in (1 \dots M) \forall j \in (1 \dots M) (({(G \circ K) ↾}_{(1 \dots M)}) (i) = ({(G \circ K) ↾}_{(1 \dots M)}) (j) \to i = j))$
136	31 134 135	sylanbrc	$⊢ φ \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1}{⟶} ℕ$
137		f1f1orn	$⊢ ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1}{⟶} ℕ \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} ran ({(G \circ K) ↾}_{(1 \dots M)})$
138	136 137	syl	$⊢ φ \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} ran ({(G \circ K) ↾}_{(1 \dots M)})$
139		f1oeq3	$⊢ (G \circ K) [(1 \dots M)] = ran ({(G \circ K) ↾}_{(1 \dots M)}) \to (({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (G \circ K) [(1 \dots M)] \leftrightarrow ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} ran ({(G \circ K) ↾}_{(1 \dots M)}))$
140	20 139	ax-mp	$⊢ ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (G \circ K) [(1 \dots M)] \leftrightarrow ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} ran ({(G \circ K) ↾}_{(1 \dots M)})$
141	138 140	sylibr	$⊢ φ \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (G \circ K) [(1 \dots M)]$
142		f1ofo	$⊢ ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{1-1 onto}{⟶} (G \circ K) [(1 \dots M)] \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{onto}{⟶} (G \circ K) [(1 \dots M)]$
143	141 142	syl	$⊢ φ \to ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{onto}{⟶} (G \circ K) [(1 \dots M)]$
144		fofi	$⊢ ((1 \dots M) \in Fin \land ({(G \circ K) ↾}_{(1 \dots M)}) : (1 \dots M) \underset{onto}{⟶} (G \circ K) [(1 \dots M)]) \to (G \circ K) [(1 \dots M)] \in Fin$
145	52 143 144	syl2anc	$⊢ φ \to (G \circ K) [(1 \dots M)] \in Fin$
146		fimaxre2	$⊢ ((G \circ K) [(1 \dots M)] \subseteq ℝ \land (G \circ K) [(1 \dots M)] \in Fin) \to \exists x \in ℝ \forall y \in (G \circ K) [(1 \dots M)] y \leq x$
147	35 145 146	syl2anc	$⊢ φ \to \exists x \in ℝ \forall y \in (G \circ K) [(1 \dots M)] y \leq x$
148	51 147	r19.29a	$⊢ φ \to \exists z \in ℕ \forall y \in (G \circ K) [(1 \dots M)] y < z$
149	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
150	149	rexrd	$⊢ φ \to B - A \in ℝ^{*}$
151	150	adantr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to B - A \in ℝ^{*}$
152		fzfid	$⊢ φ \to (1 \dots z) \in Fin$
153		elfznn	$⊢ j \in (1 \dots z) \to j \in ℕ$
154		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
155	154	ovolfsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
156	5 155	syl	$⊢ φ \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
157	156	ffvelrnda	$⊢ (φ \land j \in ℕ) \to ((abs \circ -) \circ F) (j) \in [0, +∞)$
158	153 157	sylan2	$⊢ (φ \land j \in (1 \dots z)) \to ((abs \circ -) \circ F) (j) \in [0, +∞)$
159		elrege0	$⊢ ((abs \circ -) \circ F) (j) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ F) (j) \in ℝ \land 0 \leq ((abs \circ -) \circ F) (j))$
160	158 159	sylib	$⊢ (φ \land j \in (1 \dots z)) \to (((abs \circ -) \circ F) (j) \in ℝ \land 0 \leq ((abs \circ -) \circ F) (j))$
161	160	simpld	$⊢ (φ \land j \in (1 \dots z)) \to ((abs \circ -) \circ F) (j) \in ℝ$
162	152 161	fsumrecl	$⊢ φ \to \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j) \in ℝ$
163	162	adantr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j) \in ℝ$
164	163	rexrd	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j) \in ℝ^{*}$
165	154 4	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
166	5 165	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
167	166	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
168		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
169	167 168	sstrdi	$⊢ φ \to ran S \subseteq ℝ$
170		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
171	169 170	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
172		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
173	171 172	syl	$⊢ φ \to sup (ran S ℝ^{} <) \in ℝ^{}$
174	173	adantr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to sup (ran S ℝ^{} <) \in ℝ^{}$
175	149	adantr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to B - A \in ℝ$
176	33	sselda	$⊢ (φ \land j \in (G \circ K) [(1 \dots M)]) \to j \in ℕ$
177	168 157	sselid	$⊢ (φ \land j \in ℕ) \to ((abs \circ -) \circ F) (j) \in ℝ$
178	176 177	syldan	$⊢ (φ \land j \in (G \circ K) [(1 \dots M)]) \to ((abs \circ -) \circ F) (j) \in ℝ$
179	145 178	fsumrecl	$⊢ φ \to \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j) \in ℝ$
180	179	adantr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j) \in ℝ$
181		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
182		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{2}) \to F : ℕ ⟶ ℝ^{2}$
183	5 181 182	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{2}$
184	73 111	sselid	$⊢ φ \to M \in ℕ$
185	26 184	ffvelrnd	$⊢ φ \to K (M) \in U$
186	8 185	ffvelrnd	$⊢ φ \to G (K (M)) \in ℕ$
187	183 186	ffvelrnd	$⊢ φ \to F (G (K (M))) \in ℝ^{2}$
188		xp2nd	$⊢ F (G (K (M))) \in ℝ^{2} \to 2^{nd} (F (G (K (M)))) \in ℝ$
189	187 188	syl	$⊢ φ \to 2^{nd} (F (G (K (M)))) \in ℝ$
190	24 14	sselid	$⊢ φ \to C \in U$
191	8 190	ffvelrnd	$⊢ φ \to G (C) \in ℕ$
192	183 191	ffvelrnd	$⊢ φ \to F (G (C)) \in ℝ^{2}$
193		xp1st	$⊢ F (G (C)) \in ℝ^{2} \to 1^{st} (F (G (C))) \in ℝ$
194	192 193	syl	$⊢ φ \to 1^{st} (F (G (C))) \in ℝ$
195	189 194	resubcld	$⊢ φ \to 2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C))) \in ℝ$
196		fveq2	$⊢ j = G (K (i)) \to ((abs \circ -) \circ F) (j) = ((abs \circ -) \circ F) (G (K (i)))$
197	177	recnd	$⊢ (φ \land j \in ℕ) \to ((abs \circ -) \circ F) (j) \in ℂ$
198	176 197	syldan	$⊢ (φ \land j \in (G \circ K) [(1 \dots M)]) \to ((abs \circ -) \circ F) (j) \in ℂ$
199	196 52 141 58 198	fsumf1o	$⊢ φ \to \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j) = \sum_{i = 1}^{M} ((abs \circ -) \circ F) (G (K (i)))$
200	8	adantr	$⊢ (φ \land i \in (1 \dots M)) \to G : U ⟶ ℕ$
201		ffvelrn	$⊢ (K : ℕ ⟶ U \land i \in ℕ) \to K (i) \in U$
202	26 55 201	syl2an	$⊢ (φ \land i \in (1 \dots M)) \to K (i) \in U$
203	200 202	ffvelrnd	$⊢ (φ \land i \in (1 \dots M)) \to G (K (i)) \in ℕ$
204	154	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land G (K (i)) \in ℕ) \to ((abs \circ -) \circ F) (G (K (i))) = 2^{nd} (F (G (K (i)))) - 1^{st} (F (G (K (i))))$
205	5 203 204	syl2an2r	$⊢ (φ \land i \in (1 \dots M)) \to ((abs \circ -) \circ F) (G (K (i))) = 2^{nd} (F (G (K (i)))) - 1^{st} (F (G (K (i))))$
206	205	sumeq2dv	$⊢ φ \to \sum_{i = 1}^{M} ((abs \circ -) \circ F) (G (K (i))) = \sum_{i = 1}^{M} (2^{nd} (F (G (K (i)))) - 1^{st} (F (G (K (i)))))$
207	183	adantr	$⊢ (φ \land i \in ℕ) \to F : ℕ ⟶ ℝ^{2}$
208	8	adantr	$⊢ (φ \land i \in ℕ) \to G : U ⟶ ℕ$
209	26	ffvelrnda	$⊢ (φ \land i \in ℕ) \to K (i) \in U$
210	208 209	ffvelrnd	$⊢ (φ \land i \in ℕ) \to G (K (i)) \in ℕ$
211	207 210	ffvelrnd	$⊢ (φ \land i \in ℕ) \to F (G (K (i))) \in ℝ^{2}$
212		xp2nd	$⊢ F (G (K (i))) \in ℝ^{2} \to 2^{nd} (F (G (K (i)))) \in ℝ$
213	211 212	syl	$⊢ (φ \land i \in ℕ) \to 2^{nd} (F (G (K (i)))) \in ℝ$
214	55 213	sylan2	$⊢ (φ \land i \in (1 \dots M)) \to 2^{nd} (F (G (K (i)))) \in ℝ$
215	214	recnd	$⊢ (φ \land i \in (1 \dots M)) \to 2^{nd} (F (G (K (i)))) \in ℂ$
216	183	adantr	$⊢ (φ \land i \in (1 \dots M)) \to F : ℕ ⟶ ℝ^{2}$
217	216 203	ffvelrnd	$⊢ (φ \land i \in (1 \dots M)) \to F (G (K (i))) \in ℝ^{2}$
218		xp1st	$⊢ F (G (K (i))) \in ℝ^{2} \to 1^{st} (F (G (K (i)))) \in ℝ$
219	217 218	syl	$⊢ (φ \land i \in (1 \dots M)) \to 1^{st} (F (G (K (i)))) \in ℝ$
220	219	recnd	$⊢ (φ \land i \in (1 \dots M)) \to 1^{st} (F (G (K (i)))) \in ℂ$
221	52 215 220	fsumsub	$⊢ φ \to \sum_{i = 1}^{M} (2^{nd} (F (G (K (i)))) - 1^{st} (F (G (K (i))))) = \sum_{i = 1}^{M} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M} 1^{st} (F (G (K (i))))$
222		fzfid	$⊢ φ \to (1 \dots M - 1) \in Fin$
223		elfznn	$⊢ i \in (1 \dots M - 1) \to i \in ℕ$
224	223 213	sylan2	$⊢ (φ \land i \in (1 \dots M - 1)) \to 2^{nd} (F (G (K (i)))) \in ℝ$
225	222 224	fsumrecl	$⊢ φ \to \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) \in ℝ$
226	225	recnd	$⊢ φ \to \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) \in ℂ$
227	189	recnd	$⊢ φ \to 2^{nd} (F (G (K (M)))) \in ℂ$
228	75 111	sselid	$⊢ φ \to M \in ℤ_{\geq 1}$
229		2fveq3	$⊢ i = M \to G (K (i)) = G (K (M))$
230	229	fveq2d	$⊢ i = M \to F (G (K (i))) = F (G (K (M)))$
231	230	fveq2d	$⊢ i = M \to 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (M))))$
232	228 215 231	fsumm1	$⊢ φ \to \sum_{i = 1}^{M} 2^{nd} (F (G (K (i)))) = \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) + 2^{nd} (F (G (K (M))))$
233	226 227 232	comraddd	$⊢ φ \to \sum_{i = 1}^{M} 2^{nd} (F (G (K (i)))) = 2^{nd} (F (G (K (M)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i))))$
234		2fveq3	$⊢ i = 1 \to G (K (i)) = G (K (1))$
235	234	fveq2d	$⊢ i = 1 \to F (G (K (i))) = F (G (K (1)))$
236	235	fveq2d	$⊢ i = 1 \to 1^{st} (F (G (K (i)))) = 1^{st} (F (G (K (1))))$
237	228 220 236	fsum1p	$⊢ φ \to \sum_{i = 1}^{M} 1^{st} (F (G (K (i)))) = 1^{st} (F (G (K (1)))) + \sum_{i = 1 + 1}^{M} 1^{st} (F (G (K (i))))$
238	21 15 22 14	algr0	$⊢ φ \to K (1) = C$
239	238	fveq2d	$⊢ φ \to G (K (1)) = G (C)$
240	239	fveq2d	$⊢ φ \to F (G (K (1))) = F (G (C))$
241	240	fveq2d	$⊢ φ \to 1^{st} (F (G (K (1)))) = 1^{st} (F (G (C)))$
242	22	peano2zd	$⊢ φ \to 1 + 1 \in ℤ$
243	184	nnzd	$⊢ φ \to M \in ℤ$
244		1z	$⊢ 1 \in ℤ$
245		fzp1ss	$⊢ 1 \in ℤ \to (1 + 1 \dots M) \subseteq (1 \dots M)$
246	244 245	mp1i	$⊢ φ \to (1 + 1 \dots M) \subseteq (1 \dots M)$
247	246	sselda	$⊢ (φ \land i \in (1 + 1 \dots M)) \to i \in (1 \dots M)$
248	247 220	syldan	$⊢ (φ \land i \in (1 + 1 \dots M)) \to 1^{st} (F (G (K (i)))) \in ℂ$
249		2fveq3	$⊢ i = j + 1 \to G (K (i)) = G (K (j + 1))$
250	249	fveq2d	$⊢ i = j + 1 \to F (G (K (i))) = F (G (K (j + 1)))$
251	250	fveq2d	$⊢ i = j + 1 \to 1^{st} (F (G (K (i)))) = 1^{st} (F (G (K (j + 1))))$
252	22 242 243 248 251	fsumshftm	$⊢ φ \to \sum_{i = 1 + 1}^{M} 1^{st} (F (G (K (i)))) = \sum_{j = 1 + 1 - 1}^{M - 1} 1^{st} (F (G (K (j + 1))))$
253		ax-1cn	$⊢ 1 \in ℂ$
254	253 253	pncan3oi	$⊢ 1 + 1 - 1 = 1$
255	254	oveq1i	$⊢ (1 + 1 - 1 \dots M - 1) = (1 \dots M - 1)$
256	255	sumeq1i	$⊢ \sum_{j = 1 + 1 - 1}^{M - 1} 1^{st} (F (G (K (j + 1)))) = \sum_{j = 1}^{M - 1} 1^{st} (F (G (K (j + 1))))$
257		fvoveq1	$⊢ j = i \to K (j + 1) = K (i + 1)$
258	257	fveq2d	$⊢ j = i \to G (K (j + 1)) = G (K (i + 1))$
259	258	fveq2d	$⊢ j = i \to F (G (K (j + 1))) = F (G (K (i + 1)))$
260	259	fveq2d	$⊢ j = i \to 1^{st} (F (G (K (j + 1)))) = 1^{st} (F (G (K (i + 1))))$
261	260	cbvsumv	$⊢ \sum_{j = 1}^{M - 1} 1^{st} (F (G (K (j + 1)))) = \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
262	256 261	eqtri	$⊢ \sum_{j = 1 + 1 - 1}^{M - 1} 1^{st} (F (G (K (j + 1)))) = \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
263	252 262	eqtrdi	$⊢ φ \to \sum_{i = 1 + 1}^{M} 1^{st} (F (G (K (i)))) = \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
264	241 263	oveq12d	$⊢ φ \to 1^{st} (F (G (K (1)))) + \sum_{i = 1 + 1}^{M} 1^{st} (F (G (K (i)))) = 1^{st} (F (G (C))) + \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
265	237 264	eqtrd	$⊢ φ \to \sum_{i = 1}^{M} 1^{st} (F (G (K (i)))) = 1^{st} (F (G (C))) + \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
266	233 265	oveq12d	$⊢ φ \to \sum_{i = 1}^{M} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M} 1^{st} (F (G (K (i)))) = 2^{nd} (F (G (K (M)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - (1^{st} (F (G (C))) + \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))))$
267	194	recnd	$⊢ φ \to 1^{st} (F (G (C))) \in ℂ$
268		peano2nn	$⊢ i \in ℕ \to i + 1 \in ℕ$
269		ffvelrn	$⊢ (K : ℕ ⟶ U \land i + 1 \in ℕ) \to K (i + 1) \in U$
270	26 268 269	syl2an	$⊢ (φ \land i \in ℕ) \to K (i + 1) \in U$
271	208 270	ffvelrnd	$⊢ (φ \land i \in ℕ) \to G (K (i + 1)) \in ℕ$
272	207 271	ffvelrnd	$⊢ (φ \land i \in ℕ) \to F (G (K (i + 1))) \in ℝ^{2}$
273		xp1st	$⊢ F (G (K (i + 1))) \in ℝ^{2} \to 1^{st} (F (G (K (i + 1)))) \in ℝ$
274	272 273	syl	$⊢ (φ \land i \in ℕ) \to 1^{st} (F (G (K (i + 1)))) \in ℝ$
275	223 274	sylan2	$⊢ (φ \land i \in (1 \dots M - 1)) \to 1^{st} (F (G (K (i + 1)))) \in ℝ$
276	222 275	fsumrecl	$⊢ φ \to \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \in ℝ$
277	276	recnd	$⊢ φ \to \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \in ℂ$
278	227 226 267 277	addsub4d	$⊢ φ \to 2^{nd} (F (G (K (M)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - (1^{st} (F (G (C))) + \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))) = (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
279	221 266 278	3eqtrd	$⊢ φ \to \sum_{i = 1}^{M} (2^{nd} (F (G (K (i)))) - 1^{st} (F (G (K (i))))) = (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
280	199 206 279	3eqtrd	$⊢ φ \to \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j) = (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
281	280 179	eqeltrrd	$⊢ φ \to (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \in ℝ$
282		fveq2	$⊢ n = M \to K (n) = K (M)$
283	282	eleq2d	$⊢ n = M \to (B \in K (n) \leftrightarrow B \in K (M))$
284	283 16	elrab2	$⊢ M \in W \leftrightarrow (M \in ℕ \land B \in K (M))$
285	111 284	sylib	$⊢ φ \to (M \in ℕ \land B \in K (M))$
286	285	simprd	$⊢ φ \to B \in K (M)$
287	1 2 3 4 5 6 7 8 9	ovolicc2lem1	$⊢ (φ \land K (M) \in U) \to (B \in K (M) \leftrightarrow (B \in ℝ \land 1^{st} (F (G (K (M)))) < B \land B < 2^{nd} (F (G (K (M))))))$
288	185 287	mpdan	$⊢ φ \to (B \in K (M) \leftrightarrow (B \in ℝ \land 1^{st} (F (G (K (M)))) < B \land B < 2^{nd} (F (G (K (M))))))$
289	286 288	mpbid	$⊢ φ \to (B \in ℝ \land 1^{st} (F (G (K (M)))) < B \land B < 2^{nd} (F (G (K (M)))))$
290	289	simp3d	$⊢ φ \to B < 2^{nd} (F (G (K (M))))$
291	1 2 3 4 5 6 7 8 9	ovolicc2lem1	$⊢ (φ \land C \in U) \to (A \in C \leftrightarrow (A \in ℝ \land 1^{st} (F (G (C))) < A \land A < 2^{nd} (F (G (C)))))$
292	190 291	mpdan	$⊢ φ \to (A \in C \leftrightarrow (A \in ℝ \land 1^{st} (F (G (C))) < A \land A < 2^{nd} (F (G (C)))))$
293	13 292	mpbid	$⊢ φ \to (A \in ℝ \land 1^{st} (F (G (C))) < A \land A < 2^{nd} (F (G (C))))$
294	293	simp2d	$⊢ φ \to 1^{st} (F (G (C))) < A$
295	2 194 189 1 290 294	lt2subd	$⊢ φ \to B - A < 2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))$
296	149 195 295	ltled	$⊢ φ \to B - A \leq 2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))$
297	223	adantl	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in ℕ$
298		simpr	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in (1 \dots M - 1)$
299	243	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to M \in ℤ$
300		elfzm11	$⊢ (1 \in ℤ \land M \in ℤ) \to (i \in (1 \dots M - 1) \leftrightarrow (i \in ℤ \land 1 \leq i \land i < M))$
301	244 299 300	sylancr	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i \in (1 \dots M - 1) \leftrightarrow (i \in ℤ \land 1 \leq i \land i < M))$
302	298 301	mpbid	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i \in ℤ \land 1 \leq i \land i < M)$
303	302	simp3d	$⊢ (φ \land i \in (1 \dots M - 1)) \to i < M$
304	297	nnred	$⊢ (φ \land i \in (1 \dots M - 1)) \to i \in ℝ$
305	112	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to M \in ℝ$
306	304 305	ltnled	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i < M \leftrightarrow \neg M \leq i)$
307	303 306	mpbid	$⊢ (φ \land i \in (1 \dots M - 1)) \to \neg M \leq i$
308		infssuzle	$⊢ (W \subseteq ℤ_{\geq 1} \land i \in W) \to sup (W ℝ <) \leq i$
309	75 308	mpan	$⊢ i \in W \to sup (W ℝ <) \leq i$
310	17 309	eqbrtrid	$⊢ i \in W \to M \leq i$
311	307 310	nsyl	$⊢ (φ \land i \in (1 \dots M - 1)) \to \neg i \in W$
312	297 311	jca	$⊢ (φ \land i \in (1 \dots M - 1)) \to (i \in ℕ \land \neg i \in W)$
313	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	ovolicc2lem2	$⊢ (φ \land (i \in ℕ \land \neg i \in W)) \to 2^{nd} (F (G (K (i)))) \leq B$
314	312 313	syldan	$⊢ (φ \land i \in (1 \dots M - 1)) \to 2^{nd} (F (G (K (i)))) \leq B$
315	314	iftrued	$⊢ (φ \land i \in (1 \dots M - 1)) \to if (2^{nd} (F (G (K (i)))) \leq B, 2^{nd} (F (G (K (i)))), B) = 2^{nd} (F (G (K (i))))$
316		2fveq3	$⊢ t = K (i) \to F (G (t)) = F (G (K (i)))$
317	316	fveq2d	$⊢ t = K (i) \to 2^{nd} (F (G (t))) = 2^{nd} (F (G (K (i))))$
318	317	breq1d	$⊢ t = K (i) \to (2^{nd} (F (G (t))) \leq B \leftrightarrow 2^{nd} (F (G (K (i)))) \leq B)$
319	318 317	ifbieq1d	$⊢ t = K (i) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) = if (2^{nd} (F (G (K (i)))) \leq B, 2^{nd} (F (G (K (i)))), B)$
320		fveq2	$⊢ t = K (i) \to H (t) = H (K (i))$
321	319 320	eleq12d	$⊢ t = K (i) \to (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in H (t) \leftrightarrow if (2^{nd} (F (G (K (i)))) \leq B, 2^{nd} (F (G (K (i)))), B) \in H (K (i)))$
322	12	ralrimiva	$⊢ φ \to \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in H (t)$
323	322	adantr	$⊢ (φ \land i \in (1 \dots M - 1)) \to \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in H (t)$
324		ffvelrn	$⊢ (K : ℕ ⟶ T \land i \in ℕ) \to K (i) \in T$
325	23 223 324	syl2an	$⊢ (φ \land i \in (1 \dots M - 1)) \to K (i) \in T$
326	321 323 325	rspcdva	$⊢ (φ \land i \in (1 \dots M - 1)) \to if (2^{nd} (F (G (K (i)))) \leq B, 2^{nd} (F (G (K (i)))), B) \in H (K (i))$
327	315 326	eqeltrrd	$⊢ (φ \land i \in (1 \dots M - 1)) \to 2^{nd} (F (G (K (i)))) \in H (K (i))$
328	21 15 22 14 11	algrp1	$⊢ (φ \land i \in ℕ) \to K (i + 1) = H (K (i))$
329	223 328	sylan2	$⊢ (φ \land i \in (1 \dots M - 1)) \to K (i + 1) = H (K (i))$
330	327 329	eleqtrrd	$⊢ (φ \land i \in (1 \dots M - 1)) \to 2^{nd} (F (G (K (i)))) \in K (i + 1)$
331	223 270	sylan2	$⊢ (φ \land i \in (1 \dots M - 1)) \to K (i + 1) \in U$
332	1 2 3 4 5 6 7 8 9	ovolicc2lem1	$⊢ (φ \land K (i + 1) \in U) \to (2^{nd} (F (G (K (i)))) \in K (i + 1) \leftrightarrow (2^{nd} (F (G (K (i)))) \in ℝ \land 1^{st} (F (G (K (i + 1)))) < 2^{nd} (F (G (K (i)))) \land 2^{nd} (F (G (K (i)))) < 2^{nd} (F (G (K (i + 1))))))$
333	331 332	syldan	$⊢ (φ \land i \in (1 \dots M - 1)) \to (2^{nd} (F (G (K (i)))) \in K (i + 1) \leftrightarrow (2^{nd} (F (G (K (i)))) \in ℝ \land 1^{st} (F (G (K (i + 1)))) < 2^{nd} (F (G (K (i)))) \land 2^{nd} (F (G (K (i)))) < 2^{nd} (F (G (K (i + 1))))))$
334	330 333	mpbid	$⊢ (φ \land i \in (1 \dots M - 1)) \to (2^{nd} (F (G (K (i)))) \in ℝ \land 1^{st} (F (G (K (i + 1)))) < 2^{nd} (F (G (K (i)))) \land 2^{nd} (F (G (K (i)))) < 2^{nd} (F (G (K (i + 1)))))$
335	334	simp2d	$⊢ (φ \land i \in (1 \dots M - 1)) \to 1^{st} (F (G (K (i + 1)))) < 2^{nd} (F (G (K (i))))$
336	275 224 335	ltled	$⊢ (φ \land i \in (1 \dots M - 1)) \to 1^{st} (F (G (K (i + 1)))) \leq 2^{nd} (F (G (K (i))))$
337	222 275 224 336	fsumle	$⊢ φ \to \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \leq \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i))))$
338	225 276	subge0d	$⊢ φ \to (0 \leq \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \leftrightarrow \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \leq \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))))$
339	337 338	mpbird	$⊢ φ \to 0 \leq \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
340	225 276	resubcld	$⊢ φ \to \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \in ℝ$
341	195 340	addge01d	$⊢ φ \to (0 \leq \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))) \leftrightarrow 2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C))) \leq (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1)))))$
342	339 341	mpbid	$⊢ φ \to 2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C))) \leq (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
343	149 195 281 296 342	letrd	$⊢ φ \to B - A \leq (2^{nd} (F (G (K (M)))) - 1^{st} (F (G (C)))) + \sum_{i = 1}^{M - 1} 2^{nd} (F (G (K (i)))) - \sum_{i = 1}^{M - 1} 1^{st} (F (G (K (i + 1))))$
344	343 280	breqtrrd	$⊢ φ \to B - A \leq \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j)$
345	344	adantr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to B - A \leq \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j)$
346		fzfid	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to (1 \dots z) \in Fin$
347	161	adantlr	$⊢ ((φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \land j \in (1 \dots z)) \to ((abs \circ -) \circ F) (j) \in ℝ$
348	160	simprd	$⊢ (φ \land j \in (1 \dots z)) \to 0 \leq ((abs \circ -) \circ F) (j)$
349	348	adantlr	$⊢ ((φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \land j \in (1 \dots z)) \to 0 \leq ((abs \circ -) \circ F) (j)$
350	33	adantr	$⊢ (φ \land z \in ℕ) \to (G \circ K) [(1 \dots M)] \subseteq ℕ$
351	350	sselda	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to y \in ℕ$
352	351	nnred	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to y \in ℝ$
353	40	ad2antlr	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to z \in ℝ$
354		ltle	$⊢ (y \in ℝ \land z \in ℝ) \to (y < z \to y \leq z)$
355	352 353 354	syl2anc	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to (y < z \to y \leq z)$
356	351 21	eleqtrdi	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to y \in ℤ_{\geq 1}$
357		nnz	$⊢ z \in ℕ \to z \in ℤ$
358	357	ad2antlr	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to z \in ℤ$
359		elfz5	$⊢ (y \in ℤ_{\geq 1} \land z \in ℤ) \to (y \in (1 \dots z) \leftrightarrow y \leq z)$
360	356 358 359	syl2anc	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to (y \in (1 \dots z) \leftrightarrow y \leq z)$
361	355 360	sylibrd	$⊢ ((φ \land z \in ℕ) \land y \in (G \circ K) [(1 \dots M)]) \to (y < z \to y \in (1 \dots z))$
362	361	ralimdva	$⊢ (φ \land z \in ℕ) \to (\forall y \in (G \circ K) [(1 \dots M)] y < z \to \forall y \in (G \circ K) [(1 \dots M)] y \in (1 \dots z))$
363	362	impr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \forall y \in (G \circ K) [(1 \dots M)] y \in (1 \dots z)$
364		dfss3	$⊢ (G \circ K) [(1 \dots M)] \subseteq (1 \dots z) \leftrightarrow \forall y \in (G \circ K) [(1 \dots M)] y \in (1 \dots z)$
365	363 364	sylibr	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to (G \circ K) [(1 \dots M)] \subseteq (1 \dots z)$
366	346 347 349 365	fsumless	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j \in (G \circ K) [(1 \dots M)]} ((abs \circ -) \circ F) (j) \leq \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j)$
367	175 180 163 345 366	letrd	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to B - A \leq \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j)$
368		eqidd	$⊢ ((φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \land j \in (1 \dots z)) \to ((abs \circ -) \circ F) (j) = ((abs \circ -) \circ F) (j)$
369		simprl	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to z \in ℕ$
370	369 21	eleqtrdi	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to z \in ℤ_{\geq 1}$
371	347	recnd	$⊢ ((φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \land j \in (1 \dots z)) \to ((abs \circ -) \circ F) (j) \in ℂ$
372	368 370 371	fsumser	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j) = seq 1 (+ ((abs \circ -) \circ F)) (z)$
373	4	fveq1i	$⊢ S (z) = seq 1 (+ ((abs \circ -) \circ F)) (z)$
374	372 373	eqtr4di	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j) = S (z)$
375	166	ffnd	$⊢ φ \to S Fn ℕ$
376		fnfvelrn	$⊢ (S Fn ℕ \land z \in ℕ) \to S (z) \in ran S$
377	375 369 376	syl2an2r	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to S (z) \in ran S$
378		supxrub	$⊢ (ran S \subseteq ℝ^{} \land S (z) \in ran S) \to S (z) \leq sup (ran S ℝ^{} <)$
379	171 377 378	syl2an2r	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to S (z) \leq sup (ran S ℝ^{*} <)$
380	374 379	eqbrtrd	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to \sum_{j = 1}^{z} ((abs \circ -) \circ F) (j) \leq sup (ran S ℝ^{*} <)$
381	151 164 174 367 380	xrletrd	$⊢ (φ \land (z \in ℕ \land \forall y \in (G \circ K) [(1 \dots M)] y < z)) \to B - A \leq sup (ran S ℝ^{*} <)$
382	148 381	rexlimddv	$⊢ φ \to B - A \leq sup (ran S ℝ^{*} <)$

Metamath Proof Explorer

Theorem ovolicc2lem4

Proof