Theorem ovolicc2lem4 25841

Description: Lemma for ovolicc2 25843. (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 12603	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
2	1	ad2antlr 740	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3		df-ima 5664	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀))
4		ovolicc2.8	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
5		nnuz 13004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ≥‘1)
6		ovolicc2.15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7		1zzd 12727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
8		ovolicc2.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ 𝑇)
9		ovolicc2.11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)
10	5, 6, 7, 8, 9	algrf 16748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾:ℕ⟶𝑇)
11		ovolicc2.10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12	11	ssrab3 4030	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑇 ⊆ 𝑈
13		fss 6726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈)
14	10, 12, 13	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾:ℕ⟶𝑈)
15		fco 6734	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺 ∘ 𝐾):ℕ⟶ℕ)
16	4, 14, 15	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 ∘ 𝐾):ℕ⟶ℕ)
17		fz1ssnn 13689	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑀) ⊆ ℕ
18		fssres 6748	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∘ 𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
19	16, 17, 18	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
20	19	frnd 6718	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ)
21	3, 20	eqsstrid 3969	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ)
22		nnssre 12339	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℝ
23	21, 22	sstrdi 3943	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ)
24	23	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ)
25		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀)))
26	24, 25	sseldd 3932	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
27		simpllr 788	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
28		nnre 12342	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
29	28	ad2antlr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
30		lelttr 11400	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧))
31	26, 27, 29, 30	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧))
32	31	ancomsd 471	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥) → 𝑦 < 𝑧))
33	32	expdimp 458	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧))
34	33	an32s 665	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧))
35	34	ralimdva 3175	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
36	35	impancom 457	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
37	36	an32s 665	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
38	37	reximdva 3176	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
39	2, 38	mpd 16	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)
40		fzfid 14116	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
41		fvres 6904	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖))
42	41	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖))
43		elfznn 13687	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
44		fvco3 6985	. . . . . . . . . . . . . . 15 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖)))
45	10, 43, 44	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖)))
46	42, 45	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖)))
47	46	adantrr 730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖)))
48		fvres 6904	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗))
49	48	ad2antll 742	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗))
50		elfznn 13687	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
51	50	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
52		fvco3 6985	. . . . . . . . . . . . . 14 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑗 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗)))
53	10, 51, 52	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗)))
54	49, 53	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾‘𝑗)))
55	47, 54	eqeq12d 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗))))
56		2fveq3 6890	. . . . . . . . . . . 12 ⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))
57	17	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑀) ⊆ ℕ)
58		elfznn 13687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
59	58	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℕ)
60	59	nnred 12350	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℝ)
61		ovolicc2.16	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}
62	61	ssrab3 4030	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑊 ⊆ ℕ
63	62, 22	sstri 3940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑊 ⊆ ℝ
64		ovolicc2.17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑀 = inf(𝑊, ℝ, < )
65	62, 5	sseqtri 3979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑊 ⊆ (ℤ≥‘1)
66		nnnfi 14109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ℕ ∈ Fin
67		ovolicc2.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
68	67	elin2d 4151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑈 ∈ Fin)
69		ssfi 9188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin)
70	68, 12, 69	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ Fin)
71	70	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑇 ∈ Fin)
72	10	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
73		2fveq3 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗))))
74	73	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))
75		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
76		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
77		ral0 4454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚
78		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
79	78	raleqdv 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚))
80	77, 79	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
81	80	ralrimivw 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
82		rabid2 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
83	81, 82	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
84	76, 83	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
85		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
86	85, 83	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 25840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
97	75, 84, 86, 96	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
98	74, 97	imbitrrid 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))
99	98	ralrimivva 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))
100		dff13 7258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐾:ℕ–1-1→𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)))
101	72, 99, 100	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ–1-1→𝑇)
102		f1domg 8998	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑇 ∈ Fin → (𝐾:ℕ–1-1→𝑇 → ℕ ≼ 𝑇))
103	71, 101, 102	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ≼ 𝑇)
104		domfi 9204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
105	70, 103, 104	syl2an2r 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ∈ Fin)
106	105	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
107	106	necon3bd 2970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
108	66, 107	mpi 21	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑊 ≠ ∅)
109		infssuzcl 13059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ⊆ (ℤ≥‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
110	65, 108, 109	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
111	64, 110	eqeltrid 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ 𝑊)
112	63, 111	sselid 3929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℝ)
113	112	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℝ)
114	63	sseli 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ)
115	114	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ)
116		elfzle2 13661	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ≤ 𝑀)
117	116	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑀)
118		infssuzle 13058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ⊆ (ℤ≥‘1) ∧ 𝑚 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
119	65, 118	mpan 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
120	64, 119	eqbrtrid 5140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚)
121	120	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ≤ 𝑚)
122	60, 113, 115, 117, 121	letrd 11467	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑚)
123	122	ralrimiva 3155	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
124	57, 123	ssrabdv 4021	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
125	124	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
126		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
127	125, 126	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
128		simprr 785	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
129	125, 128	sseldd 3932	. . . . . . . . . . . . . 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 3206	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
135		dff13 7258	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
136	19, 134, 135	sylanbrc 595	. . . . . . . 8 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
137		f1f1orn 6836	. . . . . . . 8 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
138	136, 137	syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
139		f1oeq3 6814	. . . . . . . 8 ⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀))))
140	3, 139	ax-mp 5	. . . . . . 7 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
141	138, 140	sylibr 237	. . . . . 6 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)))
142		f1ofo 6832	. . . . . 6 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀)))
143	141, 142	syl 18	. . . . 5 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀)))
144		fofi 9305	. . . . 5 ⊢ (((1...𝑀) ∈ Fin ∧ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin)
145	40, 143, 144	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin)
146		fimaxre2 12262	. . . 4 ⊢ ((((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥)
147	23, 145, 146	syl2anc 596	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥)
148	39, 147	r19.29a 3171	. 2 ⊢ (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)
149	88, 87	resubcld 11744	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
150	149	rexrd 11359	. . . 4 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ*)
151	150	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ*)
152		fzfid 14116	. . . . . 6 ⊢ (𝜑 → (1...𝑧) ∈ Fin)
153		elfznn 13687	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
154		eqid 2761	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
155	154	ovolfsf 25792	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
156	91, 155	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
157	156	ffvelcdmda 7084	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
158	153, 157	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
159		elrege0 13585	. . . . . . . 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 15900	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
163	162	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
164	163	rexrd 11359	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
165	154, 90	ovolsf 25793	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
166	91, 165	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
167	166	frnd 6718	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
168		rge0ssre 13587	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ
169	167, 168	sstrdi 3943	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
170		ressxr 11353	. . . . . 6 ⊢ ℝ ⊆ ℝ*
171	169, 170	sstrdi 3943	. . . . 5 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
172		supxrcl 13445	. . . . 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 3931	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
177	168, 157	sselid 3929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
178	176, 177	syldan 603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
179	145, 178	fsumrecl 15900	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
180	179	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
181		inss2 4183	. . . . . . . . . . 11 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
182		fss 6726	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
183	91, 181, 182	sylancl 598	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
184	62, 111	sselid 3929	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
185	14, 184	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝑀) ∈ 𝑈)
186	4, 185	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘(𝐾‘𝑀)) ∈ ℕ)
187	183, 186	ffvelcdmd 7085	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ))
188		xp2nd 8034	. . . . . . . . 9 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ)
189	187, 188	syl 18	. . . . . . . 8 ⊢ (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ)
190	12, 8	sselid 3929	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ 𝑈)
191	4, 190	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℕ)
192	183, 191	ffvelcdmd 7085	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ))
193		xp1st 8033	. . . . . . . . 9 ⊢ ((𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ)
194	192, 193	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ)
195	189, 194	resubcld 11744	. . . . . . 7 ⊢ (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ∈ ℝ)
196		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘(𝐾‘𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))))
197	177	recnd 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
198	176, 197	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
199	196, 40, 141, 46, 198	fsumf1o 15889	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))))
200	4	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
201		ffvelcdm 7081	. . . . . . . . . . . . 13 ⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈)
202	14, 43, 201	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝑈)
203	200, 202	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ)
204	154	ovolfsval 25791	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾‘𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
205	91, 203, 204	syl2an2r 698	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
206	205	sumeq2dv 15869	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
207	183	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
208	4	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
209	14	ffvelcdmda 7084	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈)
210	208, 209	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ)
211	207, 210	ffvelcdmd 7085	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ))
212		xp2nd 8034	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
213	211, 212	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
214	43, 213	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
215	214	recnd 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
216	183	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
217	216, 203	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ))
218		xp1st 8033	. . . . . . . . . . . . 13 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
219	217, 218	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
220	219	recnd 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
221	40, 215, 220	fsumsub 15954	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
222		fzfid 14116	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
223		elfznn 13687	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
224	223, 213	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
225	222, 224	fsumrecl 15900	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
226	225	recnd 11337	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
227	189	recnd 11337	. . . . . . . . . . . 12 ⊢ (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℂ)
228	65, 111	sselid 3929	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
229		2fveq3 6890	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑀 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑀)))
230	229	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑀))))
231	230	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))
232	228, 215, 231	fsumm1 15917	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))
233	226, 227, 232	comraddd 11524	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
234		2fveq3 6890	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘1)))
235	234	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
236	235	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
237	228, 220, 236	fsum1p 15919	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
238	5, 6, 7, 8	algr0 16747	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾‘1) = 𝐶)
239	238	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺‘𝐶))
240	239	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺‘𝐶)))
241	240	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺‘𝐶))))
242	7	peano2zd 12806	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 + 1) ∈ ℤ)
243	184	nnzd 12719	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℤ)
244		1z 12726	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℤ
245		fzp1ss 13709	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
246	244, 245	mp1i 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
247	246	sselda 3931	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
248	247, 220	syldan 603	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
249		2fveq3 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
250	249	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
251	250	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
252	7, 242, 243, 248, 251	fsumshftm 15947	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
253		ax-1cn 11258	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
254	253, 253	pncan3oi 11573	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + 1) − 1) = 1
255	254	oveq1i 7430	. . . . . . . . . . . . . . . 16 ⊢ (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
256	255	sumeq1i 15864	. . . . . . . . . . . . . . 15 ⊢ Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
257		fvoveq1 7443	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
258	257	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
259	258	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
260	259	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
261	260	cbvsumv 15863	. . . . . . . . . . . . . . 15 ⊢ Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
262	256, 261	eqtri 2784	. . . . . . . . . . . . . 14 ⊢ Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
263	252, 262	eqtrdi 2812	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
264	241, 263	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
265	237, 264	eqtrd 2796	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
266	233, 265	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
267	194	recnd 11337	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℂ)
268		peano2nn 12347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
269		ffvelcdm 7081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
270	14, 268, 269	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
271	208, 270	ffvelcdmd 7085	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
272	207, 271	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
273		xp1st 8033	. . . . . . . . . . . . . . 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 15900	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
277	276	recnd 11337	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
278	227, 226, 267, 277	addsub4d 11716	. . . . . . . . . 10 ⊢ (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
279	221, 266, 278	3eqtrd 2800	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
280	199, 206, 279	3eqtrd 2800	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
281	280, 179	eqeltrrd 2862	. . . . . . 7 ⊢ (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
282		fveq2 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑀 → (𝐾‘𝑛) = (𝐾‘𝑀))
283	282	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑀 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑀)))
284	283, 61	elrab2 3649	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ 𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀)))
285	111, 284	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀)))
286	285	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ (𝐾‘𝑀))
287	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25838	. . . . . . . . . . . 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 25838	. . . . . . . . . . . 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 11940	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))))
296	149, 195, 295	ltled 11458	. . . . . . 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 13729	. . . . . . . . . . . . . . . . . . . . . . 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 12350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
305	112	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
306	304, 305	ltnled 11457	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖))
307	303, 306	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ≤ 𝑖)
308		infssuzle 13058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ⊆ (ℤ≥‘1) ∧ 𝑖 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
309	65, 308	mpan 703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
310	64, 309	eqbrtrid 5140	. . . . . . . . . . . . . . . . . . 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 25839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)
314	312, 313	syldan 603	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)
315	314	iftrued 4490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
316		2fveq3 6890	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (𝐾‘𝑖) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑖))))
317	316	fveq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (𝐾‘𝑖) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
318	317	breq1d 5113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (𝐾‘𝑖) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵))
319	318, 317	ifbieq1d 4507	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (𝐾‘𝑖) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵))
320		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (𝐾‘𝑖) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑖)))
321	319, 320	eleq12d 2855	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (𝐾‘𝑖) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖))))
322	94	ralrimiva 3155	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
323	322	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
324		ffvelcdm 7081	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑇)
325	10, 223, 324	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘𝑖) ∈ 𝑇)
326	321, 323, 325	rspcdva 3578	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))
327	315, 326	eqeltrrd 2862	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐻‘(𝐾‘𝑖)))
328	5, 6, 7, 8, 9	algrp1 16749	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖)))
329	223, 328	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖)))
330	327, 329	eleqtrrd 2864	. . . . . . . . . . . . 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 25838	. . . . . . . . . . . . . 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 11458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
337	222, 275, 224, 336	fsumle 15966	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
338	225, 276	subge0d 11906	. . . . . . . . 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 11744	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
341	195, 340	addge01d 11904	. . . . . . . 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 11467	. . . . . 6 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
344	343, 280	breqtrrd 5133	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
345	344	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
346		fzfid 14116	. . . . 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 3931	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
352	351	nnred 12350	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
353	28	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
354		ltle 11398	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧))
355	352, 353, 354	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧))
356	351, 5	eleqtrdi 2871	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ≥‘1))
357		nnz 12714	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
358	357	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
359		elfz5 13648	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ≥‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧))
360	356, 358, 359	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧))
361	355, 360	sylibrd 262	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ∈ (1...𝑧)))
362	361	ralimdva 3175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
363	362	impr 460	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
364		dfss3 3920	. . . . . 6 ⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
365	363, 364	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
366	346, 347, 349, 365	fsumless 15963	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
367	175, 180, 163, 345, 366	letrd 11467	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
368		eqidd 2762	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
369		simprl 783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
370	369, 5	eleqtrdi 2871	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ≥‘1))
371	347	recnd 11337	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
372	368, 370, 371	fsumser 15896	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
373	90	fveq1i 6886	. . . . 5 ⊢ (𝑆‘𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
374	372, 373	eqtr4di 2814	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆‘𝑧))
375	166	ffnd 6710	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
376		fnfvelrn 7080	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆‘𝑧) ∈ ran 𝑆)
377	375, 369, 376	syl2an2r 698	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ∈ ran 𝑆)
378		supxrub 13454	. . . . 5 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘𝑧) ∈ ran 𝑆) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
379	171, 377, 378	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
380	374, 379	eqbrtrd 5127	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
381	151, 164, 174, 367, 380	xrletrd 13291	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
382	148, 381	rexlimddv 3170	1 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  ifcif 4482  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867   class class class wbr 5103   × cxp 5649  ran crn 5652   ↾ cres 5653   “ cima 5654   ∘ ccom 5655   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –onto→wfo 6536  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7420  1^st c1st 7999  2^nd c2nd 8000   ≼ cdom 8971  Fincfn 8973  supcsup 9432  infcinf 9433  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201   + caddc 11203  +∞cpnf 11340  ℝ^*cxr 11342   < clt 11343   ≤ cle 11344   − cmin 11541  ℕcn 12335  ℤcz 12693  ℤ_≥cuz 12965  (,)cioo 13476  [,)cico 13478  [,]cicc 13479  ...cfz 13639  seqcseq 14144  abscabs 15401  Σcsu 15853

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-inf2 9642  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-sup 9434  df-inf 9435  df-oi 9504  df-card 10020  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-n0 12607  df-z 12694  df-uz 12966  df-rp 13121  df-ioo 13480  df-ico 13482  df-icc 13483  df-fz 13640  df-fzo 13789  df-seq 14145  df-exp 14205  df-hash 14475  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-clim 15655  df-sum 15854

This theorem is used by:  ovolicc2lem5  25842