Metamath Proof Explorer

Theorem ovolicc2lem4

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Hypotheses ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( 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 ⊢ 𝐾 = seq 1 ( ( 𝐻 ∘ 1st ) , ( ℕ × { 𝐶 } ) )
ovolicc2.16 ⊢ 𝑊 = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) }
ovolicc2.17 ⊢ 𝑀 = inf ( 𝑊 , ℝ , < )
Assertion ovolicc2lem4 ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5 ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
6 ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
7 ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
8 ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
9 ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
10 ovolicc2.10 ⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
11 ovolicc2.11 ⊢ ( 𝜑 → 𝐻 : 𝑇 ⟶ 𝑇 )
12 ovolicc2.12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
13 ovolicc2.13 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
14 ovolicc2.14 ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
15 ovolicc2.15 ⊢ 𝐾 = seq 1 ( ( 𝐻 ∘ 1st ) , ( ℕ × { 𝐶 } ) )
16 ovolicc2.16 ⊢ 𝑊 = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) }
17 ovolicc2.17 ⊢ 𝑀 = inf ( 𝑊 , ℝ , < )
18 arch ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑧 ∈ ℕ 𝑥 < 𝑧 )
19 18 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 ) → ∃ 𝑧 ∈ ℕ 𝑥 < 𝑧 )
20 df-ima ⊢ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) = ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) )
21 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
22 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
23 21 15 22 14 11 algrf ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ 𝑇 )
24 10 ssrab3 ⊢ 𝑇 ⊆ 𝑈
25 fss ⊢ ( ( 𝐾 : ℕ ⟶ 𝑇 ∧ 𝑇 ⊆ 𝑈 ) → 𝐾 : ℕ ⟶ 𝑈 )
26 23 24 25 sylancl ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ 𝑈 )
27 fco ⊢ ( ( 𝐺 : 𝑈 ⟶ ℕ ∧ 𝐾 : ℕ ⟶ 𝑈 ) → ( 𝐺 ∘ 𝐾 ) : ℕ ⟶ ℕ )
28 8 26 27 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐾 ) : ℕ ⟶ ℕ )
29 fz1ssnn ⊢ ( 1 ... 𝑀 ) ⊆ ℕ
30 fssres ⊢ ( ( ( 𝐺 ∘ 𝐾 ) : ℕ ⟶ ℕ ∧ ( 1 ... 𝑀 ) ⊆ ℕ ) → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) ⟶ ℕ )
31 28 29 30 sylancl ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) ⟶ ℕ )
32 31 frnd ⊢ ( 𝜑 → ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ⊆ ℕ )
33 20 32 eqsstrid ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ℕ )
34 nnssre ⊢ ℕ ⊆ ℝ
35 33 34 sstrdi ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ℝ )
36 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ℝ )
37 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) )
38 36 37 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑦 ∈ ℝ )
39 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑥 ∈ ℝ )
40 nnre ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
41 40 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑧 ∈ ℝ )
42 lelttr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧 ) → 𝑦 < 𝑧 ) )
43 38 39 41 42 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( ( 𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧 ) → 𝑦 < 𝑧 ) )
44 43 ancomsd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( ( 𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥 ) → 𝑦 < 𝑧 ) )
45 44 expdimp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) ∧ 𝑥 < 𝑧 ) → ( 𝑦 ≤ 𝑥 → 𝑦 < 𝑧 ) )
46 45 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑥 < 𝑧 ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( 𝑦 ≤ 𝑥 → 𝑦 < 𝑧 ) )
47 46 ralimdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ 𝑥 < 𝑧 ) → ( ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 → ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) )
48 47 impancom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℕ ) ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 ) → ( 𝑥 < 𝑧 → ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) )
49 48 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 ) ∧ 𝑧 ∈ ℕ ) → ( 𝑥 < 𝑧 → ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) )
50 49 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 ) → ( ∃ 𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃ 𝑧 ∈ ℕ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) )
51 19 50 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 ) → ∃ 𝑧 ∈ ℕ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 )
52 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
53 fvres ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑖 ) )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑖 ) )
55 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℕ )
56 fvco3 ⊢ ( ( 𝐾 : ℕ ⟶ 𝑇 ∧ 𝑖 ∈ ℕ ) → ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) )
57 23 55 56 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) )
58 54 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) )
59 58 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) )
60 fvres ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) = ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑗 ) )
61 60 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) = ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑗 ) )
62 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ )
63 62 adantl ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ℕ )
64 fvco3 ⊢ ( ( 𝐾 : ℕ ⟶ 𝑇 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) )
65 23 63 64 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝐺 ∘ 𝐾 ) ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) )
66 61 65 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) )
67 59 66 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) ↔ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) )
68 2fveq3 ⊢ ( ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) ) )
69 29 a1i ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ⊆ ℕ )
70 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → 𝑛 ∈ ℕ )
71 70 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑛 ∈ ℕ )
72 71 nnred ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑛 ∈ ℝ )
73 16 ssrab3 ⊢ 𝑊 ⊆ ℕ
74 73 34 sstri ⊢ 𝑊 ⊆ ℝ
75 73 21 sseqtri ⊢ 𝑊 ⊆ ( ℤ≥ ‘ 1 )
76 nnnfi ⊢ ¬ ℕ ∈ Fin
77 6 elin2d ⊢ ( 𝜑 → 𝑈 ∈ Fin )
78 ssfi ⊢ ( ( 𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈 ) → 𝑇 ∈ Fin )
79 77 24 78 sylancl ⊢ ( 𝜑 → 𝑇 ∈ Fin )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝑇 ∈ Fin )
81 23 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐾 : ℕ ⟶ 𝑇 )
82 2fveq3 ⊢ ( ( 𝐾 ‘ 𝑖 ) = ( 𝐾 ‘ 𝑗 ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) )
83 82 fveq2d ⊢ ( ( 𝐾 ‘ 𝑖 ) = ( 𝐾 ‘ 𝑗 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) ) )
84 simpll ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝜑 )
85 simprl ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑖 ∈ ℕ )
86 ral0 ⊢ ∀ 𝑚 ∈ ∅ 𝑛 ≤ 𝑚
87 simplr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑊 = ∅ )
88 87 raleqdv ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀ 𝑚 ∈ ∅ 𝑛 ≤ 𝑚 ) )
89 86 88 mpbiri ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 )
90 89 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ∀ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 )
91 rabid2 ⊢ ( ℕ = { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ↔ ∀ 𝑛 ∈ ℕ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 )
92 90 91 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ℕ = { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
93 85 92 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑖 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
94 simprr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑗 ∈ ℕ )
95 94 92 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
96 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem3 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) ) → ( 𝑖 = 𝑗 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) ) ) )
97 84 93 95 96 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( 𝑖 = 𝑗 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) ) ) )
98 83 97 syl5ibr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ ( 𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ) → ( ( 𝐾 ‘ 𝑖 ) = ( 𝐾 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
99 98 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℕ ( ( 𝐾 ‘ 𝑖 ) = ( 𝐾 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
100 dff13 ⊢ ( 𝐾 : ℕ –1-1→ 𝑇 ↔ ( 𝐾 : ℕ ⟶ 𝑇 ∧ ∀ 𝑖 ∈ ℕ ∀ 𝑗 ∈ ℕ ( ( 𝐾 ‘ 𝑖 ) = ( 𝐾 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
101 81 99 100 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐾 : ℕ –1-1→ 𝑇 )
102 f1domg ⊢ ( 𝑇 ∈ Fin → ( 𝐾 : ℕ –1-1→ 𝑇 → ℕ ≼ 𝑇 ) )
103 80 101 102 sylc ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ℕ ≼ 𝑇 )
104 domfi ⊢ ( ( 𝑇 ∈ Fin ∧ ℕ ≼ 𝑇 ) → ℕ ∈ Fin )
105 79 103 104 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ℕ ∈ Fin )
106 105 ex ⊢ ( 𝜑 → ( 𝑊 = ∅ → ℕ ∈ Fin ) )
107 106 necon3bd ⊢ ( 𝜑 → ( ¬ ℕ ∈ Fin → 𝑊 ≠ ∅ ) )
108 76 107 mpi ⊢ ( 𝜑 → 𝑊 ≠ ∅ )
109 infssuzcl ⊢ ( ( 𝑊 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑊 ≠ ∅ ) → inf ( 𝑊 , ℝ , < ) ∈ 𝑊 )
110 75 108 109 sylancr ⊢ ( 𝜑 → inf ( 𝑊 , ℝ , < ) ∈ 𝑊 )
111 17 110 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
112 74 111 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
113 112 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑀 ∈ ℝ )
114 74 sseli ⊢ ( 𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ )
115 114 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑚 ∈ ℝ )
116 elfzle2 ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → 𝑛 ≤ 𝑀 )
117 116 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑛 ≤ 𝑀 )
118 infssuzle ⊢ ( ( 𝑊 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑚 ∈ 𝑊 ) → inf ( 𝑊 , ℝ , < ) ≤ 𝑚 )
119 75 118 mpan ⊢ ( 𝑚 ∈ 𝑊 → inf ( 𝑊 , ℝ , < ) ≤ 𝑚 )
120 17 119 eqbrtrid ⊢ ( 𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚 )
121 120 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑀 ≤ 𝑚 )
122 72 113 115 117 121 letrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑚 ∈ 𝑊 ) → 𝑛 ≤ 𝑚 )
123 122 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 )
124 69 123 ssrabdv ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ⊆ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
125 124 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( 1 ... 𝑀 ) ⊆ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
126 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
127 125 126 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → 𝑖 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
128 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
129 125 128 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } )
130 127 129 jca ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑖 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ∧ 𝑗 ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 } ) )
131 130 96 syldan ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑖 = 𝑗 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) ) ) ) )
132 68 131 syl5ibr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑗 ) ) → 𝑖 = 𝑗 ) )
133 67 132 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
134 133 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
135 dff13 ⊢ ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1→ ℕ ↔ ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) ⟶ ℕ ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑖 ) = ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
136 31 134 135 sylanbrc ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1→ ℕ )
137 f1f1orn ⊢ ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1→ ℕ → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) )
138 136 137 syl ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) )
139 f1oeq3 ⊢ ( ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) = ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) → ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ↔ ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) ) )
140 20 139 ax-mp ⊢ ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ↔ ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ran ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) )
141 138 140 sylibr ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) )
142 f1ofo ⊢ ( ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –1-1-onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) )
143 141 142 syl ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) )
144 fofi ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ( ( 𝐺 ∘ 𝐾 ) ↾ ( 1 ... 𝑀 ) ) : ( 1 ... 𝑀 ) –onto→ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ∈ Fin )
145 52 143 144 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ∈ Fin )
146 fimaxre2 ⊢ ( ( ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ℝ ∧ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 )
147 35 145 146 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ≤ 𝑥 )
148 51 147 r19.29a ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℕ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 )
149 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
150 149 rexrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ* )
151 150 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ* )
152 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑧 ) ∈ Fin )
153 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑧 ) → 𝑗 ∈ ℕ )
154 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
155 154 ovolfsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
156 5 155 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
157 156 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
158 153 157 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
159 elrege0 ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ) )
160 158 159 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ) )
161 160 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
162 152 161 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
163 162 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
164 163 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ* )
165 154 4 ovolsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
166 5 165 syl ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
167 166 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
168 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
169 167 168 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ )
170 ressxr ⊢ ℝ ⊆ ℝ*
171 169 170 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* )
172 supxrcl ⊢ ( ran 𝑆 ⊆ ℝ* → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
173 171 172 syl ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
174 173 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
175 149 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
176 33 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑗 ∈ ℕ )
177 168 157 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
178 176 177 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
179 145 178 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
180 179 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
181 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
182 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
183 5 181 182 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
184 73 111 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
185 26 184 ffvelrnd ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑀 ) ∈ 𝑈 )
186 8 185 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ∈ ℕ )
187 183 186 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ∈ ( ℝ × ℝ ) )
188 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ∈ ℝ )
189 187 188 syl ⊢ ( 𝜑 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ∈ ℝ )
190 24 14 sseldi ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
191 8 190 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ℕ )
192 183 191 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ∈ ( ℝ × ℝ ) )
193 xp1st ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℝ )
194 192 193 syl ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℝ )
195 189 194 resubcld ⊢ ( 𝜑 → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) ∈ ℝ )
196 fveq2 ⊢ ( 𝑗 = ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) )
197 177 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
198 176 197 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
199 196 52 141 58 198 fsumf1o ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) )
200 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐺 : 𝑈 ⟶ ℕ )
201 ffvelrn ⊢ ( ( 𝐾 : ℕ ⟶ 𝑈 ∧ 𝑖 ∈ ℕ ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝑈 )
202 26 55 201 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝑈 )
203 200 202 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ∈ ℕ )
204 154 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
205 5 203 204 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
206 205 sumeq2dv ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
207 183 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
208 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝐺 : 𝑈 ⟶ ℕ )
209 26 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝑈 )
210 208 209 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ∈ ℕ )
211 207 210 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ∈ ( ℝ × ℝ ) )
212 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
213 211 212 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
214 55 213 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
215 214 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℂ )
216 183 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
217 216 203 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ∈ ( ℝ × ℝ ) )
218 xp1st ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
219 217 218 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
220 219 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℂ )
221 52 215 220 fsumsub ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
222 fzfid ⊢ ( 𝜑 → ( 1 ... ( 𝑀 − 1 ) ) ∈ Fin )
223 elfznn ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 𝑖 ∈ ℕ )
224 223 213 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
225 222 224 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ )
226 225 recnd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℂ )
227 189 recnd ⊢ ( 𝜑 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ∈ ℂ )
228 75 111 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
229 2fveq3 ⊢ ( 𝑖 = 𝑀 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) )
230 229 fveq2d ⊢ ( 𝑖 = 𝑀 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) )
231 230 fveq2d ⊢ ( 𝑖 = 𝑀 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) )
232 228 215 231 fsumm1 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) + ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ) )
233 226 227 232 comraddd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
234 2fveq3 ⊢ ( 𝑖 = 1 → ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) )
235 234 fveq2d ⊢ ( 𝑖 = 1 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) )
236 235 fveq2d ⊢ ( 𝑖 = 1 → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) )
237 228 220 236 fsum1p ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
238 21 15 22 14 algr0 ⊢ ( 𝜑 → ( 𝐾 ‘ 1 ) = 𝐶 )
239 238 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) = ( 𝐺 ‘ 𝐶 ) )
240 239 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
241 240 fveq2d ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) = ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) )
242 22 peano2zd ⊢ ( 𝜑 → ( 1 + 1 ) ∈ ℤ )
243 184 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
244 1z ⊢ 1 ∈ ℤ
245 fzp1ss ⊢ ( 1 ∈ ℤ → ( ( 1 + 1 ) ... 𝑀 ) ⊆ ( 1 ... 𝑀 ) )
246 244 245 mp1i ⊢ ( 𝜑 → ( ( 1 + 1 ) ... 𝑀 ) ⊆ ( 1 ... 𝑀 ) )
247 246 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝑀 ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
248 247 220 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝑀 ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℂ )
249 2fveq3 ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) = ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) )
250 249 fveq2d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) )
251 250 fveq2d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) ) )
252 22 242 243 248 251 fsumshftm ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = Σ 𝑗 ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) ) )
253 ax-1cn ⊢ 1 ∈ ℂ
254 253 253 pncan3oi ⊢ ( ( 1 + 1 ) − 1 ) = 1
255 254 oveq1i ⊢ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑀 − 1 ) ) = ( 1 ... ( 𝑀 − 1 ) )
256 255 sumeq1i ⊢ Σ 𝑗 ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) ) = Σ 𝑗 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) )
257 fvoveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝐾 ‘ ( 𝑗 + 1 ) ) = ( 𝐾 ‘ ( 𝑖 + 1 ) ) )
258 257 fveq2d ⊢ ( 𝑗 = 𝑖 → ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) )
259 258 fveq2d ⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) )
260 259 fveq2d ⊢ ( 𝑗 = 𝑖 → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) )
261 260 cbvsumv ⊢ Σ 𝑗 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) )
262 256 261 eqtri ⊢ Σ 𝑗 ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑗 + 1 ) ) ) ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) )
263 252 262 eqtrdi ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) )
264 241 263 oveq12d ⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 1 ) ) ) ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) = ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
265 237 264 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) = ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
266 233 265 oveq12d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) = ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) − ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
267 194 recnd ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℂ )
268 peano2nn ⊢ ( 𝑖 ∈ ℕ → ( 𝑖 + 1 ) ∈ ℕ )
269 ffvelrn ⊢ ( ( 𝐾 : ℕ ⟶ 𝑈 ∧ ( 𝑖 + 1 ) ∈ ℕ ) → ( 𝐾 ‘ ( 𝑖 + 1 ) ) ∈ 𝑈 )
270 26 268 269 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐾 ‘ ( 𝑖 + 1 ) ) ∈ 𝑈 )
271 208 270 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ∈ ℕ )
272 207 271 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ℝ × ℝ ) )
273 xp1st ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ∈ ℝ )
274 272 273 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ∈ ℝ )
275 223 274 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ∈ ℝ )
276 222 275 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ∈ ℝ )
277 276 recnd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ∈ ℂ )
278 227 226 267 277 addsub4d ⊢ ( 𝜑 → ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) − ( ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) + Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) = ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
279 221 266 278 3eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) = ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
280 199 206 279 3eqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
281 280 179 eqeltrrd ⊢ ( 𝜑 → ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) ∈ ℝ )
282 fveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑀 ) )
283 282 eleq2d ⊢ ( 𝑛 = 𝑀 → ( 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝐾 ‘ 𝑀 ) ) )
284 283 16 elrab2 ⊢ ( 𝑀 ∈ 𝑊 ↔ ( 𝑀 ∈ ℕ ∧ 𝐵 ∈ ( 𝐾 ‘ 𝑀 ) ) )
285 111 284 sylib ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝐵 ∈ ( 𝐾 ‘ 𝑀 ) ) )
286 285 simprd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐾 ‘ 𝑀 ) )
287 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝑀 ) ∈ 𝑈 ) → ( 𝐵 ∈ ( 𝐾 ‘ 𝑀 ) ↔ ( 𝐵 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) < 𝐵 ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ) ) )
288 185 287 mpdan ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐾 ‘ 𝑀 ) ↔ ( 𝐵 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) < 𝐵 ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ) ) )
289 286 288 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) < 𝐵 ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) ) )
290 289 simp3d ⊢ ( 𝜑 → 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) )
291 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) < 𝐴 ∧ 𝐴 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) ) )
292 190 291 mpdan ⊢ ( 𝜑 → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) < 𝐴 ∧ 𝐴 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) ) )
293 13 292 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) < 𝐴 ∧ 𝐴 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) )
294 293 simp2d ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) < 𝐴 )
295 2 194 189 1 290 294 lt2subd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) < ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) )
296 149 195 295 ltled ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) )
297 223 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ℕ )
298 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) )
299 243 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℤ )
300 elfzm11 ⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ↔ ( 𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀 ) ) )
301 244 299 300 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ↔ ( 𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀 ) ) )
302 298 301 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀 ) )
303 302 simp3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 < 𝑀 )
304 297 nnred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ℝ )
305 112 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℝ )
306 304 305 ltnled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖 ) )
307 303 306 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ¬ 𝑀 ≤ 𝑖 )
308 infssuzle ⊢ ( ( 𝑊 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑖 ∈ 𝑊 ) → inf ( 𝑊 , ℝ , < ) ≤ 𝑖 )
309 75 308 mpan ⊢ ( 𝑖 ∈ 𝑊 → inf ( 𝑊 , ℝ , < ) ≤ 𝑖 )
310 17 309 eqbrtrid ⊢ ( 𝑖 ∈ 𝑊 → 𝑀 ≤ 𝑖 )
311 307 310 nsyl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ¬ 𝑖 ∈ 𝑊 )
312 297 311 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊 ) )
313 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem2 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 )
314 312 313 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 )
315 314 iftrued ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) , 𝐵 ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) )
316 2fveq3 ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑖 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) )
317 316 fveq2d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑖 ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) )
318 317 breq1d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑖 ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 ↔ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 ) )
319 318 317 ifbieq1d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑖 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) = if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) , 𝐵 ) )
320 fveq2 ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑖 ) → ( 𝐻 ‘ 𝑡 ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑖 ) ) )
321 319 320 eleq12d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑖 ) → ( if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) ↔ if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ ( 𝐾 ‘ 𝑖 ) ) ) )
322 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
323 322 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ∀ 𝑡 ∈ 𝑇 if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
324 ffvelrn ⊢ ( ( 𝐾 : ℕ ⟶ 𝑇 ∧ 𝑖 ∈ ℕ ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝑇 )
325 23 223 324 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝑇 )
326 321 323 325 rspcdva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ ( 𝐾 ‘ 𝑖 ) ) )
327 315 326 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ( 𝐻 ‘ ( 𝐾 ‘ 𝑖 ) ) )
328 21 15 22 14 11 algrp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐾 ‘ ( 𝑖 + 1 ) ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑖 ) ) )
329 223 328 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝐾 ‘ ( 𝑖 + 1 ) ) = ( 𝐻 ‘ ( 𝐾 ‘ 𝑖 ) ) )
330 327 329 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ( 𝐾 ‘ ( 𝑖 + 1 ) ) )
331 223 270 sylan2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝐾 ‘ ( 𝑖 + 1 ) ) ∈ 𝑈 )
332 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ∈ 𝑈 ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ↔ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
333 331 332 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ↔ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
334 330 333 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ∧ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
335 334 simp2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) )
336 275 224 335 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) )
337 222 275 224 336 fsumle ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ≤ Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) )
338 225 276 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ↔ Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ≤ Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) ) )
339 337 338 mpbird ⊢ ( 𝜑 → 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
340 225 276 resubcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ∈ ℝ )
341 195 340 addge01d ⊢ ( 𝜑 → ( 0 ≤ ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ↔ ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) ≤ ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) ) )
342 339 341 mpbid ⊢ ( 𝜑 → ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) ≤ ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
343 149 195 281 296 342 letrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑀 ) ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ) + ( Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
344 343 280 breqtrrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
345 344 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝐵 − 𝐴 ) ≤ Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
346 fzfid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 1 ... 𝑧 ) ∈ Fin )
347 161 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
348 160 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
349 348 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
350 33 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ℕ )
351 350 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑦 ∈ ℕ )
352 351 nnred ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑦 ∈ ℝ )
353 40 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑧 ∈ ℝ )
354 ltle ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 < 𝑧 → 𝑦 ≤ 𝑧 ) )
355 352 353 354 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( 𝑦 < 𝑧 → 𝑦 ≤ 𝑧 ) )
356 351 21 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
357 nnz ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
358 357 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → 𝑧 ∈ ℤ )
359 elfz5 ⊢ ( ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑧 ∈ ℤ ) → ( 𝑦 ∈ ( 1 ... 𝑧 ) ↔ 𝑦 ≤ 𝑧 ) )
360 356 358 359 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( 𝑦 ∈ ( 1 ... 𝑧 ) ↔ 𝑦 ≤ 𝑧 ) )
361 355 360 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) ∧ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ) → ( 𝑦 < 𝑧 → 𝑦 ∈ ( 1 ... 𝑧 ) ) )
362 361 ralimdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℕ ) → ( ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 → ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ∈ ( 1 ... 𝑧 ) ) )
363 362 impr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ∈ ( 1 ... 𝑧 ) )
364 dfss3 ⊢ ( ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ( 1 ... 𝑧 ) ↔ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 ∈ ( 1 ... 𝑧 ) )
365 363 364 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ⊆ ( 1 ... 𝑧 ) )
366 346 347 349 365 fsumless ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
367 175 180 163 345 366 letrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝐵 − 𝐴 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
368 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) )
369 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → 𝑧 ∈ ℕ )
370 369 21 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → 𝑧 ∈ ( ℤ≥ ‘ 1 ) )
371 347 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) ∧ 𝑗 ∈ ( 1 ... 𝑧 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
372 368 370 371 fsumser ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑧 ) )
373 4 fveq1i ⊢ ( 𝑆 ‘ 𝑧 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑧 )
374 372 373 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) = ( 𝑆 ‘ 𝑧 ) )
375 166 ffnd ⊢ ( 𝜑 → 𝑆 Fn ℕ )
376 fnfvelrn ⊢ ( ( 𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ ) → ( 𝑆 ‘ 𝑧 ) ∈ ran 𝑆 )
377 375 369 376 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝑆 ‘ 𝑧 ) ∈ ran 𝑆 )
378 supxrub ⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( 𝑆 ‘ 𝑧 ) ∈ ran 𝑆 ) → ( 𝑆 ‘ 𝑧 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
379 171 377 378 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝑆 ‘ 𝑧 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
380 374 379 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑧 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑗 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
381 151 164 174 367 380 xrletrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ℕ ∧ ∀ 𝑦 ∈ ( ( 𝐺 ∘ 𝐾 ) “ ( 1 ... 𝑀 ) ) 𝑦 < 𝑧 ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
382 148 381 rexlimddv ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )