poimirlem29

Description: Lemma for poimir connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	poimir.i	⊢ 𝐼 = ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) )
	poimir.r	⊢ 𝑅 = ( ∏_t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
	poimir.1	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾_t 𝐼 ) Cn 𝑅 ) )
	poimirlem30.x	⊢ 𝑋 = ( ( 𝐹 ‘ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 )
	poimirlem30.2	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
	poimirlem30.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) )
	poimirlem30.4	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ^◡ ≤ } ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 )
Assertion	poimirlem29	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		poimir.0	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		poimir.i	⊢ 𝐼 = ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) )
3		poimir.r	⊢ 𝑅 = ( ∏_t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
4		poimir.1	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾_t 𝐼 ) Cn 𝑅 ) )
5		poimirlem30.x	⊢ 𝑋 = ( ( 𝐹 ‘ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 )
6		poimirlem30.2	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
7		poimirlem30.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) )
8		poimirlem30.4	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ^◡ ≤ } ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 )
9		fzfi	⊢ ( 1 ... 𝑁 ) ∈ Fin
10		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
11	10	fconst6	⊢ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top
12		pttop	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top ) → ( ∏_t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ∈ Top )
13	9 11 12	mp2an	⊢ ( ∏_t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ∈ Top
14	3 13	eqeltri	⊢ 𝑅 ∈ Top
15		ovex	⊢ ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) ) ∈ V
16	2 15	eqeltri	⊢ 𝐼 ∈ V
17		elrest	⊢ ( ( 𝑅 ∈ Top ∧ 𝐼 ∈ V ) → ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ↔ ∃ 𝑧 ∈ 𝑅 𝑣 = ( 𝑧 ∩ 𝐼 ) ) )
18	14 16 17	mp2an	⊢ ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ↔ ∃ 𝑧 ∈ 𝑅 𝑣 = ( 𝑧 ∩ 𝐼 ) )
19		eqid	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
20	3 19	ptrecube	⊢ ( ( 𝑧 ∈ 𝑅 ∧ 𝐶 ∈ 𝑧 ) → ∃ 𝑐 ∈ ℝ⁺ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ⊆ 𝑧 )
21	20	ex	⊢ ( 𝑧 ∈ 𝑅 → ( 𝐶 ∈ 𝑧 → ∃ 𝑐 ∈ ℝ⁺ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ⊆ 𝑧 ) )
22		inss1	⊢ ( 𝑧 ∩ 𝐼 ) ⊆ 𝑧
23		sseq1	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( 𝑣 ⊆ 𝑧 ↔ ( 𝑧 ∩ 𝐼 ) ⊆ 𝑧 ) )
24	22 23	mpbiri	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → 𝑣 ⊆ 𝑧 )
25	24	sseld	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( 𝐶 ∈ 𝑣 → 𝐶 ∈ 𝑧 ) )
26		ssrin	⊢ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ⊆ 𝑧 → ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ ( 𝑧 ∩ 𝐼 ) )
27		sseq2	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ↔ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ ( 𝑧 ∩ 𝐼 ) ) )
28	26 27	imbitrrid	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ⊆ 𝑧 → ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) )
29	28	reximdv	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( ∃ 𝑐 ∈ ℝ⁺ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ⊆ 𝑧 → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) )
30	25 29	imim12d	⊢ ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( ( 𝐶 ∈ 𝑧 → ∃ 𝑐 ∈ ℝ⁺ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ⊆ 𝑧 ) → ( 𝐶 ∈ 𝑣 → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) ) )
31	21 30	syl5com	⊢ ( 𝑧 ∈ 𝑅 → ( 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( 𝐶 ∈ 𝑣 → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) ) )
32	31	rexlimiv	⊢ ( ∃ 𝑧 ∈ 𝑅 𝑣 = ( 𝑧 ∩ 𝐼 ) → ( 𝐶 ∈ 𝑣 → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) )
33	18 32	sylbi	⊢ ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) → ( 𝐶 ∈ 𝑣 → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) )
34	33	imp	⊢ ( ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∧ 𝐶 ∈ 𝑣 ) → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 )
35	34	adantl	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∧ 𝐶 ∈ 𝑣 ) ) → ∃ 𝑐 ∈ ℝ⁺ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 )
36		resttop	⊢ ( ( 𝑅 ∈ Top ∧ 𝐼 ∈ V ) → ( 𝑅 ↾_t 𝐼 ) ∈ Top )
37	14 16 36	mp2an	⊢ ( 𝑅 ↾_t 𝐼 ) ∈ Top
38		reex	⊢ ℝ ∈ V
39		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
40		mapss	⊢ ( ( ℝ ∈ V ∧ ( 0 [,] 1 ) ⊆ ℝ ) → ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑_m ( 1 ... 𝑁 ) ) )
41	38 39 40	mp2an	⊢ ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑_m ( 1 ... 𝑁 ) )
42	2 41	eqsstri	⊢ 𝐼 ⊆ ( ℝ ↑_m ( 1 ... 𝑁 ) )
43		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
44		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
45	3 44	ptuniconst	⊢ ( ( ( 1 ... 𝑁 ) ∈ V ∧ ( topGen ‘ ran (,) ) ∈ Top ) → ( ℝ ↑_m ( 1 ... 𝑁 ) ) = ∪ 𝑅 )
46	43 10 45	mp2an	⊢ ( ℝ ↑_m ( 1 ... 𝑁 ) ) = ∪ 𝑅
47	46	restuni	⊢ ( ( 𝑅 ∈ Top ∧ 𝐼 ⊆ ( ℝ ↑_m ( 1 ... 𝑁 ) ) ) → 𝐼 = ∪ ( 𝑅 ↾_t 𝐼 ) )
48	14 42 47	mp2an	⊢ 𝐼 = ∪ ( 𝑅 ↾_t 𝐼 )
49	48	eltopss	⊢ ( ( ( 𝑅 ↾_t 𝐼 ) ∈ Top ∧ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ) → 𝑣 ⊆ 𝐼 )
50	37 49	mpan	⊢ ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) → 𝑣 ⊆ 𝐼 )
51	50	sselda	⊢ ( ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∧ 𝐶 ∈ 𝑣 ) → 𝐶 ∈ 𝐼 )
52		2rp	⊢ 2 ∈ ℝ⁺
53		rpdivcl	⊢ ( ( 2 ∈ ℝ⁺ ∧ 𝑐 ∈ ℝ⁺ ) → ( 2 / 𝑐 ) ∈ ℝ⁺ )
54	52 53	mpan	⊢ ( 𝑐 ∈ ℝ⁺ → ( 2 / 𝑐 ) ∈ ℝ⁺ )
55	54	rpred	⊢ ( 𝑐 ∈ ℝ⁺ → ( 2 / 𝑐 ) ∈ ℝ )
56		ceicl	⊢ ( ( 2 / 𝑐 ) ∈ ℝ → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℤ )
57	55 56	syl	⊢ ( 𝑐 ∈ ℝ⁺ → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℤ )
58		0red	⊢ ( 𝑐 ∈ ℝ⁺ → 0 ∈ ℝ )
59	57	zred	⊢ ( 𝑐 ∈ ℝ⁺ → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℝ )
60	54	rpgt0d	⊢ ( 𝑐 ∈ ℝ⁺ → 0 < ( 2 / 𝑐 ) )
61		ceige	⊢ ( ( 2 / 𝑐 ) ∈ ℝ → ( 2 / 𝑐 ) ≤ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) )
62	55 61	syl	⊢ ( 𝑐 ∈ ℝ⁺ → ( 2 / 𝑐 ) ≤ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) )
63	58 55 59 60 62	ltletrd	⊢ ( 𝑐 ∈ ℝ⁺ → 0 < - ( ⌊ ‘ - ( 2 / 𝑐 ) ) )
64		elnnz	⊢ ( - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℕ ↔ ( - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℤ ∧ 0 < - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) )
65	57 63 64	sylanbrc	⊢ ( 𝑐 ∈ ℝ⁺ → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℕ )
66		fveq2	⊢ ( 𝑖 = - ( ⌊ ‘ - ( 2 / 𝑐 ) ) → ( ℤ_≥ ‘ 𝑖 ) = ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) )
67		oveq2	⊢ ( 𝑖 = - ( ⌊ ‘ - ( 2 / 𝑐 ) ) → ( 1 / 𝑖 ) = ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) )
68	67	oveq2d	⊢ ( 𝑖 = - ( ⌊ ‘ - ( 2 / 𝑐 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) = ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) )
69	68	eleq2d	⊢ ( 𝑖 = - ( ⌊ ‘ - ( 2 / 𝑐 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
70	69	ralbidv	⊢ ( 𝑖 = - ( ⌊ ‘ - ( 2 / 𝑐 ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
71	66 70	rexeqbidv	⊢ ( 𝑖 = - ( ⌊ ‘ - ( 2 / 𝑐 ) ) → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) ↔ ∃ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
72	71	rspcv	⊢ ( - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℕ → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
73	65 72	syl	⊢ ( 𝑐 ∈ ℝ⁺ → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
74	73	adantl	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
75		uznnssnn	⊢ ( - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℕ → ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ⊆ ℕ )
76	65 75	syl	⊢ ( 𝑐 ∈ ℝ⁺ → ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ⊆ ℕ )
77	76	sseld	⊢ ( 𝑐 ∈ ℝ⁺ → ( 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → 𝑘 ∈ ℕ ) )
78	77	adantl	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) → ( 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → 𝑘 ∈ ℕ ) )
79	78	imdistani	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) )
80	65	nnrpd	⊢ ( 𝑐 ∈ ℝ⁺ → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℝ⁺ )
81	54 80	lerecd	⊢ ( 𝑐 ∈ ℝ⁺ → ( ( 2 / 𝑐 ) ≤ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ↔ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 1 / ( 2 / 𝑐 ) ) ) )
82	62 81	mpbid	⊢ ( 𝑐 ∈ ℝ⁺ → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 1 / ( 2 / 𝑐 ) ) )
83		rpcn	⊢ ( 𝑐 ∈ ℝ⁺ → 𝑐 ∈ ℂ )
84		rpne0	⊢ ( 𝑐 ∈ ℝ⁺ → 𝑐 ≠ 0 )
85		2cn	⊢ 2 ∈ ℂ
86		2ne0	⊢ 2 ≠ 0
87		recdiv	⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 𝑐 ∈ ℂ ∧ 𝑐 ≠ 0 ) ) → ( 1 / ( 2 / 𝑐 ) ) = ( 𝑐 / 2 ) )
88	85 86 87	mpanl12	⊢ ( ( 𝑐 ∈ ℂ ∧ 𝑐 ≠ 0 ) → ( 1 / ( 2 / 𝑐 ) ) = ( 𝑐 / 2 ) )
89	83 84 88	syl2anc	⊢ ( 𝑐 ∈ ℝ⁺ → ( 1 / ( 2 / 𝑐 ) ) = ( 𝑐 / 2 ) )
90	82 89	breqtrd	⊢ ( 𝑐 ∈ ℝ⁺ → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 𝑐 / 2 ) )
91	90	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 𝑐 / 2 ) )
92		elmapi	⊢ ( 𝐶 ∈ ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) ) → 𝐶 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
93	92 2	eleq2s	⊢ ( 𝐶 ∈ 𝐼 → 𝐶 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
94	93	ad4antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐶 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
95	94	ffvelcdmda	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ( 0 [,] 1 ) )
96	39 95	sselid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ℝ )
97		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
98		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
99	97 98	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝜑 ∧ 𝑘 ∈ ℕ ) )
100	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
101		xp1st	⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) )
102		elmapi	⊢ ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ℕ₀ )
103	100 101 102	3syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ℕ₀ )
104	103	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) ∈ ℕ₀ )
105	104	nn0red	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) ∈ ℝ )
106		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
107	105 106	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
108	99 107	sylan	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
109	96 108	resubcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℝ )
110	109	recnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℂ )
111	110	abscld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ )
112	65	nnrecred	⊢ ( 𝑐 ∈ ℝ⁺ → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ )
113	112	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ )
114		rphalfcl	⊢ ( 𝑐 ∈ ℝ⁺ → ( 𝑐 / 2 ) ∈ ℝ⁺ )
115	114	rpred	⊢ ( 𝑐 ∈ ℝ⁺ → ( 𝑐 / 2 ) ∈ ℝ )
116	115	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝑐 / 2 ) ∈ ℝ )
117		ltletr	⊢ ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ ∧ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ ∧ ( 𝑐 / 2 ) ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∧ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 𝑐 / 2 ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) ) )
118	111 113 116 117	syl3anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∧ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 𝑐 / 2 ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) ) )
119	91 118	mpan2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) ) )
120	79 119	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) ) )
121		simpl	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) → 𝜑 )
122	76	sselda	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → 𝑘 ∈ ℕ )
123	121 122	anim12i	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) → ( 𝜑 ∧ 𝑘 ∈ ℕ ) )
124	123	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 𝜑 ∧ 𝑘 ∈ ℕ ) )
125		1re	⊢ 1 ∈ ℝ
126		snssi	⊢ ( 1 ∈ ℝ → { 1 } ⊆ ℝ )
127	125 126	ax-mp	⊢ { 1 } ⊆ ℝ
128		0re	⊢ 0 ∈ ℝ
129		snssi	⊢ ( 0 ∈ ℝ → { 0 } ⊆ ℝ )
130	128 129	ax-mp	⊢ { 0 } ⊆ ℝ
131	127 130	unssi	⊢ ( { 1 } ∪ { 0 } ) ⊆ ℝ
132		1ex	⊢ 1 ∈ V
133	132	fconst	⊢ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 }
134		c0ex	⊢ 0 ∈ V
135	134	fconst	⊢ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 }
136	133 135	pm3.2i	⊢ ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } )
137		xp2nd	⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
138	100 137	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
139		fvex	⊢ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ V
140		f1oeq1	⊢ ( 𝑓 = ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
141	139 140	elab	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
142	138 141	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
143		dff1o3	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ^◡ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
144	143	simprbi	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ^◡ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) )
145		imain	⊢ ( Fun ^◡ ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
146	142 144 145	3syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
147		elfznn0	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℕ₀ )
148	147	nn0red	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
149	148	ltp1d	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
150		fzdisj	⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
151	149 150	syl	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
152	151	imaeq2d	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ∅ ) )
153		ima0	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ∅ ) = ∅
154	152 153	eqtrdi	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
155	146 154	sylan9req	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
156		fun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } ) ∧ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
157	136 155 156	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
158		imaundi	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
159		nn0p1nn	⊢ ( 𝑗 ∈ ℕ₀ → ( 𝑗 + 1 ) ∈ ℕ )
160	147 159	syl	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ )
161		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
162	160 161	eleqtrdi	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
163		elfzuz3	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ_≥ ‘ 𝑗 ) )
164		fzsplit2	⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
165	162 163 164	syl2anc	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
166	165	imaeq2d	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
167		f1ofo	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
168		foima	⊢ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
169	142 167 168	3syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
170	166 169	sylan9req	⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
171	170	ancoms	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
172	158 171	eqtr3id	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
173	172	feq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) ) )
174	157 173	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
175	174	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ ( { 1 } ∪ { 0 } ) )
176	131 175	sselid	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ ℝ )
177		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
178	176 177	nndivred	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
179	178	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
180	179	absnegd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
181	124 180	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
182	124 175	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ ( { 1 } ∪ { 0 } ) )
183		elun	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ ( { 1 } ∪ { 0 } ) ↔ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } ∨ ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } ) )
184	182 183	sylib	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } ∨ ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } ) )
185		nnrecre	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
186		nnrp	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺ )
187	186	rpreccld	⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ⁺ )
188	187	rpge0d	⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 1 / 𝑘 ) )
189	185 188	absidd	⊢ ( 𝑘 ∈ ℕ → ( abs ‘ ( 1 / 𝑘 ) ) = ( 1 / 𝑘 ) )
190	122 189	syl	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( abs ‘ ( 1 / 𝑘 ) ) = ( 1 / 𝑘 ) )
191	122	nnrecred	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
192	112	adantr	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ )
193	115	adantr	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 𝑐 / 2 ) ∈ ℝ )
194		eluzle	⊢ ( 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ≤ 𝑘 )
195	194	adantl	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ≤ 𝑘 )
196	65	adantr	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℕ )
197	196	nnrpd	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ∈ ℝ⁺ )
198	122	nnrpd	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → 𝑘 ∈ ℝ⁺ )
199	197 198	lerecd	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ≤ 𝑘 ↔ ( 1 / 𝑘 ) ≤ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) )
200	195 199	mpbid	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 1 / 𝑘 ) ≤ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) )
201	90	adantr	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ≤ ( 𝑐 / 2 ) )
202	191 192 193 200 201	letrd	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( 1 / 𝑘 ) ≤ ( 𝑐 / 2 ) )
203	190 202	eqbrtrd	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( abs ‘ ( 1 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) )
204		elsni	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) = 1 )
205	204	fvoveq1d	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( abs ‘ ( 1 / 𝑘 ) ) )
206	205	breq1d	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } → ( ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ↔ ( abs ‘ ( 1 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
207	203 206	syl5ibrcom	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
208	114	rpge0d	⊢ ( 𝑐 ∈ ℝ⁺ → 0 ≤ ( 𝑐 / 2 ) )
209		nncn	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
210		nnne0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
211	209 210	div0d	⊢ ( 𝑘 ∈ ℕ → ( 0 / 𝑘 ) = 0 )
212	211	abs00bd	⊢ ( 𝑘 ∈ ℕ → ( abs ‘ ( 0 / 𝑘 ) ) = 0 )
213	212	breq1d	⊢ ( 𝑘 ∈ ℕ → ( ( abs ‘ ( 0 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ↔ 0 ≤ ( 𝑐 / 2 ) ) )
214	213	biimparc	⊢ ( ( 0 ≤ ( 𝑐 / 2 ) ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( 0 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) )
215	208 214	sylan	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( 0 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) )
216	122 215	syldan	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( abs ‘ ( 0 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) )
217		elsni	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) = 0 )
218	217	fvoveq1d	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( abs ‘ ( 0 / 𝑘 ) ) )
219	218	breq1d	⊢ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } → ( ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ↔ ( abs ‘ ( 0 / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
220	216 219	syl5ibrcom	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
221	207 220	jaod	⊢ ( ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } ∨ ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } ) → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
222	221	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } ∨ ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } ) → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
223	222	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 1 } ∨ ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ { 0 } ) → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) )
224	184 223	mpd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) )
225	181 224	eqbrtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) )
226	79 111	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ )
227		simpll	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) → 𝜑 )
228	227	anim1i	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) → ( 𝜑 ∧ 𝑘 ∈ ℕ ) )
229	178	renegcld	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
230	228 229	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
231	230	recnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
232	231	abscld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℝ )
233	79 232	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℝ )
234	115 115	jca	⊢ ( 𝑐 ∈ ℝ⁺ → ( ( 𝑐 / 2 ) ∈ ℝ ∧ ( 𝑐 / 2 ) ∈ ℝ ) )
235	234	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐 / 2 ) ∈ ℝ ∧ ( 𝑐 / 2 ) ∈ ℝ ) )
236		ltleadd	⊢ ( ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ ∧ ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℝ ) ∧ ( ( 𝑐 / 2 ) ∈ ℝ ∧ ( 𝑐 / 2 ) ∈ ℝ ) ) → ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) ∧ ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
237	226 233 235 236	syl21anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) ∧ ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ≤ ( 𝑐 / 2 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
238	225 237	mpan2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 𝑐 / 2 ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
239	110 231	abstrid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ≤ ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
240	109 230	readdcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℝ )
241	240	recnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ∈ ℂ )
242	241	abscld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ )
243	111 232	readdcld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ )
244	115 115	readdcld	⊢ ( 𝑐 ∈ ℝ⁺ → ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ∈ ℝ )
245	244	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ∈ ℝ )
246		lelttr	⊢ ( ( ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ ∧ ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∈ ℝ ∧ ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ∈ ℝ ) → ( ( ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ≤ ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∧ ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
247	242 243 245 246	syl3anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ≤ ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) ∧ ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
248	239 247	mpand	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
249	79 248	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) + ( abs ‘ - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
250	120 238 249	3syld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
251	105	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) ∈ ℝ )
252	251 176	readdcld	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) ∈ ℝ )
253	252 177	nndivred	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ )
254	124 253	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ )
255	250 254	jctild	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) ) )
256	255	adantld	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) ) )
257	79	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) )
258	93	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) → 𝐶 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
259	258	ffvelcdmda	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ( 0 [,] 1 ) )
260	39 259	sselid	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ℝ )
261	80	rpreccld	⊢ ( 𝑐 ∈ ℝ⁺ → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ⁺ )
262	261	rpxrd	⊢ ( 𝑐 ∈ ℝ⁺ → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ^* )
263	262	ad3antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ^* )
264	19	rexmet	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
265		elbl	⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝐶 ‘ 𝑚 ) ∈ ℝ ∧ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ^* ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
266	264 265	mp3an1	⊢ ( ( ( 𝐶 ‘ 𝑚 ) ∈ ℝ ∧ ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∈ ℝ^* ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
267	260 263 266	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
268		elmapfn	⊢ ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ₀ ↑_m ( 1 ... 𝑁 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
269	100 101 268	3syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
270		vex	⊢ 𝑘 ∈ V
271		fnconstg	⊢ ( 𝑘 ∈ V → ( ( 1 ... 𝑁 ) × { 𝑘 } ) Fn ( 1 ... 𝑁 ) )
272	270 271	mp1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 ... 𝑁 ) × { 𝑘 } ) Fn ( 1 ... 𝑁 ) )
273		fzfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... 𝑁 ) ∈ Fin )
274		inidm	⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
275		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) = ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) )
276	270	fvconst2	⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { 𝑘 } ) ‘ 𝑚 ) = 𝑘 )
277	276	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { 𝑘 } ) ‘ 𝑚 ) = 𝑘 )
278	269 272 273 273 274 275 277	ofval	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) = ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) )
279	278	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) = ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) )
280	227 279	sylanl1	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) = ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) )
281	227 107	sylanl1	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
282	19	remetdval	⊢ ( ( ( 𝐶 ‘ 𝑚 ) ∈ ℝ ∧ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
283	260 281 282	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
284	280 283	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) = ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
285	284	breq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ↔ ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) )
286	285	anbi2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
287	267 286	bitrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
288	257 287	sylan	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) )
289		rpxr	⊢ ( 𝑐 ∈ ℝ⁺ → 𝑐 ∈ ℝ^* )
290	289	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑐 ∈ ℝ^* )
291		elbl	⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝐶 ‘ 𝑚 ) ∈ ℝ ∧ 𝑐 ∈ ℝ^* ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < 𝑐 ) ) )
292	264 291	mp3an1	⊢ ( ( ( 𝐶 ‘ 𝑚 ) ∈ ℝ ∧ 𝑐 ∈ ℝ^* ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < 𝑐 ) ) )
293	96 290 292	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < 𝑐 ) ) )
294		elun	⊢ ( 𝑧 ∈ ( { 1 } ∪ { 0 } ) ↔ ( 𝑧 ∈ { 1 } ∨ 𝑧 ∈ { 0 } ) )
295		fzofzp1	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( 𝑣 + 1 ) ∈ ( 0 ... 𝑘 ) )
296		elsni	⊢ ( 𝑧 ∈ { 1 } → 𝑧 = 1 )
297	296	oveq2d	⊢ ( 𝑧 ∈ { 1 } → ( 𝑣 + 𝑧 ) = ( 𝑣 + 1 ) )
298	297	eleq1d	⊢ ( 𝑧 ∈ { 1 } → ( ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) ↔ ( 𝑣 + 1 ) ∈ ( 0 ... 𝑘 ) ) )
299	295 298	syl5ibrcom	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( 𝑧 ∈ { 1 } → ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) ) )
300		elfzonn0	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → 𝑣 ∈ ℕ₀ )
301	300	nn0cnd	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → 𝑣 ∈ ℂ )
302	301	addridd	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( 𝑣 + 0 ) = 𝑣 )
303		elfzofz	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → 𝑣 ∈ ( 0 ... 𝑘 ) )
304	302 303	eqeltrd	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( 𝑣 + 0 ) ∈ ( 0 ... 𝑘 ) )
305		elsni	⊢ ( 𝑧 ∈ { 0 } → 𝑧 = 0 )
306	305	oveq2d	⊢ ( 𝑧 ∈ { 0 } → ( 𝑣 + 𝑧 ) = ( 𝑣 + 0 ) )
307	306	eleq1d	⊢ ( 𝑧 ∈ { 0 } → ( ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) ↔ ( 𝑣 + 0 ) ∈ ( 0 ... 𝑘 ) ) )
308	304 307	syl5ibrcom	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( 𝑧 ∈ { 0 } → ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) ) )
309	299 308	jaod	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( ( 𝑧 ∈ { 1 } ∨ 𝑧 ∈ { 0 } ) → ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) ) )
310	294 309	biimtrid	⊢ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) → ( 𝑧 ∈ ( { 1 } ∪ { 0 } ) → ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) ) )
311	310	imp	⊢ ( ( 𝑣 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑧 ∈ ( { 1 } ∪ { 0 } ) ) → ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) )
312	311	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑣 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑧 ∈ ( { 1 } ∪ { 0 } ) ) ) → ( 𝑣 + 𝑧 ) ∈ ( 0 ... 𝑘 ) )
313		dffn3	⊢ ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ran ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) )
314	269 313	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ran ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) )
315	314 7	fssd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) )
316	315	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) )
317		fzfid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
318	312 316 174 317 317 274	off	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝑘 ) )
319	318	ffnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) Fn ( 1 ... 𝑁 ) )
320	270 271	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) × { 𝑘 } ) Fn ( 1 ... 𝑁 ) )
321	269	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
322	174	ffnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) Fn ( 1 ... 𝑁 ) )
323		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) = ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) )
324		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) = ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) )
325	321 322 317 317 274 323 324	ofval	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ‘ 𝑚 ) = ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) )
326	276	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { 𝑘 } ) ‘ 𝑚 ) = 𝑘 )
327	319 320 317 317 274 325 326	ofval	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) = ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) )
328	327	eleq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ) )
329	228 328	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ) )
330	327	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) = ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) )
331	330	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) = ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) )
332	93	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐶 : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
333	332	ffvelcdmda	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ( 0 [,] 1 ) )
334	39 333	sselid	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ℝ )
335	253	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ )
336	19	remetdval	⊢ ( ( ( 𝐶 ‘ 𝑚 ) ∈ ℝ ∧ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) = ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) ) )
337	334 335 336	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) = ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) ) )
338	251	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) ∈ ℂ )
339	176	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ∈ ℂ )
340	209	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
341	210	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ≠ 0 )
342	338 339 340 341	divdird	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) = ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) + ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
343	107	recnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
344	343	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
345	344 179	subnegd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) − - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) = ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) + ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
346	342 345	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) = ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) − - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
347	346	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) = ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) − - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
348	347	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) = ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) − - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
349	334	recnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑚 ) ∈ ℂ )
350	107	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
351	350	adantlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℝ )
352	351	recnd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
353	179	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
354	353	negcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ∈ ℂ )
355	349 352 354	subsubd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) − - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) = ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
356	348 355	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) = ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) )
357	356	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( abs ‘ ( ( 𝐶 ‘ 𝑚 ) − ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ) ) = ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
358	331 337 357	3eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) = ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
359	358	adantl3r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) = ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) )
360	83	2halvesd	⊢ ( 𝑐 ∈ ℝ⁺ → ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) = 𝑐 )
361	360	eqcomd	⊢ ( 𝑐 ∈ ℝ⁺ → 𝑐 = ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) )
362	361	ad4antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑐 = ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) )
363	359 362	breq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < 𝑐 ↔ ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) )
364	329 363	anbi12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ℝ ∧ ( ( 𝐶 ‘ 𝑚 ) ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ) < 𝑐 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) ) )
365	293 364	bitrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) ) )
366	79 365	sylanl1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) + ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) ) / 𝑘 ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐶 ‘ 𝑚 ) − ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ‘ 𝑚 ) / 𝑘 ) ) + - ( ( ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ‘ 𝑚 ) / 𝑘 ) ) ) < ( ( 𝑐 / 2 ) + ( 𝑐 / 2 ) ) ) ) )
367	256 288 366	3imtr4d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) )
368	367	ralimdva	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) )
369		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
370		elfznn0	⊢ ( 𝑣 ∈ ( 0 ... 𝑘 ) → 𝑣 ∈ ℕ₀ )
371	370	nn0red	⊢ ( 𝑣 ∈ ( 0 ... 𝑘 ) → 𝑣 ∈ ℝ )
372		nndivre	⊢ ( ( 𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑣 / 𝑘 ) ∈ ℝ )
373	371 372	sylan	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑣 / 𝑘 ) ∈ ℝ )
374		elfzle1	⊢ ( 𝑣 ∈ ( 0 ... 𝑘 ) → 0 ≤ 𝑣 )
375	371 374	jca	⊢ ( 𝑣 ∈ ( 0 ... 𝑘 ) → ( 𝑣 ∈ ℝ ∧ 0 ≤ 𝑣 ) )
376	186	rpregt0d	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
377		divge0	⊢ ( ( ( 𝑣 ∈ ℝ ∧ 0 ≤ 𝑣 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → 0 ≤ ( 𝑣 / 𝑘 ) )
378	375 376 377	syl2an	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝑣 / 𝑘 ) )
379		elfzle2	⊢ ( 𝑣 ∈ ( 0 ... 𝑘 ) → 𝑣 ≤ 𝑘 )
380	379	adantr	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑣 ≤ 𝑘 )
381	371	adantr	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑣 ∈ ℝ )
382		1red	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ )
383	186	adantl	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ⁺ )
384	381 382 383	ledivmuld	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑣 / 𝑘 ) ≤ 1 ↔ 𝑣 ≤ ( 𝑘 · 1 ) ) )
385	209	mulridd	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · 1 ) = 𝑘 )
386	385	breq2d	⊢ ( 𝑘 ∈ ℕ → ( 𝑣 ≤ ( 𝑘 · 1 ) ↔ 𝑣 ≤ 𝑘 ) )
387	386	adantl	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑣 ≤ ( 𝑘 · 1 ) ↔ 𝑣 ≤ 𝑘 ) )
388	384 387	bitrd	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑣 / 𝑘 ) ≤ 1 ↔ 𝑣 ≤ 𝑘 ) )
389	380 388	mpbird	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑣 / 𝑘 ) ≤ 1 )
390		elicc01	⊢ ( ( 𝑣 / 𝑘 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝑣 / 𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝑣 / 𝑘 ) ∧ ( 𝑣 / 𝑘 ) ≤ 1 ) )
391	373 378 389 390	syl3anbrc	⊢ ( ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑣 / 𝑘 ) ∈ ( 0 [,] 1 ) )
392	391	ancoms	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑣 ∈ ( 0 ... 𝑘 ) ) → ( 𝑣 / 𝑘 ) ∈ ( 0 [,] 1 ) )
393		elsni	⊢ ( 𝑧 ∈ { 𝑘 } → 𝑧 = 𝑘 )
394	393	oveq2d	⊢ ( 𝑧 ∈ { 𝑘 } → ( 𝑣 / 𝑧 ) = ( 𝑣 / 𝑘 ) )
395	394	eleq1d	⊢ ( 𝑧 ∈ { 𝑘 } → ( ( 𝑣 / 𝑧 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑣 / 𝑘 ) ∈ ( 0 [,] 1 ) ) )
396	392 395	syl5ibrcom	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑣 ∈ ( 0 ... 𝑘 ) ) → ( 𝑧 ∈ { 𝑘 } → ( 𝑣 / 𝑧 ) ∈ ( 0 [,] 1 ) ) )
397	396	impr	⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑧 ∈ { 𝑘 } ) ) → ( 𝑣 / 𝑧 ) ∈ ( 0 [,] 1 ) )
398	369 397	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑣 ∈ ( 0 ... 𝑘 ) ∧ 𝑧 ∈ { 𝑘 } ) ) → ( 𝑣 / 𝑧 ) ∈ ( 0 [,] 1 ) )
399	270	fconst	⊢ ( ( 1 ... 𝑁 ) × { 𝑘 } ) : ( 1 ... 𝑁 ) ⟶ { 𝑘 }
400	399	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) × { 𝑘 } ) : ( 1 ... 𝑁 ) ⟶ { 𝑘 } )
401	398 318 400 317 317 274	off	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
402	401	ffnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) )
403	124 402	sylan	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) )
404	368 403	jctild	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) ) )
405	2	eleq2i	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ↔ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) ) )
406		ovex	⊢ ( 0 [,] 1 ) ∈ V
407	406 43	elmap	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( ( 0 [,] 1 ) ↑_m ( 1 ... 𝑁 ) ) ↔ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
408	405 407	bitri	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ↔ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
409	401 408	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 )
410	124 409	sylan	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 )
411	404 410	jctird	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) ∧ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ) ) )
412		elin	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∧ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ) )
413		ovex	⊢ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ V
414	413	elixp	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ↔ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) )
415	414	anbi1i	⊢ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∧ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) ∧ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ) )
416	412 415	bitri	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ↔ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) Fn ( 1 ... 𝑁 ) ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ) ∧ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ) )
417	411 416	imbitrrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ) )
418		ssel	⊢ ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ) )
419	418	com12	⊢ ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ) )
420	417 419	syl6	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ) ) )
421	420	impd	⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ) )
422	421	ralrimdva	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ∧ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) → ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ) )
423	422	expd	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ) ) )
424	8	3exp2	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑟 ∈ { ≤ , ^◡ ≤ } → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 ) ) ) )
425	424	imp43	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ^◡ ≤ } ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 )
426		r19.29	⊢ ( ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ∧ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ∧ 0 𝑟 𝑋 ) )
427		fveq2	⊢ ( 𝑧 = ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
428	427	fveq1d	⊢ ( 𝑧 = ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
429	428 5	eqtr4di	⊢ ( 𝑧 = ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) = 𝑋 )
430	429	breq2d	⊢ ( 𝑧 = ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ↔ 0 𝑟 𝑋 ) )
431	430	rspcev	⊢ ( ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ∧ 0 𝑟 𝑋 ) → ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) )
432	431	rexlimivw	⊢ ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ∧ 0 𝑟 𝑋 ) → ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) )
433	426 432	syl	⊢ ( ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 ∧ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 ) → ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) )
434	433	expcom	⊢ ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 𝑋 → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 → ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
435	425 434	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ^◡ ≤ } ) ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 → ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
436	435	ralrimdvva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
437	122 436	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ℝ⁺ ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
438	437	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
439	438	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f + ( ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2^nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
440	423 439	syl6d	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
441	440	rexlimdva	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / - ( ⌊ ‘ - ( 2 / 𝑐 ) ) ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
442	74 441	syld	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
443	442	com23	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ 𝑐 ∈ ℝ⁺ ) → ( ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
444	443	impr	⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝐼 ) ∧ ( 𝑐 ∈ ℝ⁺ ∧ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
445	51 444	sylanl2	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∧ 𝐶 ∈ 𝑣 ) ) ∧ ( 𝑐 ∈ ℝ⁺ ∧ ( X 𝑚 ∈ ( 1 ... 𝑁 ) ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑐 ) ∩ 𝐼 ) ⊆ 𝑣 ) ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
446	35 445	rexlimddv	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∧ 𝐶 ∈ 𝑣 ) ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
447	446	expr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ) → ( 𝐶 ∈ 𝑣 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
448	447	com23	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ( 𝐶 ∈ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
449		r19.21v	⊢ ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ↔ ( 𝐶 ∈ 𝑣 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
450	448 449	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ) → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
451	450	ralrimdva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )
452		ralcom	⊢ ( ∀ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) )
453	451 452	imbitrdi	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℕ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑖 ) ∀ 𝑚 ∈ ( 1 ... 𝑁 ) ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘_f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑚 ) ∈ ( ( 𝐶 ‘ 𝑚 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) ( 1 / 𝑖 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ∀ 𝑣 ∈ ( 𝑅 ↾_t 𝐼 ) ( 𝐶 ∈ 𝑣 → ∀ 𝑟 ∈ { ≤ , ^◡ ≤ } ∃ 𝑧 ∈ 𝑣 0 𝑟 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ) ) )

Metamath Proof Explorer

Theorem poimirlem29

Proof