ovolicc2lem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ovolicc2lem4		Structured version Visualization version GIF version

Theorem ovolicc2lem4 25423

Description: Lemma for ovolicc2 25425. (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((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
ovolicc2.13	⊢ (𝜑 → 𝐴 ∈ 𝐶)
ovolicc2.14	⊢ (𝜑 → 𝐶 ∈ 𝑇)
ovolicc2.15	⊢ 𝐾 = seq1((𝐻 ∘ 1^st ), (ℕ × {𝐶}))
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 12485	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
2	1	ad2antlr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3		df-ima 5685	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀))
4		ovolicc2.8	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)
5		nnuz 12881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
6		ovolicc2.15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐾 = seq1((𝐻 ∘ 1^st ), (ℕ × {𝐶}))
7		1zzd 12609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
8		ovolicc2.14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ 𝑇)
9		ovolicc2.11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)
10	5, 6, 7, 8, 9	algrf 16529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾:ℕ⟶𝑇)
11		ovolicc2.10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12	11	ssrab3 4076	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑇 ⊆ 𝑈
13		fss 6733	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈)
14	10, 12, 13	sylancl 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾:ℕ⟶𝑈)
15		fco 6741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺 ∘ 𝐾):ℕ⟶ℕ)
16	4, 14, 15	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐺 ∘ 𝐾):ℕ⟶ℕ)
17		fz1ssnn 13550	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑀) ⊆ ℕ
18		fssres 6757	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∘ 𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
19	16, 17, 18	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
20	19	frnd 6724	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ)
21	3, 20	eqsstrid 4026	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ)
22		nnssre 12232	. . . . . . . . . . . . . . 15 ⊢ ℕ ⊆ ℝ
23	21, 22	sstrdi 3990	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ)
24	23	ad3antrrr 729	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ)
25		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀)))
26	24, 25	sseldd 3979	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
27		simpllr 775	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
28		nnre 12235	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
29	28	ad2antlr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
30		lelttr 11320	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧))
31	26, 27, 29, 30	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧))
32	31	ancomsd 465	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥) → 𝑦 < 𝑧))
33	32	expdimp 452	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧))
34	33	an32s 651	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧))
35	34	ralimdva 3162	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
36	35	impancom 451	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
37	36	an32s 651	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
38	37	reximdva 3163	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧))
39	2, 38	mpd 15	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)
40		fzfid 13956	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
41		fvres 6910	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖))
42	41	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖))
43		elfznn 13548	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
44		fvco3 6991	. . . . . . . . . . . . . . 15 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖)))
45	10, 43, 44	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖)))
46	42, 45	eqtrd 2767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖)))
47	46	adantrr 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖)))
48		fvres 6910	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗))
49	48	ad2antll 728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗))
50		elfznn 13548	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
51	50	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
52		fvco3 6991	. . . . . . . . . . . . . 14 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑗 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗)))
53	10, 51, 52	syl2an 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗)))
54	49, 53	eqtrd 2767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾‘𝑗)))
55	47, 54	eqeq12d 2743	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗))))
56		2fveq3 6896	. . . . . . . . . . . 12 ⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))
57	17	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑀) ⊆ ℕ)
58		elfznn 13548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
59	58	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℕ)
60	59	nnred 12243	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℝ)
61		ovolicc2.16	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}
62	61	ssrab3 4076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑊 ⊆ ℕ
63	62, 22	sstri 3987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑊 ⊆ ℝ
64		ovolicc2.17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑀 = inf(𝑊, ℝ, < )
65	62, 5	sseqtri 4014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑊 ⊆ (ℤ_≥‘1)
66		nnnfi 13949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ℕ ∈ Fin
67		ovolicc2.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
68	67	elin2d 4195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑈 ∈ Fin)
69		ssfi 9187	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin)
70	68, 12, 69	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ Fin)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑇 ∈ Fin)
72	10	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
73		2fveq3 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗))))
74	73	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))
75		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
76		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
77		ral0 4508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚
78		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
79	78	raleqdv 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚))
80	77, 79	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
81	80	ralrimivw 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
82		rabid2 3459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
83	81, 82	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
84	76, 83	eleqtrd 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
85		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
86	85, 83	eleqtrd 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
95		ovolicc2.13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
96	87, 88, 89, 90, 91, 67, 92, 4, 93, 11, 9, 94, 95, 8, 6, 61	ovolicc2lem3 25422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑖 = 𝑗 ↔ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
97	75, 84, 86, 96	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
98	74, 97	imbitrrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))
99	98	ralrimivva 3195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))
100		dff13 7259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐾:ℕ–1-1→𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)))
101	72, 99, 100	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ–1-1→𝑇)
102		f1domg 8982	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑇 ∈ Fin → (𝐾:ℕ–1-1→𝑇 → ℕ ≼ 𝑇))
103	71, 101, 102	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ≼ 𝑇)
104		domfi 9206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
105	70, 103, 104	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ∈ Fin)
106	105	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
107	106	necon3bd 2949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
108	66, 107	mpi 20	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑊 ≠ ∅)
109		infssuzcl 12932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑊 ⊆ (ℤ_≥‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
110	65, 108, 109	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
111	64, 110	eqeltrid 2832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ 𝑊)
112	63, 111	sselid 3976	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℝ)
113	112	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℝ)
114	63	sseli 3974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ)
115	114	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ)
116		elfzle2 13523	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ≤ 𝑀)
117	116	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑀)
118		infssuzle 12931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ⊆ (ℤ_≥‘1) ∧ 𝑚 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
119	65, 118	mpan 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
120	64, 119	eqbrtrid 5177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚)
121	120	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ≤ 𝑚)
122	60, 113, 115, 117, 121	letrd 11387	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑚)
123	122	ralrimiva 3141	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚)
124	57, 123	ssrabdv 4067	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
125	124	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
126		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
127	125, 126	sseldd 3979	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
128		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
129	125, 128	sseldd 3979	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})
130	127, 129	jca 511	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}))
131	130, 96	syldan 590	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))))
132	56, 131	imbitrrid 245	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → 𝑖 = 𝑗))
133	55, 132	sylbid 239	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
134	133	ralrimivva 3195	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
135		dff13 7259	. . . . . . . . 9 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
136	19, 134, 135	sylanbrc 582	. . . . . . . 8 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
137		f1f1orn 6844	. . . . . . . 8 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
138	136, 137	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)))
139		f1oeq3 6823	. . . . . . . 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 233	. . . . . 6 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)))
142		f1ofo 6840	. . . . . 6 ⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀)))
143	141, 142	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀)))
144		fofi 9352	. . . . 5 ⊢ (((1...𝑀) ∈ Fin ∧ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin)
145	40, 143, 144	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin)
146		fimaxre2 12175	. . . 4 ⊢ ((((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥)
147	23, 145, 146	syl2anc 583	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥)
148	39, 147	r19.29a 3157	. 2 ⊢ (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)
149	88, 87	resubcld 11658	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
150	149	rexrd 11280	. . . 4 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ^*)
151	150	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ^*)
152		fzfid 13956	. . . . . 6 ⊢ (𝜑 → (1...𝑧) ∈ Fin)
153		elfznn 13548	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
154		eqid 2727	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
155	154	ovolfsf 25374	. . . . . . . . . . 11 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
156	91, 155	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
157	156	ffvelcdmda 7088	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
158	153, 157	sylan2 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
159		elrege0 13449	. . . . . . . 8 ⊢ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
160	158, 159	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
161	160	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
162	152, 161	fsumrecl 15698	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
163	162	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
164	163	rexrd 11280	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ^*)
165	154, 90	ovolsf 25375	. . . . . . . . 9 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
166	91, 165	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
167	166	frnd 6724	. . . . . . 7 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
168		rge0ssre 13451	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ
169	167, 168	sstrdi 3990	. . . . . 6 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
170		ressxr 11274	. . . . . 6 ⊢ ℝ ⊆ ℝ^*
171	169, 170	sstrdi 3990	. . . . 5 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
172		supxrcl 13312	. . . . 5 ⊢ (ran 𝑆 ⊆ ℝ^* → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
173	171, 172	syl 17	. . . 4 ⊢ (𝜑 → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
174	173	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ^, < ) ∈ ℝ^)
175	149	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ)
176	21	sselda 3978	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
177	168, 157	sselid 3976	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
178	176, 177	syldan 590	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
179	145, 178	fsumrecl 15698	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
180	179	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
181		inss2 4225	. . . . . . . . . . 11 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
182		fss 6733	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
183	91, 181, 182	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ))
184	62, 111	sselid 3976	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
185	14, 184	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝑀) ∈ 𝑈)
186	4, 185	ffvelcdmd 7089	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘(𝐾‘𝑀)) ∈ ℕ)
187	183, 186	ffvelcdmd 7089	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ))
188		xp2nd 8018	. . . . . . . . 9 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ)
189	187, 188	syl 17	. . . . . . . 8 ⊢ (𝜑 → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ)
190	12, 8	sselid 3976	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ 𝑈)
191	4, 190	ffvelcdmd 7089	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝐶) ∈ ℕ)
192	183, 191	ffvelcdmd 7089	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ))
193		xp1st 8017	. . . . . . . . 9 ⊢ ((𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ) → (1^st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ)
194	192, 193	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1^st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ)
195	189, 194	resubcld 11658	. . . . . . 7 ⊢ (𝜑 → ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) ∈ ℝ)
196		fveq2 6891	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘(𝐾‘𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))))
197	177	recnd 11258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
198	176, 197	syldan 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
199	196, 40, 141, 46, 198	fsumf1o 15687	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))))
200	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
201		ffvelcdm 7085	. . . . . . . . . . . . 13 ⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈)
202	14, 43, 201	syl2an 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝑈)
203	200, 202	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ)
204	154	ovolfsval 25373	. . . . . . . . . . 11 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾‘𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
205	91, 203, 204	syl2an2r 684	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
206	205	sumeq2dv 15667	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = Σ𝑖 ∈ (1...𝑀)((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
207	183	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
208	4	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
209	14	ffvelcdmda 7088	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈)
210	208, 209	ffvelcdmd 7089	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ)
211	207, 210	ffvelcdmd 7089	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ))
212		xp2nd 8018	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
213	211, 212	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
214	43, 213	sylan2 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
215	214	recnd 11258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
216	183	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
217	216, 203	ffvelcdmd 7089	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ))
218		xp1st 8017	. . . . . . . . . . . . 13 ⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
219	217, 218	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
220	219	recnd 11258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
221	40, 215, 220	fsumsub 15752	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
222		fzfid 13956	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
223		elfznn 13548	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
224	223, 213	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
225	222, 224	fsumrecl 15698	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ)
226	225	recnd 11258	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
227	189	recnd 11258	. . . . . . . . . . . 12 ⊢ (𝜑 → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℂ)
228	65, 111	sselid 3976	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
229		2fveq3 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑀 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑀)))
230	229	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑀))))
231	230	fveq2d 6895	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑀 → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))
232	228, 215, 231	fsumm1 15715	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))
233	226, 227, 232	comraddd 11444	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
234		2fveq3 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘1)))
235	234	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
236	235	fveq2d 6895	. . . . . . . . . . . . 13 ⊢ (𝑖 = 1 → (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1^st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
237	228, 220, 236	fsum1p 15717	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1^st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
238	5, 6, 7, 8	algr0 16528	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾‘1) = 𝐶)
239	238	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺‘𝐶))
240	239	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺‘𝐶)))
241	240	fveq2d 6895	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1^st ‘(𝐹‘(𝐺‘𝐶))))
242	7	peano2zd 12685	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 + 1) ∈ ℤ)
243	184	nnzd 12601	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℤ)
244		1z 12608	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℤ
245		fzp1ss 13570	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
246	244, 245	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
247	246	sselda 3978	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
248	247, 220	syldan 590	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ)
249		2fveq3 6896	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
250	249	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
251	250	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 + 1) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
252	7, 242, 243, 248, 251	fsumshftm 15745	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
253		ax-1cn 11182	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
254	253, 253	pncan3oi 11492	. . . . . . . . . . . . . . . . 17 ⊢ ((1 + 1) − 1) = 1
255	254	oveq1i 7424	. . . . . . . . . . . . . . . 16 ⊢ (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
256	255	sumeq1i 15662	. . . . . . . . . . . . . . 15 ⊢ Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
257		fvoveq1 7437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
258	257	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
259	258	fveq2d 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
260	259	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑖 → (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
261	260	cbvsumv 15660	. . . . . . . . . . . . . . 15 ⊢ Σ𝑗 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
262	256, 261	eqtri 2755	. . . . . . . . . . . . . 14 ⊢ Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
263	252, 262	eqtrdi 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
264	241, 263	oveq12d 7432	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = ((1^st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
265	237, 264	eqtrd 2767	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1^st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
266	233, 265	oveq12d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1^st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
267	194	recnd 11258	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℂ)
268		peano2nn 12240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
269		ffvelcdm 7085	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
270	14, 268, 269	syl2an 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
271	208, 270	ffvelcdmd 7089	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
272	207, 271	ffvelcdmd 7089	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
273		xp1st 8017	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
274	272, 273	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
275	223, 274	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
276	222, 275	fsumrecl 15698	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
277	276	recnd 11258	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
278	227, 226, 267, 277	addsub4d 11634	. . . . . . . . . 10 ⊢ (𝜑 → (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1^st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
279	221, 266, 278	3eqtrd 2771	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
280	199, 206, 279	3eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
281	280, 179	eqeltrrd 2829	. . . . . . 7 ⊢ (𝜑 → (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
282		fveq2 6891	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑀 → (𝐾‘𝑛) = (𝐾‘𝑀))
283	282	eleq2d 2814	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑀 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑀)))
284	283, 61	elrab2 3683	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ 𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀)))
285	111, 284	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀)))
286	285	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ (𝐾‘𝑀))
287	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25420	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐾‘𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))))
288	185, 287	mpdan 686	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))))
289	286, 288	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))
290	289	simp3d 1142	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))
291	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25420	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑈) → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2^nd ‘(𝐹‘(𝐺‘𝐶))))))
292	190, 291	mpdan 686	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2^nd ‘(𝐹‘(𝐺‘𝐶))))))
293	95, 292	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2^nd ‘(𝐹‘(𝐺‘𝐶)))))
294	293	simp2d 1141	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘(𝐹‘(𝐺‘𝐶))) < 𝐴)
295	88, 194, 189, 87, 290, 294	lt2subd 11854	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐴) < ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))))
296	149, 195, 295	ltled 11378	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))))
297	223	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
298		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
299	243	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
300		elfzm11 13590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
301	244, 299, 300	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)))
302	298, 301	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))
303	302	simp3d 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
304	297	nnred 12243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
305	112	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
306	304, 305	ltnled 11377	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖))
307	303, 306	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ≤ 𝑖)
308		infssuzle 12931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ⊆ (ℤ_≥‘1) ∧ 𝑖 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
309	65, 308	mpan 689	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
310	64, 309	eqbrtrid 5177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑊 → 𝑀 ≤ 𝑖)
311	307, 310	nsyl 140	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖 ∈ 𝑊)
312	297, 311	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊))
313	87, 88, 89, 90, 91, 67, 92, 4, 93, 11, 9, 94, 95, 8, 6, 61	ovolicc2lem2 25421	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)
314	312, 313	syldan 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)
315	314	iftrued 4532	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
316		2fveq3 6896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (𝐾‘𝑖) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑖))))
317	316	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = (𝐾‘𝑖) → (2^nd ‘(𝐹‘(𝐺‘𝑡))) = (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
318	317	breq1d 5152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = (𝐾‘𝑖) → ((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵))
319	318, 317	ifbieq1d 4548	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (𝐾‘𝑖) → if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵))
320		fveq2 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (𝐾‘𝑖) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑖)))
321	319, 320	eleq12d 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (𝐾‘𝑖) → (if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖))))
322	94	ralrimiva 3141	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
323	322	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡 ∈ 𝑇 if((2^nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))
324		ffvelcdm 7085	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑇)
325	10, 223, 324	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘𝑖) ∈ 𝑇)
326	321, 323, 325	rspcdva 3608	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))
327	315, 326	eqeltrrd 2829	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐻‘(𝐾‘𝑖)))
328	5, 6, 7, 8, 9	algrp1 16530	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖)))
329	223, 328	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖)))
330	327, 329	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
331	223, 270	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
332	87, 88, 89, 90, 91, 67, 92, 4, 93	ovolicc2lem1 25420	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
333	331, 332	syldan 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
334	330, 333	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
335	334	simp2d 1141	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
336	275, 224, 335	ltled 11378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
337	222, 275, 224, 336	fsumle 15763	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))
338	225, 276	subge0d 11820	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))))
339	337, 338	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
340	225, 276	resubcld 11658	. . . . . . . . 9 ⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
341	195, 340	addge01d 11818	. . . . . . . 8 ⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))))
342	339, 341	mpbid 231	. . . . . . 7 ⊢ (𝜑 → ((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
343	149, 195, 281, 296, 342	letrd 11387	. . . . . 6 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (((2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1^st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2^nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1^st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
344	343, 280	breqtrrd 5170	. . . . 5 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
345	344	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
346		fzfid 13956	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
347	161	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
348	160	simprd 495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
349	348	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
350	21	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ)
351	350	sselda 3978	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
352	351	nnred 12243	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
353	28	ad2antlr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
354		ltle 11318	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧))
355	352, 353, 354	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧))
356	351, 5	eleqtrdi 2838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ_≥‘1))
357		nnz 12595	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
358	357	ad2antlr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
359		elfz5 13511	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ_≥‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧))
360	356, 358, 359	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧))
361	355, 360	sylibrd 259	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ∈ (1...𝑧)))
362	361	ralimdva 3162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
363	362	impr 454	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
364		dfss3 3966	. . . . . 6 ⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
365	363, 364	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
366	346, 347, 349, 365	fsumless 15760	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
367	175, 180, 163, 345, 366	letrd 11387	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
368		eqidd 2728	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
369		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
370	369, 5	eleqtrdi 2838	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ_≥‘1))
371	347	recnd 11258	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
372	368, 370, 371	fsumser 15694	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
373	90	fveq1i 6892	. . . . 5 ⊢ (𝑆‘𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
374	372, 373	eqtr4di 2785	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆‘𝑧))
375	166	ffnd 6717	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn ℕ)
376		fnfvelrn 7084	. . . . . 6 ⊢ ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆‘𝑧) ∈ ran 𝑆)
377	375, 369, 376	syl2an2r 684	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ∈ ran 𝑆)
378		supxrub 13321	. . . . 5 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘𝑧) ∈ ran 𝑆) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ^*, < ))
379	171, 377, 378	syl2an2r 684	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ^*, < ))
380	374, 379	eqbrtrd 5164	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
381	151, 164, 174, 367, 380	xrletrd 13159	. 2 ⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))
382	148, 381	rexlimddv 3156	1 ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ^*, < ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ≠ wne 2935 ∀wral 3056 ∃wrex 3065 {crab 3427 ∩ cin 3943 ⊆ wss 3944 ∅c0 4318 ifcif 4524 𝒫 cpw 4598 {csn 4624 ∪ cuni 4903 class class class wbr 5142 × cxp 5670 ran crn 5673 ↾ cres 5674 “ cima 5675 ∘ ccom 5676 Fn wfn 6537 ⟶wf 6538 –1-1→wf1 6539 –onto→wfo 6540 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7414 1^st c1st 7983 2^nd c2nd 7984 ≼ cdom 8951 Fincfn 8953 supcsup 9449 infcinf 9450 ℂcc 11122 ℝcr 11123 0cc0 11124 1c1 11125 + caddc 11127 +∞cpnf 11261 ℝ^*cxr 11263 < clt 11264 ≤ cle 11265 − cmin 11460 ℕcn 12228 ℤcz 12574 ℤ_≥cuz 12838 (,)cioo 13342 [,)cico 13344 [,]cicc 13345 ...cfz 13502 seqcseq 13984 abscabs 15199 Σcsu 15650

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7732 ax-inf2 9650 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7863 df-1st 7985 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-1o 8478 df-er 8716 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-sup 9451 df-inf 9452 df-oi 9519 df-card 9948 df-pnf 11266 df-mnf 11267 df-xr 11268 df-ltxr 11269 df-le 11270 df-sub 11462 df-neg 11463 df-div 11888 df-nn 12229 df-2 12291 df-3 12292 df-n0 12489 df-z 12575 df-uz 12839 df-rp 12993 df-ioo 13346 df-ico 13348 df-icc 13349 df-fz 13503 df-fzo 13646 df-seq 13985 df-exp 14045 df-hash 14308 df-cj 15064 df-re 15065 df-im 15066 df-sqrt 15200 df-abs 15201 df-clim 15450 df-sum 15651

This theorem is referenced by: ovolicc2lem5 25424

W3C validator