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 33771
Description: Lemma for poimir 33775 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
poimir.r 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
poimirlem30.x 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)
poimirlem30.2 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
poimirlem30.3 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
poimirlem30.4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
Assertion
Ref Expression
poimirlem29 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((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 12979 . . . . . . . . . . . . 13 (1...𝑁) ∈ Fin
3 retop 22785 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
43fconst6 6235 . . . . . . . . . . . . 13 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
5 pttop 21606 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
62, 4, 5mp2an 672 . . . . . . . . . . . 12 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
71, 6eqeltri 2846 . . . . . . . . . . 11 𝑅 ∈ Top
8 poimir.i . . . . . . . . . . . 12 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
9 ovex 6823 . . . . . . . . . . . 12 ((0[,]1) ↑𝑚 (1...𝑁)) ∈ V
108, 9eqeltri 2846 . . . . . . . . . . 11 𝐼 ∈ V
11 elrest 16296 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼)))
127, 10, 11mp2an 672 . . . . . . . . . 10 (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼))
13 eqid 2771 . . . . . . . . . . . . . 14 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
141, 13ptrecube 33742 . . . . . . . . . . . . 13 ((𝑧𝑅𝐶𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧)
1514ex 397 . . . . . . . . . . . 12 (𝑧𝑅 → (𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧))
16 inss1 3981 . . . . . . . . . . . . . . 15 (𝑧𝐼) ⊆ 𝑧
17 sseq1 3775 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → (𝑣𝑧 ↔ (𝑧𝐼) ⊆ 𝑧))
1816, 17mpbiri 248 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → 𝑣𝑧)
1918sseld 3751 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (𝐶𝑣𝐶𝑧))
20 ssrin 3986 . . . . . . . . . . . . . . 15 (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼))
21 sseq2 3776 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼)))
2220, 21syl5ibr 236 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2322reximdv 3164 . . . . . . . . . . . . 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 3175 . . . . . . . . . 10 (∃𝑧𝑅 𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2712, 26sylbi 207 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2827imp 393 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
2928adantl 467 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
30 resttop 21185 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Top)
317, 10, 30mp2an 672 . . . . . . . . . 10 (𝑅t 𝐼) ∈ Top
32 reex 10229 . . . . . . . . . . . . . 14 ℝ ∈ V
33 unitssre 12526 . . . . . . . . . . . . . 14 (0[,]1) ⊆ ℝ
34 mapss 8054 . . . . . . . . . . . . . 14 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
3532, 33, 34mp2an 672 . . . . . . . . . . . . 13 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
368, 35eqsstri 3784 . . . . . . . . . . . 12 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
37 ovex 6823 . . . . . . . . . . . . . 14 (1...𝑁) ∈ V
38 uniretop 22786 . . . . . . . . . . . . . . 15 ℝ = (topGen‘ran (,))
391, 38ptuniconst 21622 . . . . . . . . . . . . . 14 (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
4037, 3, 39mp2an 672 . . . . . . . . . . . . 13 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
4140restuni 21187 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
427, 36, 41mp2an 672 . . . . . . . . . . 11 𝐼 = (𝑅t 𝐼)
4342eltopss 20932 . . . . . . . . . 10 (((𝑅t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅t 𝐼)) → 𝑣𝐼)
4431, 43mpan 670 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → 𝑣𝐼)
4544sselda 3752 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → 𝐶𝐼)
46 2rp 12040 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
47 rpdivcl 12059 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ+𝑐 ∈ ℝ+) → (2 / 𝑐) ∈ ℝ+)
4846, 47mpan 670 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ+)
4948rpred 12075 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ)
50 ceicl 12850 . . . . . . . . . . . . . . 15 ((2 / 𝑐) ∈ ℝ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
5149, 50syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
52 0red 10243 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 ∈ ℝ)
5351zred 11684 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ)
5448rpgt0d 12078 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 < (2 / 𝑐))
55 ceige 12852 . . . . . . . . . . . . . . . 16 ((2 / 𝑐) ∈ ℝ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5649, 55syl 17 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5752, 49, 53, 54, 56ltletrd 10399 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → 0 < -(⌊‘-(2 / 𝑐)))
58 elnnz 11589 . . . . . . . . . . . . . 14 (-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2 / 𝑐)) ∈ ℤ ∧ 0 < -(⌊‘-(2 / 𝑐))))
5951, 57, 58sylanbrc 572 . . . . . . . . . . . . 13 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
60 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (ℤ𝑖) = (ℤ‘-(⌊‘-(2 / 𝑐))))
61 oveq2 6801 . . . . . . . . . . . . . . . . . 18 (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 / 𝑐))))
6261oveq2d 6809 . . . . . . . . . . . . . . . . 17 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))
6362eleq2d 2836 . . . . . . . . . . . . . . . 16 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6463ralbidv 3135 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6560, 64rexeqbidv 3302 . . . . . . . . . . . . . 14 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6665rspcv 3456 . . . . . . . . . . . . 13 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6759, 66syl 17 . . . . . . . . . . . 12 (𝑐 ∈ ℝ+ → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6867adantl 467 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
69 uznnssnn 11937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7059, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7170sseld 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7271adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7372imdistani 558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
7459nnrpd 12073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
7548, 74lerecd 12094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → ((2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)) ↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))))
7656, 75mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))
77 rpcn 12044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ∈ ℂ)
78 rpne0 12051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ≠ 0)
79 2cn 11293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℂ
80 2ne0 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ≠ 0
81 recdiv 10933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8279, 80, 81mpanl12 682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8377, 78, 82syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / (2 / 𝑐)) = (𝑐 / 2))
8476, 83breqtrd 4812 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
8584ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
86 elmapi 8031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐶 ∈ ((0[,]1) ↑𝑚 (1...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8786, 8eleq2s 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐶𝐼𝐶:(1...𝑁)⟶(0[,]1))
8887ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8988ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
9033, 89sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
91 simp-4l 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
92 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
9391, 92jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑𝑘 ∈ ℕ))
94 poimirlem30.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9594ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
96 xp1st 7347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)))
97 elmapi 8031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9998ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℕ0)
10099nn0red 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
101 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
102100, 101nndivred 11271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10393, 102sylan 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10490, 103resubcld 10660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℝ)
105104recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℂ)
106105abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
10759nnrecred 11268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
108107ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
109 rphalfcl 12061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ+)
110109rpred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ)
111110ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ)
112 ltletr 10331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
113106, 108, 111, 112syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11485, 113mpan2d 674 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11573, 114sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
116 simpl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝐶𝐼) → 𝜑)
11770sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ)
118116, 117anim12i 600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (𝜑𝑘 ∈ ℕ))
119118anassrs 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝜑𝑘 ∈ ℕ))
120 1re 10241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 ∈ ℝ
121 snssi 4474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (1 ∈ ℝ → {1} ⊆ ℝ)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {1} ⊆ ℝ
123 0re 10242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 0 ∈ ℝ
124 snssi 4474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (0 ∈ ℝ → {0} ⊆ ℝ)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {0} ⊆ ℝ
126122, 125unssi 3939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({1} ∪ {0}) ⊆ ℝ
127 1ex 10237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ V
128127fconst 6231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1}
129 c0ex 10236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ∈ V
130129fconst 6231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
131128, 130pm3.2i 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
132 xp2nd 7348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
13395, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
134 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (2nd ‘(𝐺𝑘)) ∈ V
135 f1oeq1 6268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑓 = (2nd ‘(𝐺𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
136134, 135elab 3501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
137133, 136sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
138 dff1o3 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(𝐺𝑘))))
139138simprbi 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(𝐺𝑘)))
140 imain 6114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (Fun (2nd ‘(𝐺𝑘)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
141137, 139, 1403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
142 elfznn0 12640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
143142nn0red 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
144143ltp1d 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
145 fzdisj 12575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
146144, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
147146imaeq2d 5607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺𝑘)) “ ∅))
148 ima0 5622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)) “ ∅) = ∅
149147, 148syl6eq 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
150141, 149sylan9req 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
151 fun 6206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
153 imaundi 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))
154 nn0p1nn 11534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
156 nnuz 11925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℕ = (ℤ‘1)
157155, 156syl6eleq 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
158 elfzuz3 12546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
159 fzsplit2 12573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
160157, 158, 159syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
161160imaeq2d 5607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
162 f1ofo 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁))
163 foima 6261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
164137, 162, 1633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
165161, 164sylan9req 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑁) ∧ (𝜑𝑘 ∈ ℕ)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
166165ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
167153, 166syl5eqr 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
168167feq2d 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
170169ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
171126, 170sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ)
172 simpllr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
173171, 172nndivred 11271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
174173recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
175174absnegd 14396 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
176119, 175sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
177119, 170sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
178 elun 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}))
180 nnrecre 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
181 nnrp 12045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
182181rpreccld 12085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
183182rpge0d 12079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
184180, 183absidd 14369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ → (abs‘(1 / 𝑘)) = (1 / 𝑘))
185117, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
186117nnrecred 11268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ)
187107adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
188110adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ)
189 eluzle 11901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
190189adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
19159adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
192191nnrpd 12073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
193117nnrpd 12073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+)
194192, 193lerecd 12094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))))
195190, 194mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))
19684adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
197186, 187, 188, 195, 196letrd 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2))
198185, 197eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))
199 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1)
200199fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘)))
201200breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)))
202198, 201syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
203109rpge0d 12079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ ℝ+ → 0 ≤ (𝑐 / 2))
204 nncn 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
205 nnne0 11255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
206204, 205div0d 11002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
207206abs00bd 14239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (abs‘(0 / 𝑘)) = 0)
208207breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → ((abs‘(0 / 𝑘)) ≤ (𝑐 / 2) ↔ 0 ≤ (𝑐 / 2)))
209208biimparc 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((0 ≤ (𝑐 / 2) ∧ 𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
210203, 209sylan 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
211117, 210syldan 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
212 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0)
213212fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘)))
214213breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)))
215211, 214syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
216202, 215jaod 846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
22173, 106sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
222 simpll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑)
223222anim1i 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑𝑘 ∈ ℕ))
224173renegcld 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
225223, 224sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
226225recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
227226abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
22873, 227sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
229110, 110jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
230229ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
231 ltleadd 10713 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1475 . . . . . . . . . . . . . . . . . . . . . . . . . 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 674 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
234105, 226abstrid 14403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
235104, 225readdcld 10271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
236235recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ)
237236abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
238106, 227readdcld 10271 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
239110, 110readdcld 10271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
240239ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
241 lelttr 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
247246, 171readdcld 10271 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ)
248247, 172nndivred 11271 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
249119, 248sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
250245, 249jctild 515 . . . . . . . . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))) → (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
25273adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
25387ad3antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1))
254253ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
25533, 254sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
25674rpreccld 12085 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ+)
257256rpxrd 12076 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
258257ad3antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
25913rexmet 22814 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
260 elbl 22413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
261259, 260mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
262255, 258, 261syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
263 elmapfn 8032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
26495, 96, 2633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
265 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑘 ∈ V
266 fnconstg 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
267265, 266mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
268 fzfid 12980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
269 inidm 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
270 eqidd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
271265fvconst2 6613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
272271adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
273264, 267, 268, 268, 269, 270, 272ofval 7053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))
274273oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
275222, 274sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
276222, 102sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
27713remetdval 22812 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐶𝑚) ∈ ℝ ∧ (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
278255, 276, 277syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
279275, 278eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
280279breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))
281280anbi2d 614 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
282262, 281bitrd 268 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
283252, 282sylan 569 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
284 rpxr 12043 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
285284ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*)
286 elbl 22413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
287259, 286mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐶𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
28890, 285, 287syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
289 elun 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ ({1} ∪ {0}) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ {0}))
290 fzofzp1 12773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘))
291 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {1} → 𝑧 = 1)
292291oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1))
293292eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘)))
294290, 293syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘)))
295 elfzonn0 12721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0)
296295nn0cnd 11555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ)
297296addid1d 10438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣)
298 elfzofz 12693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘))
299297, 298eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘))
300 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {0} → 𝑧 = 0)
301300oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0))
302301eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘)))
303299, 302syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘)))
304294, 303jaod 846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
305289, 304syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
306305imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘))
307306adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘))
308 dffn3 6194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
309264, 308sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
310 poimirlem30.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
311309, 310fssd 6197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
312311adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
313 fzfid 12980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
314307, 312, 169, 313, 313, 269off 7059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
315 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁))
316314, 315syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁))
317265, 266mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
318264adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
319 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
320169, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
321 eqidd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
322 eqidd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))
323318, 320, 313, 313, 269, 321, 322ofval 7053 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)))
324271adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
325316, 317, 313, 313, 269, 323, 324ofval 7053 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
326325eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
327223, 326sylanl1 659 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
328325adantl3r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
329328oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))
33087ad3antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
331330ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
33233, 331sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
333248adantl3r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
33413remetdval 22812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐶𝑚) ∈ ℝ ∧ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
335332, 333, 334syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
336246recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℂ)
337171recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ)
338204ad3antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
339205ad3antlr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0)
340336, 337, 338, 339divdird 11041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
341102recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
342341adantlr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
343342, 174subnegd 10601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
344340, 343eqtr4d 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
345344oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
346345adantl3r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
347332recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℂ)
348102adantllr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
349348adantlr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
350349recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
351174adantl3r 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
352351negcld 10581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
353347, 350, 352subsubd 10622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
354346, 353eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
355354fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
356329, 335, 3553eqtrd 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
357356adantl3r 744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
358772halvesd 11480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) = 𝑐)
359358eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
360359ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
361357, 360breq12d 4799 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐 ↔ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
362327, 361anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐) ↔ (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
363288, 362bitrd 268 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
36473, 363sylanl1 659 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))))
365251, 283, 3643imtr4d 283 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
366365ralimdva 3111 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
367 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
368 elfznn0 12640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0)
369368nn0red 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ)
370 nndivre 11258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
371369, 370sylan 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
372 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣)
373369, 372jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣))
374181rpregt0d 12081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
375 divge0 11094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑣 ∈ ℝ ∧ 0 ≤ 𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑣 / 𝑘))
376373, 374, 375syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘))
377 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣𝑘)
378377adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣𝑘)
379369adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ)
380 1red 10257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
381181adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
382379, 380, 381ledivmuld 12128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1)))
383204mulid1d 10259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
384383breq2d 4798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
385384adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
386382, 385bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣𝑘))
387378, 386mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1)
388123, 120elicc2i 12444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1))
389371, 376, 387, 388syl3anbrc 1428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1))
390389ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1))
391 elsni 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {𝑘} → 𝑧 = 𝑘)
392391oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘))
393392eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1)))
394390, 393syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1)))
395394impr 442 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
396367, 395sylan 569 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
397265fconst 6231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
398397a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
399396, 314, 398, 313, 313, 269off 7059 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
400 ffn 6185 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
401399, 400syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
402119, 401sylan 569 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
403366, 402jctild 515 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐))))
4048eleq2i 2842 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
405 ovex 6823 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) ∈ V
406405, 37elmap 8038 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
407404, 406bitri 264 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
408399, 407sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
409119, 408sylan 569 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
410403, 409jctird 516 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)))
411 elin 3947 . . . . . . . . . . . . . . . . . . 19 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
412 ovex 6823 . . . . . . . . . . . . . . . . . . . . 21 (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
413412elixp 8069 . . . . . . . . . . . . . . . . . . . 20 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
414413anbi1i 610 . . . . . . . . . . . . . . . . . . 19 (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼) ↔ (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
415411, 414bitri 264 . . . . . . . . . . . . . . . . . 18 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
416410, 415syl6ibr 242 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼)))
417 ssel 3746 . . . . . . . . . . . . . . . . . 18 ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
418417com12 32 . . . . . . . . . . . . . . . . 17 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
419416, 418syl6 35 . . . . . . . . . . . . . . . 16 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
420419impd 396 . . . . . . . . . . . . . . 15 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
421420ralrimdva 3118 . . . . . . . . . . . . . 14 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
422421expd 400 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
423 poimirlem30.4 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
4244233exp2 1447 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋))))
425424imp43 414 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
426 r19.29 3220 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋))
427 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))))
428427fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
429 poimirlem30.x . . . . . . . . . . . . . . . . . . . . . . . 24 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)
430428, 429syl6eqr 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = 𝑋)
431430breq2d 4798 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → (0𝑟((𝐹𝑧)‘𝑛) ↔ 0𝑟𝑋))
432431rspcev 3460 . . . . . . . . . . . . . . . . . . . . 21 (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
433432rexlimivw 3177 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
434426, 433syl 17 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
435434expcom 398 . . . . . . . . . . . . . . . . . 18 (∃𝑗 ∈ (0...𝑁)0𝑟𝑋 → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
436425, 435syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
437436ralrimdvva 3123 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
438117, 437sylan2 580 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
439438anassrs 458 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
440439adantllr 698 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
441422, 440syl6d 75 . . . . . . . . . . . 12 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
442441rexlimdva 3179 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
44368, 442syld 47 . . . . . . . . . 10 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
444443com23 86 . . . . . . . . 9 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
445444impr 442 . . . . . . . 8 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44645, 445sylanl2 660 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44729, 446rexlimddv 3183 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
448447expr 444 . . . . 5 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (𝐶𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
449448com23 86 . . . 4 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
450 r19.21v 3109 . . . 4 (∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
451449, 450syl6ibr 242 . . 3 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
452451ralrimdva 3118 . 2 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
453 ralcom 3246 . 2 (∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
454452, 453syl6ib 241 1 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 834  w3a 1071   = wceq 1631  wcel 2145  {cab 2757  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cun 3721  cin 3722  wss 3723  c0 4063  {csn 4316  {cpr 4318   cuni 4574   class class class wbr 4786   × cxp 5247  ccnv 5248  ran crn 5250  cres 5251  cima 5252  ccom 5253  Fun wfun 6025   Fn wfn 6026  wf 6027  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  𝑓 cof 7042  1st c1st 7313  2nd c2nd 7314  𝑚 cmap 8009  Xcixp 8062  Fincfn 8109  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  *cxr 10275   < clt 10276  cle 10277  cmin 10468  -cneg 10469   / cdiv 10886  cn 11222  2c2 11272  0cn0 11494  cz 11579  cuz 11888  +crp 12035  (,)cioo 12380  [,]cicc 12383  ...cfz 12533  ..^cfzo 12673  cfl 12799  abscabs 14182  t crest 16289  topGenctg 16306  tcpt 16307  ∞Metcxmt 19946  ballcbl 19948  Topctop 20918   Cn ccn 21249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-rest 16291  df-topgen 16312  df-pt 16313  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-bases 20971
This theorem is referenced by:  poimirlem30  33772
  Copyright terms: Public domain W3C validator