Theorem ovolicc2lem4 25896

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

Hypotheses

Ref	Expression
ovolicc.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ovolicc.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ovolicc.3	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ovolicc2.4	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolicc2.5	⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovolicc2.6	⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
ovolicc2.7	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)
ovolicc2.8	⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
ovolicc2.9	⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
ovolicc2.10	⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
ovolicc2.11	⊢ (𝜑 → 𝐻:𝑇⟶𝑇)
ovolicc2.12	⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
ovolicc2.13	⊢ (𝜑 → 𝐴 ∈ 𝐶)
ovolicc2.14	⊢ (𝜑 → 𝐶 ∈ 𝑇)
ovolicc2.15	⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
ovolicc2.16	⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}
ovolicc2.17	⊢ 𝑀 = inf(𝑊, ℝ, < )

Assertion

Ref	Expression
ovolicc2lem4	⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))

Distinct variable groups:   𝑡,𝑛,𝑢,𝐴   𝐵,𝑛,𝑡,𝑢   𝑡,𝐻   𝐶,𝑛,𝑡   𝑛,𝐹,𝑡   𝑛,𝐾,𝑡,𝑢   𝑛,𝐺,𝑡   𝑛,𝑀,𝑡   𝑛,𝑊   𝜑,𝑛,𝑡   𝑇,𝑛,𝑡   𝑈,𝑛,𝑡,𝑢

Allowed substitution hints:   𝜑(𝑢)   𝐶(𝑢)   𝑆(𝑢, 𝑡, 𝑛)   𝑇(𝑢)   𝐹(𝑢)   𝐺(𝑢)   𝐻(𝑢, 𝑛)   𝑀(𝑢)   𝑊(𝑢, 𝑡)

Proof of Theorem ovolicc2lem4

Dummy variables 𝑚 𝑥 𝑦 𝑧 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		arch 12643	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
2	1	ad2antlr 740	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3		df-ima 5671	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀))
4		ovolicc2.8	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
5		nnuz 13044	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ≥‘1)
6		ovolicc2.15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7		1zzd 12767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
8		ovolicc2.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ 𝑇)
9		ovolicc2.11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)
10	5, 6, 7, 8, 9	algrf 16792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾:ℕ⟶𝑇)
11		ovolicc2.10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12	11	ssrab3 4010	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑇 ⊆ 𝑈
13		fss 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈)
14	10, 12, 13	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾:ℕ⟶𝑈)
15		fco 6764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺 ∘ 𝐾):ℕ⟶ℕ)
16	4, 14, 15	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 ∘ 𝐾):ℕ⟶ℕ)
17		fz1ssnn 13729	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑀) ⊆ ℕ
18		fssres 6778	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∘ 𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
19	16, 17, 18	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
20	19	frnd 6748	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ)
21	3, 20	eqsstrid 3951	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ)
22		nnssre 12379	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℝ
23	21, 22	sstrdi 3925	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ)
24	23	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ)
25		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀)))
26	24, 25	sseldd 3914	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
27		simpllr 788	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
28		nnre 12382	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
29	28	ad2antlr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
30		lelttr 11439	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧))
31	26, 27, 29, 30	syl3anc 1399	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧))
32	31	ancomsd 471	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥) → 𝑦 < 𝑧))
33	32	expdimp 458	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧))
34	33	an32s 665	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧))
35	34	ralimdva 3178	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
36	35	impancom 457	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
37	36	an32s 665	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
38	37	reximdva 3179	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
39	2, 38	mpd 16	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)
40		fzfid 14156	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
41		fvres 6935	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖))
42	41	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖))
43		elfznn 13727	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
44		fvco3 7016	. . . . . . . . . . . . . . 15 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖)))
45	10, 43, 44	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖)))
46	42, 45	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖)))
47	46	adantrr 730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖)))
48		fvres 6935	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗))
49	48	ad2antll 742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗))
50		elfznn 13727	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
51	50	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
52		fvco3 7016	. . . . . . . . . . . . . 14 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑗 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗)))
53	10, 51, 52	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗)))
54	49, 53	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾‘𝑗)))
55	47, 54	eqeq12d 2779	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗))))
56		2fveq3 6921	. . . . . . . . . . . 12 ⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))
57	17	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑀) ⊆ ℕ)
58		elfznn 13727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
59	58	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℕ)
60	59	nnred 12390	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℝ)
61		ovolicc2.16	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}
62	61	ssrab3 4010	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑊 ⊆ ℕ
63	62, 22	sstri 3922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑊 ⊆ ℝ
64		ovolicc2.17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑀 = inf(𝑊, ℝ, < )
65	62, 5	sseqtri 3961	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑊 ⊆ (ℤ≥‘1)
66		nnnfi 14149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ℕ ∈ Fin
67		ovolicc2.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
68	67	elin2d 4105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑈 ∈ Fin)
69		ssfi 9226	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin)
70	68, 12, 69	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ Fin)
71	70	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑇 ∈ Fin)
72	10	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
73		2fveq3 6921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗))))
74	73	fveq2d 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))
75		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
76		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
77		ral0 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚
78		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
79	78	raleqdv 3323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚))
80	77, 79	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
81	80	ralrimivw 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
82		rabid2 3448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
83	81, 82	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
84	76, 83	eleqtrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
85		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
86	85, 83	eleqtrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
87		ovolicc.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐴 ∈ ℝ)
88		ovolicc.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐵 ∈ ℝ)
89		ovolicc.3	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
90		ovolicc2.4	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
91		ovolicc2.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
92		ovolicc2.7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)
93		ovolicc2.9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)
94		ovolicc2.12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
95		ovolicc2.13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
96	87, 88, 89, 90, 91, 67, 92, 4, 93, 11, 9, 94, 95, 8, 6, 61	ovolicc2lem3 25895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
97	75, 84, 86, 96	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
98	74, 97	imbitrrid 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))
99	98	ralrimivva 3209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))
100		dff13 7289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐾:ℕ⟶1-1𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)))
101	72, 99, 100	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶1-1𝑇)
102		f1domg 9036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑇 ∈ Fin → (𝐾:ℕ⟶1-1𝑇 → ℕ ≼ 𝑇))
103	71, 101, 102	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ≼ 𝑇)
104		domfi 9242	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
105	70, 103, 104	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ∈ Fin)
106	105	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
107	106	necon3bd 2973	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
108	66, 107	mpi 21	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑊 ≠ ∅)
109		infssuzcl 13099	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ⊆ (ℤ≥‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
110	65, 108, 109	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
111	64, 110	eqeltrid 2868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ 𝑊)
112	63, 111	sselid 3911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℝ)
113	112	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℝ)
114	63	sseli 3909	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ)
115	114	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ)
116		elfzle2 13701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ≤ 𝑀)
117	116	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑀)
118		infssuzle 13098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ⊆ (ℤ≥‘1) ∧ 𝑚 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
119	65, 118	mpan 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
120	64, 119	eqbrtrid 5146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚)
121	120	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ≤ 𝑚)
122	60, 113, 115, 117, 121	letrd 11506	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑚)
123	122	ralrimiva 3158	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
124	57, 123	ssrabdv 4001	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
125	124	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
126		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
127	125, 126	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
128		simprr 785	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
129	125, 128	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
130	127, 129	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}))
131	130, 96	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
132	56, 131	imbitrrid 249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → 𝑖 = 𝑗))
133	55, 132	sylbid 243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
134	133	ralrimivva 3209	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
135		dff13 7289	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ℕ ↔ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
136	19, 134, 135	sylanbrc 595	. . . . . . . 8 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ℕ)
137		f1f1orn 6866	. . . . . . . 8 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ℕ → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ontoran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
138	136, 137	syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ontoran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
139		f1oeq3 6844	. . . . . . . 8 ⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1onto((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ontoran ((𝐺 ∘ 𝐾) ↾ (1...𝑀))))
140	3, 139	ax-mp 5	. . . . . . 7 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1onto((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1ontoran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
141	138, 140	sylibr 237	. . . . . 6 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1onto((𝐺 ∘ 𝐾) “ (1...𝑀)))
142		f1ofo 6862	. . . . . 6 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶1-1onto((𝐺 ∘ 𝐾) “ (1...𝑀)) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶onto((𝐺 ∘ 𝐾) “ (1...𝑀)))
143	141, 142	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶onto((𝐺 ∘ 𝐾) “ (1...𝑀)))
144		fofi 9343	. . . . 5 ⊢ (((1...𝑀) ∈ Fin ∧ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶onto((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin)
145	40, 143, 144	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin)
146		fimaxre2 12302	. . . 4 ⊢ ((((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥)
147	23, 145, 146	syl2anc 596	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥)
148	39, 147	r19.29a 3174	. 2 ⊢ (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)
149	88, 87	resubcld 11783	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
150	149	rexrd 11398	. . . 4 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ*)
151	150	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ*)
152		fzfid 14156	. . . . . 6 ⊢ (𝜑 → (1...𝑧) ∈ Fin)
153		elfznn 13727	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
154		eqid 2763	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
155	154	ovolfsf 25847	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
156	91, 155	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
157	156	ffvelcdmda 7116	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
158	153, 157	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
159		elrege0 13625	. . . . . . . 8 ⊢ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
160	158, 159	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
161	160	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
162	152, 161	fsumrecl 15944	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
163	162	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
164	163	rexrd 11398	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
165	154, 90	ovolsf 25848	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
166	91, 165	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
167	166	frnd 6748	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
168		rge0ssre 13627	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ
169	167, 168	sstrdi 3925	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
170		ressxr 11392	. . . . . 6 ⊢ ℝ ⊆ ℝ*
171	169, 170	sstrdi 3925	. . . . 5 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
172		supxrcl 13485	. . . . 5 ⊢ (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
173	171, 172	syl 18	. . . 4 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
174	173	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
175	149	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ)
176	21	sselda 3913	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
177	168, 157	sselid 3911	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
178	176, 177	syldan 603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
179	145, 178	fsumrecl 15944	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
180	179	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
181		inss2 4137	. . . . . . . . . . 11 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
182		fss 6756	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
183	91, 181, 182	sylancl 598	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
184	62, 111	sselid 3911	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
185	14, 184	ffvelcdmd 7117	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝑀) ∈ 𝑈)
186	4, 185	ffvelcdmd 7117	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘(𝐾‘𝑀)) ∈ ℕ)
187	183, 186	ffvelcdmd 7117	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ))
188		xp2nd 8068	. . . . . . . . 9 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ)
189	187, 188	syl 18	. . . . . . . 8 ⊢ (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ)
190	12, 8	sselid 3911	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ 𝑈)
191	4, 190	ffvelcdmd 7117	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℕ)
192	183, 191	ffvelcdmd 7117	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ))
193		xp1st 8067	. . . . . . . . 9 ⊢ ((𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ)
194	192, 193	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ)
195	189, 194	resubcld 11783	. . . . . . 7 ⊢ (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ∈ ℝ)
196		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘(𝐾‘𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))))
197	177	recnd 11376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
198	176, 197	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
199	196, 40, 141, 46, 198	fsumf1o 15933	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))))
200	4	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
201		ffvelcdm 7113	. . . . . . . . . . . . 13 ⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈)
202	14, 43, 201	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝑈)
203	200, 202	ffvelcdmd 7117	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ)
204	154	ovolfsval 25846	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾‘𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
205	91, 203, 204	syl2an2r 698	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
206	205	sumeq2dv 15913	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
207	183	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
208	4	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
209	14	ffvelcdmda 7116	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈)
210	208, 209	ffvelcdmd 7117	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ)
211	207, 210	ffvelcdmd 7117	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ))
212		xp2nd 8068	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
213	211, 212	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
214	43, 213	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
215	214	recnd 11376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
216	183	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
217	216, 203	ffvelcdmd 7117	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ))
218		xp1st 8067	. . . . . . . . . . . . 13 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
219	217, 218	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
220	219	recnd 11376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
221	40, 215, 220	fsumsub 15998	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
222		fzfid 14156	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
223		elfznn 13727	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
224	223, 213	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
225	222, 224	fsumrecl 15944	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
226	225	recnd 11376	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
227	189	recnd 11376	. . . . . . . . . . . 12 ⊢ (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℂ)
228	65, 111	sselid 3911	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
229		2fveq3 6921	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑀 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑀)))
230	229	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑀))))
231	230	fveq2d 6920	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))
232	228, 215, 231	fsumm1 15961	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))
233	226, 227, 232	comraddd 11563	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
234		2fveq3 6921	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘1)))
235	234	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
236	235	fveq2d 6920	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
237	228, 220, 236	fsum1p 15963	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
238	5, 6, 7, 8	algr0 16791	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾‘1) = 𝐶)
239	238	fveq2d 6920	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺‘𝐶))
240	239	fveq2d 6920	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺‘𝐶)))
241	240	fveq2d 6920	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺‘𝐶))))
242	7	peano2zd 12846	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 + 1) ∈ ℤ)
243	184	nnzd 12759	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℤ)
244		1z 12766	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℤ
245		fzp1ss 13749	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
246	244, 245	mp1i 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
247	246	sselda 3913	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
248	247, 220	syldan 603	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
249		2fveq3 6921	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
250	249	fveq2d 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
251	250	fveq2d 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
252	7, 242, 243, 248, 251	fsumshftm 15991	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
253		ax-1cn 11297	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
254	253, 253	pncan3oi 11612	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + 1) − 1) = 1
255	254	oveq1i 7461	. . . . . . . . . . . . . . . 16 ⊢ (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
256	255	sumeq1i 15908	. . . . . . . . . . . . . . 15 ⊢ Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
257		fvoveq1 7474	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
258	257	fveq2d 6920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
259	258	fveq2d 6920	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
260	259	fveq2d 6920	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
261	260	cbvsumv 15907	. . . . . . . . . . . . . . 15 ⊢ Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
262	256, 261	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
263	252, 262	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
264	241, 263	oveq12d 7469	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
265	237, 264	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
266	233, 265	oveq12d 7469	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
267	194	recnd 11376	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℂ)
268		peano2nn 12387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
269		ffvelcdm 7113	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
270	14, 268, 269	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
271	208, 270	ffvelcdmd 7117	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
272	207, 271	ffvelcdmd 7117	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
273		xp1st 8067	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
274	272, 273	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
275	223, 274	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
276	222, 275	fsumrecl 15944	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
277	276	recnd 11376	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
278	227, 226, 267, 277	addsub4d 11755	. . . . . . . . . 10 ⊢ (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
279	221, 266, 278	3eqtrd 2802	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
280	199, 206, 279	3eqtrd 2802	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
281	280, 179	eqeltrrd 2865	. . . . . . 7 ⊢ (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
282		fveq2 6916	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑀 → (𝐾‘𝑛) = (𝐾‘𝑀))
283	282	eleq2d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑀 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑀)))
284	283, 61	elrab2 3652	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ 𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀)))
285	111, 284	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀)))
286	285	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ (𝐾‘𝑀))
287	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25893	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐾‘𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))))
288	185, 287	mpdan 700	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))))
289	286, 288	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))
290	289	simp3d 1162	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))
291	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25893	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑈) → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶))))))
292	190, 291	mpdan 700	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶))))))
293	95, 292	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))
294	293	simp2d 1161	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴)
295	88, 194, 189, 87, 290, 294	lt2subd 11980	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))))
296	149, 195, 295	ltled 11497	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))))
297	223	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
298		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
299	243	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
300		elfzm11 13769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
301	244, 299, 300	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
302	298, 301	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))
303	302	simp3d 1162	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
304	297	nnred 12390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
305	112	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
306	304, 305	ltnled 11496	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖))
307	303, 306	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ≤ 𝑖)
308		infssuzle 13098	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ⊆ (ℤ≥‘1) ∧ 𝑖 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
309	65, 308	mpan 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
310	64, 309	eqbrtrid 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑊 → 𝑀 ≤ 𝑖)
311	307, 310	nsyl 141	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖 ∈ 𝑊)
312	297, 311	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊))
313	87, 88, 89, 90, 91, 67, 92, 4, 93, 11, 9, 94, 95, 8, 6, 61	ovolicc2lem2 25894	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)
314	312, 313	syldan 603	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)
315	314	iftrued 4493	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
316		2fveq3 6921	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (𝐾‘𝑖) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑖))))
317	316	fveq2d 6920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (𝐾‘𝑖) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
318	317	breq1d 5118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (𝐾‘𝑖) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵))
319	318, 317	ifbieq1d 4510	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (𝐾‘𝑖) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵))
320		fveq2 6916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (𝐾‘𝑖) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑖)))
321	319, 320	eleq12d 2858	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (𝐾‘𝑖) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖))))
322	94	ralrimiva 3158	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
323	322	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
324		ffvelcdm 7113	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑇)
325	10, 223, 324	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘𝑖) ∈ 𝑇)
326	321, 323, 325	rspcdva 3581	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))
327	315, 326	eqeltrrd 2865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐻‘(𝐾‘𝑖)))
328	5, 6, 7, 8, 9	algrp1 16793	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖)))
329	223, 328	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖)))
330	327, 329	eleqtrrd 2867	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
331	223, 270	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
332	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
333	331, 332	syldan 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
334	330, 333	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
335	334	simp2d 1161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
336	275, 224, 335	ltled 11497	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
337	222, 275, 224, 336	fsumle 16010	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
338	225, 276	subge0d 11946	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
339	337, 338	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
340	225, 276	resubcld 11783	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
341	195, 340	addge01d 11944	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))))
342	339, 341	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
343	149, 195, 281, 296, 342	letrd 11506	. . . . . 6 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
344	343, 280	breqtrrd 5139	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
345	344	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
346		fzfid 14156	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
347	161	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
348	160	simprd 501	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
349	348	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
350	21	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ)
351	350	sselda 3913	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
352	351	nnred 12390	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
353	28	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
354		ltle 11437	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧))
355	352, 353, 354	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧))
356	351, 5	eleqtrdi 2874	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ≥‘1))
357		nnz 12754	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
358	357	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
359		elfz5 13688	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ≥‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧))
360	356, 358, 359	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧))
361	355, 360	sylibrd 262	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ∈ (1...𝑧)))
362	361	ralimdva 3178	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
363	362	impr 460	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
364		dfss3 3902	. . . . . 6 ⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
365	363, 364	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
366	346, 347, 349, 365	fsumless 16007	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
367	175, 180, 163, 345, 366	letrd 11506	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
368		eqidd 2764	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
369		simprl 783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
370	369, 5	eleqtrdi 2874	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ≥‘1))
371	347	recnd 11376	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
372	368, 370, 371	fsumser 15940	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
373	90	fveq1i 6917	. . . . 5 ⊢ (𝑆‘𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
374	372, 373	eqtr4di 2816	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆‘𝑧))
375	166	ffnd 6740	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
376		fnfvelrn 7112	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆‘𝑧) ∈ ran 𝑆)
377	375, 369, 376	syl2an2r 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ∈ ran 𝑆)
378		supxrub 13494	. . . . 5 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘𝑧) ∈ ran 𝑆) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
379	171, 377, 378	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
380	374, 379	eqbrtrd 5133	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
381	151, 164, 174, 367, 380	xrletrd 13331	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
382	148, 381	rexlimddv 3173	1 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  ifcif 4485  𝒫 cpw 4560  {csn 4588  ∪ cuni 4872   class class class wbr 5108   × cxp 5656  ran crn 5659   ↾ cres 5660   “ cima 5661   ∘ ccom 5662   Fn wfn 6561  ⟶wf 6562  ⟶1-1wf1 6563  ⟶ontowfo 6564  ⟶1-1ontowf1o 6565  ‘cfv 6566  (class class class)co 7451  1^st c1st 8033  2^nd c2nd 8034   ≼ cdom 9009  Fincfn 9011  supcsup 9469  infcinf 9470  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240   + caddc 11242  +∞cpnf 11379  ℝ^*cxr 11381   < clt 11382   ≤ cle 11383   − cmin 11580  ℕcn 12375  ℤcz 12733  ℤ_≥cuz 13005  (,)cioo 13516  [,)cico 13518  [,]cicc 13519  ...cfz 13679  seqcseq 14184  abscabs 15444  Σcsu 15897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-1st 8035  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-sup 9471  df-inf 9472  df-oi 9541  df-card 10057  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-nn 12376  df-2 12445  df-3 12446  df-n0 12647  df-z 12734  df-uz 13006  df-rp 13161  df-ioo 13520  df-ico 13522  df-icc 13523  df-fz 13680  df-fzo 13829  df-seq 14185  df-exp 14245  df-hash 14516  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-clim 15699  df-sum 15898

This theorem is used by:  ovolicc2lem5  25897