| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvmliftlem.n | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 2 |  | nnuz 12922 | . . . 4
⊢ ℕ =
(ℤ≥‘1) | 
| 3 | 1, 2 | eleqtrdi 2850 | . . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) | 
| 4 |  | eluzfz2 13573 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘1) → 𝑁 ∈ (1...𝑁)) | 
| 5 | 3, 4 | syl 17 | . 2
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) | 
| 6 |  | eleq1 2828 | . . . . . 6
⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁))) | 
| 7 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑦 = 1 → (1...𝑦) = (1...1)) | 
| 8 |  | 1z 12649 | . . . . . . . . . . . 12
⊢ 1 ∈
ℤ | 
| 9 |  | fzsn 13607 | . . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (1...1) = {1}) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . . . . . . 11
⊢ (1...1) =
{1} | 
| 11 | 7, 10 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑦 = 1 → (1...𝑦) = {1}) | 
| 12 | 11 | iuneq1d 5018 | . . . . . . . . 9
⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘)) | 
| 13 |  | 1ex 11258 | . . . . . . . . . 10
⊢ 1 ∈
V | 
| 14 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1)) | 
| 15 | 13, 14 | iunxsn 5090 | . . . . . . . . 9
⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1) | 
| 16 | 12, 15 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1)) | 
| 17 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁)) | 
| 18 | 17 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁))) | 
| 19 | 18 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑦 = 1 → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,](1 / 𝑁)))) | 
| 20 | 19 | oveq1d 7447 | . . . . . . . 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 5872 | . . . . . . . 8
⊢ (𝑦 = 1 → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1))) | 
| 23 | 18 | reseq2d 5996 | . . . . . . . 8
⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁)))) | 
| 24 | 22, 23 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑦 = 1 → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))) | 
| 25 | 21, 24 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = 1 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))) | 
| 26 | 6, 25 | imbi12d 344 | . . . . 5
⊢ (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))) | 
| 27 | 26 | imbi2d 340 | . . . 4
⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))) | 
| 28 |  | eleq1 2828 | . . . . . 6
⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁))) | 
| 29 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛)) | 
| 30 | 29 | iuneq1d 5018 | . . . . . . . 8
⊢ (𝑦 = 𝑛 → ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 31 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁)) | 
| 32 | 31 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁))) | 
| 33 | 32 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,](𝑛 / 𝑁)))) | 
| 34 | 33 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑦 = 𝑛 → ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶)) | 
| 35 | 30, 34 | eleq12d 2834 | . . . . . . 7
⊢ (𝑦 = 𝑛 → (∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶))) | 
| 36 | 30 | coeq2d 5872 | . . . . . . . 8
⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘))) | 
| 37 | 32 | reseq2d 5996 | . . . . . . . 8
⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) | 
| 38 | 36, 37 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑦 = 𝑛 → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) | 
| 39 | 35, 38 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = 𝑛 → ((∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) | 
| 40 | 28, 39 | imbi12d 344 | . . . . 5
⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))) | 
| 41 | 40 | imbi2d 340 | . . . 4
⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))) | 
| 42 |  | eleq1 2828 | . . . . . 6
⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁))) | 
| 43 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1))) | 
| 44 | 43 | iuneq1d 5018 | . . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) | 
| 45 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁)) | 
| 46 | 45 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁))) | 
| 47 | 46 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁)))) | 
| 48 | 47 | oveq1d 7447 | . . . . . . . 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 5872 | . . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))) | 
| 51 | 46 | reseq2d 5996 | . . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))) | 
| 52 | 50, 51 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑦 = (𝑛 + 1) → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))) | 
| 53 | 49, 52 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = (𝑛 + 1) → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))) | 
| 54 | 42, 53 | imbi12d 344 | . . . . 5
⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))) | 
| 55 | 54 | imbi2d 340 | . . . 4
⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))) | 
| 56 |  | eleq1 2828 | . . . . . 6
⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁))) | 
| 57 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁)) | 
| 58 | 57 | iuneq1d 5018 | . . . . . . . . 9
⊢ (𝑦 = 𝑁 → ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)) | 
| 59 |  | cvmliftlem.k | . . . . . . . . 9
⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘) | 
| 60 | 58, 59 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑦 = 𝑁 → ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾) | 
| 61 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁)) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁))) | 
| 63 | 62 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑦 = 𝑁 → (𝐿 ↾t (0[,](𝑦 / 𝑁))) = (𝐿 ↾t (0[,](𝑁 / 𝑁)))) | 
| 64 | 63 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑦 = 𝑁 → ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶)) | 
| 65 | 60, 64 | eleq12d 2834 | . . . . . . 7
⊢ (𝑦 = 𝑁 → (∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶))) | 
| 66 | 60 | coeq2d 5872 | . . . . . . . 8
⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾)) | 
| 67 | 62 | reseq2d 5996 | . . . . . . . 8
⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))) | 
| 68 | 66, 67 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑦 = 𝑁 → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))) | 
| 69 | 65, 68 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = 𝑁 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))) | 
| 70 | 56, 69 | imbi12d 344 | . . . . 5
⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))) | 
| 71 | 70 | imbi2d 340 | . . . 4
⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))) | 
| 72 |  | eluzfz1 13572 | . . . . . . . . 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 2736 | . . . . . . . . 9
⊢ (((1
− 1) / 𝑁)[,](1 /
𝑁)) = (((1 − 1) /
𝑁)[,](1 / 𝑁)) | 
| 86 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85 | cvmliftlem8 35298 | . . . . . . . 8
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶)) | 
| 87 | 73, 86 | mpdan 687 | . . . . . . 7
⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶)) | 
| 88 |  | 1m1e0 12339 | . . . . . . . . . . . 12
⊢ (1
− 1) = 0 | 
| 89 | 88 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((1
− 1) / 𝑁) = (0 /
𝑁) | 
| 90 | 1 | nncnd 12283 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 91 | 1 | nnne0d 12317 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 92 | 90, 91 | div0d 12043 | . . . . . . . . . . 11
⊢ (𝜑 → (0 / 𝑁) = 0) | 
| 93 | 89, 92 | eqtrid 2788 | . . . . . . . . . 10
⊢ (𝜑 → ((1 − 1) / 𝑁) = 0) | 
| 94 | 93 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁))) | 
| 95 | 94 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾t (0[,](1 / 𝑁)))) | 
| 96 | 95 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → ((𝐿 ↾t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶)) | 
| 97 | 87, 96 | eleqtrd 2842 | . . . . . 6
⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾t (0[,](1 / 𝑁))) Cn 𝐶)) | 
| 98 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁)) | 
| 99 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85 | cvmliftlem7 35297 | . . . . . . . . . 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 35296 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) | 
| 101 | 73, 100 | mpdan 687 | . . . . . . . 8
⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))) | 
| 102 | 101 | simprd 495 | . . . . . . 7
⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))) | 
| 103 | 94 | reseq2d 5996 | . . . . . . 7
⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁)))) | 
| 104 | 102, 103 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))) | 
| 105 | 97, 104 | jca 511 | . . . . 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 12923 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) | 
| 108 | 107 | biimpi 216 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) | 
| 109 | 108 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) | 
| 110 |  | peano2fzr 13578 | . . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁)) | 
| 111 | 110 | ex 412 | . . . . . . 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 2736 | . . . . . . . . 9
⊢ ∪ (𝐿
↾t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁))) | 
| 116 |  | 0re 11264 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 117 | 114 | simplbi 497 | . . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) | 
| 118 | 117 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) | 
| 119 | 118 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ (1...𝑁)) | 
| 120 |  | elfznn 13594 | . . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ) | 
| 121 | 119, 120 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ) | 
| 122 | 121 | nnred 12282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ) | 
| 123 | 1 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ) | 
| 124 | 122, 123 | nndivred 12321 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ) | 
| 125 |  | iccssre 13470 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ ((𝑛 +
1) / 𝑁) ∈ ℝ)
→ (0[,]((𝑛 + 1) /
𝑁)) ⊆
ℝ) | 
| 126 | 116, 124,
125 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) | 
| 127 | 117 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑛 ∈ ℕ) | 
| 128 | 127 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ) | 
| 129 | 128 | nnred 12282 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ) | 
| 130 | 129, 123 | nndivred 12321 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ) | 
| 131 |  | icccld 24788 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (𝑛 /
𝑁) ∈ ℝ) →
(0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran
(,)))) | 
| 132 | 116, 130,
131 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran
(,)))) | 
| 133 | 83 | fveq2i 6908 | . . . . . . . . . . 11
⊢
(Clsd‘𝐿) =
(Clsd‘(topGen‘ran (,))) | 
| 134 | 132, 133 | eleqtrrdi 2851 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿)) | 
| 135 |  | ssun1 4177 | . . . . . . . . . . 11
⊢
(0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) | 
| 136 | 116 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ) | 
| 137 | 128 | nnnn0d 12589 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ0) | 
| 138 | 137 | nn0ge0d 12592 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛) | 
| 139 | 123 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ) | 
| 140 | 123 | nngt0d 12316 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁) | 
| 141 |  | divge0 12138 | . . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁)) | 
| 142 | 129, 138,
139, 140, 141 | syl22anc 838 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁)) | 
| 143 | 129 | ltp1d 12199 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1)) | 
| 144 |  | ltdiv1 12133 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))) | 
| 145 | 129, 122,
139, 140, 144 | syl112anc 1375 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))) | 
| 146 | 143, 145 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)) | 
| 147 | 130, 124,
146 | ltled 11410 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) | 
| 148 |  | elicc2 13453 | . . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ ((𝑛 +
1) / 𝑁) ∈ ℝ)
→ ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)))) | 
| 149 | 116, 124,
148 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)))) | 
| 150 | 130, 142,
147, 149 | mpbir3and 1342 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) | 
| 151 |  | iccsplit 13526 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ((𝑛 +
1) / 𝑁) ∈ ℝ
∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 152 | 136, 124,
150, 151 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 153 | 135, 152 | sseqtrrid 4026 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) | 
| 154 |  | uniretop 24784 | . . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) | 
| 155 | 83 | unieqi 4918 | . . . . . . . . . . . 12
⊢ ∪ 𝐿 =
∪ (topGen‘ran (,)) | 
| 156 | 154, 155 | eqtr4i 2767 | . . . . . . . . . . 11
⊢ ℝ =
∪ 𝐿 | 
| 157 | 156 | restcldi 23182 | . . . . . . . . . 10
⊢
(((0[,]((𝑛 + 1) /
𝑁)) ⊆ ℝ ∧
(0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) | 
| 158 | 126, 134,
153, 157 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) | 
| 159 |  | icccld 24788 | . . . . . . . . . . . 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 4178 | . . . . . . . . . . 11
⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) | 
| 163 | 162, 152 | sseqtrrid 4026 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) | 
| 164 | 156 | restcldi 23182 | . . . . . . . . . 10
⊢
(((0[,]((𝑛 + 1) /
𝑁)) ⊆ ℝ ∧
((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) | 
| 165 | 126, 161,
163, 164 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))))) | 
| 166 |  | retop 24783 | . . . . . . . . . . . 12
⊢
(topGen‘ran (,)) ∈ Top | 
| 167 | 83, 166 | eqeltri 2836 | . . . . . . . . . . 11
⊢ 𝐿 ∈ Top | 
| 168 | 156 | restuni 23171 | . . . . . . . . . . 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 2778 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))) | 
| 171 | 114 | simprbi 496 | . . . . . . . . . . . . . . . 16
⊢ (𝜒 → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) | 
| 172 | 171 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) | 
| 173 | 172 | simpld 494 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶)) | 
| 174 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ∪ (𝐿
↾t (0[,](𝑛
/ 𝑁))) = ∪ (𝐿
↾t (0[,](𝑛
/ 𝑁))) | 
| 175 | 174, 75 | cnf 23255 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))⟶𝐵) | 
| 176 | 173, 175 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))⟶𝐵) | 
| 177 |  | iccssre 13470 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ (𝑛 /
𝑁) ∈ ℝ) →
(0[,](𝑛 / 𝑁)) ⊆ ℝ) | 
| 178 | 116, 130,
177 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ) | 
| 179 | 156 | restuni 23171 | . . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))) | 
| 180 | 167, 178,
179 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))) | 
| 181 | 180 | feq2d 6721 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾t (0[,](𝑛 / 𝑁)))⟶𝐵)) | 
| 182 | 176, 181 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵) | 
| 183 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) | 
| 184 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁)) | 
| 185 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183 | cvmliftlem7 35297 | . . . . . . . . . . . . . . . 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 35296 | . . . . . . . . . . . . . . 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 494 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵) | 
| 189 | 128 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ) | 
| 190 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ | 
| 191 |  | pncan 11515 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) | 
| 192 | 189, 190,
191 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛) | 
| 193 | 192 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁)) | 
| 194 | 193 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) | 
| 195 | 194 | feq2d 6721 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)) | 
| 196 | 188, 195 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵) | 
| 197 | 176 | ffund 6739 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 198 | 128, 108 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈
(ℤ≥‘1)) | 
| 199 |  | eluzfz2 13573 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ (1...𝑛)) | 
| 200 | 198, 199 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛)) | 
| 201 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛)) | 
| 202 | 201 | ssiun2s 5047 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 203 | 200, 202 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 204 |  | peano2rem 11577 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) | 
| 205 | 129, 204 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ) | 
| 206 | 205, 123 | nndivred 12321 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ) | 
| 207 | 206 | rexrd 11312 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈
ℝ*) | 
| 208 | 130 | rexrd 11312 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈
ℝ*) | 
| 209 | 129 | ltm1d 12201 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛) | 
| 210 |  | ltdiv1 12133 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))) | 
| 211 | 205, 129,
139, 140, 210 | syl112anc 1375 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))) | 
| 212 | 209, 211 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)) | 
| 213 | 206, 130,
212 | ltled 11410 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) | 
| 214 |  | ubicc2 13506 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))) | 
| 215 | 207, 208,
213, 214 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))) | 
| 216 | 198, 119,
110 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁)) | 
| 217 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) | 
| 218 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁)) | 
| 219 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217 | cvmliftlem7 35297 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))})) | 
| 220 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219 | cvmliftlem6 35296 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))))) | 
| 221 | 216, 220 | syldan 591 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))))) | 
| 222 | 221 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵) | 
| 223 | 222 | fdmd 6745 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))) | 
| 224 | 215, 223 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) | 
| 225 |  | funssfv 6926 | . . . . . . . . . . . . . . . . . 18
⊢ ((Fun
∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) | 
| 226 | 197, 203,
224, 225 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) | 
| 227 | 192 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛)) | 
| 228 | 227, 193 | fveq12d 6912 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) | 
| 229 | 74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84 | cvmliftlem9 35299 | . . . . . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))) | 
| 232 | 230, 231 | eqtr3d 2778 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))) | 
| 233 | 226, 228,
232 | 3eqtr2d 2782 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))) | 
| 234 | 233 | opeq2d 4879 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → 〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉 = 〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉) | 
| 235 | 234 | sneqd 4637 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → {〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉} = {〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉}) | 
| 236 | 182 | ffnd 6736 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁))) | 
| 237 |  | 0xr 11309 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ* | 
| 238 | 237 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → 0 ∈
ℝ*) | 
| 239 |  | ubicc2 13506 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 0 ≤
(𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) | 
| 240 | 238, 208,
142, 239 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) | 
| 241 |  | fnressn 7177 | . . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉}) | 
| 242 | 236, 240,
241 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))〉}) | 
| 243 | 196 | ffnd 6736 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) | 
| 244 | 124 | rexrd 11312 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈
ℝ*) | 
| 245 |  | lbicc2 13505 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) | 
| 246 | 208, 244,
147, 245 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) | 
| 247 |  | fnressn 7177 | . . . . . . . . . . . . . . 15
⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉}) | 
| 248 | 243, 246,
247 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {〈(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))〉}) | 
| 249 | 235, 242,
248 | 3eqtr4d 2786 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)})) | 
| 250 |  | df-icc 13395 | . . . . . . . . . . . . . . . . 17
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | 
| 251 |  | xrmaxle 13226 | . . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ (if(0 ≤ (𝑛 /
𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧))) | 
| 252 |  | xrlemin 13227 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℝ*
∧ (𝑛 / 𝑁) ∈ ℝ*
∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)
→ (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁)))) | 
| 253 | 250, 251,
252 | ixxin 13405 | . . . . . . . . . . . . . . . 16
⊢ (((0
∈ ℝ* ∧ (𝑛 / 𝑁) ∈ ℝ*) ∧ ((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ*)) →
((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)))) | 
| 254 | 238, 208,
208, 244, 253 | syl22anc 838 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)))) | 
| 255 | 142 | iftrued 4532 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁)) | 
| 256 | 147 | iftrued 4532 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁)) | 
| 257 | 255, 256 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁))) | 
| 258 |  | iccid 13433 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 / 𝑁) ∈ ℝ* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)}) | 
| 259 | 208, 258 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)}) | 
| 260 | 254, 257,
259 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)}) | 
| 261 | 260 | reseq2d 5996 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)})) | 
| 262 | 260 | reseq2d 5996 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)})) | 
| 263 | 249, 261,
262 | 3eqtr4d 2786 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) | 
| 264 |  | fresaun 6778 | . . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵) | 
| 265 | 182, 196,
263, 264 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵) | 
| 266 |  | fzsuc 13612 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)})) | 
| 267 | 198, 266 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)})) | 
| 268 | 267 | iuneq1d 5018 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘)) | 
| 269 |  | iunxun 5093 | . . . . . . . . . . . . . 14
⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪
𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) | 
| 270 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 + 1) ∈ V | 
| 271 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))) | 
| 272 | 270, 271 | iunxsn 5090 | . . . . . . . . . . . . . . 15
⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)) | 
| 273 | 272 | uneq2i 4164 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪
𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) | 
| 274 | 269, 273 | eqtri 2764 | . . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) | 
| 275 | 268, 274 | eqtr2di 2793 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) | 
| 276 | 275 | feq1d 6719 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)) | 
| 277 | 265, 276 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵) | 
| 278 | 170 | feq2d 6721 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)) | 
| 279 | 277, 278 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾t
(0[,]((𝑛 + 1) / 𝑁)))⟶𝐵) | 
| 280 | 275 | reseq1d 5995 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁)))) | 
| 281 |  | fresaunres1 6780 | . . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 282 | 182, 196,
263, 281 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 283 | 280, 282 | eqtr3d 2778 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) | 
| 284 | 167 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top) | 
| 285 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢
(0[,]((𝑛 + 1) /
𝑁)) ∈
V | 
| 286 | 285 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V) | 
| 287 |  | restabs 23174 | . . . . . . . . . . . 12
⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿 ↾t (0[,](𝑛 / 𝑁)))) | 
| 288 | 284, 153,
286, 287 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t (0[,](𝑛 / 𝑁))) = (𝐿 ↾t (0[,](𝑛 / 𝑁)))) | 
| 289 | 288 | oveq1d 7447 | . . . . . . . . . 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 35298 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) | 
| 292 | 119, 291 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) | 
| 293 | 194 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 294 | 293 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) | 
| 295 | 292, 294 | eleqtrd 2842 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) | 
| 296 | 275 | reseq1d 5995 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 297 |  | fresaunres2 6779 | . . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1))) | 
| 298 | 182, 196,
263, 297 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1))) | 
| 299 | 296, 298 | eqtr3d 2778 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1))) | 
| 300 |  | restabs 23174 | . . . . . . . . . . . 12
⊢ ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 301 | 284, 163,
286, 300 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 302 | 301 | oveq1d 7447 | . . . . . . . . . 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 23303 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝜒) → ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)) | 
| 305 | 152 | reseq2d 5996 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) | 
| 306 | 172 | simprd 495 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) | 
| 307 | 187 | simprd 495 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 308 | 194 | reseq2d 5996 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 309 | 307, 308 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 310 | 306, 309 | uneq12d 4168 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) | 
| 311 |  | coundi 6266 | . . . . . . . . . 10
⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) | 
| 312 |  | resundi 6010 | . . . . . . . . . 10
⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) | 
| 313 | 310, 311,
312 | 3eqtr4g 2801 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) | 
| 314 | 275 | coeq2d 5872 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))) | 
| 315 | 305, 313,
314 | 3eqtr2rd 2783 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))) | 
| 316 | 304, 315 | jca 511 | . . . . . . 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 456 | . . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪
𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))) | 
| 319 | 113, 318 | animpimp2impd 846 | . . . 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 12285 | . . 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[,](𝑁 / 𝑁))))) |