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 33409
Description: Lemma for poimir 33413 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 12754 . . . . . . . . . . . . 13 (1...𝑁) ∈ Fin
3 retop 22546 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
43fconst6 6082 . . . . . . . . . . . . 13 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
5 pttop 21366 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
62, 4, 5mp2an 707 . . . . . . . . . . . 12 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
71, 6eqeltri 2695 . . . . . . . . . . 11 𝑅 ∈ Top
8 poimir.i . . . . . . . . . . . 12 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
9 ovex 6663 . . . . . . . . . . . 12 ((0[,]1) ↑𝑚 (1...𝑁)) ∈ V
108, 9eqeltri 2695 . . . . . . . . . . 11 𝐼 ∈ V
11 elrest 16069 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼)))
127, 10, 11mp2an 707 . . . . . . . . . 10 (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼))
13 eqid 2620 . . . . . . . . . . . . . 14 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
141, 13ptrecube 33380 . . . . . . . . . . . . 13 ((𝑧𝑅𝐶𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧)
1514ex 450 . . . . . . . . . . . 12 (𝑧𝑅 → (𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧))
16 inss1 3825 . . . . . . . . . . . . . . 15 (𝑧𝐼) ⊆ 𝑧
17 sseq1 3618 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → (𝑣𝑧 ↔ (𝑧𝐼) ⊆ 𝑧))
1816, 17mpbiri 248 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → 𝑣𝑧)
1918sseld 3594 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (𝐶𝑣𝐶𝑧))
20 ssrin 3830 . . . . . . . . . . . . . . 15 (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼))
21 sseq2 3619 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼)))
2220, 21syl5ibr 236 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2322reximdv 3013 . . . . . . . . . . . . 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 3023 . . . . . . . . . 10 (∃𝑧𝑅 𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2712, 26sylbi 207 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2827imp 445 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
2928adantl 482 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
30 resttop 20945 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Top)
317, 10, 30mp2an 707 . . . . . . . . . 10 (𝑅t 𝐼) ∈ Top
32 reex 10012 . . . . . . . . . . . . . 14 ℝ ∈ V
33 unitssre 12304 . . . . . . . . . . . . . 14 (0[,]1) ⊆ ℝ
34 mapss 7885 . . . . . . . . . . . . . 14 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
3532, 33, 34mp2an 707 . . . . . . . . . . . . 13 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
368, 35eqsstri 3627 . . . . . . . . . . . 12 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
37 ovex 6663 . . . . . . . . . . . . . 14 (1...𝑁) ∈ V
38 uniretop 22547 . . . . . . . . . . . . . . 15 ℝ = (topGen‘ran (,))
391, 38ptuniconst 21382 . . . . . . . . . . . . . 14 (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
4037, 3, 39mp2an 707 . . . . . . . . . . . . 13 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
4140restuni 20947 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
427, 36, 41mp2an 707 . . . . . . . . . . 11 𝐼 = (𝑅t 𝐼)
4342eltopss 20693 . . . . . . . . . 10 (((𝑅t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅t 𝐼)) → 𝑣𝐼)
4431, 43mpan 705 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → 𝑣𝐼)
4544sselda 3595 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → 𝐶𝐼)
46 2rp 11822 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
47 rpdivcl 11841 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ+𝑐 ∈ ℝ+) → (2 / 𝑐) ∈ ℝ+)
4846, 47mpan 705 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ+)
4948rpred 11857 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ)
50 ceicl 12625 . . . . . . . . . . . . . . 15 ((2 / 𝑐) ∈ ℝ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
5149, 50syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
52 0red 10026 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 ∈ ℝ)
5351zred 11467 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ)
5448rpgt0d 11860 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 < (2 / 𝑐))
55 ceige 12627 . . . . . . . . . . . . . . . 16 ((2 / 𝑐) ∈ ℝ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5649, 55syl 17 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5752, 49, 53, 54, 56ltletrd 10182 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → 0 < -(⌊‘-(2 / 𝑐)))
58 elnnz 11372 . . . . . . . . . . . . . 14 (-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2 / 𝑐)) ∈ ℤ ∧ 0 < -(⌊‘-(2 / 𝑐))))
5951, 57, 58sylanbrc 697 . . . . . . . . . . . . 13 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
60 fveq2 6178 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (ℤ𝑖) = (ℤ‘-(⌊‘-(2 / 𝑐))))
61 oveq2 6643 . . . . . . . . . . . . . . . . . 18 (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 / 𝑐))))
6261oveq2d 6651 . . . . . . . . . . . . . . . . 17 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))
6362eleq2d 2685 . . . . . . . . . . . . . . . 16 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6463ralbidv 2983 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6560, 64rexeqbidv 3148 . . . . . . . . . . . . . 14 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6665rspcv 3300 . . . . . . . . . . . . 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 482 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
69 uznnssnn 11720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7059, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7170sseld 3594 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7271adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7372imdistani 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
7459nnrpd 11855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
7548, 74lerecd 11876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → ((2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)) ↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))))
7656, 75mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))
77 rpcn 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ∈ ℂ)
78 rpne0 11833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ≠ 0)
79 2cn 11076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℂ
80 2ne0 11098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ≠ 0
81 recdiv 10716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8279, 80, 81mpanl12 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8377, 78, 82syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / (2 / 𝑐)) = (𝑐 / 2))
8476, 83breqtrd 4670 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
8584ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
86 elmapi 7864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐶 ∈ ((0[,]1) ↑𝑚 (1...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8786, 8eleq2s 2717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐶𝐼𝐶:(1...𝑁)⟶(0[,]1))
8887ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8988ffvelrnda 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
9033, 89sseldi 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
91 simp-4l 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
92 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
9391, 92jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑𝑘 ∈ ℕ))
94 poimirlem30.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9594ffvelrnda 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
96 xp1st 7183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)))
97 elmapi 7864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9998ffvelrnda 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℕ0)
10099nn0red 11337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
101 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
102100, 101nndivred 11054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10393, 102sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10490, 103resubcld 10443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℝ)
105104recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℂ)
106105abscld 14156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
10759nnrecred 11051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
108107ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
109 rphalfcl 11843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ+)
110109rpred 11857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ)
111110ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ)
112 ltletr 10114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
113106, 108, 111, 112syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11485, 113mpan2d 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11573, 114sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
116 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝐶𝐼) → 𝜑)
11770sselda 3595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ)
118116, 117anim12i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (𝜑𝑘 ∈ ℕ))
119118anassrs 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝜑𝑘 ∈ ℕ))
120 1re 10024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 ∈ ℝ
121 snssi 4330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (1 ∈ ℝ → {1} ⊆ ℝ)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {1} ⊆ ℝ
123 0re 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 0 ∈ ℝ
124 snssi 4330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (0 ∈ ℝ → {0} ⊆ ℝ)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {0} ⊆ ℝ
126122, 125unssi 3780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({1} ∪ {0}) ⊆ ℝ
127 1ex 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ V
128127fconst 6078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1}
129 c0ex 10019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ∈ V
130129fconst 6078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
131128, 130pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
132 xp2nd 7184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (2nd ‘(𝐺𝑘)) ∈ V
135 f1oeq1 6114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑓 = (2nd ‘(𝐺𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
136134, 135elab 3344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(𝐺𝑘))))
139138simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(𝐺𝑘)))
140 imain 5962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (Fun (2nd ‘(𝐺𝑘)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
141137, 139, 1403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
142 elfznn0 12417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
143142nn0red 11337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
144143ltp1d 10939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
145 fzdisj 12353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
146144, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
147146imaeq2d 5454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺𝑘)) “ ∅))
148 ima0 5469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)) “ ∅) = ∅
149147, 148syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
150141, 149sylan9req 2675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
151 fun 6053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
153 imaundi 5533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))
154 nn0p1nn 11317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
156 nnuz 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℕ = (ℤ‘1)
157155, 156syl6eleq 2709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
158 elfzuz3 12324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
159 fzsplit2 12351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
160157, 158, 159syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
161160imaeq2d 5454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
162 f1ofo 6131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁))
163 foima 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
164137, 162, 1633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
165161, 164sylan9req 2675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑁) ∧ (𝜑𝑘 ∈ ℕ)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
166165ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
167153, 166syl5eqr 2668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
168167feq2d 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
171126, 170sseldi 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ)
172 simpllr 798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
173171, 172nndivred 11054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
174173recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
175174absnegd 14169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
176119, 175sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
177119, 170sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
178 elun 3745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
181 nnrp 11827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
182181rpreccld 11867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
183182rpge0d 11861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
184180, 183absidd 14142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ → (abs‘(1 / 𝑘)) = (1 / 𝑘))
185117, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
186117nnrecred 11051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ)
187107adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
188110adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ)
189 eluzle 11685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
190189adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
19159adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
192191nnrpd 11855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
193117nnrpd 11855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+)
194192, 193lerecd 11876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))))
195190, 194mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))
19684adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
197186, 187, 188, 195, 196letrd 10179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2))
198185, 197eqbrtrd 4666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))
199 elsni 4185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1)
200199oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) = (1 / 𝑘))
201200fveq2d 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘)))
202201breq1d 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)))
203198, 202syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
204109rpge0d 11861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ ℝ+ → 0 ≤ (𝑐 / 2))
205 nncn 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
206 nnne0 11038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
207205, 206div0d 10785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
208207abs00bd 14012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (abs‘(0 / 𝑘)) = 0)
209208breq1d 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → ((abs‘(0 / 𝑘)) ≤ (𝑐 / 2) ↔ 0 ≤ (𝑐 / 2)))
210209biimparc 504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((0 ≤ (𝑐 / 2) ∧ 𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
211204, 210sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
212117, 211syldan 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
213 elsni 4185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0)
214213oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) = (0 / 𝑘))
215214fveq2d 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘)))
216215breq1d 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)))
217212, 216syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
218203, 217jaod 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
219218adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
220219ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
221179, 220mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
222176, 221eqbrtrd 4666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
22373, 106sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
224 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑)
225224anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑𝑘 ∈ ℕ))
226173renegcld 10442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
227225, 226sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
228227recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
229228abscld 14156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
23073, 229sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
231110, 110jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
232231ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
233 ltleadd 10496 . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
234223, 230, 232, 233syl21anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
235222, 234mpan2d 709 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
236105, 228abstrid 14176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
237104, 227readdcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
238237recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ)
239238abscld 14156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
240106, 229readdcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
241110, 110readdcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
242241ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
243 lelttr 10113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
244239, 240, 242, 243syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
245236, 244mpand 710 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
24673, 245sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . 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))))
247115, 235, 2463syld 60 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
248100adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
249248, 171readdcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ)
250249, 172nndivred 11054 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
251119, 250sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
252247, 251jctild 565 . . . . . . . . . . . . . . . . . . . . . . 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)))))
253252adantld 483 . . . . . . . . . . . . . . . . . . . . . 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)))))
25473adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
25587ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1))
256255ffvelrnda 6345 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
25733, 256sseldi 3593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
25874rpreccld 11867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ+)
259258rpxrd 11858 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
260259ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
26113rexmet 22575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
262 elbl 22174 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
263261, 262mp3an1 1409 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
264257, 260, 263syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
265 elmapfn 7865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
26695, 96, 2653syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
267 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑘 ∈ V
268 fnconstg 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
269267, 268mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
270 fzfid 12755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
271 inidm 3814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
272 eqidd 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
273267fvconst2 6454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
274273adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
275266, 269, 270, 270, 271, 272, 274ofval 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))
276275oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
277224, 276sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
278224, 102sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
27913remetdval 22573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐶𝑚) ∈ ℝ ∧ (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
280257, 278, 279syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
281277, 280eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
282281breq1d 4654 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))
283282anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
284264, 283bitrd 268 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
285254, 284sylan 488 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
286 rpxr 11825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
287286ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*)
288 elbl 22174 . . . . . . . . . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
289261, 288mp3an1 1409 . . . . . . . . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
29090, 287, 289syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘}))‘𝑚)) < 𝑐)))
291 elun 3745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ ({1} ∪ {0}) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ {0}))
292 fzofzp1 12549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘))
293 elsni 4185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {1} → 𝑧 = 1)
294293oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1))
295294eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘)))
296292, 295syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘)))
297 elfzonn0 12496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0)
298297nn0cnd 11338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ)
299298addid1d 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣)
300 elfzofz 12469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘))
301299, 300eqeltrd 2699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘))
302 elsni 4185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {0} → 𝑧 = 0)
303302oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0))
304303eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘)))
305301, 304syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘)))
306296, 305jaod 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
307291, 306syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
308307imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘))
309308adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘))
310 dffn3 6041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
311266, 310sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
312 poimirlem30.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
313311, 312fssd 6044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
314313adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
315 fzfid 12755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
316309, 314, 169, 315, 315, 271off 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
317 ffn 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁))
318316, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁))
319267, 268mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
320266adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
321 ffn 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
322169, 321syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
323 eqidd 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
324 eqidd 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))
325320, 322, 315, 315, 271, 323, 324ofval 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)))
326273adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
327318, 319, 315, 315, 271, 325, 326ofval 6891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
328327eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
329225, 328sylanl1 681 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
330327adantl3r 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
331330oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))
33287ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
333332ffvelrnda 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
33433, 333sseldi 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
335250adantl3r 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
33613remetdval 22573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐶𝑚) ∈ ℝ ∧ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
337334, 335, 336syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
338248recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℂ)
339171recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ)
340205ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
341206ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0)
342338, 339, 340, 341divdird 10824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
343102recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
344343adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
345344, 174subnegd 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
346342, 345eqtr4d 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
347346oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
348347adantl3r 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
349334recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℂ)
350102adantllr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
351350adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
352351recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
353174adantl3r 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
354353negcld 10364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
355349, 352, 354subsubd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
356348, 355eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
357356fveq2d 6182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
358331, 337, 3573eqtrd 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
359358adantl3r 785 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
360772halvesd 11263 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) = 𝑐)
361360eqcomd 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
362361ad4antlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
363359, 362breq12d 4657 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐 ↔ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
364329, 363anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 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)))))
365290, 364bitrd 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)))))
36673, 365sylanl1 681 . . . . . . . . . . . . . . . . . . . . . 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)))))
367253, 285, 3663imtr4d 283 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
368367ralimdva 2959 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
369 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
370 elfznn0 12417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0)
371370nn0red 11337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ)
372 nndivre 11041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
373371, 372sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
374 elfzle1 12329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣)
375371, 374jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣))
376181rpregt0d 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
377 divge0 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑣 ∈ ℝ ∧ 0 ≤ 𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑣 / 𝑘))
378375, 376, 377syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘))
379 elfzle2 12330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣𝑘)
380379adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣𝑘)
381371adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ)
382 1red 10040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
383181adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
384381, 382, 383ledivmuld 11910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1)))
385205mulid1d 10042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
386385breq2d 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
387386adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
388384, 387bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣𝑘))
389380, 388mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1)
390123, 120elicc2i 12224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1))
391373, 378, 389, 390syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1))
392391ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1))
393 elsni 4185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {𝑘} → 𝑧 = 𝑘)
394393oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘))
395394eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1)))
396392, 395syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1)))
397396impr 648 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
398369, 397sylan 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
399267fconst 6078 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
400399a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
401398, 316, 400, 315, 315, 271off 6897 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
402 ffn 6032 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
403401, 402syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
404119, 403sylan 488 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
405368, 404jctild 565 . . . . . . . . . . . . . . . . . . 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 ∘ − ) ↾ (ℝ × ℝ)))𝑐))))
4068eleq2i 2691 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
407 ovex 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) ∈ V
408407, 37elmap 7871 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
409406, 408bitri 264 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
410401, 409sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
411119, 410sylan 488 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
412405, 411jctird 566 . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘})) ∈ 𝐼)))
413 elin 3788 . . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘})) ∈ 𝐼))
414 ovex 6663 . . . . . . . . . . . . . . . . . . . . 21 (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
415414elixp 7900 . . . . . . . . . . . . . . . . . . . 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 ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
416415anbi1i 730 . . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘})) ∈ 𝐼))
417413, 416bitri 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...𝑁) × {𝑘})) ∈ 𝐼))
418412, 417syl6ibr 242 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼)))
419 ssel 3589 . . . . . . . . . . . . . . . . . 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...𝑁) × {𝑘})) ∈ 𝑣))
420419com12 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...𝑁) × {𝑘})) ∈ 𝑣))
421418, 420syl6 35 . . . . . . . . . . . . . . . 16 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
422421impd 447 . . . . . . . . . . . . . . 15 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
423422ralrimdva 2966 . . . . . . . . . . . . . 14 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
424423expd 452 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
425 poimirlem30.4 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
4264253exp2 1283 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋))))
427426imp43 620 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
428 r19.29 3068 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋))
429 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))))
430429fveq1d 6180 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
431 poimirlem30.x . . . . . . . . . . . . . . . . . . . . . . . 24 𝑋 = ((𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)
432430, 431syl6eqr 2672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = 𝑋)
433432breq2d 4656 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → (0𝑟((𝐹𝑧)‘𝑛) ↔ 0𝑟𝑋))
434433rspcev 3304 . . . . . . . . . . . . . . . . . . . . 21 (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
435434rexlimivw 3025 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
436428, 435syl 17 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
437436expcom 451 . . . . . . . . . . . . . . . . . 18 (∃𝑗 ∈ (0...𝑁)0𝑟𝑋 → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
438427, 437syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
439438ralrimdvva 2971 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
440117, 439sylan2 491 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
441440anassrs 679 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
442441adantllr 754 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
443424, 442syl6d 75 . . . . . . . . . . . 12 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
444443rexlimdva 3027 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
44568, 444syld 47 . . . . . . . . . 10 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
446445com23 86 . . . . . . . . 9 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
447446impr 648 . . . . . . . 8 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44845, 447sylanl2 682 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44929, 448rexlimddv 3031 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
450449expr 642 . . . . 5 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (𝐶𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
451450com23 86 . . . 4 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
452 r19.21v 2957 . . . 4 (∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
453451, 452syl6ibr 242 . . 3 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
454453ralrimdva 2966 . 2 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
455 ralcom 3093 . 2 (∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
456454, 455syl6ib 241 1 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1481  wcel 1988  {cab 2606  wne 2791  wral 2909  wrex 2910  Vcvv 3195  cun 3565  cin 3566  wss 3567  c0 3907  {csn 4168  {cpr 4170   cuni 4427   class class class wbr 4644   × cxp 5102  ccnv 5103  ran crn 5105  cres 5106  cima 5107  ccom 5108  Fun wfun 5870   Fn wfn 5871  wf 5872  ontowfo 5874  1-1-ontowf1o 5875  cfv 5876  (class class class)co 6635  𝑓 cof 6880  1st c1st 7151  2nd c2nd 7152  𝑚 cmap 7842  Xcixp 7893  Fincfn 7940  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  *cxr 10058   < clt 10059  cle 10060  cmin 10251  -cneg 10252   / cdiv 10669  cn 11005  2c2 11055  0cn0 11277  cz 11362  cuz 11672  +crp 11817  (,)cioo 12160  [,]cicc 12163  ...cfz 12311  ..^cfzo 12449  cfl 12574  abscabs 13955  t crest 16062  topGenctg 16079  tcpt 16080  ∞Metcxmt 19712  ballcbl 19714  Topctop 20679   Cn ccn 21009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-map 7844  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fi 8302  df-sup 8333  df-inf 8334  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-rest 16064  df-topgen 16085  df-pt 16086  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-top 20680  df-topon 20697  df-bases 20731
This theorem is referenced by:  poimirlem30  33410
  Copyright terms: Public domain W3C validator