Step | Hyp | Ref
| Expression |
1 | | poimir.r |
. . . . . . . . . . . 12
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
2 | | fzfi 13431 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ∈
Fin |
3 | | retop 23514 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
4 | 3 | fconst6 6568 |
. . . . . . . . . . . . 13
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top |
5 | | pttop 22333 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top) →
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Top) |
6 | 2, 4, 5 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Top |
7 | 1, 6 | eqeltri 2829 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ Top |
8 | | poimir.i |
. . . . . . . . . . . 12
⊢ 𝐼 = ((0[,]1) ↑m
(1...𝑁)) |
9 | | ovex 7203 |
. . . . . . . . . . . 12
⊢ ((0[,]1)
↑m (1...𝑁))
∈ V |
10 | 8, 9 | eqeltri 2829 |
. . . . . . . . . . 11
⊢ 𝐼 ∈ V |
11 | | elrest 16804 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅 ↾t 𝐼) ↔ ∃𝑧 ∈ 𝑅 𝑣 = (𝑧 ∩ 𝐼))) |
12 | 7, 10, 11 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (𝑅 ↾t 𝐼) ↔ ∃𝑧 ∈ 𝑅 𝑣 = (𝑧 ∩ 𝐼)) |
13 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
14 | 1, 13 | ptrecube 35400 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑅 ∧ 𝐶 ∈ 𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧) |
15 | 14 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑅 → (𝐶 ∈ 𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧)) |
16 | | inss1 4119 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∩ 𝐼) ⊆ 𝑧 |
17 | | sseq1 3902 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (𝑣 ⊆ 𝑧 ↔ (𝑧 ∩ 𝐼) ⊆ 𝑧)) |
18 | 16, 17 | mpbiri 261 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 ∩ 𝐼) → 𝑣 ⊆ 𝑧) |
19 | 18 | sseld 3876 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (𝐶 ∈ 𝑣 → 𝐶 ∈ 𝑧)) |
20 | | ssrin 4124 |
. . . . . . . . . . . . . . 15
⊢ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧 ∩ 𝐼)) |
21 | | sseq2 3903 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 ∩ 𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧 ∩ 𝐼))) |
22 | 20, 21 | syl5ibr 249 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
23 | 22 | reximdv 3183 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
24 | 19, 23 | imim12d 81 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑧 ∩ 𝐼) → ((𝐶 ∈ 𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))) |
25 | 15, 24 | syl5com 31 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑅 → (𝑣 = (𝑧 ∩ 𝐼) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))) |
26 | 25 | rexlimiv 3190 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑅 𝑣 = (𝑧 ∩ 𝐼) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
27 | 12, 26 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝑅 ↾t 𝐼) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
28 | 27 | imp 410 |
. . . . . . . 8
⊢ ((𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) |
29 | 28 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) |
30 | | resttop 21911 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅 ↾t 𝐼) ∈ Top) |
31 | 7, 10, 30 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑅 ↾t 𝐼) ∈ Top |
32 | | reex 10706 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
33 | | unitssre 12973 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
⊆ ℝ |
34 | | mapss 8499 |
. . . . . . . . . . . . . 14
⊢ ((ℝ
∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑m
(1...𝑁)) ⊆ (ℝ
↑m (1...𝑁))) |
35 | 32, 33, 34 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
↑m (1...𝑁))
⊆ (ℝ ↑m (1...𝑁)) |
36 | 8, 35 | eqsstri 3911 |
. . . . . . . . . . . 12
⊢ 𝐼 ⊆ (ℝ
↑m (1...𝑁)) |
37 | | ovex 7203 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) ∈
V |
38 | | uniretop 23515 |
. . . . . . . . . . . . . . 15
⊢ ℝ =
∪ (topGen‘ran (,)) |
39 | 1, 38 | ptuniconst 22349 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑁) ∈ V
∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑m
(1...𝑁)) = ∪ 𝑅) |
40 | 37, 3, 39 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (ℝ
↑m (1...𝑁))
= ∪ 𝑅 |
41 | 40 | restuni 21913 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ
↑m (1...𝑁))) → 𝐼 = ∪ (𝑅 ↾t 𝐼)) |
42 | 7, 36, 41 | mp2an 692 |
. . . . . . . . . . 11
⊢ 𝐼 = ∪
(𝑅 ↾t
𝐼) |
43 | 42 | eltopss 21658 |
. . . . . . . . . 10
⊢ (((𝑅 ↾t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → 𝑣 ⊆ 𝐼) |
44 | 31, 43 | mpan 690 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝑅 ↾t 𝐼) → 𝑣 ⊆ 𝐼) |
45 | 44 | sselda 3877 |
. . . . . . . 8
⊢ ((𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣) → 𝐶 ∈ 𝐼) |
46 | | 2rp 12477 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
47 | | rpdivcl 12497 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ+ ∧ 𝑐 ∈ ℝ+) → (2 /
𝑐) ∈
ℝ+) |
48 | 46, 47 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ ℝ+
→ (2 / 𝑐) ∈
ℝ+) |
49 | 48 | rpred 12514 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ (2 / 𝑐) ∈
ℝ) |
50 | | ceicl 13302 |
. . . . . . . . . . . . . . 15
⊢ ((2 /
𝑐) ∈ ℝ →
-(⌊‘-(2 / 𝑐))
∈ ℤ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈ ℤ) |
52 | | 0red 10722 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ 0 ∈ ℝ) |
53 | 51 | zred 12168 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈ ℝ) |
54 | 48 | rpgt0d 12517 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ 0 < (2 / 𝑐)) |
55 | | ceige 13304 |
. . . . . . . . . . . . . . . 16
⊢ ((2 /
𝑐) ∈ ℝ → (2
/ 𝑐) ≤
-(⌊‘-(2 / 𝑐))) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ (2 / 𝑐) ≤
-(⌊‘-(2 / 𝑐))) |
57 | 52, 49, 53, 54, 56 | ltletrd 10878 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ℝ+
→ 0 < -(⌊‘-(2 / 𝑐))) |
58 | | elnnz 12072 |
. . . . . . . . . . . . . 14
⊢
(-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2
/ 𝑐)) ∈ ℤ ∧
0 < -(⌊‘-(2 / 𝑐)))) |
59 | 51, 57, 58 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈ ℕ) |
60 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) →
(ℤ≥‘𝑖) =
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) |
61 | | oveq2 7178 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 /
𝑐)))) |
62 | 61 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) = ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))) |
63 | 62 | eleq2d 2818 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
64 | 63 | ralbidv 3109 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
65 | 60, 64 | rexeqbidv 3305 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
66 | 65 | rspcv 3521 |
. . . . . . . . . . . . 13
⊢
(-(⌊‘-(2 / 𝑐)) ∈ ℕ → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
67 | 59, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ℝ+
→ (∀𝑖 ∈
ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
68 | 67 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) →
(∀𝑖 ∈ ℕ
∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
69 | | uznnssnn 12377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(-(⌊‘-(2 / 𝑐)) ∈ ℕ →
(ℤ≥‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ) |
70 | 59, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (ℤ≥‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ) |
71 | 70 | sseld 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ (𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ)) |
72 | 71 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ)) |
73 | 72 | imdistani 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
ℕ)) |
74 | 59 | nnrpd 12512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈
ℝ+) |
75 | 48, 74 | lerecd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ ((2 / 𝑐) ≤
-(⌊‘-(2 / 𝑐))
↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))) |
76 | 56, 75 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))) |
77 | | rpcn 12482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℂ) |
78 | | rpne0 12488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ≠
0) |
79 | | 2cn 11791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ∈
ℂ |
80 | | 2ne0 11820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ≠
0 |
81 | | recdiv 11424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2)) |
82 | 79, 80, 81 | mpanl12 702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2)) |
83 | 77, 78, 82 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (1 / (2 / 𝑐)) =
(𝑐 / 2)) |
84 | 76, 83 | breqtrd 5056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) |
85 | 84 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) |
86 | | elmapi 8459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐶 ∈ ((0[,]1)
↑m (1...𝑁))
→ 𝐶:(1...𝑁)⟶(0[,]1)) |
87 | 86, 8 | eleq2s 2851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐶 ∈ 𝐼 → 𝐶:(1...𝑁)⟶(0[,]1)) |
88 | 87 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1)) |
89 | 88 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ (0[,]1)) |
90 | 33, 89 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℝ) |
91 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑) |
92 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ) |
93 | 91, 92 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
94 | | poimirlem30.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
95 | 94 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
96 | | xp1st 7746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐺‘𝑘) ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑m (1...𝑁))) |
97 | | elmapi 8459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑m (1...𝑁))
→ (1st ‘(𝐺‘𝑘)):(1...𝑁)⟶ℕ0) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶ℕ0) |
99 | 98 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈
ℕ0) |
100 | 99 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈ ℝ) |
101 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
102 | 100, 101 | nndivred 11770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
103 | 93, 102 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
104 | 90, 103 | resubcld 11146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) ∈ ℝ) |
105 | 104 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) ∈ ℂ) |
106 | 105 | abscld 14886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ) |
107 | 59 | nnrecred 11767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ) |
108 | 107 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ) |
109 | | rphalfcl 12499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ (𝑐 / 2) ∈
ℝ+) |
110 | 109 | rpred 12514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (𝑐 / 2) ∈
ℝ) |
111 | 110 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ) |
112 | | ltletr 10810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 /
-(⌊‘-(2 / 𝑐)))
∈ ℝ ∧ (𝑐 /
2) ∈ ℝ) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 /
-(⌊‘-(2 / 𝑐)))
≤ (𝑐 / 2)) →
(abs‘((𝐶‘𝑚) − (((1st
‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2))) |
113 | 106, 108,
111, 112 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 /
-(⌊‘-(2 / 𝑐)))
≤ (𝑐 / 2)) →
(abs‘((𝐶‘𝑚) − (((1st
‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2))) |
114 | 85, 113 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2))) |
115 | 73, 114 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2))) |
116 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝐶 ∈ 𝐼) → 𝜑) |
117 | 70 | sselda 3877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ) |
118 | 116, 117 | anim12i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ (𝑐 ∈ ℝ+ ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))))) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
119 | 118 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
120 | | 1re 10719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 1 ∈
ℝ |
121 | | snssi 4696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (1 ∈
ℝ → {1} ⊆ ℝ) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ {1}
⊆ ℝ |
123 | | 0re 10721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 0 ∈
ℝ |
124 | | snssi 4696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (0 ∈
ℝ → {0} ⊆ ℝ) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ {0}
⊆ ℝ |
126 | 122, 125 | unssi 4075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ({1}
∪ {0}) ⊆ ℝ |
127 | | 1ex 10715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 1 ∈
V |
128 | 127 | fconst 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2nd
‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} |
129 | | c0ex 10713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 0 ∈
V |
130 | 129 | fconst 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0} |
131 | 128, 130 | pm3.2i 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2nd
‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} ∧
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}) |
132 | | xp2nd 7747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐺‘𝑘) ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
133 | 95, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
134 | | fvex 6687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(2nd ‘(𝐺‘𝑘)) ∈ V |
135 | | f1oeq1 6606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑓 = (2nd ‘(𝐺‘𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))) |
136 | 134, 135 | elab 3573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((2nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
137 | 133, 136 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
138 | | dff1o3 6624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(𝐺‘𝑘)))) |
139 | 138 | simprbi 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(𝐺‘𝑘))) |
140 | | imain 6424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (Fun
◡(2nd ‘(𝐺‘𝑘)) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))) |
141 | 137, 139,
140 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))) |
142 | | elfznn0 13091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0) |
143 | 142 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) |
144 | 143 | ltp1d 11648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1)) |
145 | | fzdisj 13025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
147 | 146 | imaeq2d 5903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺‘𝑘)) “ ∅)) |
148 | | ima0 5919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((2nd ‘(𝐺‘𝑘)) “ ∅) =
∅ |
149 | 147, 148 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅) |
150 | 141, 149 | sylan9req 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅) |
151 | | fun 6540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2nd
‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} ∧
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ (((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅) → ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
152 | 131, 150,
151 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
153 | | imaundi 5982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) |
154 | | nn0p1nn 12015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
155 | 142, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ) |
156 | | nnuz 12363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ℕ =
(ℤ≥‘1) |
157 | 155, 156 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
158 | | elfzuz3 12995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝑗)) |
159 | | fzsplit2 13023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
160 | 157, 158,
159 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
161 | 160 | imaeq2d 5903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))) |
162 | | f1ofo 6625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁)) |
163 | | foima 6597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = (1...𝑁)) |
164 | 137, 162,
163 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐺‘𝑘)) “ (1...𝑁)) = (1...𝑁)) |
165 | 161, 164 | sylan9req 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑗 ∈ (0...𝑁) ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((2nd
‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
166 | 165 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
167 | 153, 166 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
168 | 167 | feq2d 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))) |
169 | 152, 168 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})) |
170 | 169 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0})) |
171 | 126, 170 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ) |
172 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
173 | 171, 172 | nndivred 11770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ) |
174 | 173 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
175 | 174 | absnegd 14899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
176 | 119, 175 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
177 | 119, 170 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0})) |
178 | | elun 4039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0}) ↔
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0})) |
179 | 177, 178 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0})) |
180 | | nnrecre 11758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
181 | | nnrp 12483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
182 | 181 | rpreccld 12524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
183 | 182 | rpge0d 12518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ 𝑘)) |
184 | 180, 183 | absidd 14872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 ∈ ℕ →
(abs‘(1 / 𝑘)) = (1 /
𝑘)) |
185 | 117, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘)) |
186 | 117 | nnrecred 11767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ) |
187 | 107 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ) |
188 | 110 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ) |
189 | | eluzle 12337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘) |
190 | 189 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘) |
191 | 59 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈
ℕ) |
192 | 191 | nnrpd 12512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈
ℝ+) |
193 | 117 | nnrpd 12512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+) |
194 | 192, 193 | lerecd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))) |
195 | 190, 194 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))) |
196 | 84 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) |
197 | 186, 187,
188, 195, 196 | letrd 10875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2)) |
198 | 185, 197 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)) |
199 | | elsni 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1) |
200 | 199 | fvoveq1d 7192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘))) |
201 | 200 | breq1d 5040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} →
((abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))) |
202 | 198, 201 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
203 | 109 | rpge0d 12518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 ∈ ℝ+
→ 0 ≤ (𝑐 /
2)) |
204 | | nncn 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
205 | | nnne0 11750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
206 | 204, 205 | div0d 11493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 ∈ ℕ → (0 /
𝑘) = 0) |
207 | 206 | abs00bd 14741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ ℕ →
(abs‘(0 / 𝑘)) =
0) |
208 | 207 | breq1d 5040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ →
((abs‘(0 / 𝑘)) ≤
(𝑐 / 2) ↔ 0 ≤
(𝑐 / 2))) |
209 | 208 | biimparc 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((0 ≤
(𝑐 / 2) ∧ 𝑘 ∈ ℕ) →
(abs‘(0 / 𝑘)) ≤
(𝑐 / 2)) |
210 | 203, 209 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
→ (abs‘(0 / 𝑘))
≤ (𝑐 /
2)) |
211 | 117, 210 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)) |
212 | | elsni 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0) |
213 | 212 | fvoveq1d 7192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘))) |
214 | 213 | breq1d 5040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} →
((abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))) |
215 | 211, 214 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
216 | 202, 215 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
217 | 216 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
218 | 217 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
219 | 179, 218 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) |
220 | 176, 219 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) |
221 | 73, 106 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ) |
222 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑) |
223 | 222 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
224 | 173 | renegcld 11145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ) |
225 | 223, 224 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ) |
226 | 225 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
227 | 226 | abscld 14886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) |
228 | 73, 227 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) |
229 | 110, 110 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ ((𝑐 / 2) ∈
ℝ ∧ (𝑐 / 2)
∈ ℝ)) |
230 | 229 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈
ℝ)) |
231 | | ltleadd 11201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧
(abs‘-((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) ∧ ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈ ℝ)) →
(((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) ∧ (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
232 | 221, 228,
230, 231 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) ∧ (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
233 | 220, 232 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
234 | 105, 226 | abstrid 14906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
235 | 104, 225 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) |
236 | 235 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ) |
237 | 236 | abscld 14886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ) |
238 | 106, 227 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ) |
239 | 110, 110 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ ((𝑐 / 2) + (𝑐 / 2)) ∈
ℝ) |
240 | 239 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ) |
241 | | lelttr 10809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ ∧ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ ∧ ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ) →
(((abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∧ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
242 | 237, 238,
240, 241 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∧ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
243 | 234, 242 | mpand 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
244 | 73, 243 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
245 | 115, 233,
244 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
246 | 100 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈ ℝ) |
247 | 246, 171 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ) |
248 | 247, 172 | nndivred 11770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) |
249 | 119, 248 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) |
250 | 245, 249 | jctild 529 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
251 | 250 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))) → (((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
252 | 73 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
ℕ)) |
253 | 87 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1)) |
254 | 253 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ (0[,]1)) |
255 | 33, 254 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℝ) |
256 | 74 | rpreccld 12524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ+) |
257 | 256 | rpxrd 12515 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ*) |
258 | 257 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ*) |
259 | 13 | rexmet 23543 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
260 | | elbl 23141 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝐶‘𝑚) ∈ ℝ ∧ (1 /
-(⌊‘-(2 / 𝑐)))
∈ ℝ*) → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))))) |
261 | 259, 260 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ (1 /
-(⌊‘-(2 / 𝑐)))
∈ ℝ*) → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))))) |
262 | 255, 258,
261 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))))) |
263 | | elmapfn 8475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑m (1...𝑁))
→ (1st ‘(𝐺‘𝑘)) Fn (1...𝑁)) |
264 | 95, 96, 263 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)) Fn (1...𝑁)) |
265 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑘 ∈ V |
266 | | fnconstg 6566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
267 | 265, 266 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
268 | | fzfid 13432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin) |
269 | | inidm 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
270 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) = ((1st ‘(𝐺‘𝑘))‘𝑚)) |
271 | 265 | fvconst2 6976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘) |
272 | 271 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘) |
273 | 264, 267,
268, 268, 269, 270, 272 | ofval 7435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) |
274 | 273 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) |
275 | 222, 274 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) |
276 | 222, 102 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
277 | 13 | remetdval 23541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ (((1st
‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)))) |
278 | 255, 276,
277 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)))) |
279 | 275, 278 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)))) |
280 | 279 | breq1d 5040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))) |
281 | 280 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st
‘(𝐺‘𝑘)) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))) |
282 | 262, 281 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))) |
283 | 252, 282 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))) |
284 | | rpxr 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℝ*) |
285 | 284 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*) |
286 | | elbl 23141 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝐶‘𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) →
(((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐))) |
287 | 259, 286 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) →
(((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐))) |
288 | 90, 285, 287 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐))) |
289 | | elun 4039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ ({1} ∪ {0}) ↔
(𝑧 ∈ {1} ∨ 𝑧 ∈ {0})) |
290 | | fzofzp1 13225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘)) |
291 | | elsni 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈ {1} → 𝑧 = 1) |
292 | 291 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1)) |
293 | 292 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘))) |
294 | 290, 293 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘))) |
295 | | elfzonn0 13173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0) |
296 | 295 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ) |
297 | 296 | addid1d 10918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣) |
298 | | elfzofz 13144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘)) |
299 | 297, 298 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘)) |
300 | | elsni 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈ {0} → 𝑧 = 0) |
301 | 300 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0)) |
302 | 301 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘))) |
303 | 299, 302 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘))) |
304 | 294, 303 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘))) |
305 | 289, 304 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘))) |
306 | 305 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘)) |
307 | 306 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘)) |
308 | | dffn3 6517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((1st ‘(𝐺‘𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺‘𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺‘𝑘))) |
309 | 264, 308 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺‘𝑘))) |
310 | | poimirlem30.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st
‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) |
311 | 309, 310 | fssd 6522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘)) |
312 | 311 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘)) |
313 | | fzfid 13432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin) |
314 | 307, 312,
169, 313, 313, 269 | off 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘)) |
315 | 314 | ffnd 6505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁)) |
316 | 265, 266 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
317 | 264 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺‘𝑘)) Fn (1...𝑁)) |
318 | 169 | ffnd 6505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
319 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) = ((1st ‘(𝐺‘𝑘))‘𝑚)) |
320 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) |
321 | 317, 318,
313, 313, 269, 319, 320 | ofval 7435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑚) = (((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))) |
322 | 271 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘) |
323 | 315, 316,
313, 313, 269, 321, 322 | ofval 7435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) |
324 | 323 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)) |
325 | 223, 324 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)) |
326 | 323 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) |
327 | 326 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) |
328 | 87 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1)) |
329 | 328 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ (0[,]1)) |
330 | 33, 329 | sseldi 3875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℝ) |
331 | 248 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) |
332 | 13 | remetdval 23541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ ((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))) |
333 | 330, 331,
332 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))) |
334 | 246 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈ ℂ) |
335 | 171 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ) |
336 | 204 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ) |
337 | 205 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0) |
338 | 334, 335,
336, 337 | divdird 11532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
339 | 102 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℂ) |
340 | 339 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℂ) |
341 | 340, 174 | subnegd 11082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
342 | 338, 341 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
343 | 342 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
344 | 343 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
345 | 330 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℂ) |
346 | 102 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
347 | 346 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
348 | 347 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℂ) |
349 | 174 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
350 | 349 | negcld 11062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
351 | 345, 348,
350 | subsubd 11103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
352 | 344, 351 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
353 | 352 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
354 | 327, 333,
353 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
355 | 354 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
356 | 77 | 2halvesd 11962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ ((𝑐 / 2) + (𝑐 / 2)) = 𝑐) |
357 | 356 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ ℝ+
→ 𝑐 = ((𝑐 / 2) + (𝑐 / 2))) |
358 | 357 | ad4antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2))) |
359 | 355, 358 | breq12d 5043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐 ↔ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
360 | 325, 359 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐) ↔ (((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
361 | 288, 360 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
362 | 73, 361 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
363 | 251, 283,
362 | 3imtr4d 297 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐))) |
364 | 363 | ralimdva 3091 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐))) |
365 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ) |
366 | | elfznn0 13091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0) |
367 | 366 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ) |
368 | | nndivre 11757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ) |
369 | 367, 368 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ) |
370 | | elfzle1 13001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣) |
371 | 367, 370 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣)) |
372 | 181 | rpregt0d 12520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
373 | | divge0 11587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑣 ∈ ℝ ∧ 0 ≤
𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝑣 / 𝑘)) |
374 | 371, 372,
373 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘)) |
375 | | elfzle2 13002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ (0...𝑘) → 𝑣 ≤ 𝑘) |
376 | 375 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ≤ 𝑘) |
377 | 367 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ) |
378 | | 1red 10720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈
ℝ) |
379 | 181 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
380 | 377, 378,
379 | ledivmuld 12567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1))) |
381 | 204 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘) |
382 | 381 | breq2d 5042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣 ≤ 𝑘)) |
383 | 382 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣 ≤ 𝑘)) |
384 | 380, 383 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ 𝑘)) |
385 | 376, 384 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1) |
386 | | elicc01 12940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1)) |
387 | 369, 374,
385, 386 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1)) |
388 | 387 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1)) |
389 | | elsni 4533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ {𝑘} → 𝑧 = 𝑘) |
390 | 389 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘)) |
391 | 390 | eleq1d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1))) |
392 | 388, 391 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1))) |
393 | 392 | impr 458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1)) |
394 | 365, 393 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1)) |
395 | 265 | fconst 6564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑁) ×
{𝑘}):(1...𝑁)⟶{𝑘} |
396 | 395 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}) |
397 | 394, 314,
396, 313, 313, 269 | off 7442 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
398 | 397 | ffnd 6505 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁)) |
399 | 119, 398 | sylan 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁)) |
400 | 364, 399 | jctild 529 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)))) |
401 | 8 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑m (1...𝑁))) |
402 | | ovex 7203 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0[,]1)
∈ V |
403 | 402, 37 | elmap 8481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑m (1...𝑁))
↔ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
404 | 401, 403 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
405 | 397, 404 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼) |
406 | 119, 405 | sylan 583 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼) |
407 | 400, 406 | jctird 530 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼))) |
408 | | elin 3859 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼)) |
409 | | ovex 7203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ V |
410 | 409 | elixp 8514 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐))) |
411 | 410 | anbi1i 627 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼) ↔ (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼)) |
412 | 408, 411 | bitri 278 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ (((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼)) |
413 | 407, 412 | syl6ibr 255 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼))) |
414 | | ssel 3870 |
. . . . . . . . . . . . . . . . . 18
⊢ ((X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣)) |
415 | 414 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣)) |
416 | 413, 415 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣))) |
417 | 416 | impd 414 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → (((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣)) |
418 | 417 | ralrimdva 3101 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣)) |
419 | 418 | expd 419 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣))) |
420 | | poimirlem30.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) |
421 | 420 | 3exp2 1355 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ◡ ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)))) |
422 | 421 | imp43 431 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) |
423 | | r19.29 3167 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑗 ∈
(0...𝑁)(((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋)) |
424 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) → (𝐹‘𝑧) = (𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))) |
425 | 424 | fveq1d 6676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑛)) |
426 | | poimirlem30.x |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑛) |
427 | 425, 426 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = 𝑋) |
428 | 427 | breq2d 5042 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) → (0𝑟((𝐹‘𝑧)‘𝑛) ↔ 0𝑟𝑋)) |
429 | 428 | rspcev 3526 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) |
430 | 429 | rexlimivw 3192 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑗 ∈
(0...𝑁)((((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) |
431 | 423, 430 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑗 ∈
(0...𝑁)(((1st
‘(𝐺‘𝑘)) ∘f +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) |
432 | 431 | expcom 417 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑗 ∈
(0...𝑁)0𝑟𝑋 → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
433 | 422, 432 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
434 | 433 | ralrimdvva 3106 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
435 | 117, 434 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑐 ∈ ℝ+ ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
436 | 435 | anassrs 471 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
437 | 436 | adantllr 719 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f + ((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
438 | 419, 437 | syl6d 75 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
439 | 438 | rexlimdva 3194 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) →
(∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
440 | 68, 439 | syld 47 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) →
(∀𝑖 ∈ ℕ
∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
441 | 440 | com23 86 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) → ((X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
442 | 441 | impr 458 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
443 | 45, 442 | sylanl2 681 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
444 | 29, 443 | rexlimddv 3201 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
445 | 444 | expr 460 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → (𝐶 ∈ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
446 | 445 | com23 86 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → (𝐶 ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
447 | | r19.21v 3089 |
. . . 4
⊢
(∀𝑛 ∈
(1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) ↔ (𝐶 ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
448 | 446, 447 | syl6ibr 255 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
449 | 448 | ralrimdva 3101 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅 ↾t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
450 | | ralcom 3258 |
. 2
⊢
(∀𝑣 ∈
(𝑅 ↾t
𝐼)∀𝑛 ∈ (1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
451 | 449, 450 | syl6ib 254 |
1
⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘f / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |