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

Theorem ovolicc2lem4 23095
 Description: Lemma for ovolicc2 23097. (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 11166 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
21ad2antlr 759 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3 df-ima 5051 . . . . . . . . . . . . . . . 16 ((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀))
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐺:𝑈⟶ℕ)
5 nnuz 11599 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7 1zzd 11285 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℤ)
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶𝑇)
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻:𝑇𝑇)
105, 6, 7, 8, 9algrf 15124 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾:ℕ⟶𝑇)
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12 ssrab2 3650 . . . . . . . . . . . . . . . . . . . . 21 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
1311, 12eqsstri 3598 . . . . . . . . . . . . . . . . . . . 20 𝑇𝑈
14 fss 5969 . . . . . . . . . . . . . . . . . . . 20 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
1510, 13, 14sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶𝑈)
16 fco 5971 . . . . . . . . . . . . . . . . . . 19 ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺𝐾):ℕ⟶ℕ)
174, 15, 16syl2anc 691 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝐾):ℕ⟶ℕ)
18 elfznn 12241 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
1918ssriv 3572 . . . . . . . . . . . . . . . . . 18 (1...𝑀) ⊆ ℕ
20 fssres 5983 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2117, 19, 20sylancl 693 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
22 frn 5966 . . . . . . . . . . . . . . . . 17 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
2321, 22syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
243, 23syl5eqss 3612 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
25 nnssre 10901 . . . . . . . . . . . . . . 15 ℕ ⊆ ℝ
2624, 25syl6ss 3580 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
2726ad3antrrr 762 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
28 simpr 476 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀)))
2927, 28sseldd 3569 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
30 simpllr 795 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
31 nnre 10904 . . . . . . . . . . . . 13 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
3231ad2antlr 759 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
33 lelttr 10007 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3429, 30, 32, 33syl3anc 1318 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3534ancomsd 469 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧𝑦𝑥) → 𝑦 < 𝑧))
3635expdimp 452 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦𝑥𝑦 < 𝑧))
3736an32s 842 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦𝑥𝑦 < 𝑧))
3837ralimdva 2945 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3938impancom 455 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4039an32s 842 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4140reximdva 3000 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
422, 41mpd 15 . . 3 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
43 fzfid 12634 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
44 fvres 6117 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
4544adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
46 fvco3 6185 . . . . . . . . . . . . . . 15 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4710, 18, 46syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4845, 47eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
4948adantrr 749 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
50 fvres 6117 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
5150ad2antll 761 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
52 elfznn 12241 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
5352adantl 481 . . . . . . . . . . . . . 14 ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
54 fvco3 6185 . . . . . . . . . . . . . 14 ((𝐾:ℕ⟶𝑇𝑗 ∈ ℕ) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5510, 53, 54syl2an 493 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5651, 55eqtrd 2644 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾𝑗)))
5749, 56eqeq12d 2625 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗))))
58 fveq2 6103 . . . . . . . . . . . . 13 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
5958fveq2d 6107 . . . . . . . . . . . 12 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
6019a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑀) ⊆ ℕ)
61 elfznn 12241 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
6261ad2antlr 759 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℕ)
6362nnred 10912 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℝ)
64 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
65 ssrab2 3650 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
6664, 65eqsstri 3598 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 ⊆ ℕ
6766, 25sstri 3577 . . . . . . . . . . . . . . . . . . . . 21 𝑊 ⊆ ℝ
68 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 = inf(𝑊, ℝ, < )
6966, 5sseqtri 3600 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 ⊆ (ℤ‘1)
70 1z 11284 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℤ
715uzinf 12626 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ ℕ ∈ Fin
73 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
74 elin 3758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin) ↔ (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7573, 74sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7675simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑈 ∈ Fin)
77 ssfi 8065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
7876, 13, 77sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑇 ∈ Fin)
7978adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → 𝑇 ∈ Fin)
8010adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
81 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾𝑖) = (𝐾𝑗) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)))
8281fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾𝑖) = (𝐾𝑗) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
8382fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐾𝑖) = (𝐾𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
84 simpll 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
85 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
86 ral0 4028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑚 ∈ ∅ 𝑛𝑚
87 simplr 788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
8887raleqdv 3121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛𝑚))
8986, 88mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚𝑊 𝑛𝑚)
9089ralrimivw 2950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
91 rabid2 3096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
9290, 91sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
9385, 92eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
94 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
9594, 92eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
96 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴 ∈ ℝ)
97 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐵 ∈ ℝ)
98 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝐵)
99 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
100 ovolicc2.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
101 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (𝐴[,]𝐵) ⊆ 𝑈)
102 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑈) → (((,) ∘ 𝐹)‘(𝐺𝑡)) = 𝑡)
103 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
104 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐴𝐶)
10596, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem3 23094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10684, 93, 95, 105syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10783, 106syl5ibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
108107ralrimivva 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
109 dff13 6416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾:ℕ–1-1𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗)))
11080, 108, 109sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑊 = ∅) → 𝐾:ℕ–1-1𝑇)
111 f1domg 7861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 ∈ Fin → (𝐾:ℕ–1-1𝑇 → ℕ ≼ 𝑇))
11279, 110, 111sylc 63 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → ℕ ≼ 𝑇)
113 domfi 8066 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
11479, 112, 113syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑊 = ∅) → ℕ ∈ Fin)
115114ex 449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
116115necon3bd 2796 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
11772, 116mpi 20 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑊 ≠ ∅)
118 infssuzcl 11648 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
11969, 117, 118sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
12068, 119syl5eqel 2692 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀𝑊)
12167, 120sseldi 3566 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
122121ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀 ∈ ℝ)
12367sseli 3564 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑚 ∈ ℝ)
124123adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
125 elfzle2 12216 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑀) → 𝑛𝑀)
126125ad2antlr 759 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑀)
127 infssuzle 11647 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑚𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
12869, 127mpan 702 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
12968, 128syl5eqbr 4618 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑀𝑚)
130129adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀𝑚)
13163, 122, 124, 126, 130letrd 10073 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑚)
132131ralrimiva 2949 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑀)) → ∀𝑚𝑊 𝑛𝑚)
13360, 132ssrabdv 3644 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
134133adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
135 simprl 790 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
136134, 135sseldd 3569 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
137 simprr 792 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
138134, 137sseldd 3569 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
139136, 138jca 553 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}))
140139, 105syldan 486 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
14159, 140syl5ibr 235 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → 𝑖 = 𝑗))
14257, 141sylbid 229 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
143142ralrimivva 2954 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
144 dff13 6416 . . . . . . . . 9 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
14521, 143, 144sylanbrc 695 . . . . . . . 8 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
146 f1f1orn 6061 . . . . . . . 8 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀)))
147145, 146syl 17 . . . . . . 7 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀)))
148 f1oeq3 6042 . . . . . . . 8 (((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) ↔ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀))))
1493, 148ax-mp 5 . . . . . . 7 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) ↔ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran ((𝐺𝐾) ↾ (1...𝑀)))
150147, 149sylibr 223 . . . . . 6 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)))
151 f1ofo 6057 . . . . . 6 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
152150, 151syl 17 . . . . 5 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
153 fofi 8135 . . . . 5 (((1...𝑀) ∈ Fin ∧ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
15443, 152, 153syl2anc 691 . . . 4 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
155 fimaxre2 10848 . . . 4 ((((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15626, 154, 155syl2anc 691 . . 3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15742, 156r19.29a 3060 . 2 (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
15897, 96resubcld 10337 . . . . 5 (𝜑 → (𝐵𝐴) ∈ ℝ)
159158rexrd 9968 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ*)
160159adantr 480 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ*)
161 fzfid 12634 . . . . . 6 (𝜑 → (1...𝑧) ∈ Fin)
162 elfznn 12241 . . . . . . . . 9 (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
163 eqid 2610 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
164163ovolfsf 23047 . . . . . . . . . . 11 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
165100, 164syl 17 . . . . . . . . . 10 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
166165ffvelrnda 6267 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
167162, 166sylan2 490 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
168 elrege0 12149 . . . . . . . 8 ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
169167, 168sylib 207 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
170169simpld 474 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
171161, 170fsumrecl 14312 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
172171adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
173172rexrd 9968 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
174163, 99ovolsf 23048 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
175100, 174syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
176 frn 5966 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
177175, 176syl 17 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
178 rge0ssre 12151 . . . . . . 7 (0[,)+∞) ⊆ ℝ
179177, 178syl6ss 3580 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
180 ressxr 9962 . . . . . 6 ℝ ⊆ ℝ*
181179, 180syl6ss 3580 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
182 supxrcl 12017 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
183181, 182syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
184183adantr 480 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
185158adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ)
18624sselda 3568 . . . . . . 7 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
187178, 166sseldi 3566 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
188186, 187syldan 486 . . . . . 6 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
189154, 188fsumrecl 14312 . . . . 5 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
190189adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
191 inss2 3796 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
192 fss 5969 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
193100, 191, 192sylancl 693 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
19466, 120sseldi 3566 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
19515, 194ffvelrnd 6268 . . . . . . . . . . 11 (𝜑 → (𝐾𝑀) ∈ 𝑈)
1964, 195ffvelrnd 6268 . . . . . . . . . 10 (𝜑 → (𝐺‘(𝐾𝑀)) ∈ ℕ)
197193, 196ffvelrnd 6268 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ))
198 xp2nd 7090 . . . . . . . . 9 ((𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
199197, 198syl 17 . . . . . . . 8 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
20013, 8sseldi 3566 . . . . . . . . . . 11 (𝜑𝐶𝑈)
2014, 200ffvelrnd 6268 . . . . . . . . . 10 (𝜑 → (𝐺𝐶) ∈ ℕ)
202193, 201ffvelrnd 6268 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ))
203 xp1st 7089 . . . . . . . . 9 ((𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
204202, 203syl 17 . . . . . . . 8 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
205199, 204resubcld 10337 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ∈ ℝ)
206 fveq2 6103 . . . . . . . . . 10 (𝑗 = (𝐺‘(𝐾𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
207187recnd 9947 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
208186, 207syldan 486 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
209206, 43, 150, 48, 208fsumf1o 14301 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
210100adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2114adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
212 ffvelrn 6265 . . . . . . . . . . . . 13 ((𝐾:ℕ⟶𝑈𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
21315, 18, 212syl2an 493 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) ∈ 𝑈)
214211, 213ffvelrnd 6268 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
215163ovolfsval 23046 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
216210, 214, 215syl2anc 691 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
217216sumeq2dv 14281 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
218193adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
2194adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
22015ffvelrnda 6267 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
221219, 220ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
222218, 221ffvelrnd 6268 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
223 xp2nd 7090 . . . . . . . . . . . . . 14 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
224222, 223syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
22518, 224sylan2 490 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
226225recnd 9947 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
227193adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
228227, 214ffvelrnd 6268 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
229 xp1st 7089 . . . . . . . . . . . . 13 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
230228, 229syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
231230recnd 9947 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
23243, 226, 231fsumsub 14362 . . . . . . . . . 10 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
23369, 120sseldi 3566 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ‘1))
234 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑀 → (𝐾𝑖) = (𝐾𝑀))
235234fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑀)))
236235fveq2d 6107 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑀))))
237236fveq2d 6107 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
238233, 226, 237fsumm1 14324 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
239 fzfid 12634 . . . . . . . . . . . . . . 15 (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
240 elfznn 12241 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
241240, 224sylan2 490 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
242239, 241fsumrecl 14312 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
243242recnd 9947 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
244199recnd 9947 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℂ)
245243, 244addcomd 10117 . . . . . . . . . . . 12 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
246238, 245eqtrd 2644 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
247 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝐾𝑖) = (𝐾‘1))
248247fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑖 = 1 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘1)))
249248fveq2d 6107 . . . . . . . . . . . . . 14 (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
250249fveq2d 6107 . . . . . . . . . . . . 13 (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
251233, 231, 250fsum1p 14326 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
2525, 6, 7, 8algr0 15123 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾‘1) = 𝐶)
253252fveq2d 6107 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺𝐶))
254253fveq2d 6107 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺𝐶)))
255254fveq2d 6107 . . . . . . . . . . . . 13 (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺𝐶))))
2567peano2zd 11361 . . . . . . . . . . . . . . 15 (𝜑 → (1 + 1) ∈ ℤ)
257194nnzd 11357 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
258 fzp1ss 12262 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
25970, 258mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
260259sselda 3568 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
261260, 231syldan 486 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
262 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 + 1) → (𝐾𝑖) = (𝐾‘(𝑗 + 1)))
263262fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
264263fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
265264fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
2667, 256, 257, 261, 265fsumshftm 14355 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
267 ax-1cn 9873 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
268267, 267pncan3oi 10176 . . . . . . . . . . . . . . . . 17 ((1 + 1) − 1) = 1
269268oveq1i 6559 . . . . . . . . . . . . . . . 16 (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
270269sumeq1i 14276 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
271 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
272271fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
273272fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
274273fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
275274fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
276275cbvsumv 14274 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
277270, 276eqtri 2632 . . . . . . . . . . . . . 14 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
278266, 277syl6eq 2660 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
279255, 278oveq12d 6567 . . . . . . . . . . . 12 (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
280251, 279eqtrd 2644 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
281246, 280oveq12d 6567 . . . . . . . . . 10 (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
282204recnd 9947 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℂ)
283 peano2nn 10909 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
284 ffvelrn 6265 . . . . . . . . . . . . . . . . . 18 ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
28515, 283, 284syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
286219, 285ffvelrnd 6268 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
287218, 286ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
288 xp1st 7089 . . . . . . . . . . . . . . 15 ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
289287, 288syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
290240, 289sylan2 490 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
291239, 290fsumrecl 14312 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
292291recnd 9947 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
293244, 243, 282, 292addsub4d 10318 . . . . . . . . . 10 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
294232, 281, 2933eqtrd 2648 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
295209, 217, 2943eqtrd 2648 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
296295, 189eqeltrrd 2689 . . . . . . 7 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
297 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑛 = 𝑀 → (𝐾𝑛) = (𝐾𝑀))
298297eleq2d 2673 . . . . . . . . . . . . . 14 (𝑛 = 𝑀 → (𝐵 ∈ (𝐾𝑛) ↔ 𝐵 ∈ (𝐾𝑀)))
299298, 64elrab2 3333 . . . . . . . . . . . . 13 (𝑀𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
300120, 299sylib 207 . . . . . . . . . . . 12 (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
301300simprd 478 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐾𝑀))
30296, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23092 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐾𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
303195, 302mpdan 699 . . . . . . . . . . 11 (𝜑 → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
304301, 303mpbid 221 . . . . . . . . . 10 (𝜑 → (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
305304simp3d 1068 . . . . . . . . 9 (𝜑𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
30696, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23092 . . . . . . . . . . . 12 ((𝜑𝐶𝑈) → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
307200, 306mpdan 699 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
308104, 307mpbid 221 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶)))))
309308simp2d 1067 . . . . . . . . 9 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴)
31097, 204, 199, 96, 305, 309lt2subd 10530 . . . . . . . 8 (𝜑 → (𝐵𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
311158, 205, 310ltled 10064 . . . . . . 7 (𝜑 → (𝐵𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
312240adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
313 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
314257adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
315 elfzm11 12280 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
31670, 314, 315sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
317313, 316mpbid 221 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀))
318317simp3d 1068 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
319312nnred 10912 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
320121adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
321319, 320ltnled 10063 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀𝑖))
322318, 321mpbid 221 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀𝑖)
323 infssuzle 11647 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑖𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
32469, 323mpan 702 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
32568, 324syl5eqbr 4618 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑊𝑀𝑖)
326322, 325nsyl 134 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖𝑊)
327312, 326jca 553 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊))
32896, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem2 23093 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
329327, 328syldan 486 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
330329iftrued 4044 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
331 ffvelrn 6265 . . . . . . . . . . . . . . . . 17 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑇)
33210, 240, 331syl2an 493 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾𝑖) ∈ 𝑇)
333103ralrimiva 2949 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
334333adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
335 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑖) → (𝐺𝑡) = (𝐺‘(𝐾𝑖)))
336335fveq2d 6107 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑖) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑖))))
337336fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑖) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
338337breq1d 4593 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐾𝑖) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵))
339338, 337ifbieq1d 4059 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵))
340 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → (𝐻𝑡) = (𝐻‘(𝐾𝑖)))
341339, 340eleq12d 2682 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
342341rspcv 3278 . . . . . . . . . . . . . . . 16 ((𝐾𝑖) ∈ 𝑇 → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
343332, 334, 342sylc 63 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖)))
344330, 343eqeltrrd 2689 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐻‘(𝐾𝑖)))
3455, 6, 7, 8, 9algrp1 15125 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
346240, 345sylan2 490 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
347344, 346eleqtrrd 2691 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
348240, 285sylan2 490 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
34996, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23092 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
350348, 349syldan 486 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
351347, 350mpbid 221 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
352351simp2d 1067 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
353290, 241, 352ltled 10064 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
354239, 290, 241, 353fsumle 14372 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
355242, 291subge0d 10496 . . . . . . . . 9 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
356354, 355mpbird 246 . . . . . . . 8 (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
357242, 291resubcld 10337 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
358205, 357addge01d 10494 . . . . . . . 8 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))))
359356, 358mpbid 221 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
360158, 205, 296, 311, 359letrd 10073 . . . . . 6 (𝜑 → (𝐵𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
361360, 295breqtrrd 4611 . . . . 5 (𝜑 → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
362361adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
363 fzfid 12634 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
364170adantlr 747 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
365169simprd 478 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
366365adantlr 747 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
36724adantr 480 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℕ) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
368367sselda 3568 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
369368nnred 10912 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
37031ad2antlr 759 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
371 ltle 10005 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧𝑦𝑧))
372369, 370, 371syl2anc 691 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦𝑧))
373368, 5syl6eleq 2698 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ‘1))
374 nnz 11276 . . . . . . . . . . 11 (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
375374ad2antlr 759 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
376 elfz5 12205 . . . . . . . . . 10 ((𝑦 ∈ (ℤ‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
377373, 375, 376syl2anc 691 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
378372, 377sylibrd 248 . . . . . . . 8 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦 ∈ (1...𝑧)))
379378ralimdva 2945 . . . . . . 7 ((𝜑𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
380379impr 647 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
381 dfss3 3558 . . . . . 6 (((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
382380, 381sylibr 223 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
383363, 364, 366, 382fsumless 14369 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
384185, 190, 172, 362, 383letrd 10073 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
385 eqidd 2611 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
386 simprl 790 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
387386, 5syl6eleq 2698 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ‘1))
388364recnd 9947 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
389385, 387, 388fsumser 14308 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
39099fveq1i 6104 . . . . 5 (𝑆𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
391389, 390syl6eqr 2662 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆𝑧))
392181adantr 480 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆ ℝ*)
393 ffn 5958 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
394175, 393syl 17 . . . . . . 7 (𝜑𝑆 Fn ℕ)
395394adantr 480 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ)
396 fnfvelrn 6264 . . . . . 6 ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆𝑧) ∈ ran 𝑆)
397395, 386, 396syl2anc 691 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ∈ ran 𝑆)
398 supxrub 12026 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑧) ∈ ran 𝑆) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
399392, 397, 398syl2anc 691 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
400391, 399eqbrtrd 4605 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
401160, 173, 184, 384, 400xrletrd 11869 . 2 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
402157, 401rexlimddv 3017 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   class class class wbr 4583   × cxp 5036  ran crn 5039   ↾ cres 5040   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  1st c1st 7057  2nd c2nd 7058   ≼ cdom 7839  Fincfn 7841  supcsup 8229  infcinf 8230  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℤcz 11254  ℤ≥cuz 11563  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  ...cfz 12197  seqcseq 12663  abscabs 13822  Σcsu 14264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265 This theorem is referenced by:  ovolicc2lem5  23096
 Copyright terms: Public domain W3C validator