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 36107
Description: Lemma for poimir 36111 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 13877 . . . . . . . . . . . . 13 (1...𝑁) ∈ Fin
3 retop 24125 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
43fconst6 6732 . . . . . . . . . . . . 13 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
5 pttop 22933 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
62, 4, 5mp2an 690 . . . . . . . . . . . 12 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
71, 6eqeltri 2834 . . . . . . . . . . 11 𝑅 ∈ Top
8 poimir.i . . . . . . . . . . . 12 𝐼 = ((0[,]1) ↑m (1...𝑁))
9 ovex 7390 . . . . . . . . . . . 12 ((0[,]1) ↑m (1...𝑁)) ∈ V
108, 9eqeltri 2834 . . . . . . . . . . 11 𝐼 ∈ V
11 elrest 17309 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼)))
127, 10, 11mp2an 690 . . . . . . . . . 10 (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼))
13 eqid 2736 . . . . . . . . . . . . . 14 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
141, 13ptrecube 36078 . . . . . . . . . . . . 13 ((𝑧𝑅𝐶𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧)
1514ex 413 . . . . . . . . . . . 12 (𝑧𝑅 → (𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧))
16 inss1 4188 . . . . . . . . . . . . . . 15 (𝑧𝐼) ⊆ 𝑧
17 sseq1 3969 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → (𝑣𝑧 ↔ (𝑧𝐼) ⊆ 𝑧))
1816, 17mpbiri 257 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → 𝑣𝑧)
1918sseld 3943 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (𝐶𝑣𝐶𝑧))
20 ssrin 4193 . . . . . . . . . . . . . . 15 (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼))
21 sseq2 3970 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼)))
2220, 21syl5ibr 245 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2322reximdv 3167 . . . . . . . . . . . . 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 3145 . . . . . . . . . 10 (∃𝑧𝑅 𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2712, 26sylbi 216 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2827imp 407 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
2928adantl 482 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
30 resttop 22511 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Top)
317, 10, 30mp2an 690 . . . . . . . . . 10 (𝑅t 𝐼) ∈ Top
32 reex 11142 . . . . . . . . . . . . . 14 ℝ ∈ V
33 unitssre 13416 . . . . . . . . . . . . . 14 (0[,]1) ⊆ ℝ
34 mapss 8827 . . . . . . . . . . . . . 14 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁)))
3532, 33, 34mp2an 690 . . . . . . . . . . . . 13 ((0[,]1) ↑m (1...𝑁)) ⊆ (ℝ ↑m (1...𝑁))
368, 35eqsstri 3978 . . . . . . . . . . . 12 𝐼 ⊆ (ℝ ↑m (1...𝑁))
37 ovex 7390 . . . . . . . . . . . . . 14 (1...𝑁) ∈ V
38 uniretop 24126 . . . . . . . . . . . . . . 15 ℝ = (topGen‘ran (,))
391, 38ptuniconst 22949 . . . . . . . . . . . . . 14 (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑m (1...𝑁)) = 𝑅)
4037, 3, 39mp2an 690 . . . . . . . . . . . . 13 (ℝ ↑m (1...𝑁)) = 𝑅
4140restuni 22513 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑m (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
427, 36, 41mp2an 690 . . . . . . . . . . 11 𝐼 = (𝑅t 𝐼)
4342eltopss 22256 . . . . . . . . . 10 (((𝑅t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅t 𝐼)) → 𝑣𝐼)
4431, 43mpan 688 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → 𝑣𝐼)
4544sselda 3944 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → 𝐶𝐼)
46 2rp 12920 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
47 rpdivcl 12940 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ+𝑐 ∈ ℝ+) → (2 / 𝑐) ∈ ℝ+)
4846, 47mpan 688 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ+)
4948rpred 12957 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ)
50 ceicl 13746 . . . . . . . . . . . . . . 15 ((2 / 𝑐) ∈ ℝ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
5149, 50syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
52 0red 11158 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 ∈ ℝ)
5351zred 12607 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ)
5448rpgt0d 12960 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 < (2 / 𝑐))
55 ceige 13749 . . . . . . . . . . . . . . . 16 ((2 / 𝑐) ∈ ℝ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5649, 55syl 17 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5752, 49, 53, 54, 56ltletrd 11315 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → 0 < -(⌊‘-(2 / 𝑐)))
58 elnnz 12509 . . . . . . . . . . . . . 14 (-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2 / 𝑐)) ∈ ℤ ∧ 0 < -(⌊‘-(2 / 𝑐))))
5951, 57, 58sylanbrc 583 . . . . . . . . . . . . 13 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
60 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (ℤ𝑖) = (ℤ‘-(⌊‘-(2 / 𝑐))))
61 oveq2 7365 . . . . . . . . . . . . . . . . . 18 (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 / 𝑐))))
6261oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))
6362eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6463ralbidv 3174 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6560, 64rexeqbidv 3320 . . . . . . . . . . . . . 14 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6665rspcv 3577 . . . . . . . . . . . . 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 12820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7059, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7170sseld 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7372imdistani 569 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
7459nnrpd 12955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
7548, 74lerecd 12976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → ((2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)) ↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))))
7656, 75mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))
77 rpcn 12925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ∈ ℂ)
78 rpne0 12931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ≠ 0)
79 2cn 12228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℂ
80 2ne0 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ≠ 0
81 recdiv 11861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8279, 80, 81mpanl12 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8377, 78, 82syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / (2 / 𝑐)) = (𝑐 / 2))
8476, 83breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
8584ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
86 elmapi 8787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐶 ∈ ((0[,]1) ↑m (1...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8786, 8eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐶𝐼𝐶:(1...𝑁)⟶(0[,]1))
8887ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8988ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
9033, 89sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
91 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
92 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
9391, 92jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑𝑘 ∈ ℕ))
94 poimirlem30.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑𝐺:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9594ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
96 xp1st 7953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺𝑘) ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)))
97 elmapi 8787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9998ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℕ0)
10099nn0red 12474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
101 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
102100, 101nndivred 12207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10393, 102sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10490, 103resubcld 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℝ)
105104recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℂ)
106105abscld 15321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
10759nnrecred 12204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
108107ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
109 rphalfcl 12942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ+)
110109rpred 12957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ)
111110ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ)
112 ltletr 11247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
113106, 108, 111, 112syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11485, 113mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11573, 114sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
116 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝐶𝐼) → 𝜑)
11770sselda 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ)
118116, 117anim12i 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (𝜑𝑘 ∈ ℕ))
119118anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝜑𝑘 ∈ ℕ))
120 1re 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 ∈ ℝ
121 snssi 4768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (1 ∈ ℝ → {1} ⊆ ℝ)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {1} ⊆ ℝ
123 0re 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 0 ∈ ℝ
124 snssi 4768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (0 ∈ ℝ → {0} ⊆ ℝ)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {0} ⊆ ℝ
126122, 125unssi 4145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({1} ∪ {0}) ⊆ ℝ
127 1ex 11151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ V
128127fconst 6728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1}
129 c0ex 11149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ∈ V
130129fconst 6728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (2nd ‘(𝐺𝑘)) ∈ V
135 f1oeq1 6772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑓 = (2nd ‘(𝐺𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
136134, 135elab 3630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
137133, 136sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
138 dff1o3 6790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (Fun (2nd ‘(𝐺𝑘)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
141137, 139, 1403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
142 elfznn0 13534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
143142nn0red 12474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
144143ltp1d 12085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
145 fzdisj 13468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
146144, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
147146imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺𝑘)) “ ∅))
148 ima0 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)) “ ∅) = ∅
149147, 148eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
150141, 149sylan9req 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
151 fun 6704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))
154 nn0p1nn 12452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
156 nnuz 12806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℕ = (ℤ‘1)
157155, 156eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
158 elfzuz3 13438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
159 fzsplit2 13466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
160157, 158, 159syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
161160imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
162 f1ofo 6791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁))
163 foima 6761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
164137, 162, 1633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
165161, 164sylan9req 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑁) ∧ (𝜑𝑘 ∈ ℕ)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
166165ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
167153, 166eqtr3id 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
168167feq2d 6654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
170169ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
171126, 170sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ)
172 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
173171, 172nndivred 12207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
174173recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
175174absnegd 15334 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
176119, 175sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
177119, 170sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
178 elun 4108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}))
180 nnrecre 12195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
181 nnrp 12926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
182181rpreccld 12967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
183182rpge0d 12961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
184180, 183absidd 15307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ → (abs‘(1 / 𝑘)) = (1 / 𝑘))
185117, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
186117nnrecred 12204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ)
187107adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
188110adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ)
189 eluzle 12776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
190189adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
19159adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
192191nnrpd 12955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
193117nnrpd 12955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+)
194192, 193lerecd 12976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))))
195190, 194mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))
19684adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
197186, 187, 188, 195, 196letrd 11312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2))
198185, 197eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))
199 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1)
200199fvoveq1d 7379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘)))
201200breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)))
202198, 201syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
203109rpge0d 12961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ ℝ+ → 0 ≤ (𝑐 / 2))
204 nncn 12161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
205 nnne0 12187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
206204, 205div0d 11930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
207206abs00bd 15176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (abs‘(0 / 𝑘)) = 0)
208207breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0)
213212fvoveq1d 7379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘)))
214213breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)))
215211, 214syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
216202, 215jaod 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
22173, 106sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
222 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑)
223222anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑𝑘 ∈ ℕ))
224173renegcld 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
225223, 224sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
226225recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
227226abscld 15321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
22873, 227sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
229110, 110jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
230229ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
231 ltleadd 11638 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 836 . . . . . . . . . . . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
234105, 226abstrid 15341 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
235104, 225readdcld 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
236235recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ)
237236abscld 15321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
238106, 227readdcld 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
239110, 110readdcld 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
240239ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
241 lelttr 11245 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
247246, 171readdcld 11184 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ)
248247, 172nndivred 12207 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
249119, 248sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1))
254253ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
25533, 254sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
25674rpreccld 12967 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ+)
257256rpxrd 12958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
258257ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
25913rexmet 24154 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
260 elbl 23741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
261259, 260mp3an1 1448 . . . . . . . . . . . . . . . . . . . . . . . . 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 8803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1st ‘(𝐺𝑘)) ∈ (ℕ0m (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
26495, 96, 2633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
265 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑘 ∈ V
266 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
267265, 266mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
268 fzfid 13878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
269 inidm 4178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
270 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
271265fvconst2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
272271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
273264, 267, 268, 268, 269, 270, 272ofval 7628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))
274273oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
275222, 274sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
276222, 102sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
27713remetdval 24152 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐶𝑚) ∈ ℝ ∧ (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
278255, 276, 277syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
279275, 278eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
280279breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))
281280anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
282262, 281bitrd 278 . . . . . . . . . . . . . . . . . . . . . . 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 12924 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
285284ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*)
286 elbl 23741 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1448 . . . . . . . . . . . . . . . . . . . . . . . . 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 4108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ ({1} ∪ {0}) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ {0}))
290 fzofzp1 13669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘))
291 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {1} → 𝑧 = 1)
292291oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1))
293292eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘)))
294290, 293syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘)))
295 elfzonn0 13617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0)
296295nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ)
297296addid1d 11355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣)
298 elfzofz 13588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘))
299297, 298eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘))
300 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {0} → 𝑧 = 0)
301300oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0))
302301eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘)))
303299, 302syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘)))
304294, 303jaod 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
305289, 304biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
306305imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘))
307306adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘))
308 dffn3 6681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
309264, 308sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
310 poimirlem30.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
311309, 310fssd 6686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
312311adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
313 fzfid 13878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
314307, 312, 169, 313, 313, 269off 7635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
315314ffnd 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
319 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
320 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))
321317, 318, 313, 313, 269, 319, 320ofval 7628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
324323eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
325223, 324sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
326323adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
327326oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))
32887ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
329328ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
33033, 329sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
331248adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
33213remetdval 24152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℂ)
335171recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ)
336204ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
337205ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0)
338334, 335, 336, 337divdird 11969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
339102recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
340339adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
341340, 174subnegd 11519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
342338, 341eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
343342oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
344343adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
345330recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℂ)
346102adantllr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
347346adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
348347recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
349174adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
350349negcld 11499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
351345, 348, 350subsubd 11540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
352344, 351eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
353352fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
354327, 333, 3533eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
355354adantl3r 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
356772halvesd 12399 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) = 𝑐)
357356eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
358357ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
359355, 358breq12d 5118 . . . . . . . . . . . . . . . . . . . . . . . . 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 631 . . . . . . . . . . . . . . . . . . . . . . . 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 278 . . . . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . . . . 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 293 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
364363ralimdva 3164 . . . . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
366 elfznn0 13534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0)
367366nn0red 12474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ)
368 nndivre 12194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
369367, 368sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
370 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣)
371367, 370jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣))
372181rpregt0d 12963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
373 divge0 12024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑣 ∈ ℝ ∧ 0 ≤ 𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑣 / 𝑘))
374371, 372, 373syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘))
375 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣𝑘)
376375adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣𝑘)
377367adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ)
378 1red 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
379181adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
380377, 378, 379ledivmuld 13010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1)))
381204mulid1d 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
382381breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
383382adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
384380, 383bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣𝑘))
385376, 384mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1)
386 elicc01 13383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1))
387369, 374, 385, 386syl3anbrc 1343 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1))
388387ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1))
389 elsni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {𝑘} → 𝑧 = 𝑘)
390389oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘))
391390eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1)))
392388, 391syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1)))
393392impr 455 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
394365, 393sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
395265fconst 6728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
396395a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
397394, 314, 396, 313, 313, 269off 7635 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
398397ffnd 6669 . . . . . . . . . . . . . . . . . . . . 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 2829 . . . . . . . . . . . . . . . . . . . . . 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 7390 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) ∈ V
403402, 37elmap 8809 . . . . . . . . . . . . . . . . . . . . . 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 274 . . . . . . . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . . . . . . . . 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 3926 . . . . . . . . . . . . . . . . . . 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 7390 . . . . . . . . . . . . . . . . . . . . 21 (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ V
410409elixp 8842 . . . . . . . . . . . . . . . . . . . 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 624 . . . . . . . . . . . . . . . . . . 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 274 . . . . . . . . . . . . . . . . . 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 251 . . . . . . . . . . . . . . . . 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 3937 . . . . . . . . . . . . . . . . . 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 3151 . . . . . . . . . . . . . 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 1354 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋))))
422421imp43 428 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
423 r19.29 3117 . . . . . . . . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
425424fveq1d 6844 . . . . . . . . . . . . . . . . . . . . . . . 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, 426eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = 𝑋)
428427breq2d 5117 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) → (0𝑟((𝐹𝑧)‘𝑛) ↔ 0𝑟𝑋))
429428rspcev 3581 . . . . . . . . . . . . . . . . . . . . 21 (((((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
430429rexlimivw 3148 . . . . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘f + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
435117, 434sylan2 593 . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . 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 3152 . . . . . . . . . . 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 679 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44429, 443rexlimddv 3158 . . . . . 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 3176 . . . 4 (∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
448446, 447syl6ibr 251 . . 3 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
449448ralrimdva 3151 . 2 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
450 ralcom 3272 . 2 (∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
451449, 450syl6ib 250 1 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  {cpr 4588   cuni 4865   class class class wbr 5105   × cxp 5631  ccnv 5632  ran crn 5634  cres 5635  cima 5636  ccom 5637  Fun wfun 6490   Fn wfn 6491  wf 6492  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  f cof 7615  1st c1st 7919  2nd c2nd 7920  m cmap 8765  Xcixp 8835  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  +crp 12915  (,)cioo 13264  [,]cicc 13267  ...cfz 13424  ..^cfzo 13567  cfl 13695  abscabs 15119  t crest 17302  topGenctg 17319  tcpt 17320  ∞Metcxmet 20781  ballcbl 20783  Topctop 22242   Cn ccn 22575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-rest 17304  df-topgen 17325  df-pt 17326  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-bases 22296
This theorem is referenced by:  poimirlem30  36108
  Copyright terms: Public domain W3C validator