Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem29 Structured version   Visualization version   GIF version

Theorem poimirlem29 34807
Description: Lemma for poimir 34811 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑m (1...𝑁))
poimir.r 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
poimirlem30.x 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛)
poimirlem30.2 (𝜑𝐺:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
poimirlem30.3 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
poimirlem30.4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
Assertion
Ref Expression
poimirlem29 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
Distinct variable groups:   𝑓,𝑖,𝑗,𝑘,𝑚,𝑛,𝑧   𝜑,𝑗,𝑚,𝑛   𝑗,𝐹,𝑚,𝑛   𝑗,𝑁,𝑚,𝑛   𝜑,𝑖,𝑘   𝑓,𝑁,𝑖,𝑘   𝜑,𝑧   𝑓,𝐹,𝑘,𝑧   𝑧,𝑁   𝐶,𝑖,𝑘,𝑚,𝑛,𝑧   𝑖,𝑟,𝑣,𝑗,𝑘,𝑚,𝑛,𝑧,𝜑   𝑓,𝑟,𝑣   𝑖,𝐹,𝑟,𝑣   𝑓,𝐺,𝑖,𝑗,𝑘,𝑚,𝑛,𝑟,𝑣,𝑧   𝑓,𝐼,𝑖,𝑗,𝑘,𝑚,𝑛,𝑟,𝑣,𝑧   𝑁,𝑟,𝑣   𝑅,𝑓,𝑖,𝑗,𝑘,𝑚,𝑛,𝑟,𝑣,𝑧   𝑓,𝑋,𝑖,𝑚,𝑟,𝑣,𝑧   𝐶,𝑓,𝑗,𝑣
Allowed substitution hints:   𝜑(𝑓)   𝐶(𝑟)   𝑋(𝑗,𝑘,𝑛)

Proof of Theorem poimirlem29
Dummy variable 𝑐 is distinct from all other variables.
StepHypRef Expression
1 poimir.r . . . . . . . . . . . 12 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
2 fzfi 13335 . . . . . . . . . . . . 13 (1...𝑁) ∈ Fin
3 retop 23304 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
43fconst6 6568 . . . . . . . . . . . . 13 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
5 pttop 22125 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
62, 4, 5mp2an 688 . . . . . . . . . . . 12 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
71, 6eqeltri 2914 . . . . . . . . . . 11 𝑅 ∈ Top
8 poimir.i . . . . . . . . . . . 12 𝐼 = ((0[,]1) ↑m (1...𝑁))
9 ovex 7183 . . . . . . . . . . . 12 ((0[,]1) ↑m (1...𝑁)) ∈ V
108, 9eqeltri 2914 . . . . . . . . . . 11 𝐼 ∈ V
11 elrest 16696 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼)))
127, 10, 11mp2an 688 . . . . . . . . . 10 (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼))
13 eqid 2826 . . . . . . . . . . . . . 14 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
141, 13ptrecube 34778 . . . . . . . . . . . . 13 ((𝑧𝑅𝐶𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧)
1514ex 413 . . . . . . . . . . . 12 (𝑧𝑅 → (𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧))
16 inss1 4209 . . . . . . . . . . . . . . 15 (𝑧𝐼) ⊆ 𝑧
17 sseq1 3996 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → (𝑣𝑧 ↔ (𝑧𝐼) ⊆ 𝑧))
1816, 17mpbiri 259 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → 𝑣𝑧)
1918sseld 3970 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (𝐶𝑣𝐶𝑧))
20 ssrin 4214 . . . . . . . . . . . . . . 15 (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼))
21 sseq2 3997 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼)))
2220, 21syl5ibr 247 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2322reximdv 3278 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2419, 23imim12d 81 . . . . . . . . . . . 12 (𝑣 = (𝑧𝐼) → ((𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)))
2515, 24syl5com 31 . . . . . . . . . . 11 (𝑧𝑅 → (𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)))
2625rexlimiv 3285 . . . . . . . . . 10 (∃𝑧𝑅 𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2712, 26sylbi 218 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2827imp 407 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
2928adantl 482 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
30 resttop 21703 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Top)
317, 10, 30mp2an 688 . . . . . . . . . 10 (𝑅t 𝐼) ∈ Top
32 reex 10622 . . . . . . . . . . . . . 14 ℝ ∈ V
33 unitssre 12880 . . . . . . . . . . . . . 14 (0[,]1) ⊆ ℝ
34 mapss 8447 . . . . . . . . . . . . . 14 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁)))
3532, 33, 34mp2an 688 . . . . . . . . . . . . 13 ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁))
368, 35eqsstri 4005 . . . . . . . . . . . 12 𝐼 ⊆ (ℝ ↑m (1...𝑁))
37 ovex 7183 . . . . . . . . . . . . . 14 (1...𝑁) ∈ V
38 uniretop 23305 . . . . . . . . . . . . . . 15 ℝ = (topGen‘ran (,))
391, 38ptuniconst 22141 . . . . . . . . . . . . . 14 (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑m (1...𝑁)) = 𝑅)
4037, 3, 39mp2an 688 . . . . . . . . . . . . 13 (ℝ ↑m (1...𝑁)) = 𝑅
4140restuni 21705 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑m (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
427, 36, 41mp2an 688 . . . . . . . . . . 11 𝐼 = (𝑅t 𝐼)
4342eltopss 21450 . . . . . . . . . 10 (((𝑅t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅t 𝐼)) → 𝑣𝐼)
4431, 43mpan 686 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → 𝑣𝐼)
4544sselda 3971 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → 𝐶𝐼)
46 2rp 12389 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
47 rpdivcl 12409 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ+𝑐 ∈ ℝ+) → (2 / 𝑐) ∈ ℝ+)
4846, 47mpan 686 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ+)
4948rpred 12426 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ)
50 ceicl 13206 . . . . . . . . . . . . . . 15 ((2 / 𝑐) ∈ ℝ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
5149, 50syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
52 0red 10638 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 ∈ ℝ)
5351zred 12081 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ)
5448rpgt0d 12429 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 < (2 / 𝑐))
55 ceige 13208 . . . . . . . . . . . . . . . 16 ((2 / 𝑐) ∈ ℝ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5649, 55syl 17 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5752, 49, 53, 54, 56ltletrd 10794 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → 0 < -(⌊‘-(2 / 𝑐)))
58 elnnz 11985 . . . . . . . . . . . . . 14 (-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2 / 𝑐)) ∈ ℤ ∧ 0 < -(⌊‘-(2 / 𝑐))))
5951, 57, 58sylanbrc 583 . . . . . . . . . . . . 13 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
60 fveq2 6669 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (ℤ𝑖) = (ℤ‘-(⌊‘-(2 / 𝑐))))
61 oveq2 7158 . . . . . . . . . . . . . . . . . 18 (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 / 𝑐))))
6261oveq2d 7166 . . . . . . . . . . . . . . . . 17 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))
6362eleq2d 2903 . . . . . . . . . . . . . . . 16 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6463ralbidv 3202 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6560, 64rexeqbidv 3408 . . . . . . . . . . . . . 14 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6665rspcv 3622 . . . . . . . . . . . . 13 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6759, 66syl 17 . . . . . . . . . . . 12 (𝑐 ∈ ℝ+ → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6867adantl 482 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
69 uznnssnn 12289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7059, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7170sseld 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7372imdistani 569 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
7459nnrpd 12424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
7548, 74lerecd 12445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → ((2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)) ↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))))
7656, 75mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))
77 rpcn 12394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ∈ ℂ)
78 rpne0 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ≠ 0)
79 2cn 11706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℂ
80 2ne0 11735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ≠ 0
81 recdiv 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8279, 80, 81mpanl12 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8377, 78, 82syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / (2 / 𝑐)) = (𝑐 / 2))
8476, 83breqtrd 5089 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
8584ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
86 elmapi 8423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐶 ∈ ((0[,]1) ↑m (1...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8786, 8eleq2s 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐶𝐼𝐶:(1...𝑁)⟶(0[,]1))
8887ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8988ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
9033, 89sseldi 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
91 simp-4l 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
92 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
9391, 92jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑𝑘 ∈ ℕ))
94 poimirlem30.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑𝐺:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9594ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
96 xp1st 7717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)))
97 elmapi 8423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9998ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℕ0)
10099nn0red 11950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
101 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
102100, 101nndivred 11685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10393, 102sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10490, 103resubcld 11062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℝ)
105104recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℂ)
106105abscld 14791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
10759nnrecred 11682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
108107ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
109 rphalfcl 12411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ+)
110109rpred 12426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ)
111110ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ)
112 ltletr 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
113106, 108, 111, 112syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11485, 113mpan2d 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11573, 114sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
116 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝐶𝐼) → 𝜑)
11770sselda 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ)
118116, 117anim12i 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (𝜑𝑘 ∈ ℕ))
119118anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝜑𝑘 ∈ ℕ))
120 1re 10635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 ∈ ℝ
121 snssi 4740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (1 ∈ ℝ → {1} ⊆ ℝ)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {1} ⊆ ℝ
123 0re 10637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 0 ∈ ℝ
124 snssi 4740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (0 ∈ ℝ → {0} ⊆ ℝ)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {0} ⊆ ℝ
126122, 125unssi 4165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({1} ∪ {0}) ⊆ ℝ
127 1ex 10631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ V
128127fconst 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1}
129 c0ex 10629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ∈ V
130129fconst 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
131128, 130pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
132 xp2nd 7718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
13395, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
134 fvex 6682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (2nd ‘(𝐺𝑘)) ∈ V
135 f1oeq1 6603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑓 = (2nd ‘(𝐺𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
136134, 135elab 3671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
137133, 136sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
138 dff1o3 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(𝐺𝑘))))
139138simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(𝐺𝑘)))
140 imain 6438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (Fun (2nd ‘(𝐺𝑘)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
141137, 139, 1403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
142 elfznn0 12995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
143142nn0red 11950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
144143ltp1d 11564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
145 fzdisj 12929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
146144, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
147146imaeq2d 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺𝑘)) “ ∅))
148 ima0 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)) “ ∅) = ∅
149147, 148syl6eq 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
150141, 149sylan9req 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
151 fun 6539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
152131, 150, 151sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
153 imaundi 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))
154 nn0p1nn 11930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
156 nnuz 12275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℕ = (ℤ‘1)
157155, 156syl6eleq 2928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
158 elfzuz3 12900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
159 fzsplit2 12927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
160157, 158, 159syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
161160imaeq2d 5928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
162 f1ofo 6621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁))
163 foima 6594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
164137, 162, 1633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
165161, 164sylan9req 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑁) ∧ (𝜑𝑘 ∈ ℕ)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
166165ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
167153, 166syl5eqr 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
168167feq2d 6499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
169152, 168mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
170169ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
171126, 170sseldi 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ)
172 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
173171, 172nndivred 11685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
174173recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
175174absnegd 14804 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
176119, 175sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
177119, 170sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
178 elun 4129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}) ↔ ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}))
179177, 178sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}))
180 nnrecre 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
181 nnrp 12395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
182181rpreccld 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
183182rpge0d 12430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
184180, 183absidd 14777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ → (abs‘(1 / 𝑘)) = (1 / 𝑘))
185117, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
186117nnrecred 11682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ)
187107adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
188110adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ)
189 eluzle 12250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
190189adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
19159adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
192191nnrpd 12424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
193117nnrpd 12424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+)
194192, 193lerecd 12445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))))
195190, 194mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))
19684adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
197186, 187, 188, 195, 196letrd 10791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2))
198185, 197eqbrtrd 5085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))
199 elsni 4581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1)
200199fvoveq1d 7172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘)))
201200breq1d 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)))
202198, 201syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
203109rpge0d 12430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ ℝ+ → 0 ≤ (𝑐 / 2))
204 nncn 11640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
205 nnne0 11665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
206204, 205div0d 11409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
207206abs00bd 14646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (abs‘(0 / 𝑘)) = 0)
208207breq1d 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → ((abs‘(0 / 𝑘)) ≤ (𝑐 / 2) ↔ 0 ≤ (𝑐 / 2)))
209208biimparc 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((0 ≤ (𝑐 / 2) ∧ 𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
210203, 209sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
211117, 210syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
212 elsni 4581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0)
213212fvoveq1d 7172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘)))
214213breq1d 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)))
215211, 214syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
216202, 215jaod 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
217216adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
218217ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
219179, 218mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
220176, 219eqbrtrd 5085 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
22173, 106sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
222 simpll 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑)
223222anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑𝑘 ∈ ℕ))
224173renegcld 11061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
225223, 224sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
226225recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
227226abscld 14791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
22873, 227sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
229110, 110jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
230229ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
231 ltleadd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) ∧ ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) ∧ (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
232221, 228, 230, 231syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) ∧ (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
233220, 232mpan2d 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
234105, 226abstrid 14811 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
235104, 225readdcld 10664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
236235recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ)
237236abscld 14791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
238106, 227readdcld 10664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
239110, 110readdcld 10664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
240239ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
241 lelttr 10725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ ∧ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ ∧ ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ) → (((abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∧ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
242237, 238, 240, 241syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∧ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
243234, 242mpand 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
24473, 243sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
245115, 233, 2443syld 60 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
246100adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
247246, 171readdcld 10664 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ)
248247, 172nndivred 11685 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
249119, 248sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
250245, 249jctild 526 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
251250adantld 491 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))) → (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
25273adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
25387ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1))
254253ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
25533, 254sseldi 3969 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
25674rpreccld 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ+)
257256rpxrd 12427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
258257ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
25913rexmet 23333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
260 elbl 22932 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
261259, 260mp3an1 1441 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
262255, 258, 261syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
263 elmapfn 8424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
26495, 96, 2633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
265 vex 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑘 ∈ V
266 fnconstg 6566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
267265, 266mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
268 fzfid 13336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
269 inidm 4199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
270 eqidd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
271265fvconst2 6964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
272271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
273264, 267, 268, 268, 269, 270, 272ofval 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))
274273oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
275222, 274sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
276222, 102sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
27713remetdval 23331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐶𝑚) ∈ ℝ ∧ (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
278255, 276, 277syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
279275, 278eqtrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
280279breq1d 5073 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))
281280anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
282262, 281bitrd 280 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
283252, 282sylan 580 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
284 rpxr 12393 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
285284ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*)
286 elbl 22932 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
287259, 286mp3an1 1441 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐶𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
28890, 285, 287syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
289 elun 4129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ ({1} ∪ {0}) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ {0}))
290 fzofzp1 13129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘))
291 elsni 4581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {1} → 𝑧 = 1)
292291oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1))
293292eleq1d 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘)))
294290, 293syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘)))
295 elfzonn0 13077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0)
296295nn0cnd 11951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ)
297296addid1d 10834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣)
298 elfzofz 13048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘))
299297, 298eqeltrd 2918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘))
300 elsni 4581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {0} → 𝑧 = 0)
301300oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0))
302301eleq1d 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘)))
303299, 302syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘)))
304294, 303jaod 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
305289, 304syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
306305imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘))
307306adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘))
308 dffn3 6524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
309264, 308sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
310 poimirlem30.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
311309, 310fssd 6527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
312311adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
313 fzfid 13336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
314307, 312, 169, 313, 313, 269off 7418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
315314ffnd 6514 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁))
316265, 266mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
317264adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
318169ffnd 6514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
319 eqidd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
320 eqidd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))
321317, 318, 313, 313, 269, 319, 320ofval 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)))
322271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
323315, 316, 313, 313, 269, 321, 322ofval 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
324323eleq1d 2902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
325223, 324sylanl1 676 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
326323adantl3r 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
327326oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))
32887ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
329328ffvelrnda 6849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
33033, 329sseldi 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
331248adantl3r 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
33213remetdval 23331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐶𝑚) ∈ ℝ ∧ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
333330, 331, 332syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
334246recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℂ)
335171recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ)
336204ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
337205ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0)
338334, 335, 336, 337divdird 11448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
339102recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
340339adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
341340, 174subnegd 10998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
342338, 341eqtr4d 2864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
343342oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
344343adantl3r 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
345330recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℂ)
346102adantllr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
347346adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
348347recnd 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
349174adantl3r 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
350349negcld 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
351345, 348, 350subsubd 11019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
352344, 351eqtrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
353352fveq2d 6673 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
354327, 333, 3533eqtrd 2865 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
355354adantl3r 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
356772halvesd 11877 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) = 𝑐)
357356eqcomd 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
358357ad4antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
359355, 358breq12d 5076 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐 ↔ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
360325, 359anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐) ↔ (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
361288, 360bitrd 280 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
36273, 361sylanl1 676 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
363251, 283, 3623imtr4d 295 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
364363ralimdva 3182 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
365 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
366 elfznn0 12995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0)
367366nn0red 11950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ)
368 nndivre 11672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
369367, 368sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
370 elfzle1 12905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣)
371367, 370jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣))
372181rpregt0d 12432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
373 divge0 11503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑣 ∈ ℝ ∧ 0 ≤ 𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑣 / 𝑘))
374371, 372, 373syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘))
375 elfzle2 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣𝑘)
376375adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣𝑘)
377367adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ)
378 1red 10636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
379181adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
380377, 378, 379ledivmuld 12479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1)))
381204mulid1d 10652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
382381breq2d 5075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
383382adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
384380, 383bitrd 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣𝑘))
385376, 384mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1)
386 elicc01 12849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1))
387369, 374, 385, 386syl3anbrc 1337 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1))
388387ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1))
389 elsni 4581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {𝑘} → 𝑧 = 𝑘)
390389oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘))
391390eleq1d 2902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1)))
392388, 391syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1)))
393392impr 455 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
394365, 393sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
395265fconst 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
396395a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
397394, 314, 396, 313, 313, 269off 7418 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
398397ffnd 6514 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
399119, 398sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
400364, 399jctild 526 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐))))
4018eleq2i 2909 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
402 ovex 7183 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) ∈ V
403402, 37elmap 8430 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
404401, 403bitri 276 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
405397, 404sylibr 235 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
406119, 405sylan 580 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
407400, 406jctird 527 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼)))
408 elin 4173 . . . . . . . . . . . . . . . . . . 19 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
409 ovex 7183 . . . . . . . . . . . . . . . . . . . . 21 (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ V
410409elixp 8462 . . . . . . . . . . . . . . . . . . . 20 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
411410anbi1i 623 . . . . . . . . . . . . . . . . . . 19 (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼) ↔ (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
412408, 411bitri 276 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
413407, 412syl6ibr 253 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼)))
414 ssel 3965 . . . . . . . . . . . . . . . . . 18 ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣))
415414com12 32 . . . . . . . . . . . . . . . . 17 ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣))
416413, 415syl6 35 . . . . . . . . . . . . . . . 16 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
417416impd 411 . . . . . . . . . . . . . . 15 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣))
418417ralrimdva 3194 . . . . . . . . . . . . . 14 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣))
419418expd 416 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
420 poimirlem30.4 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
4214203exp2 1348 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋))))
422421imp43 428 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
423 r19.29 3259 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋))
424 fveq2 6669 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
425424fveq1d 6671 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛))
426 poimirlem30.x . . . . . . . . . . . . . . . . . . . . . . . 24 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑛)
427425, 426syl6eqr 2879 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = 𝑋)
428427breq2d 5075 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → (0𝑟((𝐹𝑧)‘𝑛) ↔ 0𝑟𝑋))
429428rspcev 3627 . . . . . . . . . . . . . . . . . . . . 21 (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
430429rexlimivw 3287 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
431423, 430syl 17 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
432431expcom 414 . . . . . . . . . . . . . . . . . 18 (∃𝑗 ∈ (0...𝑁)0𝑟𝑋 → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
433422, 432syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
434433ralrimdvva 3199 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
435117, 434sylan2 592 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
436435anassrs 468 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
437436adantllr 715 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
438419, 437syl6d 75 . . . . . . . . . . . 12 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
439438rexlimdva 3289 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
44068, 439syld 47 . . . . . . . . . 10 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
441440com23 86 . . . . . . . . 9 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
442441impr 455 . . . . . . . 8 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44345, 442sylanl2 677 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44429, 443rexlimddv 3296 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
445444expr 457 . . . . 5 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (𝐶𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
446445com23 86 . . . 4 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
447 r19.21v 3180 . . . 4 (∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
448446, 447syl6ibr 253 . . 3 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
449448ralrimdva 3194 . 2 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
450 ralcom 3359 . 2 (∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
451449, 450syl6ib 252 1 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2107  {cab 2804  wne 3021  wral 3143  wrex 3144  Vcvv 3500  cun 3938  cin 3939  wss 3940  c0 4295  {csn 4564  {cpr 4566   cuni 4837   class class class wbr 5063   × cxp 5552  ccnv 5553  ran crn 5555  cres 5556  cima 5557  ccom 5558  Fun wfun 6348   Fn wfn 6349  wf 6350  ontowfo 6352  1-1-ontowf1o 6353  cfv 6354  (class class class)co 7150  f cof 7401  1st c1st 7683  2nd c2nd 7684  m cmap 8401  Xcixp 8455  Fincfn 8503  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  *cxr 10668   < clt 10669  cle 10670  cmin 10864  -cneg 10865   / cdiv 11291  cn 11632  2c2 11686  0cn0 11891  cz 11975  cuz 12237  +crp 12384  (,)cioo 12733  [,]cicc 12736  ...cfz 12887  ..^cfzo 13028  cfl 13155  abscabs 14588  t crest 16689  topGenctg 16706  tcpt 16707  ∞Metcxmet 20465  ballcbl 20467  Topctop 21436   Cn ccn 21767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8284  df-map 8403  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fi 8869  df-sup 8900  df-inf 8901  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-n0 11892  df-z 11976  df-uz 12238  df-q 12343  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13425  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-rest 16691  df-topgen 16712  df-pt 16713  df-psmet 20472  df-xmet 20473  df-met 20474  df-bl 20475  df-mopn 20476  df-top 21437  df-topon 21454  df-bases 21489
This theorem is referenced by:  poimirlem30  34808
  Copyright terms: Public domain W3C validator