Step | Hyp | Ref
| Expression |
1 | | poimir.r |
. . . . . . . . . . . 12
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
2 | | fzfi 12633 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ∈
Fin |
3 | | retop 22375 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
4 | 3 | fconst6 6008 |
. . . . . . . . . . . . 13
⊢
((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top |
5 | | pttop 21195 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{(topGen‘ran (,))}):(1...𝑁)⟶Top) →
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Top) |
6 | 2, 4, 5 | mp2an 704 |
. . . . . . . . . . . 12
⊢
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈
Top |
7 | 1, 6 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝑅 ∈ Top |
8 | | poimir.i |
. . . . . . . . . . . 12
⊢ 𝐼 = ((0[,]1)
↑𝑚 (1...𝑁)) |
9 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ ((0[,]1)
↑𝑚 (1...𝑁)) ∈ V |
10 | 8, 9 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐼 ∈ V |
11 | | elrest 15911 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑣 ∈ (𝑅 ↾t 𝐼) ↔ ∃𝑧 ∈ 𝑅 𝑣 = (𝑧 ∩ 𝐼))) |
12 | 7, 10, 11 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (𝑅 ↾t 𝐼) ↔ ∃𝑧 ∈ 𝑅 𝑣 = (𝑧 ∩ 𝐼)) |
13 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
14 | 1, 13 | ptrecube 32579 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑅 ∧ 𝐶 ∈ 𝑧) → ∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧) |
15 | 14 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑅 → (𝐶 ∈ 𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧)) |
16 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∩ 𝐼) ⊆ 𝑧 |
17 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (𝑣 ⊆ 𝑧 ↔ (𝑧 ∩ 𝐼) ⊆ 𝑧)) |
18 | 16, 17 | mpbiri 247 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 ∩ 𝐼) → 𝑣 ⊆ 𝑧) |
19 | 18 | sseld 3567 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (𝐶 ∈ 𝑣 → 𝐶 ∈ 𝑧)) |
20 | | ssrin 3800 |
. . . . . . . . . . . . . . 15
⊢ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧 ∩ 𝐼)) |
21 | | sseq2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 ∩ 𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 ↔ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ (𝑧 ∩ 𝐼))) |
22 | 20, 21 | syl5ibr 235 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧 → (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
23 | 22 | reximdv 2999 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑧 ∩ 𝐼) → (∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
24 | 19, 23 | imim12d 79 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑧 ∩ 𝐼) → ((𝐶 ∈ 𝑧 → ∃𝑐 ∈ ℝ+ X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ⊆ 𝑧) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))) |
25 | 15, 24 | syl5com 31 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑅 → (𝑣 = (𝑧 ∩ 𝐼) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣))) |
26 | 25 | rexlimiv 3009 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑅 𝑣 = (𝑧 ∩ 𝐼) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
27 | 12, 26 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝑅 ↾t 𝐼) → (𝐶 ∈ 𝑣 → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) |
28 | 27 | imp 444 |
. . . . . . . 8
⊢ ((𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣)) → ∃𝑐 ∈ ℝ+ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) |
30 | | resttop 20774 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝐼 ∈ V) → (𝑅 ↾t 𝐼) ∈ Top) |
31 | 7, 10, 30 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑅 ↾t 𝐼) ∈ Top |
32 | | reex 9906 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
33 | | unitssre 12190 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
⊆ ℝ |
34 | | mapss 7786 |
. . . . . . . . . . . . . 14
⊢ ((ℝ
∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1)
↑𝑚 (1...𝑁)) ⊆ (ℝ
↑𝑚 (1...𝑁))) |
35 | 32, 33, 34 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ ((0[,]1)
↑𝑚 (1...𝑁)) ⊆ (ℝ
↑𝑚 (1...𝑁)) |
36 | 8, 35 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ 𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁)) |
37 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) ∈
V |
38 | | uniretop 22376 |
. . . . . . . . . . . . . . 15
⊢ ℝ =
∪ (topGen‘ran (,)) |
39 | 1, 38 | ptuniconst 21211 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑁) ∈ V
∧ (topGen‘ran (,)) ∈ Top) → (ℝ
↑𝑚 (1...𝑁)) = ∪ 𝑅) |
40 | 37, 3, 39 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (ℝ
↑𝑚 (1...𝑁)) = ∪ 𝑅 |
41 | 40 | restuni 20776 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ
↑𝑚 (1...𝑁))) → 𝐼 = ∪ (𝑅 ↾t 𝐼)) |
42 | 7, 36, 41 | mp2an 704 |
. . . . . . . . . . 11
⊢ 𝐼 = ∪
(𝑅 ↾t
𝐼) |
43 | 42 | eltopss 20537 |
. . . . . . . . . 10
⊢ (((𝑅 ↾t 𝐼) ∈ Top ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → 𝑣 ⊆ 𝐼) |
44 | 31, 43 | mpan 702 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝑅 ↾t 𝐼) → 𝑣 ⊆ 𝐼) |
45 | 44 | sselda 3568 |
. . . . . . . 8
⊢ ((𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣) → 𝐶 ∈ 𝐼) |
46 | | 2rp 11713 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
47 | | rpdivcl 11732 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ+ ∧ 𝑐 ∈ ℝ+) → (2 /
𝑐) ∈
ℝ+) |
48 | 46, 47 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ ℝ+
→ (2 / 𝑐) ∈
ℝ+) |
49 | 48 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ (2 / 𝑐) ∈
ℝ) |
50 | | ceicl 12504 |
. . . . . . . . . . . . . . 15
⊢ ((2 /
𝑐) ∈ ℝ →
-(⌊‘-(2 / 𝑐))
∈ ℤ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈ ℤ) |
52 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ 0 ∈ ℝ) |
53 | 51 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈ ℝ) |
54 | 48 | rpgt0d 11751 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ 0 < (2 / 𝑐)) |
55 | | ceige 12506 |
. . . . . . . . . . . . . . . 16
⊢ ((2 /
𝑐) ∈ ℝ → (2
/ 𝑐) ≤
-(⌊‘-(2 / 𝑐))) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℝ+
→ (2 / 𝑐) ≤
-(⌊‘-(2 / 𝑐))) |
57 | 52, 49, 53, 54, 56 | ltletrd 10076 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ℝ+
→ 0 < -(⌊‘-(2 / 𝑐))) |
58 | | elnnz 11264 |
. . . . . . . . . . . . . 14
⊢
(-(⌊‘-(2 / 𝑐)) ∈ ℕ ↔ (-(⌊‘-(2
/ 𝑐)) ∈ ℤ ∧
0 < -(⌊‘-(2 / 𝑐)))) |
59 | 51, 57, 58 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈ ℕ) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) →
(ℤ≥‘𝑖) =
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) |
61 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → (1 / 𝑖) = (1 / -(⌊‘-(2 /
𝑐)))) |
62 | 61 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) = ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐))))) |
63 | 62 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → ((((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
64 | 63 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
65 | 60, 64 | rexeqbidv 3130 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = -(⌊‘-(2 / 𝑐)) → (∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) ↔ ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
66 | 65 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢
(-(⌊‘-(2 / 𝑐)) ∈ ℕ → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
67 | 59, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ℝ+
→ (∀𝑖 ∈
ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
68 | 67 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) →
(∀𝑖 ∈ ℕ
∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))))) |
69 | | uznnssnn 11611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(-(⌊‘-(2 / 𝑐)) ∈ ℕ →
(ℤ≥‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ) |
70 | 59, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (ℤ≥‘-(⌊‘-(2 / 𝑐))) ⊆ ℕ) |
71 | 70 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ (𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ)) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) → (𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))) → 𝑘 ∈ ℕ)) |
73 | 72 | imdistani 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
ℕ)) |
74 | 59 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 ∈ ℝ+
→ -(⌊‘-(2 / 𝑐)) ∈
ℝ+) |
75 | 48, 74 | lerecd 11767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ ((2 / 𝑐) ≤
-(⌊‘-(2 / 𝑐))
↔ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐)))) |
76 | 56, 75 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ≤ (1 / (2 / 𝑐))) |
77 | | rpcn 11717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℂ) |
78 | | rpne0 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ≠
0) |
79 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ∈
ℂ |
80 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 2 ≠
0 |
81 | | recdiv 10610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (𝑐 ∈ ℂ ∧ 𝑐 ≠ 0)) → (1 / (2 / 𝑐)) = (𝑐 / 2)) |
82 | 79, 80, 81 | mpanl12 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑐 ∈ ℂ ∧ 𝑐 ≠ 0) → (1 / (2 / 𝑐)) = (𝑐 / 2)) |
83 | 77, 78, 82 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (1 / (2 / 𝑐)) =
(𝑐 / 2)) |
84 | 76, 83 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) |
85 | 84 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) |
86 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐶 ∈ ((0[,]1)
↑𝑚 (1...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1)) |
87 | 86, 8 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐶 ∈ 𝐼 → 𝐶:(1...𝑁)⟶(0[,]1)) |
88 | 87 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1)) |
89 | 88 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ (0[,]1)) |
90 | 33, 89 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℝ) |
91 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑) |
92 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ) |
93 | 91, 92 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
94 | | poimirlem30.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 𝐺:ℕ⟶((ℕ0
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
95 | 94 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ((ℕ0
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
96 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐺‘𝑘) ∈ ((ℕ0
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
97 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑𝑚 (1...𝑁)) → (1st ‘(𝐺‘𝑘)):(1...𝑁)⟶ℕ0) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶ℕ0) |
99 | 98 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈
ℕ0) |
100 | 99 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈ ℝ) |
101 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
102 | 100, 101 | nndivred 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
103 | 93, 102 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
104 | 90, 103 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) ∈ ℝ) |
105 | 104 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) ∈ ℂ) |
106 | 105 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ) |
107 | 59 | nnrecred 10943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ∈ ℝ) |
108 | 107 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ) |
109 | | rphalfcl 11734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ ℝ+
→ (𝑐 / 2) ∈
ℝ+) |
110 | 109 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ (𝑐 / 2) ∈
ℝ) |
111 | 110 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝑐 / 2) ∈ ℝ) |
112 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ ∧ (1 /
-(⌊‘-(2 / 𝑐)))
∈ ℝ ∧ (𝑐 /
2) ∈ ℝ) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 /
-(⌊‘-(2 / 𝑐)))
≤ (𝑐 / 2)) →
(abs‘((𝐶‘𝑚) − (((1st
‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2))) |
113 | 106, 108,
111, 112 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) ∧ (1 /
-(⌊‘-(2 / 𝑐)))
≤ (𝑐 / 2)) →
(abs‘((𝐶‘𝑚) − (((1st
‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2))) |
114 | 85, 113 | mpan2d 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝐶 ∈ 𝐼) → 𝜑) |
117 | 70 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℕ) |
118 | 116, 117 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ (𝑐 ∈ ℝ+ ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))))) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
119 | 118 | anassrs 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
120 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 1 ∈
ℝ |
121 | | snssi 4280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (1 ∈
ℝ → {1} ⊆ ℝ) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ {1}
⊆ ℝ |
123 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 0 ∈
ℝ |
124 | | snssi 4280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (0 ∈
ℝ → {0} ⊆ ℝ) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ {0}
⊆ ℝ |
126 | 122, 125 | unssi 3750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ({1}
∪ {0}) ⊆ ℝ |
127 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 1 ∈
V |
128 | 127 | fconst 6004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2nd
‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} |
129 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 0 ∈
V |
130 | 129 | fconst 6004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0} |
131 | 128, 130 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2nd
‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} ∧
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}) |
132 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐺‘𝑘) ∈ ((ℕ0
↑𝑚 (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 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(2nd ‘(𝐺‘𝑘)) ∈ V |
135 | | f1oeq1 6040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑓 = (2nd ‘(𝐺‘𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))) |
136 | 134, 135 | elab 3319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((2nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
137 | 133, 136 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
138 | | dff1o3 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(𝐺‘𝑘)))) |
139 | 138 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(𝐺‘𝑘))) |
140 | | imain 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 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 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0) |
143 | 142 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) |
144 | 143 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1)) |
145 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
147 | 146 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺‘𝑘)) “ ∅)) |
148 | | ima0 5400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((2nd ‘(𝐺‘𝑘)) “ ∅) =
∅ |
149 | 147, 148 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅) |
150 | 141, 149 | sylan9req 2665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅) |
151 | | fun 5979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 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 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
153 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) |
154 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
155 | 142, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ) |
156 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ℕ =
(ℤ≥‘1) |
157 | 155, 156 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
158 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝑗)) |
159 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
160 | 157, 158,
159 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
161 | 160 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))) |
162 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁)) |
163 | | foima 6033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((2nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = (1...𝑁)) |
164 | 137, 162,
163 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐺‘𝑘)) “ (1...𝑁)) = (1...𝑁)) |
165 | 161, 164 | sylan9req 2665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑗 ∈ (0...𝑁) ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((2nd
‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
166 | 165 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
167 | 153, 166 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
168 | 167 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})) |
170 | 169 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ({1} ∪ {0})) |
171 | 126, 170 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℝ) |
172 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
173 | 171, 172 | nndivred 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ) |
174 | 173 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
175 | 174 | absnegd 14036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0})) |
180 | | nnrecre 10934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
181 | | nnrp 11718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
182 | 181 | rpreccld 11758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
183 | 182 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ 𝑘)) |
184 | 180, 183 | absidd 14009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑘 ∈ ℕ →
(abs‘(1 / 𝑘)) = (1 /
𝑘)) |
185 | 117, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) = (1 / 𝑘)) |
186 | 117 | nnrecred 10943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ∈ ℝ) |
187 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ) |
188 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (𝑐 / 2) ∈ ℝ) |
189 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘) |
190 | 189 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ≤ 𝑘) |
191 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈
ℕ) |
192 | 191 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → -(⌊‘-(2 / 𝑐)) ∈
ℝ+) |
193 | 117 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → 𝑘 ∈ ℝ+) |
194 | 192, 193 | lerecd 11767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (-(⌊‘-(2 / 𝑐)) ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐))))) |
195 | 190, 194 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (1 / -(⌊‘-(2 / 𝑐)))) |
196 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / -(⌊‘-(2 / 𝑐))) ≤ (𝑐 / 2)) |
197 | 186, 187,
188, 195, 196 | letrd 10073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (1 / 𝑘) ≤ (𝑐 / 2)) |
198 | 185, 197 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (abs‘(1 / 𝑘)) ≤ (𝑐 / 2)) |
199 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 1) |
200 | 199 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} → ((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) = (1 / 𝑘)) |
201 | 200 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(1 / 𝑘))) |
202 | 201 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} →
((abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(1 / 𝑘)) ≤ (𝑐 / 2))) |
203 | 198, 202 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
204 | 109 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 ∈ ℝ+
→ 0 ≤ (𝑐 /
2)) |
205 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
206 | | nnne0 10930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
207 | 205, 206 | div0d 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑘 ∈ ℕ → (0 /
𝑘) = 0) |
208 | 207 | abs00bd 13879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑘 ∈ ℕ →
(abs‘(0 / 𝑘)) =
0) |
209 | 208 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑘 ∈ ℕ →
((abs‘(0 / 𝑘)) ≤
(𝑐 / 2) ↔ 0 ≤
(𝑐 / 2))) |
210 | 209 | biimparc 503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((0 ≤
(𝑐 / 2) ∧ 𝑘 ∈ ℕ) →
(abs‘(0 / 𝑘)) ≤
(𝑐 / 2)) |
211 | 204, 210 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
→ (abs‘(0 / 𝑘))
≤ (𝑐 /
2)) |
212 | 117, 211 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (abs‘(0 / 𝑘)) ≤ (𝑐 / 2)) |
213 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = 0) |
214 | 213 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} → ((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) = (0 / 𝑘)) |
215 | 214 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = (abs‘(0 / 𝑘))) |
216 | 215 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} →
((abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2) ↔ (abs‘(0 / 𝑘)) ≤ (𝑐 / 2))) |
217 | 212, 216 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → ((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0} →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
218 | 203, 217 | jaod 394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑐 ∈ ℝ+
∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
219 | 218 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {1} ∨ (((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ {0}) →
(abs‘((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2))) |
220 | 219 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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))) |
221 | 179, 220 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) |
222 | 176, 221 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ≤ (𝑐 / 2)) |
223 | 73, 106 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) ∈ ℝ) |
224 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) → 𝜑) |
225 | 224 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝜑 ∧ 𝑘 ∈ ℕ)) |
226 | 173 | renegcld 10336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ) |
227 | 225, 226 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℝ) |
228 | 227 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
229 | 228 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) |
230 | 73, 229 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) |
231 | 110, 110 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ ((𝑐 / 2) ∈
ℝ ∧ (𝑐 / 2)
∈ ℝ)) |
232 | 231 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) ∈ ℝ ∧ (𝑐 / 2) ∈
ℝ)) |
233 | | ltleadd 10390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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)))) |
234 | 223, 230,
232, 233 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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)))) |
235 | 222, 234 | mpan2d 706 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (𝑐 / 2) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
236 | 105, 228 | abstrid 14043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ≤ ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
237 | 104, 227 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℝ) |
238 | 237 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) ∈ ℂ) |
239 | 238 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ) |
240 | 106, 229 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) ∈ ℝ) |
241 | 110, 110 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ ℝ+
→ ((𝑐 / 2) + (𝑐 / 2)) ∈
ℝ) |
242 | 241 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝑐 / 2) + (𝑐 / 2)) ∈ ℝ) |
243 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))) |
244 | 239, 240,
242, 243 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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)))) |
245 | 236, 244 | mpand 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) + (abs‘-((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
246 | 73, 245 | 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)))) |
247 | 115, 235,
246 | 3syld 58 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))) → (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
248 | 100 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈ ℝ) |
249 | 248, 171 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) ∈ ℝ) |
250 | 249, 172 | nndivred 10946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) |
251 | 119, 250 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) |
252 | 247, 251 | jctild 564 |
. . . . . . . . . . . . . . . . . . . . . . 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))))) |
253 | 252 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))) → (((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
254 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
ℕ)) |
255 | 87 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → 𝐶:(1...𝑁)⟶(0[,]1)) |
256 | 255 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ (0[,]1)) |
257 | 33, 256 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℝ) |
258 | 74 | rpreccld 11758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ+) |
259 | 258 | rpxrd 11749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ ℝ+
→ (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ*) |
260 | 259 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (1 / -(⌊‘-(2 / 𝑐))) ∈
ℝ*) |
261 | 13 | rexmet 22402 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
262 | | elbl 22003 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝐶‘𝑚) ∈ ℝ ∧ (1 /
-(⌊‘-(2 / 𝑐)))
∈ ℝ*) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))))) |
263 | 261, 262 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ (1 /
-(⌊‘-(2 / 𝑐)))
∈ ℝ*) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))))) |
264 | 257, 260,
263 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))))) |
265 | | elmapfn 7766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((1st ‘(𝐺‘𝑘)) ∈ (ℕ0
↑𝑚 (1...𝑁)) → (1st ‘(𝐺‘𝑘)) Fn (1...𝑁)) |
266 | 95, 96, 265 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)) Fn (1...𝑁)) |
267 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑘 ∈ V |
268 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
269 | 267, 268 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
270 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑁) ∈ Fin) |
271 | | inidm 3784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
272 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) = ((1st ‘(𝐺‘𝑘))‘𝑚)) |
273 | 267 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘) |
274 | 273 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘) |
275 | 266, 269,
270, 270, 271, 272, 274 | ofval 6804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) |
276 | 275 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) |
277 | 224, 276 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) |
278 | 224, 102 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
279 | 13 | remetdval 22400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ (((1st
‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)))) |
280 | 257, 278,
279 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) = (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)))) |
281 | 277, 280 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)))) |
282 | 281 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐))) ↔ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐))))) |
283 | 282 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < (1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st
‘(𝐺‘𝑘)) ∘𝑓 /
((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))) |
284 | 264, 283 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))) |
285 | 254, 284 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ (abs‘((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘))) < (1 / -(⌊‘-(2 / 𝑐)))))) |
286 | | rpxr 11716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ ℝ+
→ 𝑐 ∈
ℝ*) |
287 | 286 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 ∈ ℝ*) |
288 | | elbl 22003 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝐶‘𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) →
(((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐))) |
289 | 261, 288 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ 𝑐 ∈ ℝ*) →
(((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐))) |
290 | 90, 287, 289 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐))) |
291 | | elun 3715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ ({1} ∪ {0}) ↔
(𝑧 ∈ {1} ∨ 𝑧 ∈ {0})) |
292 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑣 ∈ (0..^𝑘) → (𝑣 + 1) ∈ (0...𝑘)) |
293 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈ {1} → 𝑧 = 1) |
294 | 293 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 ∈ {1} → (𝑣 + 𝑧) = (𝑣 + 1)) |
295 | 294 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ {1} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 1) ∈ (0...𝑘))) |
296 | 292, 295 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {1} → (𝑣 + 𝑧) ∈ (0...𝑘))) |
297 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℕ0) |
298 | 297 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ ℂ) |
299 | 298 | addid1d 10115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) = 𝑣) |
300 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑣 ∈ (0..^𝑘) → 𝑣 ∈ (0...𝑘)) |
301 | 299, 300 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑣 ∈ (0..^𝑘) → (𝑣 + 0) ∈ (0...𝑘)) |
302 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈ {0} → 𝑧 = 0) |
303 | 302 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 ∈ {0} → (𝑣 + 𝑧) = (𝑣 + 0)) |
304 | 303 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ {0} → ((𝑣 + 𝑧) ∈ (0...𝑘) ↔ (𝑣 + 0) ∈ (0...𝑘))) |
305 | 301, 304 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ {0} → (𝑣 + 𝑧) ∈ (0...𝑘))) |
306 | 296, 305 | jaod 394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑣 ∈ (0..^𝑘) → ((𝑧 ∈ {1} ∨ 𝑧 ∈ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘))) |
307 | 291, 306 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑣 ∈ (0..^𝑘) → (𝑧 ∈ ({1} ∪ {0}) → (𝑣 + 𝑧) ∈ (0...𝑘))) |
308 | 307 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0})) → (𝑣 + 𝑧) ∈ (0...𝑘)) |
309 | 308 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0..^𝑘) ∧ 𝑧 ∈ ({1} ∪ {0}))) → (𝑣 + 𝑧) ∈ (0...𝑘)) |
310 | | dffn3 5967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((1st ‘(𝐺‘𝑘)) Fn (1...𝑁) ↔ (1st ‘(𝐺‘𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺‘𝑘))) |
311 | 266, 310 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶ran (1st ‘(𝐺‘𝑘))) |
312 | | poimirlem30.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1st
‘(𝐺‘𝑘)) ⊆ (0..^𝑘)) |
313 | 311, 312 | fssd 5970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘)) |
314 | 313 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘)) |
315 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin) |
316 | 309, 314,
169, 315, 315, 271 | off 6810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘)) |
317 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘) → ((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁)) |
318 | 316, 317 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) Fn (1...𝑁)) |
319 | 267, 268 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
320 | 266 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺‘𝑘)) Fn (1...𝑁)) |
321 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}) →
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
322 | 169, 321 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
323 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) = ((1st ‘(𝐺‘𝑘))‘𝑚)) |
324 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) = (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) |
325 | 320, 322,
315, 315, 271, 323, 324 | ofval 6804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑚) = (((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚))) |
326 | 273 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑚) = 𝑘) |
327 | 318, 319,
315, 315, 271, 325, 326 | ofval 6804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) |
328 | 327 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)) |
329 | 225, 328 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ↔ ((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ)) |
330 | 327 | adantl3r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) = ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) |
331 | 330 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) |
332 | 87 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐶:(1...𝑁)⟶(0[,]1)) |
333 | 332 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ (0[,]1)) |
334 | 33, 333 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℝ) |
335 | 250 | adantl3r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) |
336 | 13 | remetdval 22400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐶‘𝑚) ∈ ℝ ∧ ((((1st
‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))) |
337 | 334, 335,
336 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (abs‘((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)))) |
338 | 248 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((1st ‘(𝐺‘𝑘))‘𝑚) ∈ ℂ) |
339 | 171 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) ∈ ℂ) |
340 | 205 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ ℂ) |
341 | 206 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ≠ 0) |
342 | 338, 339,
340, 341 | divdird 10718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
343 | 102 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℂ) |
344 | 343 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℂ) |
345 | 344, 174 | subnegd 10278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)) = ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) + ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
346 | 342, 345 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) = ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
347 | 346 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
348 | 347 | adantl3r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
349 | 334 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (𝐶‘𝑚) ∈ ℂ) |
350 | 102 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
351 | 350 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℝ) |
352 | 351 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) ∈ ℂ) |
353 | 174 | adantl3r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
354 | 353 | negcld 10258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → -((((((2nd
‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘) ∈ ℂ) |
355 | 349, 352,
354 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘) − -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) = (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
356 | 348, 355 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘)) = (((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) |
357 | 356 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (abs‘((𝐶‘𝑚) − ((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘))) = (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
358 | 331, 337,
357 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
359 | 358 | adantl3r 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) = (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘)))) |
360 | 77 | 2halvesd 11155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ ℝ+
→ ((𝑐 / 2) + (𝑐 / 2)) = 𝑐) |
361 | 360 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ ℝ+
→ 𝑐 = ((𝑐 / 2) + (𝑐 / 2))) |
362 | 361 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑐 = ((𝑐 / 2) + (𝑐 / 2))) |
363 | 359, 362 | breq12d 4596 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐 ↔ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2)))) |
364 | 329, 363 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ℝ ∧ ((𝐶‘𝑚)((abs ∘ − ) ↾ (ℝ
× ℝ))((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚)) < 𝑐) ↔ (((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
365 | 290, 364 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
366 | 73, 365 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ (((((1st ‘(𝐺‘𝑘))‘𝑚) + (((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚)) / 𝑘) ∈ ℝ ∧ (abs‘(((𝐶‘𝑚) − (((1st ‘(𝐺‘𝑘))‘𝑚) / 𝑘)) + -((((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑚) / 𝑘))) < ((𝑐 / 2) + (𝑐 / 2))))) |
367 | 253, 285,
366 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑚 ∈ (1...𝑁)) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐))) |
368 | 367 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐))) |
369 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ) |
370 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℕ0) |
371 | 370 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ (0...𝑘) → 𝑣 ∈ ℝ) |
372 | | nndivre 10933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ) |
373 | 371, 372 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ ℝ) |
374 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ (0...𝑘) → 0 ≤ 𝑣) |
375 | 371, 374 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑣 ∈ (0...𝑘) → (𝑣 ∈ ℝ ∧ 0 ≤ 𝑣)) |
376 | 181 | rpregt0d 11754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
377 | | divge0 10771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑣 ∈ ℝ ∧ 0 ≤
𝑣) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝑣 / 𝑘)) |
378 | 375, 376,
377 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑣 / 𝑘)) |
379 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ (0...𝑘) → 𝑣 ≤ 𝑘) |
380 | 379 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ≤ 𝑘) |
381 | 371 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑣 ∈ ℝ) |
382 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈
ℝ) |
383 | 181 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
384 | 381, 382,
383 | ledivmuld 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ (𝑘 · 1))) |
385 | 205 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘) |
386 | 385 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ ℕ → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣 ≤ 𝑘)) |
387 | 386 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 ≤ (𝑘 · 1) ↔ 𝑣 ≤ 𝑘)) |
388 | 384, 387 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑣 / 𝑘) ≤ 1 ↔ 𝑣 ≤ 𝑘)) |
389 | 380, 388 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ≤ 1) |
390 | 123, 120 | elicc2i 12110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 / 𝑘) ∈ (0[,]1) ↔ ((𝑣 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑣 / 𝑘) ∧ (𝑣 / 𝑘) ≤ 1)) |
391 | 373, 378,
389, 390 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑣 / 𝑘) ∈ (0[,]1)) |
392 | 391 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑣 / 𝑘) ∈ (0[,]1)) |
393 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ {𝑘} → 𝑧 = 𝑘) |
394 | 393 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) = (𝑣 / 𝑘)) |
395 | 394 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ {𝑘} → ((𝑣 / 𝑧) ∈ (0[,]1) ↔ (𝑣 / 𝑘) ∈ (0[,]1))) |
396 | 392, 395 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ ∧ 𝑣 ∈ (0...𝑘)) → (𝑧 ∈ {𝑘} → (𝑣 / 𝑧) ∈ (0[,]1))) |
397 | 396 | impr 647 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℕ ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1)) |
398 | 369, 397 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑣 ∈ (0...𝑘) ∧ 𝑧 ∈ {𝑘})) → (𝑣 / 𝑧) ∈ (0[,]1)) |
399 | 267 | fconst 6004 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑁) ×
{𝑘}):(1...𝑁)⟶{𝑘} |
400 | 399 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}) |
401 | 398, 316,
400, 315, 315, 271 | off 6810 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
402 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1) → (((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁)) |
403 | 401, 402 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁)) |
404 | 119, 403 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁)) |
405 | 368, 404 | jctild 564 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)))) |
406 | 8 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑𝑚 (1...𝑁))) |
407 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0[,]1)
∈ V |
408 | 407, 37 | elmap 7772 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑𝑚 (1...𝑁)) ↔ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
409 | 406, 408 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
410 | 401, 409 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼) |
411 | 119, 410 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼) |
412 | 405, 411 | jctird 565 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))) |
413 | | elin 3758 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)) |
414 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ V |
415 | 414 | elixp 7801 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ↔ ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐))) |
416 | 415 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∧ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼) ↔ (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)) |
417 | 413, 416 | bitri 263 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ↔ (((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) Fn (1...𝑁) ∧ ∀𝑚 ∈ (1...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐)) ∧ (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)) |
418 | 412, 417 | syl6ibr 241 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼))) |
419 | | ssel 3562 |
. . . . . . . . . . . . . . . . . 18
⊢ ((X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)) |
420 | 419 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)) |
421 | 418, 420 | syl6 34 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))) |
422 | 421 | impd 446 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) ∧ 𝑗 ∈ (0...𝑁)) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → (((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)) |
423 | 422 | ralrimdva 2952 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → ((∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) ∧ (X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣) → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣)) |
424 | 423 | expd 451 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣))) |
425 | | poimirlem30.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) |
426 | 425 | 3exp2 1277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ◡ ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋)))) |
427 | 426 | imp43 619 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) |
428 | | r19.29 3054 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑗 ∈
(0...𝑁)(((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑗 ∈ (0...𝑁)((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋)) |
429 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) → (𝐹‘𝑧) = (𝐹‘(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})))) |
430 | 429 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)) |
431 | | poimirlem30.x |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑋 = ((𝐹‘(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) |
432 | 430, 431 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = 𝑋) |
433 | 432 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) → (0𝑟((𝐹‘𝑧)‘𝑛) ↔ 0𝑟𝑋)) |
434 | 433 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) |
435 | 434 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑗 ∈
(0...𝑁)((((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ 0𝑟𝑋) → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) |
436 | 428, 435 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑗 ∈
(0...𝑁)(((1st
‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 ∧ ∃𝑗 ∈ (0...𝑁)0𝑟𝑋) → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) |
437 | 436 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑗 ∈
(0...𝑁)0𝑟𝑋 → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
438 | 427, 437 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
439 | 438 | ralrimdvva 2957 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
440 | 117, 439 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑐 ∈ ℝ+ ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐))))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
441 | 440 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
442 | 441 | adantllr 751 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑗 ∈ (0...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 +
((((2nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
∘𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
443 | 424, 442 | syl6d 73 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))) → (∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
444 | 443 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) →
(∃𝑘 ∈
(ℤ≥‘-(⌊‘-(2 / 𝑐)))∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / -(⌊‘-(2 / 𝑐)))) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
445 | 68, 444 | syld 46 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) →
(∀𝑖 ∈ ℕ
∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ((X𝑚 ∈ (1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
446 | 445 | com23 84 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ 𝑐 ∈ ℝ+) → ((X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
447 | 446 | impr 647 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ 𝐼) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
448 | 45, 447 | sylanl2 681 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣)) ∧ (𝑐 ∈ ℝ+ ∧ (X𝑚 ∈
(1...𝑁)((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑐) ∩ 𝐼) ⊆ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
449 | 29, 448 | rexlimddv 3017 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ (𝑅 ↾t 𝐼) ∧ 𝐶 ∈ 𝑣)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
450 | 449 | expr 641 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → (𝐶 ∈ 𝑣 → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
451 | 450 | com23 84 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → (𝐶 ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
452 | | r19.21v 2943 |
. . . 4
⊢
(∀𝑛 ∈
(1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) ↔ (𝐶 ∈ 𝑣 → ∀𝑛 ∈ (1...𝑁)∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
453 | 451, 452 | syl6ibr 241 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑅 ↾t 𝐼)) → (∀𝑖 ∈ ℕ ∃𝑘 ∈ (ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
454 | 453 | ralrimdva 2952 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑣 ∈ (𝑅 ↾t 𝐼)∀𝑛 ∈ (1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |
455 | | ralcom 3079 |
. 2
⊢
(∀𝑣 ∈
(𝑅 ↾t
𝐼)∀𝑛 ∈ (1...𝑁)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
456 | 454, 455 | syl6ib 240 |
1
⊢ (𝜑 → (∀𝑖 ∈ ℕ ∃𝑘 ∈
(ℤ≥‘𝑖)∀𝑚 ∈ (1...𝑁)(((1st ‘(𝐺‘𝑘)) ∘𝑓 / ((1...𝑁) × {𝑘}))‘𝑚) ∈ ((𝐶‘𝑚)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))(1 / 𝑖)) → ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝐶 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛)))) |