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

Theorem ovolicc2lem4 23499
Description: Lemma for ovolicc2 23501. (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.
StepHypRef Expression
1 arch 11554 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
21ad2antlr 709 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3 df-ima 5322 . . . . . . . . . . . . . . . 16 ((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀))
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐺:𝑈⟶ℕ)
5 nnuz 11939 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7 1zzd 11672 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℤ)
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶𝑇)
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻:𝑇𝑇)
105, 6, 7, 8, 9algrf 15503 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾:ℕ⟶𝑇)
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12 ssrab2 3882 . . . . . . . . . . . . . . . . . . . . 21 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
1311, 12eqsstri 3830 . . . . . . . . . . . . . . . . . . . 20 𝑇𝑈
14 fss 6267 . . . . . . . . . . . . . . . . . . . 20 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
1510, 13, 14sylancl 576 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶𝑈)
16 fco 6271 . . . . . . . . . . . . . . . . . . 19 ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺𝐾):ℕ⟶ℕ)
174, 15, 16syl2anc 575 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝐾):ℕ⟶ℕ)
18 elfznn 12591 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
1918ssriv 3800 . . . . . . . . . . . . . . . . . 18 (1...𝑀) ⊆ ℕ
20 fssres 6283 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2117, 19, 20sylancl 576 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2221frnd 6261 . . . . . . . . . . . . . . . 16 (𝜑 → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
233, 22syl5eqss 3844 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
24 nnssre 11307 . . . . . . . . . . . . . . 15 ℕ ⊆ ℝ
2523, 24syl6ss 3808 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
2625ad3antrrr 712 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
27 simpr 473 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀)))
2826, 27sseldd 3797 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
29 simpllr 784 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
30 nnre 11310 . . . . . . . . . . . . 13 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
3130ad2antlr 709 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
32 lelttr 10411 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3328, 29, 31, 32syl3anc 1483 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3433ancomsd 453 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧𝑦𝑥) → 𝑦 < 𝑧))
3534expdimp 442 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦𝑥𝑦 < 𝑧))
3635an32s 634 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦𝑥𝑦 < 𝑧))
3736ralimdva 3148 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3837impancom 441 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3938an32s 634 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4039reximdva 3202 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
412, 40mpd 15 . . 3 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
42 fzfid 12994 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
43 fvres 6425 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
4443adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
45 fvco3 6494 . . . . . . . . . . . . . . 15 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4610, 18, 45syl2an 585 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4744, 46eqtrd 2838 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
4847adantrr 699 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
49 fvres 6425 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
5049ad2antll 711 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
51 elfznn 12591 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
5251adantl 469 . . . . . . . . . . . . . 14 ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
53 fvco3 6494 . . . . . . . . . . . . . 14 ((𝐾:ℕ⟶𝑇𝑗 ∈ ℕ) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5410, 52, 53syl2an 585 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5550, 54eqtrd 2838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾𝑗)))
5648, 55eqeq12d 2819 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗))))
57 2fveq3 6411 . . . . . . . . . . . 12 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
5819a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑀) ⊆ ℕ)
59 elfznn 12591 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
6059ad2antlr 709 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℕ)
6160nnred 11318 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℝ)
62 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
63 ssrab2 3882 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
6462, 63eqsstri 3830 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 ⊆ ℕ
6564, 24sstri 3805 . . . . . . . . . . . . . . . . . . . . 21 𝑊 ⊆ ℝ
66 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 = inf(𝑊, ℝ, < )
6764, 5sseqtri 3832 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 ⊆ (ℤ‘1)
68 1z 11671 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℤ
695uzinf 12986 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
7068, 69ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ ℕ ∈ Fin
71 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
72 elin 3993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin) ↔ (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7371, 72sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7473simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑈 ∈ Fin)
75 ssfi 8417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
7674, 13, 75sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑇 ∈ Fin)
7776adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → 𝑇 ∈ Fin)
7810adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
79 2fveq3 6411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾𝑖) = (𝐾𝑗) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
8079fveq2d 6410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐾𝑖) = (𝐾𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
81 simpll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
82 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
83 ral0 4269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑚 ∈ ∅ 𝑛𝑚
84 simplr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
8584raleqdv 3331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛𝑚))
8683, 85mpbiri 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚𝑊 𝑛𝑚)
8786ralrimivw 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
88 rabid2 3305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
8987, 88sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
9082, 89eleqtrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
91 simprr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
9291, 89eleqtrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
93 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴 ∈ ℝ)
94 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐵 ∈ ℝ)
95 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝐵)
96 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
97 ovolicc2.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
98 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
99 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
100 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
101 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝐶)
10293, 94, 95, 96, 97, 71, 98, 4, 99, 11, 9, 100, 101, 8, 6, 62ovolicc2lem3 23498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10381, 90, 92, 102syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10480, 103syl5ibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
105104ralrimivva 3157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
106 dff13 6734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾:ℕ–1-1𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗)))
10778, 105, 106sylanbrc 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑊 = ∅) → 𝐾:ℕ–1-1𝑇)
108 f1domg 8210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 ∈ Fin → (𝐾:ℕ–1-1𝑇 → ℕ ≼ 𝑇))
10977, 107, 108sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → ℕ ≼ 𝑇)
110 domfi 8418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
11177, 109, 110syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑊 = ∅) → ℕ ∈ Fin)
112111ex 399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
113112necon3bd 2990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
11470, 113mpi 20 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑊 ≠ ∅)
115 infssuzcl 11989 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
11667, 114, 115sylancr 577 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
11766, 116syl5eqel 2887 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀𝑊)
11865, 117sseldi 3794 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
119118ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀 ∈ ℝ)
12065sseli 3792 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑚 ∈ ℝ)
121120adantl 469 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
122 elfzle2 12566 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑀) → 𝑛𝑀)
123122ad2antlr 709 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑀)
124 infssuzle 11988 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑚𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
12567, 124mpan 673 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
12666, 125syl5eqbr 4877 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑀𝑚)
127126adantl 469 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀𝑚)
12861, 119, 121, 123, 127letrd 10477 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑚)
129128ralrimiva 3152 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑀)) → ∀𝑚𝑊 𝑛𝑚)
13058, 129ssrabdv 3876 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
131130adantr 468 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
132 simprl 778 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
133131, 132sseldd 3797 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
134 simprr 780 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
135131, 134sseldd 3797 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
136133, 135jca 503 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}))
137136, 102syldan 581 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
13857, 137syl5ibr 237 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → 𝑖 = 𝑗))
13956, 138sylbid 231 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
140139ralrimivva 3157 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
141 dff13 6734 . . . . . . . . 9 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
14221, 140, 141sylanbrc 574 . . . . . . . 8 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
143 f1f1orn 6362 . . . . . . . 8 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀)))
144142, 143syl 17 . . . . . . 7 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀)))
145 f1oeq3 6343 . . . . . . . 8 (((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) ↔ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀))))
1463, 145ax-mp 5 . . . . . . 7 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) ↔ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀)))
147144, 146sylibr 225 . . . . . 6 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)))
148 f1ofo 6358 . . . . . 6 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
149147, 148syl 17 . . . . 5 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
150 fofi 8489 . . . . 5 (((1...𝑀) ∈ Fin ∧ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
15142, 149, 150syl2anc 575 . . . 4 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
152 fimaxre2 11252 . . . 4 ((((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15325, 151, 152syl2anc 575 . . 3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15441, 153r19.29a 3264 . 2 (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
15594, 93resubcld 10741 . . . . 5 (𝜑 → (𝐵𝐴) ∈ ℝ)
156155rexrd 10372 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ*)
157156adantr 468 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ*)
158 fzfid 12994 . . . . . 6 (𝜑 → (1...𝑧) ∈ Fin)
159 elfznn 12591 . . . . . . . . 9 (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
160 eqid 2804 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
161160ovolfsf 23450 . . . . . . . . . . 11 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
16297, 161syl 17 . . . . . . . . . 10 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
163162ffvelrnda 6579 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
164159, 163sylan2 582 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
165 elrege0 12496 . . . . . . . 8 ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
166164, 165sylib 209 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
167166simpld 484 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
168158, 167fsumrecl 14686 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
169168adantr 468 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
170169rexrd 10372 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
171160, 96ovolsf 23451 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
17297, 171syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
173172frnd 6261 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
174 rge0ssre 12498 . . . . . . 7 (0[,)+∞) ⊆ ℝ
175173, 174syl6ss 3808 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
176 ressxr 10366 . . . . . 6 ℝ ⊆ ℝ*
177175, 176syl6ss 3808 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
178 supxrcl 12361 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
179177, 178syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
180179adantr 468 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
181155adantr 468 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ)
18223sselda 3796 . . . . . . 7 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
183174, 163sseldi 3794 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
184182, 183syldan 581 . . . . . 6 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
185151, 184fsumrecl 14686 . . . . 5 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
186185adantr 468 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
187 inss2 4028 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
188 fss 6267 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
18997, 187, 188sylancl 576 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
19064, 117sseldi 3794 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
19115, 190ffvelrnd 6580 . . . . . . . . . . 11 (𝜑 → (𝐾𝑀) ∈ 𝑈)
1924, 191ffvelrnd 6580 . . . . . . . . . 10 (𝜑 → (𝐺‘(𝐾𝑀)) ∈ ℕ)
193189, 192ffvelrnd 6580 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ))
194 xp2nd 7429 . . . . . . . . 9 ((𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
195193, 194syl 17 . . . . . . . 8 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
19613, 8sseldi 3794 . . . . . . . . . . 11 (𝜑𝐶𝑈)
1974, 196ffvelrnd 6580 . . . . . . . . . 10 (𝜑 → (𝐺𝐶) ∈ ℕ)
198189, 197ffvelrnd 6580 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ))
199 xp1st 7428 . . . . . . . . 9 ((𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
200198, 199syl 17 . . . . . . . 8 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
201195, 200resubcld 10741 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ∈ ℝ)
202 fveq2 6406 . . . . . . . . . 10 (𝑗 = (𝐺‘(𝐾𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
203183recnd 10351 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
204182, 203syldan 581 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
205202, 42, 147, 47, 204fsumf1o 14675 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
20697adantr 468 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2074adantr 468 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
208 ffvelrn 6577 . . . . . . . . . . . . 13 ((𝐾:ℕ⟶𝑈𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
20915, 18, 208syl2an 585 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) ∈ 𝑈)
210207, 209ffvelrnd 6580 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
211160ovolfsval 23449 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
212206, 210, 211syl2anc 575 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
213212sumeq2dv 14654 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
214189adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
2154adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
21615ffvelrnda 6579 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
217215, 216ffvelrnd 6580 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
218214, 217ffvelrnd 6580 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
219 xp2nd 7429 . . . . . . . . . . . . . 14 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
220218, 219syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
22118, 220sylan2 582 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
222221recnd 10351 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
223189adantr 468 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
224223, 210ffvelrnd 6580 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
225 xp1st 7428 . . . . . . . . . . . . 13 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
226224, 225syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
227226recnd 10351 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
22842, 222, 227fsumsub 14740 . . . . . . . . . 10 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
22967, 117sseldi 3794 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ‘1))
230 2fveq3 6411 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑀)))
231230fveq2d 6410 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑀))))
232231fveq2d 6410 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
233229, 222, 232fsumm1 14701 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
234 fzfid 12994 . . . . . . . . . . . . . . 15 (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
235 elfznn 12591 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
236235, 220sylan2 582 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
237234, 236fsumrecl 14686 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
238237recnd 10351 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
239195recnd 10351 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℂ)
240238, 239addcomd 10521 . . . . . . . . . . . 12 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
241233, 240eqtrd 2838 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
242 2fveq3 6411 . . . . . . . . . . . . . . 15 (𝑖 = 1 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘1)))
243242fveq2d 6410 . . . . . . . . . . . . . 14 (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
244243fveq2d 6410 . . . . . . . . . . . . 13 (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
245229, 227, 244fsum1p 14703 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
2465, 6, 7, 8algr0 15502 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾‘1) = 𝐶)
247246fveq2d 6410 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺𝐶))
248247fveq2d 6410 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺𝐶)))
249248fveq2d 6410 . . . . . . . . . . . . 13 (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺𝐶))))
2507peano2zd 11749 . . . . . . . . . . . . . . 15 (𝜑 → (1 + 1) ∈ ℤ)
251190nnzd 11745 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
252 fzp1ss 12613 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
25368, 252mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
254253sselda 3796 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
255254, 227syldan 581 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
256 2fveq3 6411 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
257256fveq2d 6410 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
258257fveq2d 6410 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
2597, 250, 251, 255, 258fsumshftm 14733 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
260 ax-1cn 10277 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
261260, 260pncan3oi 10580 . . . . . . . . . . . . . . . . 17 ((1 + 1) − 1) = 1
262261oveq1i 6882 . . . . . . . . . . . . . . . 16 (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
263262sumeq1i 14649 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
264 fvoveq1 6895 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
265264fveq2d 6410 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
266265fveq2d 6410 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
267266fveq2d 6410 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
268267cbvsumv 14647 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
269263, 268eqtri 2826 . . . . . . . . . . . . . 14 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
270259, 269syl6eq 2854 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
271249, 270oveq12d 6890 . . . . . . . . . . . 12 (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
272245, 271eqtrd 2838 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
273241, 272oveq12d 6890 . . . . . . . . . 10 (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
274200recnd 10351 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℂ)
275 peano2nn 11315 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
276 ffvelrn 6577 . . . . . . . . . . . . . . . . . 18 ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
27715, 275, 276syl2an 585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
278215, 277ffvelrnd 6580 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
279214, 278ffvelrnd 6580 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
280 xp1st 7428 . . . . . . . . . . . . . . 15 ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
281279, 280syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
282235, 281sylan2 582 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
283234, 282fsumrecl 14686 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
284283recnd 10351 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
285239, 238, 274, 284addsub4d 10722 . . . . . . . . . 10 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
286228, 273, 2853eqtrd 2842 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
287205, 213, 2863eqtrd 2842 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
288287, 185eqeltrrd 2884 . . . . . . 7 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
289 fveq2 6406 . . . . . . . . . . . . . . 15 (𝑛 = 𝑀 → (𝐾𝑛) = (𝐾𝑀))
290289eleq2d 2869 . . . . . . . . . . . . . 14 (𝑛 = 𝑀 → (𝐵 ∈ (𝐾𝑛) ↔ 𝐵 ∈ (𝐾𝑀)))
291290, 62elrab2 3560 . . . . . . . . . . . . 13 (𝑀𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
292117, 291sylib 209 . . . . . . . . . . . 12 (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
293292simprd 485 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐾𝑀))
29493, 94, 95, 96, 97, 71, 98, 4, 99ovolicc2lem1 23496 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐾𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
295191, 294mpdan 670 . . . . . . . . . . 11 (𝜑 → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
296293, 295mpbid 223 . . . . . . . . . 10 (𝜑 → (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
297296simp3d 1167 . . . . . . . . 9 (𝜑𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
29893, 94, 95, 96, 97, 71, 98, 4, 99ovolicc2lem1 23496 . . . . . . . . . . . 12 ((𝜑𝐶𝑈) → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
299196, 298mpdan 670 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
300101, 299mpbid 223 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶)))))
301300simp2d 1166 . . . . . . . . 9 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴)
30294, 200, 195, 93, 297, 301lt2subd 10934 . . . . . . . 8 (𝜑 → (𝐵𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
303155, 201, 302ltled 10468 . . . . . . 7 (𝜑 → (𝐵𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
304235adantl 469 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
305 simpr 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
306251adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
307 elfzm11 12632 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
30868, 306, 307sylancr 577 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
309305, 308mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀))
310309simp3d 1167 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
311304nnred 11318 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
312118adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
313311, 312ltnled 10467 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀𝑖))
314310, 313mpbid 223 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀𝑖)
315 infssuzle 11988 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑖𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
31667, 315mpan 673 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
31766, 316syl5eqbr 4877 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑊𝑀𝑖)
318314, 317nsyl 137 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖𝑊)
319304, 318jca 503 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊))
32093, 94, 95, 96, 97, 71, 98, 4, 99, 11, 9, 100, 101, 8, 6, 62ovolicc2lem2 23497 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
321319, 320syldan 581 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
322321iftrued 4285 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
323 2fveq3 6411 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑖) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑖))))
324323fveq2d 6410 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐾𝑖) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
325324breq1d 4852 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵))
326325, 324ifbieq1d 4300 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵))
327 fveq2 6406 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → (𝐻𝑡) = (𝐻‘(𝐾𝑖)))
328326, 327eleq12d 2877 . . . . . . . . . . . . . . . 16 (𝑡 = (𝐾𝑖) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
329100ralrimiva 3152 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
330329adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
331 ffvelrn 6577 . . . . . . . . . . . . . . . . 17 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑇)
33210, 235, 331syl2an 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾𝑖) ∈ 𝑇)
333328, 330, 332rspcdva 3506 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖)))
334322, 333eqeltrrd 2884 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐻‘(𝐾𝑖)))
3355, 6, 7, 8, 9algrp1 15504 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
336235, 335sylan2 582 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
337334, 336eleqtrrd 2886 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
338235, 277sylan2 582 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
33993, 94, 95, 96, 97, 71, 98, 4, 99ovolicc2lem1 23496 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
340338, 339syldan 581 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
341337, 340mpbid 223 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
342341simp2d 1166 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
343282, 236, 342ltled 10468 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
344234, 282, 236, 343fsumle 14751 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
345237, 283subge0d 10900 . . . . . . . . 9 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
346344, 345mpbird 248 . . . . . . . 8 (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
347237, 283resubcld 10741 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
348201, 347addge01d 10898 . . . . . . . 8 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))))
349346, 348mpbid 223 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
350155, 201, 288, 303, 349letrd 10477 . . . . . 6 (𝜑 → (𝐵𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
351350, 287breqtrrd 4870 . . . . 5 (𝜑 → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
352351adantr 468 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
353 fzfid 12994 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
354167adantlr 697 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
355166simprd 485 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
356355adantlr 697 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
35723adantr 468 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℕ) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
358357sselda 3796 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
359358nnred 11318 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
36030ad2antlr 709 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
361 ltle 10409 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧𝑦𝑧))
362359, 360, 361syl2anc 575 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦𝑧))
363358, 5syl6eleq 2893 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ‘1))
364 nnz 11663 . . . . . . . . . . 11 (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
365364ad2antlr 709 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
366 elfz5 12555 . . . . . . . . . 10 ((𝑦 ∈ (ℤ‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
367363, 365, 366syl2anc 575 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
368362, 367sylibrd 250 . . . . . . . 8 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦 ∈ (1...𝑧)))
369368ralimdva 3148 . . . . . . 7 ((𝜑𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
370369impr 444 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
371 dfss3 3785 . . . . . 6 (((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
372370, 371sylibr 225 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
373353, 354, 356, 372fsumless 14748 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
374181, 186, 169, 352, 373letrd 10477 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
375 eqidd 2805 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
376 simprl 778 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
377376, 5syl6eleq 2893 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ‘1))
378354recnd 10351 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
379375, 377, 378fsumser 14682 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
38096fveq1i 6407 . . . . 5 (𝑆𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
381379, 380syl6eqr 2856 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆𝑧))
382177adantr 468 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆ ℝ*)
383172ffnd 6255 . . . . . . 7 (𝜑𝑆 Fn ℕ)
384383adantr 468 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ)
385 fnfvelrn 6576 . . . . . 6 ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆𝑧) ∈ ran 𝑆)
386384, 376, 385syl2anc 575 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ∈ ran 𝑆)
387 supxrub 12370 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑧) ∈ ran 𝑆) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
388382, 386, 387syl2anc 575 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
389381, 388eqbrtrd 4864 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
390157, 170, 180, 374, 389xrletrd 12209 . 2 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
391154, 390rexlimddv 3221 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2976  wral 3094  wrex 3095  {crab 3098  cin 3766  wss 3767  c0 4114  ifcif 4277  𝒫 cpw 4349  {csn 4368   cuni 4628   class class class wbr 4842   × cxp 5307  ran crn 5310  cres 5311  cima 5312  ccom 5313   Fn wfn 6094  wf 6095  1-1wf1 6096  ontowfo 6097  1-1-ontowf1o 6098  cfv 6099  (class class class)co 6872  1st c1st 7394  2nd c2nd 7395  cdom 8188  Fincfn 8190  supcsup 8583  infcinf 8584  cc 10217  cr 10218  0cc0 10219  1c1 10220   + caddc 10222  +∞cpnf 10354  *cxr 10356   < clt 10357  cle 10358  cmin 10549  cn 11303  cz 11641  cuz 11902  (,)cioo 12391  [,)cico 12393  [,]cicc 12394  ...cfz 12547  seqcseq 13022  abscabs 14195  Σcsu 14637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177  ax-inf2 8783  ax-cnex 10275  ax-resscn 10276  ax-1cn 10277  ax-icn 10278  ax-addcl 10279  ax-addrcl 10280  ax-mulcl 10281  ax-mulrcl 10282  ax-mulcom 10283  ax-addass 10284  ax-mulass 10285  ax-distr 10286  ax-i2m1 10287  ax-1ne0 10288  ax-1rid 10289  ax-rnegex 10290  ax-rrecex 10291  ax-cnre 10292  ax-pre-lttri 10293  ax-pre-lttrn 10294  ax-pre-ltadd 10295  ax-pre-mulgt0 10296  ax-pre-sup 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-nel 3080  df-ral 3099  df-rex 3100  df-reu 3101  df-rmo 3102  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-int 4668  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-se 5269  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-lim 5939  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6833  df-ov 6875  df-oprab 6876  df-mpt2 6877  df-om 7294  df-1st 7396  df-2nd 7397  df-wrecs 7640  df-recs 7702  df-rdg 7740  df-1o 7794  df-oadd 7798  df-er 7977  df-en 8191  df-dom 8192  df-sdom 8193  df-fin 8194  df-sup 8585  df-inf 8586  df-oi 8652  df-card 9046  df-pnf 10359  df-mnf 10360  df-xr 10361  df-ltxr 10362  df-le 10363  df-sub 10551  df-neg 10552  df-div 10968  df-nn 11304  df-2 11362  df-3 11363  df-n0 11558  df-z 11642  df-uz 11903  df-rp 12045  df-ioo 12395  df-ico 12397  df-icc 12398  df-fz 12548  df-fzo 12688  df-seq 13023  df-exp 13082  df-hash 13336  df-cj 14060  df-re 14061  df-im 14062  df-sqrt 14196  df-abs 14197  df-clim 14440  df-sum 14638
This theorem is referenced by:  ovolicc2lem5  23500
  Copyright terms: Public domain W3C validator