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

Theorem ovolicc2lem4 23735
Description: Lemma for ovolicc2 23737. (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 11644 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
21ad2antlr 717 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3 df-ima 5370 . . . . . . . . . . . . . . . 16 ((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀))
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐺:𝑈⟶ℕ)
5 nnuz 12034 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7 1zzd 11765 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℤ)
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶𝑇)
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻:𝑇𝑇)
105, 6, 7, 8, 9algrf 15702 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾:ℕ⟶𝑇)
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12 ssrab2 3908 . . . . . . . . . . . . . . . . . . . . 21 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
1311, 12eqsstri 3854 . . . . . . . . . . . . . . . . . . . 20 𝑇𝑈
14 fss 6306 . . . . . . . . . . . . . . . . . . . 20 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
1510, 13, 14sylancl 580 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶𝑈)
16 fco 6310 . . . . . . . . . . . . . . . . . . 19 ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺𝐾):ℕ⟶ℕ)
174, 15, 16syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝐾):ℕ⟶ℕ)
18 elfznn 12692 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
1918ssriv 3825 . . . . . . . . . . . . . . . . . 18 (1...𝑀) ⊆ ℕ
20 fssres 6322 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2117, 19, 20sylancl 580 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2221frnd 6300 . . . . . . . . . . . . . . . 16 (𝜑 → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
233, 22syl5eqss 3868 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
24 nnssre 11383 . . . . . . . . . . . . . . 15 ℕ ⊆ ℝ
2523, 24syl6ss 3833 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
2625ad3antrrr 720 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
27 simpr 479 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀)))
2826, 27sseldd 3822 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
29 simpllr 766 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
30 nnre 11387 . . . . . . . . . . . . 13 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
3130ad2antlr 717 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
32 lelttr 10469 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3328, 29, 31, 32syl3anc 1439 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3433ancomsd 459 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧𝑦𝑥) → 𝑦 < 𝑧))
3534expdimp 446 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦𝑥𝑦 < 𝑧))
3635an32s 642 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦𝑥𝑦 < 𝑧))
3736ralimdva 3144 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3837impancom 445 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3938an32s 642 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4039reximdva 3198 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
412, 40mpd 15 . . 3 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
42 fzfid 13096 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
43 fvres 6467 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
4443adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
45 fvco3 6537 . . . . . . . . . . . . . . 15 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4610, 18, 45syl2an 589 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4744, 46eqtrd 2814 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
4847adantrr 707 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
49 fvres 6467 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
5049ad2antll 719 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
51 elfznn 12692 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
5251adantl 475 . . . . . . . . . . . . . 14 ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
53 fvco3 6537 . . . . . . . . . . . . . 14 ((𝐾:ℕ⟶𝑇𝑗 ∈ ℕ) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5410, 52, 53syl2an 589 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5550, 54eqtrd 2814 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾𝑗)))
5648, 55eqeq12d 2793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗))))
57 2fveq3 6453 . . . . . . . . . . . 12 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
5819a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑀) ⊆ ℕ)
59 elfznn 12692 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
6059ad2antlr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℕ)
6160nnred 11396 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℝ)
62 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
63 ssrab2 3908 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
6462, 63eqsstri 3854 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 ⊆ ℕ
6564, 24sstri 3830 . . . . . . . . . . . . . . . . . . . . 21 𝑊 ⊆ ℝ
66 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 = inf(𝑊, ℝ, < )
6764, 5sseqtri 3856 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 ⊆ (ℤ‘1)
68 1z 11764 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℤ
695uzinf 13088 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
7068, 69ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ ℕ ∈ Fin
71 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
72 elin 4019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin) ↔ (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7371, 72sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7473simprd 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑈 ∈ Fin)
75 ssfi 8470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
7674, 13, 75sylancl 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑇 ∈ Fin)
7776adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → 𝑇 ∈ Fin)
7810adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
79 2fveq3 6453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾𝑖) = (𝐾𝑗) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
8079fveq2d 6452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐾𝑖) = (𝐾𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
81 simpll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
82 simprl 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
83 ral0 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑚 ∈ ∅ 𝑛𝑚
84 simplr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
8584raleqdv 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛𝑚))
8683, 85mpbiri 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚𝑊 𝑛𝑚)
8786ralrimivw 3149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
88 rabid2 3305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
8987, 88sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
9082, 89eleqtrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
91 simprr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
9291, 89eleqtrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10381, 90, 92, 102syl12anc 827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10480, 103syl5ibr 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
105104ralrimivva 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
106 dff13 6786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾:ℕ–1-1𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗)))
10778, 105, 106sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑊 = ∅) → 𝐾:ℕ–1-1𝑇)
108 f1domg 8263 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 ∈ Fin → (𝐾:ℕ–1-1𝑇 → ℕ ≼ 𝑇))
10977, 107, 108sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → ℕ ≼ 𝑇)
110 domfi 8471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
11177, 109, 110syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑊 = ∅) → ℕ ∈ Fin)
112111ex 403 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
113112necon3bd 2983 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
11470, 113mpi 20 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑊 ≠ ∅)
115 infssuzcl 12084 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
11667, 114, 115sylancr 581 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
11766, 116syl5eqel 2863 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀𝑊)
11865, 117sseldi 3819 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
119118ad2antrr 716 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀 ∈ ℝ)
12065sseli 3817 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑚 ∈ ℝ)
121120adantl 475 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
122 elfzle2 12667 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑀) → 𝑛𝑀)
123122ad2antlr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑀)
124 infssuzle 12083 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑚𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
12567, 124mpan 680 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
12666, 125syl5eqbr 4923 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑀𝑚)
127126adantl 475 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀𝑚)
12861, 119, 121, 123, 127letrd 10535 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑚)
129128ralrimiva 3148 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑀)) → ∀𝑚𝑊 𝑛𝑚)
13058, 129ssrabdv 3902 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
131130adantr 474 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
132 simprl 761 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
133131, 132sseldd 3822 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
134 simprr 763 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
135131, 134sseldd 3822 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
136133, 135jca 507 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}))
137136, 102syldan 585 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
13857, 137syl5ibr 238 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → 𝑖 = 𝑗))
13956, 138sylbid 232 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
140139ralrimivva 3153 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
141 dff13 6786 . . . . . . . . 9 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
14221, 140, 141sylanbrc 578 . . . . . . . 8 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
143 f1f1orn 6404 . . . . . . . 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 6384 . . . . . . . 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 226 . . . . . 6 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)))
148 f1ofo 6400 . . . . . 6 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
149147, 148syl 17 . . . . 5 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
150 fofi 8542 . . . . 5 (((1...𝑀) ∈ Fin ∧ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
15142, 149, 150syl2anc 579 . . . 4 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
152 fimaxre2 11327 . . . 4 ((((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15325, 151, 152syl2anc 579 . . 3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15441, 153r19.29a 3264 . 2 (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
15594, 93resubcld 10806 . . . . 5 (𝜑 → (𝐵𝐴) ∈ ℝ)
156155rexrd 10428 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ*)
157156adantr 474 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ*)
158 fzfid 13096 . . . . . 6 (𝜑 → (1...𝑧) ∈ Fin)
159 elfznn 12692 . . . . . . . . 9 (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
160 eqid 2778 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
161160ovolfsf 23686 . . . . . . . . . . 11 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
16297, 161syl 17 . . . . . . . . . 10 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
163162ffvelrnda 6625 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
164159, 163sylan2 586 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
165 elrege0 12597 . . . . . . . 8 ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
166164, 165sylib 210 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
167166simpld 490 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
168158, 167fsumrecl 14881 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
169168adantr 474 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
170169rexrd 10428 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
171160, 96ovolsf 23687 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
17297, 171syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
173172frnd 6300 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
174 rge0ssre 12599 . . . . . . 7 (0[,)+∞) ⊆ ℝ
175173, 174syl6ss 3833 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
176 ressxr 10422 . . . . . 6 ℝ ⊆ ℝ*
177175, 176syl6ss 3833 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
178 supxrcl 12462 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
179177, 178syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
180179adantr 474 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
181155adantr 474 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ)
18223sselda 3821 . . . . . . 7 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
183174, 163sseldi 3819 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
184182, 183syldan 585 . . . . . 6 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
185151, 184fsumrecl 14881 . . . . 5 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
186185adantr 474 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
187 inss2 4054 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
188 fss 6306 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
18997, 187, 188sylancl 580 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
19064, 117sseldi 3819 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
19115, 190ffvelrnd 6626 . . . . . . . . . . 11 (𝜑 → (𝐾𝑀) ∈ 𝑈)
1924, 191ffvelrnd 6626 . . . . . . . . . 10 (𝜑 → (𝐺‘(𝐾𝑀)) ∈ ℕ)
193189, 192ffvelrnd 6626 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ))
194 xp2nd 7480 . . . . . . . . 9 ((𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
195193, 194syl 17 . . . . . . . 8 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
19613, 8sseldi 3819 . . . . . . . . . . 11 (𝜑𝐶𝑈)
1974, 196ffvelrnd 6626 . . . . . . . . . 10 (𝜑 → (𝐺𝐶) ∈ ℕ)
198189, 197ffvelrnd 6626 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ))
199 xp1st 7479 . . . . . . . . 9 ((𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
200198, 199syl 17 . . . . . . . 8 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
201195, 200resubcld 10806 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ∈ ℝ)
202 fveq2 6448 . . . . . . . . . 10 (𝑗 = (𝐺‘(𝐾𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
203183recnd 10407 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
204182, 203syldan 585 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
205202, 42, 147, 47, 204fsumf1o 14870 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
20697adantr 474 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2074adantr 474 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
208 ffvelrn 6623 . . . . . . . . . . . . 13 ((𝐾:ℕ⟶𝑈𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
20915, 18, 208syl2an 589 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) ∈ 𝑈)
210207, 209ffvelrnd 6626 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
211160ovolfsval 23685 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
212206, 210, 211syl2anc 579 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
213212sumeq2dv 14850 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
214189adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
2154adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
21615ffvelrnda 6625 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
217215, 216ffvelrnd 6626 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
218214, 217ffvelrnd 6626 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
219 xp2nd 7480 . . . . . . . . . . . . . 14 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
220218, 219syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
22118, 220sylan2 586 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
222221recnd 10407 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
223189adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
224223, 210ffvelrnd 6626 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
225 xp1st 7479 . . . . . . . . . . . . 13 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
226224, 225syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
227226recnd 10407 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
22842, 222, 227fsumsub 14933 . . . . . . . . . 10 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
22967, 117sseldi 3819 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ‘1))
230 2fveq3 6453 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑀)))
231230fveq2d 6452 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑀))))
232231fveq2d 6452 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
233229, 222, 232fsumm1 14896 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
234 fzfid 13096 . . . . . . . . . . . . . . 15 (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
235 elfznn 12692 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
236235, 220sylan2 586 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
237234, 236fsumrecl 14881 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
238237recnd 10407 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
239195recnd 10407 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℂ)
240238, 239addcomd 10580 . . . . . . . . . . . 12 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
241233, 240eqtrd 2814 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
242 2fveq3 6453 . . . . . . . . . . . . . . 15 (𝑖 = 1 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘1)))
243242fveq2d 6452 . . . . . . . . . . . . . 14 (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
244243fveq2d 6452 . . . . . . . . . . . . 13 (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
245229, 227, 244fsum1p 14898 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
2465, 6, 7, 8algr0 15701 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾‘1) = 𝐶)
247246fveq2d 6452 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺𝐶))
248247fveq2d 6452 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺𝐶)))
249248fveq2d 6452 . . . . . . . . . . . . 13 (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺𝐶))))
2507peano2zd 11842 . . . . . . . . . . . . . . 15 (𝜑 → (1 + 1) ∈ ℤ)
251190nnzd 11838 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
252 fzp1ss 12714 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
25368, 252mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
254253sselda 3821 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
255254, 227syldan 585 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
256 2fveq3 6453 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
257256fveq2d 6452 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
258257fveq2d 6452 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
2597, 250, 251, 255, 258fsumshftm 14926 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
260 ax-1cn 10332 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
261260, 260pncan3oi 10641 . . . . . . . . . . . . . . . . 17 ((1 + 1) − 1) = 1
262261oveq1i 6934 . . . . . . . . . . . . . . . 16 (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
263262sumeq1i 14845 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
264 fvoveq1 6947 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
265264fveq2d 6452 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
266265fveq2d 6452 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
267266fveq2d 6452 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
268267cbvsumv 14843 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
269263, 268eqtri 2802 . . . . . . . . . . . . . 14 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
270259, 269syl6eq 2830 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
271249, 270oveq12d 6942 . . . . . . . . . . . 12 (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
272245, 271eqtrd 2814 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
273241, 272oveq12d 6942 . . . . . . . . . 10 (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
274200recnd 10407 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℂ)
275 peano2nn 11393 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
276 ffvelrn 6623 . . . . . . . . . . . . . . . . . 18 ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
27715, 275, 276syl2an 589 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
278215, 277ffvelrnd 6626 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
279214, 278ffvelrnd 6626 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
280 xp1st 7479 . . . . . . . . . . . . . . 15 ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
281279, 280syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
282235, 281sylan2 586 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
283234, 282fsumrecl 14881 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
284283recnd 10407 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
285239, 238, 274, 284addsub4d 10783 . . . . . . . . . 10 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
286228, 273, 2853eqtrd 2818 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
287205, 213, 2863eqtrd 2818 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
288287, 185eqeltrrd 2860 . . . . . . 7 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
289 fveq2 6448 . . . . . . . . . . . . . . 15 (𝑛 = 𝑀 → (𝐾𝑛) = (𝐾𝑀))
290289eleq2d 2845 . . . . . . . . . . . . . 14 (𝑛 = 𝑀 → (𝐵 ∈ (𝐾𝑛) ↔ 𝐵 ∈ (𝐾𝑀)))
291290, 62elrab2 3576 . . . . . . . . . . . . 13 (𝑀𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
292117, 291sylib 210 . . . . . . . . . . . 12 (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
293292simprd 491 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐾𝑀))
29493, 94, 95, 96, 97, 71, 98, 4, 99ovolicc2lem1 23732 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐾𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
295191, 294mpdan 677 . . . . . . . . . . 11 (𝜑 → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
296293, 295mpbid 224 . . . . . . . . . 10 (𝜑 → (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
297296simp3d 1135 . . . . . . . . 9 (𝜑𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
29893, 94, 95, 96, 97, 71, 98, 4, 99ovolicc2lem1 23732 . . . . . . . . . . . 12 ((𝜑𝐶𝑈) → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
299196, 298mpdan 677 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
300101, 299mpbid 224 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶)))))
301300simp2d 1134 . . . . . . . . 9 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴)
30294, 200, 195, 93, 297, 301lt2subd 11002 . . . . . . . 8 (𝜑 → (𝐵𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
303155, 201, 302ltled 10526 . . . . . . 7 (𝜑 → (𝐵𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
304235adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
305 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
306251adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
307 elfzm11 12734 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
30868, 306, 307sylancr 581 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
309305, 308mpbid 224 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀))
310309simp3d 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
311304nnred 11396 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
312118adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
313311, 312ltnled 10525 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀𝑖))
314310, 313mpbid 224 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀𝑖)
315 infssuzle 12083 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑖𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
31667, 315mpan 680 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
31766, 316syl5eqbr 4923 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑊𝑀𝑖)
318314, 317nsyl 138 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖𝑊)
319304, 318jca 507 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊))
32093, 94, 95, 96, 97, 71, 98, 4, 99, 11, 9, 100, 101, 8, 6, 62ovolicc2lem2 23733 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
321319, 320syldan 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
322321iftrued 4315 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
323 2fveq3 6453 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑖) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑖))))
324323fveq2d 6452 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐾𝑖) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
325324breq1d 4898 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵))
326325, 324ifbieq1d 4330 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵))
327 fveq2 6448 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → (𝐻𝑡) = (𝐻‘(𝐾𝑖)))
328326, 327eleq12d 2853 . . . . . . . . . . . . . . . 16 (𝑡 = (𝐾𝑖) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
329100ralrimiva 3148 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
330329adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
331 ffvelrn 6623 . . . . . . . . . . . . . . . . 17 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑇)
33210, 235, 331syl2an 589 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾𝑖) ∈ 𝑇)
333328, 330, 332rspcdva 3517 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖)))
334322, 333eqeltrrd 2860 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐻‘(𝐾𝑖)))
3355, 6, 7, 8, 9algrp1 15703 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
336235, 335sylan2 586 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
337334, 336eleqtrrd 2862 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
338235, 277sylan2 586 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
33993, 94, 95, 96, 97, 71, 98, 4, 99ovolicc2lem1 23732 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
340338, 339syldan 585 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
341337, 340mpbid 224 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
342341simp2d 1134 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
343282, 236, 342ltled 10526 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
344234, 282, 236, 343fsumle 14944 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
345237, 283subge0d 10968 . . . . . . . . 9 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
346344, 345mpbird 249 . . . . . . . 8 (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
347237, 283resubcld 10806 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
348201, 347addge01d 10966 . . . . . . . 8 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))))
349346, 348mpbid 224 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
350155, 201, 288, 303, 349letrd 10535 . . . . . 6 (𝜑 → (𝐵𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
351350, 287breqtrrd 4916 . . . . 5 (𝜑 → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
352351adantr 474 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
353 fzfid 13096 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
354167adantlr 705 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
355166simprd 491 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
356355adantlr 705 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
35723adantr 474 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℕ) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
358357sselda 3821 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
359358nnred 11396 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
36030ad2antlr 717 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
361 ltle 10467 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧𝑦𝑧))
362359, 360, 361syl2anc 579 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦𝑧))
363358, 5syl6eleq 2869 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ‘1))
364 nnz 11756 . . . . . . . . . . 11 (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
365364ad2antlr 717 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
366 elfz5 12656 . . . . . . . . . 10 ((𝑦 ∈ (ℤ‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
367363, 365, 366syl2anc 579 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
368362, 367sylibrd 251 . . . . . . . 8 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦 ∈ (1...𝑧)))
369368ralimdva 3144 . . . . . . 7 ((𝜑𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
370369impr 448 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
371 dfss3 3810 . . . . . 6 (((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
372370, 371sylibr 226 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
373353, 354, 356, 372fsumless 14941 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
374181, 186, 169, 352, 373letrd 10535 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
375 eqidd 2779 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
376 simprl 761 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
377376, 5syl6eleq 2869 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ‘1))
378354recnd 10407 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
379375, 377, 378fsumser 14877 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
38096fveq1i 6449 . . . . 5 (𝑆𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
381379, 380syl6eqr 2832 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆𝑧))
382177adantr 474 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆ ℝ*)
383172ffnd 6294 . . . . . . 7 (𝜑𝑆 Fn ℕ)
384383adantr 474 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ)
385 fnfvelrn 6622 . . . . . 6 ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆𝑧) ∈ ran 𝑆)
386384, 376, 385syl2anc 579 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ∈ ran 𝑆)
387 supxrub 12471 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑧) ∈ ran 𝑆) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
388382, 386, 387syl2anc 579 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
389381, 388eqbrtrd 4910 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
390157, 170, 180, 374, 389xrletrd 12310 . 2 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
391154, 390rexlimddv 3218 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969  wral 3090  wrex 3091  {crab 3094  cin 3791  wss 3792  c0 4141  ifcif 4307  𝒫 cpw 4379  {csn 4398   cuni 4673   class class class wbr 4888   × cxp 5355  ran crn 5358  cres 5359  cima 5360  ccom 5361   Fn wfn 6132  wf 6133  1-1wf1 6134  ontowfo 6135  1-1-ontowf1o 6136  cfv 6137  (class class class)co 6924  1st c1st 7445  2nd c2nd 7446  cdom 8241  Fincfn 8243  supcsup 8636  infcinf 8637  cc 10272  cr 10273  0cc0 10274  1c1 10275   + caddc 10277  +∞cpnf 10410  *cxr 10412   < clt 10413  cle 10414  cmin 10608  cn 11379  cz 11733  cuz 11997  (,)cioo 12492  [,)cico 12494  [,]cicc 12495  ...cfz 12648  seqcseq 13124  abscabs 14387  Σcsu 14833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11036  df-nn 11380  df-2 11443  df-3 11444  df-n0 11648  df-z 11734  df-uz 11998  df-rp 12143  df-ioo 12496  df-ico 12498  df-icc 12499  df-fz 12649  df-fzo 12790  df-seq 13125  df-exp 13184  df-hash 13442  df-cj 14252  df-re 14253  df-im 14254  df-sqrt 14388  df-abs 14389  df-clim 14636  df-sum 14834
This theorem is referenced by:  ovolicc2lem5  23736
  Copyright terms: Public domain W3C validator