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 32404
Description: Lemma for poimir 32408 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 12588 . . . . . . . . . . . . 13 (1...𝑁) ∈ Fin
3 retop 22307 . . . . . . . . . . . . . 14 (topGen‘ran (,)) ∈ Top
43fconst6 5993 . . . . . . . . . . . . 13 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
5 pttop 21137 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
62, 4, 5mp2an 703 . . . . . . . . . . . 12 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
71, 6eqeltri 2683 . . . . . . . . . . 11 𝑅 ∈ Top
8 poimir.i . . . . . . . . . . . 12 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
9 ovex 6555 . . . . . . . . . . . 12 ((0[,]1) ↑𝑚 (1...𝑁)) ∈ V
108, 9eqeltri 2683 . . . . . . . . . . 11 𝐼 ∈ V
11 elrest 15857 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼)))
127, 10, 11mp2an 703 . . . . . . . . . 10 (𝑣 ∈ (𝑅t 𝐼) ↔ ∃𝑧𝑅 𝑣 = (𝑧𝐼))
13 eqid 2609 . . . . . . . . . . . . . 14 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
141, 13ptrecube 32375 . . . . . . . . . . . . 13 ((𝑧𝑅𝐶𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧)
1514ex 448 . . . . . . . . . . . 12 (𝑧𝑅 → (𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧))
16 inss1 3794 . . . . . . . . . . . . . . 15 (𝑧𝐼) ⊆ 𝑧
17 sseq1 3588 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → (𝑣𝑧 ↔ (𝑧𝐼) ⊆ 𝑧))
1816, 17mpbiri 246 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → 𝑣𝑧)
1918sseld 3566 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (𝐶𝑣𝐶𝑧))
20 ssrin 3799 . . . . . . . . . . . . . . 15 (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼))
21 sseq2 3589 . . . . . . . . . . . . . . 15 (𝑣 = (𝑧𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧𝐼)))
2220, 21syl5ibr 234 . . . . . . . . . . . . . 14 (𝑣 = (𝑧𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2322reximdv 2998 . . . . . . . . . . . . 13 (𝑣 = (𝑧𝐼) → (∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2419, 23imim12d 78 . . . . . . . . . . . 12 (𝑣 = (𝑧𝐼) → ((𝐶𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ⊆ 𝑧) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)))
2515, 24syl5com 31 . . . . . . . . . . 11 (𝑧𝑅 → (𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)))
2625rexlimiv 3008 . . . . . . . . . 10 (∃𝑧𝑅 𝑣 = (𝑧𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2712, 26sylbi 205 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → (𝐶𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))
2827imp 443 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
2928adantl 480 . . . . . . 7 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)
30 resttop 20716 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅t 𝐼) ∈ Top)
317, 10, 30mp2an 703 . . . . . . . . . 10 (𝑅t 𝐼) ∈ Top
32 reex 9883 . . . . . . . . . . . . . 14 ℝ ∈ V
33 unitssre 12146 . . . . . . . . . . . . . 14 (0[,]1) ⊆ ℝ
34 mapss 7763 . . . . . . . . . . . . . 14 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
3532, 33, 34mp2an 703 . . . . . . . . . . . . 13 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
368, 35eqsstri 3597 . . . . . . . . . . . 12 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
37 ovex 6555 . . . . . . . . . . . . . 14 (1...𝑁) ∈ V
38 uniretop 22308 . . . . . . . . . . . . . . 15 ℝ = (topGen‘ran (,))
391, 38ptuniconst 21153 . . . . . . . . . . . . . 14 (((1...𝑁) ∈ V ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
4037, 3, 39mp2an 703 . . . . . . . . . . . . 13 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
4140restuni 20718 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
427, 36, 41mp2an 703 . . . . . . . . . . 11 𝐼 = (𝑅t 𝐼)
4342eltopss 20479 . . . . . . . . . 10 (((𝑅t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅t 𝐼)) → 𝑣𝐼)
4431, 43mpan 701 . . . . . . . . 9 (𝑣 ∈ (𝑅t 𝐼) → 𝑣𝐼)
4544sselda 3567 . . . . . . . 8 ((𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣) → 𝐶𝐼)
46 2rp 11669 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
47 rpdivcl 11688 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℝ+𝑐 ∈ ℝ+) → (2 / 𝑐) ∈ ℝ+)
4846, 47mpan 701 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ+)
4948rpred 11704 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ∈ ℝ)
50 ceicl 12459 . . . . . . . . . . . . . . 15 ((2 / 𝑐) ∈ ℝ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
5149, 50syl 17 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℤ)
52 0red 9897 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 ∈ ℝ)
5351zred 11314 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ)
5448rpgt0d 11707 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → 0 < (2 / 𝑐))
55 ceige 12461 . . . . . . . . . . . . . . . 16 ((2 / 𝑐) ∈ ℝ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5649, 55syl 17 . . . . . . . . . . . . . . 15 (𝑐 ∈ ℝ+ → (2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)))
5752, 49, 53, 54, 56ltletrd 10048 . . . . . . . . . . . . . 14 (𝑐 ∈ ℝ+ → 0 < -(⌊‘-(2 / 𝑐)))
58 elnnz 11220 . . . . . . . . . . . . . 14 (-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2 / 𝑐)) ∈ ℤ ∧ 0 < -(⌊‘-(2 / 𝑐))))
5951, 57, 58sylanbrc 694 . . . . . . . . . . . . 13 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
60 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (ℤ𝑖) = (ℤ‘-(⌊‘-(2 / 𝑐))))
61 oveq2 6535 . . . . . . . . . . . . . . . . . 18 (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 / 𝑐))))
6261oveq2d 6543 . . . . . . . . . . . . . . . . 17 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) = ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))
6362eleq2d 2672 . . . . . . . . . . . . . . . 16 (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6463ralbidv 2968 . . . . . . . . . . . . . . 15 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6560, 64rexeqbidv 3129 . . . . . . . . . . . . . 14 (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
6665rspcv 3277 . . . . . . . . . . . . 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 480 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))))
69 uznnssnn 11567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (-(⌊‘-(2 / 𝑐)) ∈ ℕ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7059, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (ℤ‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ)
7170sseld 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7271adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ))
7372imdistani 721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
7459nnrpd 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 ∈ ℝ+ → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
7548, 74lerecd 11723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → ((2 / 𝑐) ≤ -(⌊‘-(2 / 𝑐)) ↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))))
7656, 75mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))
77 rpcn 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ∈ ℂ)
78 rpne0 11680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+𝑐 ≠ 0)
79 2cn 10938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℂ
80 2ne0 10960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ≠ 0
81 recdiv 10580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8279, 80, 81mpanl12 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2))
8377, 78, 82syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / (2 / 𝑐)) = (𝑐 / 2))
8476, 83breqtrd 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
8584ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
86 elmapi 7742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐶 ∈ ((0[,]1) ↑𝑚 (1...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8786, 8eleq2s 2705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐶𝐼𝐶:(1...𝑁)⟶(0[,]1))
8887ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
8988ffvelrnda 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
9033, 89sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
91 simp-4l 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
92 simplr 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
9391, 92jca 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑𝑘 ∈ ℕ))
94 poimirlem30.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9594ffvelrnda 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
96 xp1st 7066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)))
97 elmapi 7742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9895, 96, 973syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ℕ0)
9998ffvelrnda 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℕ0)
10099nn0red 11199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
101 simplr 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
102100, 101nndivred 10916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10393, 102sylan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
10490, 103resubcld 10309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℝ)
105104recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) ∈ ℂ)
106105abscld 13969 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
10759nnrecred 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
108107ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
109 rphalfcl 11690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ+)
110109rpred 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → (𝑐 / 2) ∈ ℝ)
111110ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ)
112 ltletr 9980 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
113106, 108, 111, 112syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11485, 113mpan2d 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
11573, 114sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2)))
116 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝐶𝐼) → 𝜑)
11770sselda 3567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ)
118116, 117anim12i 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (𝜑𝑘 ∈ ℕ))
119118anassrs 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝜑𝑘 ∈ ℕ))
120 1re 9895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 ∈ ℝ
121 snssi 4279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (1 ∈ ℝ → {1} ⊆ ℝ)
122120, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {1} ⊆ ℝ
123 0re 9896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 0 ∈ ℝ
124 snssi 4279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (0 ∈ ℝ → {0} ⊆ ℝ)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {0} ⊆ ℝ
126122, 125unssi 3749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({1} ∪ {0}) ⊆ ℝ
127 1ex 9891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1 ∈ V
128127fconst 5989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1}
129 c0ex 9890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 0 ∈ V
130129fconst 5989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
131128, 130pm3.2i 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
132 xp2nd 7067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (2nd ‘(𝐺𝑘)) ∈ V
135 f1oeq1 6025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑓 = (2nd ‘(𝐺𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
136134, 135elab 3318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
137133, 136sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
138 dff1o3 6041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(𝐺𝑘))))
139138simprbi 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(𝐺𝑘)))
140 imain 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (Fun (2nd ‘(𝐺𝑘)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
141137, 139, 1403syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
142 elfznn0 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
143142nn0red 11199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
144143ltp1d 10803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
145 fzdisj 12194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
146144, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
147146imaeq2d 5372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺𝑘)) “ ∅))
148 ima0 5387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2nd ‘(𝐺𝑘)) “ ∅) = ∅
149147, 148syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
150141, 149sylan9req 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
151 fun 5965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
153 imaundi 5450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))
154 nn0p1nn 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
155142, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
156 nnuz 11555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℕ = (ℤ‘1)
157155, 156syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
158 elfzuz3 12165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
159 fzsplit2 12192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
160157, 158, 159syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
161160imaeq2d 5372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
162 f1ofo 6042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁))
163 foima 6018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
164137, 162, 1633syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
165161, 164sylan9req 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ (0...𝑁) ∧ (𝜑𝑘 ∈ ℕ)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
166165ancoms 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
167153, 166syl5eqr 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
168167feq2d 5930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
170169ffvelrnda 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
171126, 170sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ)
172 simpllr 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ)
173171, 172nndivred 10916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
174173recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
175174absnegd 13982 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
176119, 175sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
177119, 170sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}))
178 elun 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}))
180 nnrecre 10904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
181 nnrp 11674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
182181rpreccld 11714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
183182rpge0d 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
184180, 183absidd 13955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ℕ → (abs‘(1 / 𝑘)) = (1 / 𝑘))
185117, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘))
186117nnrecred 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ)
187107adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ)
188110adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ)
189 eluzle 11532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
190189adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘)
19159adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℕ)
192191nnrpd 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈ ℝ+)
193117nnrpd 11702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+)
194192, 193lerecd 11723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))))
195190, 194mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))
19684adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2))
197186, 187, 188, 195, 196letrd 10045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2))
198185, 197eqbrtrd 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))
199 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1)
200199oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) = (1 / 𝑘))
201200fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘)))
202201breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)))
203198, 202syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
204109rpge0d 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 ∈ ℝ+ → 0 ≤ (𝑐 / 2))
205 nncn 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
206 nnne0 10900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
207205, 206div0d 10649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
208207abs00bd 13825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑘 ∈ ℕ → (abs‘(0 / 𝑘)) = 0)
209208breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑘 ∈ ℕ → ((abs‘(0 / 𝑘)) ≤ (𝑐 / 2) ↔ 0 ≤ (𝑐 / 2)))
210209biimparc 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((0 ≤ (𝑐 / 2) ∧ 𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
211204, 210sylan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑐 ∈ ℝ+𝑘 ∈ ℕ) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
212117, 211syldan 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))
213 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0)
214213oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) = (0 / 𝑘))
215214fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘)))
216215breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)))
217212, 216syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (abs‘((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)))
218203, 217jaod 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4599 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))
22373, 106sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) ∈ ℝ)
224 simpll 785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑)
225224anim1i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑𝑘 ∈ ℕ))
226173renegcld 10308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
227225, 226sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ)
228227recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
229228abscld 13969 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
23073, 229sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
231110, 110jca 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
232231ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ))
233 ltleadd 10360 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1316 . . . . . . . . . . . . . . . . . . . . . . . . . 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 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
236105, 228abstrid 13989 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
237104, 227readdcld 9925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ)
238237recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ)
239238abscld 13969 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
240106, 229readdcld 9925 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ)
241110, 110readdcld 9925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
242241ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ)
243 lelttr 9979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . . . . . . 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 679 . . . . . . . . . . . . . . . . . . . . . . . . 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 57 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
248100adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℝ)
249248, 171readdcld 9925 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ)
250249, 172nndivred 10916 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
251119, 250sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
252247, 251jctild 563 . . . . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ))
25587ad3antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1))
256255ffvelrnda 6252 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
25733, 256sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
25874rpreccld 11714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ+)
259258rpxrd 11705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+ → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
260259ad3antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*)
26113rexmet 22334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
262 elbl 21944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
263261, 262mp3an1 1402 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐶𝑚) ∈ ℝ ∧ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ*) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
264257, 260, 263syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))))))
265 elmapfn 7743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
26695, 96, 2653syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
267 vex 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑘 ∈ V
268 fnconstg 5991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
269267, 268mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
270 fzfid 12589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin)
271 inidm 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
272 eqidd 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
273267fvconst2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
274273adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
275266, 269, 270, 270, 271, 272, 274ofval 6781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))
276275oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
277224, 276sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)))
278224, 102sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
27913remetdval 22332 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐶𝑚) ∈ ℝ ∧ (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
280257, 278, 279syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
281277, 280eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))))
282281breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))
283282anbi2d 735 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
284264, 283bitrd 266 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
285254, 284sylan 486 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))))
286 rpxr 11672 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 ∈ ℝ+𝑐 ∈ ℝ*)
287286ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*)
288 elbl 21944 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1402 . . . . . . . . . . . . . . . . . . . . . . . . 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 690 . . . . . . . . . . . . . . . . . . . . . . . 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 3714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ ({1} ∪ {0}) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ {0}))
292 fzofzp1 12386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘))
293 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {1} → 𝑧 = 1)
294293oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1))
295294eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘)))
296292, 295syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘)))
297 elfzonn0 12335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0)
298297nn0cnd 11200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ)
299298addid1d 10087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣)
300 elfzofz 12309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘))
301299, 300eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘))
302 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ {0} → 𝑧 = 0)
303302oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0))
304303eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘)))
305301, 304syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘)))
306296, 305jaod 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
307291, 306syl5bi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘)))
308307imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘))
309308adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘))
310 dffn3 5953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
311266, 310sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺𝑘)))
312 poimirlem30.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
313311, 312fssd 5956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
314313adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
315 fzfid 12589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
316309, 314, 169, 315, 315, 271off 6787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
317 ffn 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
321 ffn 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) = ((1st ‘(𝐺𝑘))‘𝑚))
324 eqidd 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))
325320, 322, 315, 315, 271, 323, 324ofval 6781 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑚) = (((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)))
326273adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘)
327318, 319, 315, 315, 271, 325, 326ofval 6781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
328327eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
329225, 328sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ))
330327adantl3r 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))
331330oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))
33287ad3antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1))
333332ffvelrnda 6252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ (0[,]1))
33433, 333sseldi 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℝ)
335250adantl3r 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)
33613remetdval 22332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))))
338248recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺𝑘))‘𝑚) ∈ ℂ)
339171recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ)
340205ad3antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
341206ad3antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0)
342338, 339, 340, 341divdird 10688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
343102recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
344343adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
345344, 174subnegd 10250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
346342, 345eqtr4d 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
347346oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
348347adantl3r 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
349334recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶𝑚) ∈ ℂ)
350102adantllr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
351350adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℝ)
352351recnd 9924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) ∈ ℂ)
353174adantl3r 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
354353negcld 10230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ)
355349, 352, 354subsubd 10271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
356348, 355eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))
357356fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶𝑚) − ((((1st ‘(𝐺𝑘))‘𝑚) + (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
358331, 337, 3573eqtrd 2647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝐶𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
359358adantl3r 781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))))
360772halvesd 11125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 ∈ ℝ+ → ((𝑐 / 2) + (𝑐 / 2)) = 𝑐)
361360eqcomd 2615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐 ∈ ℝ+𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
362361ad4antlr 764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2)))
363359, 362breq12d 4590 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶𝑚)((abs ∘ − ) ↾ (ℝ × ℝ))((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐 ↔ (abs‘(((𝐶𝑚) − (((1st ‘(𝐺𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))
364329, 363anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . . 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 266 . . . . . . . . . . . . . . . . . . . . . . 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 679 . . . . . . . . . . . . . . . . . . . . . 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 281 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
368367ralimdva 2944 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐)))
369 simplr 787 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
370 elfznn0 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0)
371370nn0red 11199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ)
372 nndivre 10903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
373371, 372sylan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ)
374 elfzle1 12170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣)
375371, 374jca 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣))
376181rpregt0d 11710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
377 divge0 10741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑣 ∈ ℝ ∧ 0 ≤ 𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑣 / 𝑘))
378375, 376, 377syl2an 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘))
379 elfzle2 12171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ (0...𝑘) → 𝑣𝑘)
380379adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣𝑘)
381371adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ)
382 1red 9911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
383181adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
384381, 382, 383ledivmuld 11757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1)))
385205mulid1d 9913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
386385breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
387386adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣𝑘))
388384, 387bitrd 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣𝑘))
389380, 388mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1)
390123, 120elicc2i 12066 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1))
391373, 378, 389, 390syl3anbrc 1238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1))
392391ancoms 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1))
393 elsni 4141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {𝑘} → 𝑧 = 𝑘)
394393oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘))
395394eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1)))
396392, 395syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1)))
397396impr 646 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
398369, 397sylan 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1))
399267fconst 5989 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
400399a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
401398, 316, 400, 315, 315, 271off 6787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
402 ffn 5944 . . . . . . . . . . . . . . . . . . . . . 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 486 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁))
405368, 404jctild 563 . . . . . . . . . . . . . . . . . . 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 2679 . . . . . . . . . . . . . . . . . . . . . 22 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
407 ovex 6555 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) ∈ V
408407, 37elmap 7749 . . . . . . . . . . . . . . . . . . . . . 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 262 . . . . . . . . . . . . . . . . . . . . 21 ((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
410401, 409sylibr 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
411119, 410sylan 486 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
412405, 411jctird 564 . . . . . . . . . . . . . . . . . 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 3757 . . . . . . . . . . . . . . . . . . 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 6555 . . . . . . . . . . . . . . . . . . . . 21 (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V
415414elixp 7778 . . . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . . 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 262 . . . . . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . . . . . 17 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼)))
419 ssel 3561 . . . . . . . . . . . . . . . . . 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 34 . . . . . . . . . . . . . . . 16 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)))
422421impd 445 . . . . . . . . . . . . . . 15 (((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
423422ralrimdva 2951 . . . . . . . . . . . . . 14 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))
424423expd 450 . . . . . . . . . . . . 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 1276 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋))))
427426imp43 618 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)
428 r19.29 3053 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋))
429 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))))
430429fveq1d 6090 . . . . . . . . . . . . . . . . . . . . . . . 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 2661 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = 𝑋)
433432breq2d 4589 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) → (0𝑟((𝐹𝑧)‘𝑛) ↔ 0𝑟𝑋))
434433rspcev 3281 . . . . . . . . . . . . . . . . . . . . 21 (((((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))
435434rexlimivw 3010 . . . . . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . . . . 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 2956 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
440117, 439sylan2 489 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐 ∈ ℝ+𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐))))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
441440anassrs 677 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
442441adantllr 750 . . . . . . . . . . . . 13 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
443424, 442syl6d 72 . . . . . . . . . . . 12 ((((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
444443rexlimdva 3012 . . . . . . . . . . 11 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∃𝑘 ∈ (ℤ‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
44568, 444syld 45 . . . . . . . . . 10 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
446445com23 83 . . . . . . . . 9 (((𝜑𝐶𝐼) ∧ 𝑐 ∈ ℝ+) → ((X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
447446impr 646 . . . . . . . 8 (((𝜑𝐶𝐼) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44845, 447sylanl2 680 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈ (1...𝑁)((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
44929, 448rexlimddv 3016 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ (𝑅t 𝐼) ∧ 𝐶𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
450449expr 640 . . . . 5 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (𝐶𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
451450com23 83 . . . 4 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
452 r19.21v 2942 . . . 4 (∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ (𝐶𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
453451, 452syl6ibr 240 . . 3 ((𝜑𝑣 ∈ (𝑅t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
454453ralrimdva 2951 . 2 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
455 ralcom 3078 . 2 (∀𝑣 ∈ (𝑅t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
456454, 455syl6ib 239 1 (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶𝑚)(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝐶𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  {cab 2595  wne 2779  wral 2895  wrex 2896  Vcvv 3172  cun 3537  cin 3538  wss 3539  c0 3873  {csn 4124  {cpr 4126   cuni 4366   class class class wbr 4577   × cxp 5026  ccnv 5027  ran crn 5029  cres 5030  cima 5031  ccom 5032  Fun wfun 5784   Fn wfn 5785  wf 5786  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  𝑓 cof 6770  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  Xcixp 7771  Fincfn 7818  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  *cxr 9929   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10533  cn 10867  2c2 10917  0cn0 11139  cz 11210  cuz 11519  +crp 11664  (,)cioo 12002  [,]cicc 12005  ...cfz 12152  ..^cfzo 12289  cfl 12408  abscabs 13768  t crest 15850  topGenctg 15867  tcpt 15868  ∞Metcxmt 19498  ballcbl 19500  Topctop 20459   Cn ccn 20780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fi 8177  df-sup 8208  df-inf 8209  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-seq 12619  df-exp 12678  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-rest 15852  df-topgen 15873  df-pt 15874  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-top 20463  df-bases 20464  df-topon 20465
This theorem is referenced by:  poimirlem30  32405
  Copyright terms: Public domain W3C validator