Step | Hyp | Ref
| Expression |
1 | | cvmliftlem.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | nnuz 12630 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | eleqtrdi 2850 |
. . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
4 | | eluzfz2 13273 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
6 | | eleq1 2827 |
. . . . . 6
⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁))) |
7 | | oveq2 7292 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (1...𝑦) = (1...1)) |
8 | | 1z 12359 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
9 | | fzsn 13307 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (1...1) = {1}) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (1...1) =
{1} |
11 | 7, 10 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (1...𝑦) = {1}) |
12 | 11 | iuneq1d 4952 |
. . . . . . . . 9
⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘)) |
13 | | 1ex 10980 |
. . . . . . . . . 10
⊢ 1 ∈
V |
14 | | fveq2 6783 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1)) |
15 | 13, 14 | iunxsn 5021 |
. . . . . . . . 9
⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1) |
16 | 12, 15 | eqtrdi 2795 |
. . . . . . . 8
⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1)) |
17 | | oveq1 7291 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁)) |
18 | 17 | oveq2d 7300 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁))) |
19 | 18 | oveq2d 7300 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,](1 / 𝑁)))) |
20 | 19 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝑦 = 1 → ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶)) |
21 | 16, 20 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑦 = 1 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶))) |
22 | 16 | coeq2d 5774 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1))) |
23 | 18 | reseq2d 5894 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁)))) |
24 | 22, 23 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑦 = 1 → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))) |
25 | 21, 24 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = 1 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))) |
26 | 6, 25 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))) |
27 | 26 | imbi2d 341 |
. . . 4
⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))) |
28 | | eleq1 2827 |
. . . . . 6
⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁))) |
29 | | oveq2 7292 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛)) |
30 | 29 | iuneq1d 4952 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
31 | | oveq1 7291 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁)) |
32 | 31 | oveq2d 7300 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁))) |
33 | 32 | oveq2d 7300 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,](𝑛 / 𝑁)))) |
34 | 33 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶)) |
35 | 30, 34 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑦 = 𝑛 → (∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶))) |
36 | 30 | coeq2d 5774 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘))) |
37 | 32 | reseq2d 5894 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) |
38 | 36, 37 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑦 = 𝑛 → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) |
39 | 35, 38 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = 𝑛 → ((∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) |
40 | 28, 39 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))) |
41 | 40 | imbi2d 341 |
. . . 4
⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))) |
42 | | eleq1 2827 |
. . . . . 6
⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁))) |
43 | | oveq2 7292 |
. . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1))) |
44 | 43 | iuneq1d 4952 |
. . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) |
45 | | oveq1 7291 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁)) |
46 | 45 | oveq2d 7300 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁))) |
47 | 46 | oveq2d 7300 |
. . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁)))) |
48 | 47 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
49 | 44, 48 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑦 = (𝑛 + 1) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))) |
50 | 44 | coeq2d 5774 |
. . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))) |
51 | 46 | reseq2d 5894 |
. . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))) |
52 | 50, 51 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑦 = (𝑛 + 1) → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))) |
53 | 49, 52 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = (𝑛 + 1) → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))) |
54 | 42, 53 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))) |
55 | 54 | imbi2d 341 |
. . . 4
⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))) |
56 | | eleq1 2827 |
. . . . . 6
⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁))) |
57 | | oveq2 7292 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁)) |
58 | 57 | iuneq1d 4952 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)) |
59 | | cvmliftlem.k |
. . . . . . . . 9
⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘) |
60 | 58, 59 | eqtr4di 2797 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾) |
61 | | oveq1 7291 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁)) |
62 | 61 | oveq2d 7300 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁))) |
63 | 62 | oveq2d 7300 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,](𝑁 / 𝑁)))) |
64 | 63 | oveq1d 7299 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶)) |
65 | 60, 64 | eleq12d 2834 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → (∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶))) |
66 | 60 | coeq2d 5774 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾)) |
67 | 62 | reseq2d 5894 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))) |
68 | 66, 67 | eqeq12d 2755 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))) |
69 | 65, 68 | anbi12d 631 |
. . . . . 6
⊢ (𝑦 = 𝑁 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))) |
70 | 56, 69 | imbi12d 345 |
. . . . 5
⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))) |
71 | 70 | imbi2d 341 |
. . . 4
⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))) |
72 | | eluzfz1 13272 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
73 | 3, 72 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈ (1...𝑁)) |
74 | | cvmliftlem.1 |
. . . . . . . . 9
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
75 | | cvmliftlem.b |
. . . . . . . . 9
⊢ 𝐵 = ∪
𝐶 |
76 | | cvmliftlem.x |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
77 | | cvmliftlem.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
78 | | cvmliftlem.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
79 | | cvmliftlem.p |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
80 | | cvmliftlem.e |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) |
81 | | cvmliftlem.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪
𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) |
82 | | cvmliftlem.a |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) |
83 | | cvmliftlem.l |
. . . . . . . . 9
⊢ 𝐿 = (topGen‘ran
(,)) |
84 | | cvmliftlem.q |
. . . . . . . . 9
⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})) |
85 | | eqid 2739 |
. . . . . . . . 9
⊢ (((1
− 1) / 𝑁)[,](1 /
𝑁)) = (((1 − 1) /
𝑁)[,](1 / 𝑁)) |
86 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85 | cvmliftlem8 33263 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶)) |
87 | 73, 86 | mpdan 684 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶)) |
88 | | 1m1e0 12054 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
89 | 88 | oveq1i 7294 |
. . . . . . . . . . 11
⊢ ((1
− 1) / 𝑁) = (0 /
𝑁) |
90 | 1 | nncnd 11998 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
91 | 1 | nnne0d 12032 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ≠ 0) |
92 | 90, 91 | div0d 11759 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 / 𝑁) = 0) |
93 | 89, 92 | eqtrid 2791 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 − 1) / 𝑁) = 0) |
94 | 93 | oveq1d 7299 |
. . . . . . . . 9
⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁))) |
95 | 94 | oveq2d 7300 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾t (0[,](1 / 𝑁)))) |
96 | 95 | oveq1d 7299 |
. . . . . . 7
⊢ (𝜑 → ((𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶)) |
97 | 87, 96 | eleqtrd 2842 |
. . . . . 6
⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶)) |
98 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁)) |
99 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85 | cvmliftlem7 33262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) /
𝑁)) ∈ (◡𝐹 “ {(𝐺‘((1 − 1) / 𝑁))})) |
100 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99 | cvmliftlem6 33261 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) |
101 | 73, 100 | mpdan 684 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) |
102 | 101 | simprd 496 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))) |
103 | 94 | reseq2d 5894 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁)))) |
104 | 102, 103 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))) |
105 | 97, 104 | jca 512 |
. . . . 5
⊢ (𝜑 → ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))) |
106 | 105 | a1d 25 |
. . . 4
⊢ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))) |
107 | | elnnuz 12631 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
108 | 107 | biimpi 215 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
109 | 108 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
110 | | peano2fzr 13278 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁)) |
111 | 110 | ex 413 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘1) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁))) |
112 | 109, 111 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁))) |
113 | 112 | imim1d 82 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))) |
114 | | cvmliftlem10.1 |
. . . . . . 7
⊢ (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) |
115 | | eqid 2739 |
. . . . . . . . 9
⊢ ∪ (𝐿
↾t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁))) |
116 | | 0re 10986 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
117 | 114 | simplbi 498 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) |
119 | 118 | simprd 496 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ (1...𝑁)) |
120 | | elfznn 13294 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ) |
122 | 121 | nnred 11997 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ) |
123 | 1 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ) |
124 | 122, 123 | nndivred 12036 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ) |
125 | | iccssre 13170 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ ((𝑛 +
1) / 𝑁) ∈ ℝ)
→ (0[,]((𝑛 + 1) /
𝑁)) ⊆
ℝ) |
126 | 116, 124,
125 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) |
127 | 117 | simpld 495 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑛 ∈ ℕ) |
128 | 127 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ) |
129 | 128 | nnred 11997 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ) |
130 | 129, 123 | nndivred 12036 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ) |
131 | | icccld 23939 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (𝑛 /
𝑁) ∈ ℝ) →
(0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran
(,)))) |
132 | 116, 130,
131 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran
(,)))) |
133 | 83 | fveq2i 6786 |
. . . . . . . . . . 11
⊢
(Clsd‘𝐿) =
(Clsd‘(topGen‘ran (,))) |
134 | 132, 133 | eleqtrrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿)) |
135 | | ssun1 4107 |
. . . . . . . . . . 11
⊢
(0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
136 | 116 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ) |
137 | 128 | nnnn0d 12302 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ0) |
138 | 137 | nn0ge0d 12305 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛) |
139 | 123 | nnred 11997 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ) |
140 | 123 | nngt0d 12031 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁) |
141 | | divge0 11853 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁)) |
142 | 129, 138,
139, 140, 141 | syl22anc 836 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁)) |
143 | 129 | ltp1d 11914 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1)) |
144 | | ltdiv1 11848 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))) |
145 | 129, 122,
139, 140, 144 | syl112anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))) |
146 | 143, 145 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)) |
147 | 130, 124,
146 | ltled 11132 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) |
148 | | elicc2 13153 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ ((𝑛 +
1) / 𝑁) ∈ ℝ)
→ ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)))) |
149 | 116, 124,
148 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)))) |
150 | 130, 142,
147, 149 | mpbir3and 1341 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) |
151 | | iccsplit 13226 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ((𝑛 +
1) / 𝑁) ∈ ℝ
∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
152 | 136, 124,
150, 151 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
153 | 135, 152 | sseqtrrid 3975 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) |
154 | | uniretop 23935 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
155 | 83 | unieqi 4853 |
. . . . . . . . . . . 12
⊢ ∪ 𝐿 =
∪ (topGen‘ran (,)) |
156 | 154, 155 | eqtr4i 2770 |
. . . . . . . . . . 11
⊢ ℝ =
∪ 𝐿 |
157 | 156 | restcldi 22333 |
. . . . . . . . . 10
⊢
(((0[,]((𝑛 + 1) /
𝑁)) ⊆ ℝ ∧
(0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) |
158 | 126, 134,
153, 157 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) |
159 | | icccld 23939 |
. . . . . . . . . . . 12
⊢ (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran
(,)))) |
160 | 130, 124,
159 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran
(,)))) |
161 | 160, 133 | eleqtrrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿)) |
162 | | ssun2 4108 |
. . . . . . . . . . 11
⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
163 | 162, 152 | sseqtrrid 3975 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) |
164 | 156 | restcldi 22333 |
. . . . . . . . . 10
⊢
(((0[,]((𝑛 + 1) /
𝑁)) ⊆ ℝ ∧
((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) |
165 | 126, 161,
163, 164 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) |
166 | | retop 23934 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Top |
167 | 83, 166 | eqeltri 2836 |
. . . . . . . . . . 11
⊢ 𝐿 ∈ Top |
168 | 156 | restuni 22322 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))) |
169 | 167, 126,
168 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))) |
170 | 152, 169 | eqtr3d 2781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))) |
171 | 114 | simprbi 497 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) |
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) |
173 | 172 | simpld 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶)) |
174 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝐿
↾t (0[,](𝑛
/ 𝑁))) = ∪ (𝐿
↾t (0[,](𝑛
/ 𝑁))) |
175 | 174, 75 | cnf 22406 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))⟶𝐵) |
176 | 173, 175 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))⟶𝐵) |
177 | | iccssre 13170 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ (𝑛 /
𝑁) ∈ ℝ) →
(0[,](𝑛 / 𝑁)) ⊆ ℝ) |
178 | 116, 130,
177 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ) |
179 | 156 | restuni 22322 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))) |
180 | 167, 178,
179 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))) |
181 | 180 | feq2d 6595 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))⟶𝐵)) |
182 | 176, 181 | mpbird 256 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵) |
183 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) |
184 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁)) |
185 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183 | cvmliftlem7 33262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))})) |
186 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185 | cvmliftlem6 33261 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
187 | 119, 186 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
188 | 187 | simpld 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵) |
189 | 128 | nncnd 11998 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ) |
190 | | ax-1cn 10938 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
191 | | pncan 11236 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
192 | 189, 190,
191 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛) |
193 | 192 | oveq1d 7299 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁)) |
194 | 193 | oveq1d 7299 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
195 | 194 | feq2d 6595 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)) |
196 | 188, 195 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵) |
197 | 176 | ffund 6613 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
198 | 128, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈
(ℤ≥‘1)) |
199 | | eluzfz2 13273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ (1...𝑛)) |
200 | 198, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛)) |
201 | | fveq2 6783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛)) |
202 | 201 | ssiun2s 4979 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
203 | 200, 202 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
204 | | peano2rem 11297 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
205 | 129, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ) |
206 | 205, 123 | nndivred 12036 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ) |
207 | 206 | rexrd 11034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈
ℝ*) |
208 | 130 | rexrd 11034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈
ℝ*) |
209 | 129 | ltm1d 11916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛) |
210 | | ltdiv1 11848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))) |
211 | 205, 129,
139, 140, 210 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))) |
212 | 209, 211 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)) |
213 | 206, 130,
212 | ltled 11132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) |
214 | | ubicc2 13206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))) |
215 | 207, 208,
213, 214 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))) |
216 | 198, 119,
110 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁)) |
217 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) |
218 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁)) |
219 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217 | cvmliftlem7 33262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))})) |
220 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219 | cvmliftlem6 33261 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))))) |
221 | 216, 220 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))))) |
222 | 221 | simpld 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵) |
223 | 222 | fdmd 6620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))) |
224 | 215, 223 | eleqtrrd 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) |
225 | | funssfv 6804 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) |
226 | 197, 203,
224, 225 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) |
227 | 192 | fveq2d 6787 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛)) |
228 | 227, 193 | fveq12d 6790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) |
229 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84 | cvmliftlem9 33264 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁))) |
230 | 119, 229 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁))) |
231 | 193 | fveq2d 6787 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))) |
232 | 230, 231 | eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))) |
233 | 226, 228,
232 | 3eqtr2d 2785 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))) |
234 | 233 | opeq2d 4812 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → 〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉 = 〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉) |
235 | 234 | sneqd 4574 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → {〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉} = {〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉}) |
236 | 182 | ffnd 6610 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁))) |
237 | | 0xr 11031 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ* |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → 0 ∈
ℝ*) |
239 | | ubicc2 13206 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 0 ≤
(𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) |
240 | 238, 208,
142, 239 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) |
241 | | fnressn 7039 |
. . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉}) |
242 | 236, 240,
241 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉}) |
243 | 196 | ffnd 6610 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
244 | 124 | rexrd 11034 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈
ℝ*) |
245 | | lbicc2 13205 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
246 | 208, 244,
147, 245 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
247 | | fnressn 7039 |
. . . . . . . . . . . . . . 15
⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉}) |
248 | 243, 246,
247 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉}) |
249 | 235, 242,
248 | 3eqtr4d 2789 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)})) |
250 | | df-icc 13095 |
. . . . . . . . . . . . . . . . 17
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
251 | | xrmaxle 12926 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ (if(0 ≤ (𝑛 /
𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧))) |
252 | | xrlemin 12927 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℝ*
∧ (𝑛 / 𝑁) ∈ ℝ*
∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)
→ (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁)))) |
253 | 250, 251,
252 | ixxin 13105 |
. . . . . . . . . . . . . . . 16
⊢ (((0
∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*) ∧ ((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)) →
((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)))) |
254 | 238, 208,
208, 244, 253 | syl22anc 836 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)))) |
255 | 142 | iftrued 4468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁)) |
256 | 147 | iftrued 4468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁)) |
257 | 255, 256 | oveq12d 7302 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁))) |
258 | | iccid 13133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 / 𝑁) ∈ ℝ* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)}) |
259 | 208, 258 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)}) |
260 | 254, 257,
259 | 3eqtrd 2783 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)}) |
261 | 260 | reseq2d 5894 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)})) |
262 | 260 | reseq2d 5894 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)})) |
263 | 249, 261,
262 | 3eqtr4d 2789 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
264 | | fresaun 6654 |
. . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵) |
265 | 182, 196,
263, 264 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵) |
266 | | fzsuc 13312 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)})) |
267 | 198, 266 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)})) |
268 | 267 | iuneq1d 4952 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘)) |
269 | | iunxun 5024 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪
𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) |
270 | | ovex 7317 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 + 1) ∈ V |
271 | | fveq2 6783 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))) |
272 | 270, 271 | iunxsn 5021 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)) |
273 | 272 | uneq2i 4095 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪
𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) |
274 | 269, 273 | eqtri 2767 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) |
275 | 268, 274 | eqtr2di 2796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) |
276 | 275 | feq1d 6594 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)) |
277 | 265, 276 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵) |
278 | 170 | feq2d 6595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)) |
279 | 277, 278 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))⟶𝐵) |
280 | 275 | reseq1d 5893 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁)))) |
281 | | fresaunres1 6656 |
. . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
282 | 182, 196,
263, 281 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
283 | 280, 282 | eqtr3d 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) |
284 | 167 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top) |
285 | | ovex 7317 |
. . . . . . . . . . . . 13
⊢
(0[,]((𝑛 + 1) /
𝑁)) ∈
V |
286 | 285 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V) |
287 | | restabs 22325 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿 ↾t (0[,](𝑛 / 𝑁)))) |
288 | 284, 153,
286, 287 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿 ↾t (0[,](𝑛 / 𝑁)))) |
289 | 288 | oveq1d 7299 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶)) |
290 | 173, 283,
289 | 3eltr4d 2855 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) ∈ (((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶)) |
291 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183 | cvmliftlem8 33263 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
292 | 119, 291 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
293 | 194 | oveq2d 7300 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
294 | 293 | oveq1d 7299 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
295 | 292, 294 | eleqtrd 2842 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
296 | 275 | reseq1d 5893 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
297 | | fresaunres2 6655 |
. . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1))) |
298 | 182, 196,
263, 297 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1))) |
299 | 296, 298 | eqtr3d 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1))) |
300 | | restabs 22325 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
301 | 284, 163,
286, 300 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
302 | 301 | oveq1d 7299 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
303 | 295, 299,
302 | 3eltr4d 2855 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
304 | 115, 75, 158, 165, 170, 279, 290, 303 | paste 22454 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) |
305 | 152 | reseq2d 5894 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
306 | 172 | simprd 496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) |
307 | 187 | simprd 496 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
308 | 194 | reseq2d 5894 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
309 | 307, 308 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
310 | 306, 309 | uneq12d 4099 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
311 | | coundi 6155 |
. . . . . . . . . 10
⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) |
312 | | resundi 5908 |
. . . . . . . . . 10
⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
313 | 310, 311,
312 | 3eqtr4g 2804 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
314 | 275 | coeq2d 5774 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))) |
315 | 305, 313,
314 | 3eqtr2rd 2786 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))) |
316 | 304, 315 | jca 512 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))) |
317 | 114, 316 | sylan2br 595 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))) |
318 | 317 | expr 457 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))) |
319 | 113, 318 | animpimp2impd 843 |
. . . 4
⊢ (𝑛 ∈ ℕ → ((𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))) |
320 | 27, 41, 55, 71, 106, 319 | nnind 12000 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))) |
321 | 1, 320 | mpcom 38 |
. 2
⊢ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))) |
322 | 5, 321 | mpd 15 |
1
⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))) |