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

Theorem ovolicc2lem4 23269
Description: Lemma for ovolicc2 23271. (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 11274 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
21ad2antlr 762 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧)
3 df-ima 5117 . . . . . . . . . . . . . . . 16 ((𝐺𝐾) “ (1...𝑀)) = ran ((𝐺𝐾) ↾ (1...𝑀))
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐺:𝑈⟶ℕ)
5 nnuz 11708 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))
7 1zzd 11393 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℤ)
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐶𝑇)
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻:𝑇𝑇)
105, 6, 7, 8, 9algrf 15267 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾:ℕ⟶𝑇)
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21 𝑇 = {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}
12 ssrab2 3679 . . . . . . . . . . . . . . . . . . . . 21 {𝑢𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈
1311, 12eqsstri 3627 . . . . . . . . . . . . . . . . . . . 20 𝑇𝑈
14 fss 6043 . . . . . . . . . . . . . . . . . . . 20 ((𝐾:ℕ⟶𝑇𝑇𝑈) → 𝐾:ℕ⟶𝑈)
1510, 13, 14sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾:ℕ⟶𝑈)
16 fco 6045 . . . . . . . . . . . . . . . . . . 19 ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺𝐾):ℕ⟶ℕ)
174, 15, 16syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝐾):ℕ⟶ℕ)
18 elfznn 12355 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
1918ssriv 3599 . . . . . . . . . . . . . . . . . 18 (1...𝑀) ⊆ ℕ
20 fssres 6057 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
2117, 19, 20sylancl 693 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ)
22 frn 6040 . . . . . . . . . . . . . . . . 17 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
2321, 22syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ran ((𝐺𝐾) ↾ (1...𝑀)) ⊆ ℕ)
243, 23syl5eqss 3641 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
25 nnssre 11009 . . . . . . . . . . . . . . 15 ℕ ⊆ ℝ
2624, 25syl6ss 3607 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
2726ad3antrrr 765 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ)
28 simpr 477 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀)))
2927, 28sseldd 3596 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
30 simpllr 798 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ)
31 nnre 11012 . . . . . . . . . . . . 13 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
3231ad2antlr 762 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
33 lelttr 10113 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3429, 30, 32, 33syl3anc 1324 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑦𝑥𝑥 < 𝑧) → 𝑦 < 𝑧))
3534ancomsd 470 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧𝑦𝑥) → 𝑦 < 𝑧))
3635expdimp 453 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦𝑥𝑦 < 𝑧))
3736an32s 845 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦𝑥𝑦 < 𝑧))
3837ralimdva 2959 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
3938impancom 456 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4039an32s 845 . . . . 5 ((((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
4140reximdva 3014 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧))
422, 41mpd 15 . . 3 (((𝜑𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
43 fzfid 12755 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
44 fvres 6194 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
4544adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺𝐾)‘𝑖))
46 fvco3 6262 . . . . . . . . . . . . . . 15 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4710, 18, 46syl2an 494 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐺𝐾)‘𝑖) = (𝐺‘(𝐾𝑖)))
4845, 47eqtrd 2654 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
4948adantrr 752 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾𝑖)))
50 fvres 6194 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
5150ad2antll 764 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺𝐾)‘𝑗))
52 elfznn 12355 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
5352adantl 482 . . . . . . . . . . . . . 14 ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
54 fvco3 6262 . . . . . . . . . . . . . 14 ((𝐾:ℕ⟶𝑇𝑗 ∈ ℕ) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5510, 53, 54syl2an 494 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺𝐾)‘𝑗) = (𝐺‘(𝐾𝑗)))
5651, 55eqtrd 2654 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾𝑗)))
5749, 56eqeq12d 2635 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗))))
58 fveq2 6178 . . . . . . . . . . . . 13 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
5958fveq2d 6182 . . . . . . . . . . . 12 ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
6019a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑀) ⊆ ℕ)
61 elfznn 12355 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
6261ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℕ)
6362nnred 11020 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛 ∈ ℝ)
64 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)}
65 ssrab2 3679 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾𝑛)} ⊆ ℕ
6664, 65eqsstri 3627 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 ⊆ ℕ
6766, 25sstri 3604 . . . . . . . . . . . . . . . . . . . . 21 𝑊 ⊆ ℝ
68 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 = inf(𝑊, ℝ, < )
6966, 5sseqtri 3629 . . . . . . . . . . . . . . . . . . . . . . 23 𝑊 ⊆ (ℤ‘1)
70 1z 11392 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℤ
715uzinf 12747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ ℕ ∈ Fin
73 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))
74 elin 3788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin) ↔ (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7573, 74sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin))
7675simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑈 ∈ Fin)
77 ssfi 8165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑈 ∈ Fin ∧ 𝑇𝑈) → 𝑇 ∈ Fin)
7876, 13, 77sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑇 ∈ Fin)
7978adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → 𝑇 ∈ Fin)
8010adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → 𝐾:ℕ⟶𝑇)
81 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾𝑖) = (𝐾𝑗) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)))
8281fveq2d 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾𝑖) = (𝐾𝑗) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑗))))
8382fveq2d 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐾𝑖) = (𝐾𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗)))))
84 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑)
85 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ)
86 ral0 4067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑚 ∈ ∅ 𝑛𝑚
87 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅)
8887raleqdv 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚𝑊 𝑛𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛𝑚))
8986, 88mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚𝑊 𝑛𝑚)
9089ralrimivw 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
91 rabid2 3113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚𝑊 𝑛𝑚)
9290, 91sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
9385, 92eleqtrd 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
94 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ)
9594, 92eleqtrd 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10684, 93, 95, 105syl12anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
10783, 106syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
108107ralrimivva 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗))
109 dff13 6497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾:ℕ–1-1𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾𝑖) = (𝐾𝑗) → 𝑖 = 𝑗)))
11080, 108, 109sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑊 = ∅) → 𝐾:ℕ–1-1𝑇)
111 f1domg 7960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 ∈ Fin → (𝐾:ℕ–1-1𝑇 → ℕ ≼ 𝑇))
11279, 110, 111sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑊 = ∅) → ℕ ≼ 𝑇)
113 domfi 8166 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑇 ∈ Fin ∧ ℕ ≼ 𝑇) → ℕ ∈ Fin)
11479, 112, 113syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑊 = ∅) → ℕ ∈ Fin)
115114ex 450 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑊 = ∅ → ℕ ∈ Fin))
116115necon3bd 2805 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (¬ ℕ ∈ Fin → 𝑊 ≠ ∅))
11772, 116mpi 20 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑊 ≠ ∅)
118 infssuzcl 11757 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊)
11969, 117, 118sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊)
12068, 119syl5eqel 2703 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀𝑊)
12167, 120sseldi 3593 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℝ)
122121ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀 ∈ ℝ)
12367sseli 3591 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑚 ∈ ℝ)
124123adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑚 ∈ ℝ)
125 elfzle2 12330 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑀) → 𝑛𝑀)
126125ad2antlr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑀)
127 infssuzle 11756 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑚𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚)
12869, 127mpan 705 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚)
12968, 128syl5eqbr 4679 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑊𝑀𝑚)
130129adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑀𝑚)
13163, 122, 124, 126, 130letrd 10179 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ (1...𝑀)) ∧ 𝑚𝑊) → 𝑛𝑚)
132131ralrimiva 2963 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑀)) → ∀𝑚𝑊 𝑛𝑚)
13360, 132ssrabdv 3673 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
134133adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
135 simprl 793 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀))
136134, 135sseldd 3596 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
137 simprr 795 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀))
138134, 137sseldd 3596 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚})
139136, 138jca 554 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚𝑊 𝑛𝑚}))
140139, 105syldan 487 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑗))))))
14159, 140syl5ibr 236 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑗)) → 𝑖 = 𝑗))
14257, 141sylbid 230 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
143142ralrimivva 2968 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))
144 dff13 6497 . . . . . . . . 9 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)))
14521, 143, 144sylanbrc 697 . . . . . . . 8 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ)
146 f1f1orn 6135 . . . . . . . 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 6116 . . . . . . . 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 6131 . . . . . 6 (((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺𝐾) “ (1...𝑀)) → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
152150, 151syl 17 . . . . 5 (𝜑 → ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀)))
153 fofi 8237 . . . . 5 (((1...𝑀) ∈ Fin ∧ ((𝐺𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺𝐾) “ (1...𝑀))) → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
15443, 152, 153syl2anc 692 . . . 4 (𝜑 → ((𝐺𝐾) “ (1...𝑀)) ∈ Fin)
155 fimaxre2 10954 . . . 4 ((((𝐺𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15626, 154, 155syl2anc 692 . . 3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦𝑥)
15742, 156r19.29a 3074 . 2 (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)
15897, 96resubcld 10443 . . . . 5 (𝜑 → (𝐵𝐴) ∈ ℝ)
159158rexrd 10074 . . . 4 (𝜑 → (𝐵𝐴) ∈ ℝ*)
160159adantr 481 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ*)
161 fzfid 12755 . . . . . 6 (𝜑 → (1...𝑧) ∈ Fin)
162 elfznn 12355 . . . . . . . . 9 (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ)
163 eqid 2620 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
164163ovolfsf 23221 . . . . . . . . . . 11 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
165100, 164syl 17 . . . . . . . . . 10 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
166165ffvelrnda 6345 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
167162, 166sylan2 491 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞))
168 elrege0 12263 . . . . . . . 8 ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
169167, 168sylib 208 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗)))
170169simpld 475 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
171161, 170fsumrecl 14446 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
172171adantr 481 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
173172rexrd 10074 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ*)
174163, 99ovolsf 23222 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
175100, 174syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
176 frn 6040 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
177175, 176syl 17 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
178 rge0ssre 12265 . . . . . . 7 (0[,)+∞) ⊆ ℝ
179177, 178syl6ss 3607 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
180 ressxr 10068 . . . . . 6 ℝ ⊆ ℝ*
181179, 180syl6ss 3607 . . . . 5 (𝜑 → ran 𝑆 ⊆ ℝ*)
182 supxrcl 12130 . . . . 5 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
183181, 182syl 17 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
184183adantr 481 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
185158adantr 481 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ∈ ℝ)
18624sselda 3595 . . . . . . 7 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ)
187178, 166sseldi 3593 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
188186, 187syldan 487 . . . . . 6 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
189154, 188fsumrecl 14446 . . . . 5 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
190189adantr 481 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
191 inss2 3826 . . . . . . . . . . 11 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
192 fss 6043 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ × ℝ))
193100, 191, 192sylancl 693 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
19466, 120sseldi 3593 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
19515, 194ffvelrnd 6346 . . . . . . . . . . 11 (𝜑 → (𝐾𝑀) ∈ 𝑈)
1964, 195ffvelrnd 6346 . . . . . . . . . 10 (𝜑 → (𝐺‘(𝐾𝑀)) ∈ ℕ)
197193, 196ffvelrnd 6346 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ))
198 xp2nd 7184 . . . . . . . . 9 ((𝐹‘(𝐺‘(𝐾𝑀))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
199197, 198syl 17 . . . . . . . 8 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℝ)
20013, 8sseldi 3593 . . . . . . . . . . 11 (𝜑𝐶𝑈)
2014, 200ffvelrnd 6346 . . . . . . . . . 10 (𝜑 → (𝐺𝐶) ∈ ℕ)
202193, 201ffvelrnd 6346 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ))
203 xp1st 7183 . . . . . . . . 9 ((𝐹‘(𝐺𝐶)) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
204202, 203syl 17 . . . . . . . 8 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℝ)
205199, 204resubcld 10443 . . . . . . 7 (𝜑 → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) ∈ ℝ)
206 fveq2 6178 . . . . . . . . . 10 (𝑗 = (𝐺‘(𝐾𝑖)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
207187recnd 10053 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
208186, 207syldan 487 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
209206, 43, 150, 48, 208fsumf1o 14435 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))))
210100adantr 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2114adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ)
212 ffvelrn 6343 . . . . . . . . . . . . 13 ((𝐾:ℕ⟶𝑈𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
21315, 18, 212syl2an 494 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) ∈ 𝑈)
214211, 213ffvelrnd 6346 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
215163ovolfsval 23220 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐺‘(𝐾𝑖)) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
216210, 214, 215syl2anc 692 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
217216sumeq2dv 14414 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
218193adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
2194adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ)
22015ffvelrnda 6345 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑈)
221219, 220ffvelrnd 6346 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾𝑖)) ∈ ℕ)
222218, 221ffvelrnd 6346 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
223 xp2nd 7184 . . . . . . . . . . . . . 14 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
224222, 223syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
22518, 224sylan2 491 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
226225recnd 10053 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
227193adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ × ℝ))
228227, 214ffvelrnd 6346 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ))
229 xp1st 7183 . . . . . . . . . . . . 13 ((𝐹‘(𝐺‘(𝐾𝑖))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
230228, 229syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
231230recnd 10053 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
23243, 226, 231fsumsub 14501 . . . . . . . . . 10 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
23369, 120sseldi 3593 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ‘1))
234 fveq2 6178 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑀 → (𝐾𝑖) = (𝐾𝑀))
235234fveq2d 6182 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾𝑀)))
236235fveq2d 6182 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾𝑀))))
237236fveq2d 6182 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
238233, 226, 237fsumm1 14461 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
239 fzfid 12755 . . . . . . . . . . . . . . 15 (𝜑 → (1...(𝑀 − 1)) ∈ Fin)
240 elfznn 12355 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ)
241240, 224sylan2 491 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
242239, 241fsumrecl 14446 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ)
243242recnd 10053 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
244199recnd 10053 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) ∈ ℂ)
245243, 244addcomd 10223 . . . . . . . . . . . 12 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
246238, 245eqtrd 2654 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
247 fveq2 6178 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝐾𝑖) = (𝐾‘1))
248247fveq2d 6182 . . . . . . . . . . . . . . 15 (𝑖 = 1 → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘1)))
249248fveq2d 6182 . . . . . . . . . . . . . 14 (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘1))))
250249fveq2d 6182 . . . . . . . . . . . . 13 (𝑖 = 1 → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))))
251233, 231, 250fsum1p 14463 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))))
2525, 6, 7, 8algr0 15266 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾‘1) = 𝐶)
253252fveq2d 6182 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺𝐶))
254253fveq2d 6182 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺𝐶)))
255254fveq2d 6182 . . . . . . . . . . . . 13 (𝜑 → (1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺𝐶))))
2567peano2zd 11470 . . . . . . . . . . . . . . 15 (𝜑 → (1 + 1) ∈ ℤ)
257194nnzd 11466 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
258 fzp1ss 12377 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀))
25970, 258mp1i 13 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀))
260259sselda 3595 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀))
261260, 231syldan 487 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℂ)
262 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗 + 1) → (𝐾𝑖) = (𝐾‘(𝑗 + 1)))
263262fveq2d 6182 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1))))
264263fveq2d 6182 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
265264fveq2d 6182 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
2667, 256, 257, 261, 265fsumshftm 14494 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))))
267 ax-1cn 9979 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
268267, 267pncan3oi 10282 . . . . . . . . . . . . . . . . 17 ((1 + 1) − 1) = 1
269268oveq1i 6645 . . . . . . . . . . . . . . . 16 (((1 + 1) − 1)...(𝑀 − 1)) = (1...(𝑀 − 1))
270269sumeq1i 14409 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))
271 oveq1 6642 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
272271fveq2d 6182 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1)))
273272fveq2d 6182 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1))))
274273fveq2d 6182 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
275274fveq2d 6182 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
276275cbvsumv 14407 . . . . . . . . . . . . . . 15 Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
277270, 276eqtri 2642 . . . . . . . . . . . . . 14 Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))
278266, 277syl6eq 2670 . . . . . . . . . . . . 13 (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))
279255, 278oveq12d 6653 . . . . . . . . . . . 12 (𝜑 → ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
280251, 279eqtrd 2654 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖)))) = ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))
281246, 280oveq12d 6653 . . . . . . . . . 10 (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
282204recnd 10053 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) ∈ ℂ)
283 peano2nn 11017 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ → (𝑖 + 1) ∈ ℕ)
284 ffvelrn 6343 . . . . . . . . . . . . . . . . . 18 ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
28515, 283, 284syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
286219, 285ffvelrnd 6346 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ)
287218, 286ffvelrnd 6346 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ))
288 xp1st 7183 . . . . . . . . . . . . . . 15 ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
289287, 288syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ℕ) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
290240, 289sylan2 491 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
291239, 290fsumrecl 14446 . . . . . . . . . . . 12 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ)
292291recnd 10053 . . . . . . . . . . 11 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ)
293244, 243, 282, 292addsub4d 10424 . . . . . . . . . 10 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖))))) − ((1st ‘(𝐹‘(𝐺𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
294232, 281, 2933eqtrd 2658 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
295209, 217, 2943eqtrd 2658 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
296295, 189eqeltrrd 2700 . . . . . . 7 (𝜑 → (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ)
297 fveq2 6178 . . . . . . . . . . . . . . 15 (𝑛 = 𝑀 → (𝐾𝑛) = (𝐾𝑀))
298297eleq2d 2685 . . . . . . . . . . . . . 14 (𝑛 = 𝑀 → (𝐵 ∈ (𝐾𝑛) ↔ 𝐵 ∈ (𝐾𝑀)))
299298, 64elrab2 3360 . . . . . . . . . . . . 13 (𝑀𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
300120, 299sylib 208 . . . . . . . . . . . 12 (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾𝑀)))
301300simprd 479 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐾𝑀))
30296, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23266 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐾𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
303195, 302mpdan 701 . . . . . . . . . . 11 (𝜑 → (𝐵 ∈ (𝐾𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))))
304301, 303mpbid 222 . . . . . . . . . 10 (𝜑 → (𝐵 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾𝑀)))) < 𝐵𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀))))))
305304simp3d 1073 . . . . . . . . 9 (𝜑𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))))
30696, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23266 . . . . . . . . . . . 12 ((𝜑𝐶𝑈) → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
307200, 306mpdan 701 . . . . . . . . . . 11 (𝜑 → (𝐴𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶))))))
308104, 307mpbid 222 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴𝐴 < (2nd ‘(𝐹‘(𝐺𝐶)))))
309308simp2d 1072 . . . . . . . . 9 (𝜑 → (1st ‘(𝐹‘(𝐺𝐶))) < 𝐴)
31097, 204, 199, 96, 305, 309lt2subd 10636 . . . . . . . 8 (𝜑 → (𝐵𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
311158, 205, 310ltled 10170 . . . . . . 7 (𝜑 → (𝐵𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))))
312240adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ)
313 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1)))
314257adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ)
315 elfzm11 12395 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
31670, 314, 315sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀)))
317313, 316mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖𝑖 < 𝑀))
318317simp3d 1073 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀)
319312nnred 11020 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ)
320121adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ)
321319, 320ltnled 10169 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀𝑖))
322318, 321mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀𝑖)
323 infssuzle 11756 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ⊆ (ℤ‘1) ∧ 𝑖𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖)
32469, 323mpan 705 . . . . . . . . . . . . . . . . . . . 20 (𝑖𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖)
32568, 324syl5eqbr 4679 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑊𝑀𝑖)
326322, 325nsyl 135 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖𝑊)
327312, 326jca 554 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊))
32896, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem2 23267 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
329327, 328syldan 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵)
330329iftrued 4085 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
331 ffvelrn 6343 . . . . . . . . . . . . . . . . 17 ((𝐾:ℕ⟶𝑇𝑖 ∈ ℕ) → (𝐾𝑖) ∈ 𝑇)
33210, 240, 331syl2an 494 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾𝑖) ∈ 𝑇)
333103ralrimiva 2963 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
334333adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡))
335 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑖) → (𝐺𝑡) = (𝐺‘(𝐾𝑖)))
336335fveq2d 6182 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑖) → (𝐹‘(𝐺𝑡)) = (𝐹‘(𝐺‘(𝐾𝑖))))
337336fveq2d 6182 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑖) → (2nd ‘(𝐹‘(𝐺𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
338337breq1d 4654 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐾𝑖) → ((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵))
339338, 337ifbieq1d 4100 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵))
340 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐾𝑖) → (𝐻𝑡) = (𝐻‘(𝐾𝑖)))
341339, 340eleq12d 2693 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐾𝑖) → (if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
342341rspcv 3300 . . . . . . . . . . . . . . . 16 ((𝐾𝑖) ∈ 𝑇 → (∀𝑡𝑇 if((2nd ‘(𝐹‘(𝐺𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺𝑡))), 𝐵) ∈ (𝐻𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖))))
343332, 334, 342sylc 65 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → if((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))), 𝐵) ∈ (𝐻‘(𝐾𝑖)))
344330, 343eqeltrrd 2700 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐻‘(𝐾𝑖)))
3455, 6, 7, 8, 9algrp1 15268 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
346240, 345sylan2 491 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾𝑖)))
347344, 346eleqtrrd 2702 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)))
348240, 285sylan2 491 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈)
34996, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 23266 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
350348, 349syldan 487 . . . . . . . . . . . . 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 1072 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
353290, 241, 352ltled 10170 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...(𝑀 − 1))) → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
354239, 290, 241, 353fsumle 14512 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))))
355242, 291subge0d 10602 . . . . . . . . 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 10443 . . . . . . . . 9 (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ)
358205, 357addge01d 10600 . . . . . . . 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 10179 . . . . . 6 (𝜑 → (𝐵𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾𝑀)))) − (1st ‘(𝐹‘(𝐺𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))
361360, 295breqtrrd 4672 . . . . 5 (𝜑 → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
362361adantr 481 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗))
363 fzfid 12755 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin)
364170adantlr 750 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ)
365169simprd 479 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
366365adantlr 750 . . . . 5 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑗))
36724adantr 481 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ ℕ) → ((𝐺𝐾) “ (1...𝑀)) ⊆ ℕ)
368367sselda 3595 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ)
369368nnred 11020 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ)
37031ad2antlr 762 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ)
371 ltle 10111 . . . . . . . . . 10 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧𝑦𝑧))
372369, 370, 371syl2anc 692 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦𝑧))
373368, 5syl6eleq 2709 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑦 ∈ (ℤ‘1))
374 nnz 11384 . . . . . . . . . . 11 (𝑧 ∈ ℕ → 𝑧 ∈ ℤ)
375374ad2antlr 762 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ)
376 elfz5 12319 . . . . . . . . . 10 ((𝑦 ∈ (ℤ‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
377373, 375, 376syl2anc 692 . . . . . . . . 9 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦𝑧))
378372, 377sylibrd 249 . . . . . . . 8 (((𝜑𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))) → (𝑦 < 𝑧𝑦 ∈ (1...𝑧)))
379378ralimdva 2959 . . . . . . 7 ((𝜑𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)))
380379impr 648 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
381 dfss3 3585 . . . . . 6 (((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))
382380, 381sylibr 224 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺𝐾) “ (1...𝑀)) ⊆ (1...𝑧))
383363, 364, 366, 382fsumless 14509 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
384185, 190, 172, 362, 383letrd 10179 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗))
385 eqidd 2621 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗))
386 simprl 793 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ)
387386, 5syl6eleq 2709 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ (ℤ‘1))
388364recnd 10053 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℂ)
389385, 387, 388fsumser 14442 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧))
39099fveq1i 6179 . . . . 5 (𝑆𝑧) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑧)
391389, 390syl6eqr 2672 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆𝑧))
392181adantr 481 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆ ℝ*)
393 ffn 6032 . . . . . . . 8 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
394175, 393syl 17 . . . . . . 7 (𝜑𝑆 Fn ℕ)
395394adantr 481 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ)
396 fnfvelrn 6342 . . . . . 6 ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆𝑧) ∈ ran 𝑆)
397395, 386, 396syl2anc 692 . . . . 5 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ∈ ran 𝑆)
398 supxrub 12139 . . . . 5 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑧) ∈ ran 𝑆) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
399392, 397, 398syl2anc 692 . . . 4 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆𝑧) ≤ sup(ran 𝑆, ℝ*, < ))
400391, 399eqbrtrd 4666 . . 3 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
401160, 173, 184, 384, 400xrletrd 11978 . 2 ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
402157, 401rexlimddv 3031 1 (𝜑 → (𝐵𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  {crab 2913  cin 3566  wss 3567  c0 3907  ifcif 4077  𝒫 cpw 4149  {csn 4168   cuni 4427   class class class wbr 4644   × cxp 5102  ran crn 5105  cres 5106  cima 5107  ccom 5108   Fn wfn 5871  wf 5872  1-1wf1 5873  ontowfo 5874  1-1-ontowf1o 5875  cfv 5876  (class class class)co 6635  1st c1st 7151  2nd c2nd 7152  cdom 7938  Fincfn 7940  supcsup 8331  infcinf 8332  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924  +∞cpnf 10056  *cxr 10058   < clt 10059  cle 10060  cmin 10251  cn 11005  cz 11362  cuz 11672  (,)cioo 12160  [,)cico 12162  [,]cicc 12163  ...cfz 12311  seqcseq 12784  abscabs 13955  Σcsu 14397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-rp 11818  df-ioo 12164  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-sum 14398
This theorem is referenced by:  ovolicc2lem5  23270
  Copyright terms: Public domain W3C validator