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

Theorem ovolicc2lem4 23334
Description: Lemma for ovolicc2 23336. (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 11327 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
21ad2antlr 763 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3 df-ima 5156 . . . . . . . . . . . . . . . 16 ((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀))
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐺:𝑈⟶ℕ)
5 nnuz 11761 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7 1zzd 11446 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℤ)
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶𝑇)
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻:𝑇𝑇)
105, 6, 7, 8, 9algrf 15333 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾:ℕ⟶𝑇)
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12 ssrab2 3720 . . . . . . . . . . . . . . . . . . . . 21 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
1311, 12eqsstri 3668 . . . . . . . . . . . . . . . . . . . 20 𝑇𝑈
14 fss 6094 . . . . . . . . . . . . . . . . . . . 20 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
1510, 13, 14sylancl 695 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶𝑈)
16 fco 6096 . . . . . . . . . . . . . . . . . . 19 ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺𝐾):ℕ⟶ℕ)
174, 15, 16syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝐾):ℕ⟶ℕ)
18 elfznn 12408 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
1918ssriv 3640 . . . . . . . . . . . . . . . . . 18 (1...𝑀) ⊆ ℕ
20 fssres 6108 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2117, 19, 20sylancl 695 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
22 frn 6091 . . . . . . . . . . . . . . . . 17 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
2321, 22syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
243, 23syl5eqss 3682 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
25 nnssre 11062 . . . . . . . . . . . . . . 15 ℕ ⊆ ℝ
2624, 25syl6ss 3648 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
2726ad3antrrr 766 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
28 simpr 476 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀)))
2927, 28sseldd 3637 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
30 simpllr 815 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
31 nnre 11065 . . . . . . . . . . . . 13 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
3231ad2antlr 763 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
33 lelttr 10166 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3429, 30, 32, 33syl3anc 1366 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3534ancomsd 469 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧𝑦𝑥) → 𝑦 < 𝑧))
3635expdimp 452 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦𝑥𝑦 < 𝑧))
3736an32s 863 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦𝑥𝑦 < 𝑧))
3837ralimdva 2991 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3938impancom 455 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4039an32s 863 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4140reximdva 3046 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
422, 41mpd 15 . . 3 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
43 fzfid 12812 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
44 fvres 6245 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
4544adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
46 fvco3 6314 . . . . . . . . . . . . . . 15 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4710, 18, 46syl2an 493 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4845, 47eqtrd 2685 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
4948adantrr 753 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
50 fvres 6245 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
5150ad2antll 765 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
52 elfznn 12408 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
5352adantl 481 . . . . . . . . . . . . . 14 ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
54 fvco3 6314 . . . . . . . . . . . . . 14 ((𝐾:ℕ⟶𝑇𝑗 ∈ ℕ) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5510, 53, 54syl2an 493 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5651, 55eqtrd 2685 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾𝑗)))
5749, 56eqeq12d 2666 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗))))
58 fveq2 6229 . . . . . . . . . . . . 13 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
5958fveq2d 6233 . . . . . . . . . . . 12 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
6019a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑀) ⊆ ℕ)
61 elfznn 12408 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
6261ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℕ)
6362nnred 11073 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℝ)
64 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
65 ssrab2 3720 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
6664, 65eqsstri 3668 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 ⊆ ℕ
6766, 25sstri 3645 . . . . . . . . . . . . . . . . . . . . 21 𝑊 ⊆ ℝ
68 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 = inf(𝑊, ℝ, < )
6966, 5sseqtri 3670 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 ⊆ (ℤ‘1)
70 1z 11445 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℤ
715uzinf 12804 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ ℕ ∈ Fin
73 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
74 elin 3829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin) ↔ (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7573, 74sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7675simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑈 ∈ Fin)
77 ssfi 8221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
7876, 13, 77sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑇 ∈ Fin)
7978adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → 𝑇 ∈ Fin)
8010adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
81 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾𝑖) = (𝐾𝑗) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)))
8281fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾𝑖) = (𝐾𝑗) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
8382fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐾𝑖) = (𝐾𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
84 simpll 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
85 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
86 ral0 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑚 ∈ ∅ 𝑛𝑚
87 simplr 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
8887raleqdv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛𝑚))
8986, 88mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚𝑊 𝑛𝑚)
9089ralrimivw 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
91 rabid2 3148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
9290, 91sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
9385, 92eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
94 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
9594, 92eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10684, 93, 95, 105syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10783, 106syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
108107ralrimivva 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
109 dff13 6552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾:ℕ–1-1𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗)))
11080, 108, 109sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑊 = ∅) → 𝐾:ℕ–1-1𝑇)
111 f1domg 8017 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 ∈ Fin → (𝐾:ℕ–1-1𝑇 → ℕ ≼ 𝑇))
11279, 110, 111sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → ℕ ≼ 𝑇)
113 domfi 8222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
11479, 112, 113syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑊 = ∅) → ℕ ∈ Fin)
115114ex 449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
116115necon3bd 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
11772, 116mpi 20 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑊 ≠ ∅)
118 infssuzcl 11810 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
11969, 117, 118sylancr 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
12068, 119syl5eqel 2734 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀𝑊)
12167, 120sseldi 3634 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
122121ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀 ∈ ℝ)
12367sseli 3632 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑚 ∈ ℝ)
124123adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
125 elfzle2 12383 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑀) → 𝑛𝑀)
126125ad2antlr 763 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑀)
127 infssuzle 11809 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑚𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
12869, 127mpan 706 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
12968, 128syl5eqbr 4720 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑀𝑚)
130129adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀𝑚)
13163, 122, 124, 126, 130letrd 10232 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑚)
132131ralrimiva 2995 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑀)) → ∀𝑚𝑊 𝑛𝑚)
13360, 132ssrabdv 3714 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
134133adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
135 simprl 809 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
136134, 135sseldd 3637 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
137 simprr 811 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
138134, 137sseldd 3637 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
139136, 138jca 553 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}))
140139, 105syldan 486 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
14159, 140syl5ibr 236 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → 𝑖 = 𝑗))
14257, 141sylbid 230 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
143142ralrimivva 3000 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
144 dff13 6552 . . . . . . . . 9 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
14521, 143, 144sylanbrc 699 . . . . . . . 8 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
146 f1f1orn 6186 . . . . . . . 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 6167 . . . . . . . 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 224 . . . . . 6 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)))
151 f1ofo 6182 . . . . . 6 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
152150, 151syl 17 . . . . 5 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
153 fofi 8293 . . . . 5 (((1...𝑀) ∈ Fin ∧ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
15443, 152, 153syl2anc 694 . . . 4 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
155 fimaxre2 11007 . . . 4 ((((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15626, 154, 155syl2anc 694 . . 3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15742, 156r19.29a 3107 . 2 (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
15897, 96resubcld 10496 . . . . 5 (𝜑 → (𝐵𝐴) ∈ ℝ)
159158rexrd 10127 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ*)
160159adantr 480 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ*)
161 fzfid 12812 . . . . . 6 (𝜑 → (1...𝑧) ∈ Fin)
162 elfznn 12408 . . . . . . . . 9 (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
163 eqid 2651 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
164163ovolfsf 23286 . . . . . . . . . . 11 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
165100, 164syl 17 . . . . . . . . . 10 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
166165ffvelrnda 6399 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
167162, 166sylan2 490 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
168 elrege0 12316 . . . . . . . 8 ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
169167, 168sylib 208 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
170169simpld 474 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
171161, 170fsumrecl 14509 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
172171adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
173172rexrd 10127 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
174163, 99ovolsf 23287 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
175100, 174syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
176 frn 6091 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
177175, 176syl 17 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
178 rge0ssre 12318 . . . . . . 7 (0[,)+∞) ⊆ ℝ
179177, 178syl6ss 3648 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
180 ressxr 10121 . . . . . 6 ℝ ⊆ ℝ*
181179, 180syl6ss 3648 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
182 supxrcl 12183 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
183181, 182syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
184183adantr 480 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
185158adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ)
18624sselda 3636 . . . . . . 7 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
187178, 166sseldi 3634 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
188186, 187syldan 486 . . . . . 6 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
189154, 188fsumrecl 14509 . . . . 5 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
190189adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
191 inss2 3867 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
192 fss 6094 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
193100, 191, 192sylancl 695 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
19466, 120sseldi 3634 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
19515, 194ffvelrnd 6400 . . . . . . . . . . 11 (𝜑 → (𝐾𝑀) ∈ 𝑈)
1964, 195ffvelrnd 6400 . . . . . . . . . 10 (𝜑 → (𝐺‘(𝐾𝑀)) ∈ ℕ)
197193, 196ffvelrnd 6400 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ))
198 xp2nd 7243 . . . . . . . . 9 ((𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
199197, 198syl 17 . . . . . . . 8 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
20013, 8sseldi 3634 . . . . . . . . . . 11 (𝜑𝐶𝑈)
2014, 200ffvelrnd 6400 . . . . . . . . . 10 (𝜑 → (𝐺𝐶) ∈ ℕ)
202193, 201ffvelrnd 6400 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ))
203 xp1st 7242 . . . . . . . . 9 ((𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
204202, 203syl 17 . . . . . . . 8 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
205199, 204resubcld 10496 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ∈ ℝ)
206 fveq2 6229 . . . . . . . . . 10 (𝑗 = (𝐺‘(𝐾𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
207187recnd 10106 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
208186, 207syldan 486 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
209206, 43, 150, 48, 208fsumf1o 14498 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
210100adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2114adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
212 ffvelrn 6397 . . . . . . . . . . . . 13 ((𝐾:ℕ⟶𝑈𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
21315, 18, 212syl2an 493 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) ∈ 𝑈)
214211, 213ffvelrnd 6400 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
215163ovolfsval 23285 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
216210, 214, 215syl2anc 694 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
217216sumeq2dv 14477 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
218193adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
2194adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
22015ffvelrnda 6399 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
221219, 220ffvelrnd 6400 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
222218, 221ffvelrnd 6400 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
223 xp2nd 7243 . . . . . . . . . . . . . 14 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
224222, 223syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
22518, 224sylan2 490 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
226225recnd 10106 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
227193adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
228227, 214ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
229 xp1st 7242 . . . . . . . . . . . . 13 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
230228, 229syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
231230recnd 10106 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
23243, 226, 231fsumsub 14564 . . . . . . . . . 10 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
23369, 120sseldi 3634 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ‘1))
234 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑀 → (𝐾𝑖) = (𝐾𝑀))
235234fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑀)))
236235fveq2d 6233 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑀))))
237236fveq2d 6233 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
238233, 226, 237fsumm1 14524 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
239 fzfid 12812 . . . . . . . . . . . . . . 15 (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
240 elfznn 12408 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
241240, 224sylan2 490 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
242239, 241fsumrecl 14509 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
243242recnd 10106 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
244199recnd 10106 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℂ)
245243, 244addcomd 10276 . . . . . . . . . . . 12 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
246238, 245eqtrd 2685 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
247 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝐾𝑖) = (𝐾‘1))
248247fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑖 = 1 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘1)))
249248fveq2d 6233 . . . . . . . . . . . . . 14 (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
250249fveq2d 6233 . . . . . . . . . . . . 13 (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
251233, 231, 250fsum1p 14526 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
2525, 6, 7, 8algr0 15332 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾‘1) = 𝐶)
253252fveq2d 6233 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺𝐶))
254253fveq2d 6233 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺𝐶)))
255254fveq2d 6233 . . . . . . . . . . . . 13 (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺𝐶))))
2567peano2zd 11523 . . . . . . . . . . . . . . 15 (𝜑 → (1 + 1) ∈ ℤ)
257194nnzd 11519 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
258 fzp1ss 12430 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
25970, 258mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
260259sselda 3636 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
261260, 231syldan 486 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
262 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 + 1) → (𝐾𝑖) = (𝐾‘(𝑗 + 1)))
263262fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
264263fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
265264fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
2667, 256, 257, 261, 265fsumshftm 14557 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
267 ax-1cn 10032 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
268267, 267pncan3oi 10335 . . . . . . . . . . . . . . . . 17 ((1 + 1) − 1) = 1
269268oveq1i 6700 . . . . . . . . . . . . . . . 16 (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
270269sumeq1i 14472 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
271 oveq1 6697 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
272271fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
273272fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
274273fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
275274fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
276275cbvsumv 14470 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
277270, 276eqtri 2673 . . . . . . . . . . . . . 14 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
278266, 277syl6eq 2701 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
279255, 278oveq12d 6708 . . . . . . . . . . . 12 (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
280251, 279eqtrd 2685 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
281246, 280oveq12d 6708 . . . . . . . . . 10 (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
282204recnd 10106 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℂ)
283 peano2nn 11070 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
284 ffvelrn 6397 . . . . . . . . . . . . . . . . . 18 ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
28515, 283, 284syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
286219, 285ffvelrnd 6400 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
287218, 286ffvelrnd 6400 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
288 xp1st 7242 . . . . . . . . . . . . . . 15 ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
289287, 288syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
290240, 289sylan2 490 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
291239, 290fsumrecl 14509 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
292291recnd 10106 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
293244, 243, 282, 292addsub4d 10477 . . . . . . . . . 10 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
294232, 281, 2933eqtrd 2689 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
295209, 217, 2943eqtrd 2689 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
296295, 189eqeltrrd 2731 . . . . . . 7 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
297 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑛 = 𝑀 → (𝐾𝑛) = (𝐾𝑀))
298297eleq2d 2716 . . . . . . . . . . . . . 14 (𝑛 = 𝑀 → (𝐵 ∈ (𝐾𝑛) ↔ 𝐵 ∈ (𝐾𝑀)))
299298, 64elrab2 3399 . . . . . . . . . . . . 13 (𝑀𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
300120, 299sylib 208 . . . . . . . . . . . 12 (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
301300simprd 478 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐾𝑀))
30296, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23331 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐾𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
303195, 302mpdan 703 . . . . . . . . . . 11 (𝜑 → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
304301, 303mpbid 222 . . . . . . . . . 10 (𝜑 → (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
305304simp3d 1095 . . . . . . . . 9 (𝜑𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
30696, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23331 . . . . . . . . . . . 12 ((𝜑𝐶𝑈) → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
307200, 306mpdan 703 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
308104, 307mpbid 222 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶)))))
309308simp2d 1094 . . . . . . . . 9 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴)
31097, 204, 199, 96, 305, 309lt2subd 10689 . . . . . . . 8 (𝜑 → (𝐵𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
311158, 205, 310ltled 10223 . . . . . . 7 (𝜑 → (𝐵𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
312240adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
313 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
314257adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
315 elfzm11 12449 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
31670, 314, 315sylancr 696 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
317313, 316mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀))
318317simp3d 1095 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
319312nnred 11073 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
320121adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
321319, 320ltnled 10222 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀𝑖))
322318, 321mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀𝑖)
323 infssuzle 11809 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑖𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
32469, 323mpan 706 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
32568, 324syl5eqbr 4720 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑊𝑀𝑖)
326322, 325nsyl 135 . . . . . . . . . . . . . . . . . 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 23332 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
329327, 328syldan 486 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
330329iftrued 4127 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
331 ffvelrn 6397 . . . . . . . . . . . . . . . . 17 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑇)
33210, 240, 331syl2an 493 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾𝑖) ∈ 𝑇)
333103ralrimiva 2995 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
334333adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
335 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑖) → (𝐺𝑡) = (𝐺‘(𝐾𝑖)))
336335fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑖) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑖))))
337336fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑖) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
338337breq1d 4695 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐾𝑖) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵))
339338, 337ifbieq1d 4142 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵))
340 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → (𝐻𝑡) = (𝐻‘(𝐾𝑖)))
341339, 340eleq12d 2724 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
342341rspcv 3336 . . . . . . . . . . . . . . . 16 ((𝐾𝑖) ∈ 𝑇 → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
343332, 334, 342sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖)))
344330, 343eqeltrrd 2731 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐻‘(𝐾𝑖)))
3455, 6, 7, 8, 9algrp1 15334 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
346240, 345sylan2 490 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
347344, 346eleqtrrd 2733 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
348240, 285sylan2 490 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
34996, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23331 . . . . . . . . . . . . . 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 222 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
352351simp2d 1094 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
353290, 241, 352ltled 10223 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
354239, 290, 241, 353fsumle 14575 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
355242, 291subge0d 10655 . . . . . . . . 9 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
356354, 355mpbird 247 . . . . . . . 8 (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
357242, 291resubcld 10496 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
358205, 357addge01d 10653 . . . . . . . 8 (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))))
359356, 358mpbid 222 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
360158, 205, 296, 311, 359letrd 10232 . . . . . 6 (𝜑 → (𝐵𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
361360, 295breqtrrd 4713 . . . . 5 (𝜑 → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
362361adantr 480 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
363 fzfid 12812 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
364170adantlr 751 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
365169simprd 478 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
366365adantlr 751 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
36724adantr 480 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℕ) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
368367sselda 3636 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
369368nnred 11073 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
37031ad2antlr 763 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
371 ltle 10164 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧𝑦𝑧))
372369, 370, 371syl2anc 694 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦𝑧))
373368, 5syl6eleq 2740 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ‘1))
374 nnz 11437 . . . . . . . . . . 11 (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
375374ad2antlr 763 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
376 elfz5 12372 . . . . . . . . . 10 ((𝑦 ∈ (ℤ‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
377373, 375, 376syl2anc 694 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
378372, 377sylibrd 249 . . . . . . . 8 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦 ∈ (1...𝑧)))
379378ralimdva 2991 . . . . . . 7 ((𝜑𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
380379impr 648 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
381 dfss3 3625 . . . . . 6 (((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
382380, 381sylibr 224 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
383363, 364, 366, 382fsumless 14572 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
384185, 190, 172, 362, 383letrd 10232 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
385 eqidd 2652 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
386 simprl 809 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
387386, 5syl6eleq 2740 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ‘1))
388364recnd 10106 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
389385, 387, 388fsumser 14505 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
39099fveq1i 6230 . . . . 5 (𝑆𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
391389, 390syl6eqr 2703 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆𝑧))
392181adantr 480 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆ ℝ*)
393 ffn 6083 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
394175, 393syl 17 . . . . . . 7 (𝜑𝑆 Fn ℕ)
395394adantr 480 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ)
396 fnfvelrn 6396 . . . . . 6 ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆𝑧) ∈ ran 𝑆)
397395, 386, 396syl2anc 694 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ∈ ran 𝑆)
398 supxrub 12192 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑧) ∈ ran 𝑆) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
399392, 397, 398syl2anc 694 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
400391, 399eqbrtrd 4707 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
401160, 173, 184, 384, 400xrletrd 12031 . 2 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
402157, 401rexlimddv 3064 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  cin 3606  wss 3607  c0 3948  ifcif 4119  𝒫 cpw 4191  {csn 4210   cuni 4468   class class class wbr 4685   × cxp 5141  ran crn 5144  cres 5145  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  cdom 7995  Fincfn 7997  supcsup 8387  infcinf 8388  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977  +∞cpnf 10109  *cxr 10111   < clt 10112  cle 10113  cmin 10304  cn 11058  cz 11415  cuz 11725  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  ...cfz 12364  seqcseq 12841  abscabs 14018  Σcsu 14460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461
This theorem is referenced by:  ovolicc2lem5  23335
  Copyright terms: Public domain W3C validator