| Step | Hyp | Ref
| Expression |
| 1 | | fzssp1 13607 |
. . . 4
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
| 2 | | cvmliftlem.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 3 | 2 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑁 ∈ ℂ) |
| 5 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 6 | | npcan 11517 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
| 7 | 4, 5, 6 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑁 − 1) + 1) = 𝑁) |
| 8 | 7 | oveq2d 7447 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...((𝑁 − 1) + 1)) = (0...𝑁)) |
| 9 | 1, 8 | sseqtrid 4026 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
| 10 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → 𝑀 ∈ (1...𝑁)) |
| 11 | | elfzelz 13564 |
. . . . 5
⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℤ) |
| 12 | 2 | nnzd 12640 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 13 | | elfzm1b 13642 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1)))) |
| 14 | 11, 12, 13 | syl2anr 597 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1)))) |
| 15 | 10, 14 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...(𝑁 − 1))) |
| 16 | 9, 15 | sseldd 3984 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → (𝑀 − 1) ∈ (0...𝑁)) |
| 17 | | elfznn0 13660 |
. . . 4
⊢ ((𝑀 − 1) ∈ (0...𝑁) → (𝑀 − 1) ∈
ℕ0) |
| 18 | 17 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → (𝑀 − 1) ∈
ℕ0) |
| 19 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑦 = 0 → (𝑦 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁))) |
| 20 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (𝑄‘𝑦) = (𝑄‘0)) |
| 21 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (𝑦 / 𝑁) = (0 / 𝑁)) |
| 22 | 20, 21 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑦 = 0 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘0)‘(0 / 𝑁))) |
| 23 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(0 / 𝑁))) |
| 24 | 23 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝑦 = 0 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(0 / 𝑁))}) |
| 25 | 24 | imaeq2d 6078 |
. . . . . . . 8
⊢ (𝑦 = 0 → (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (◡𝐹 “ {(𝐺‘(0 / 𝑁))})) |
| 26 | 22, 25 | eleq12d 2835 |
. . . . . . 7
⊢ (𝑦 = 0 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘0)‘(0 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))}))) |
| 27 | 19, 26 | imbi12d 344 |
. . . . . 6
⊢ (𝑦 = 0 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))})))) |
| 28 | 27 | imbi2d 340 |
. . . . 5
⊢ (𝑦 = 0 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))}))))) |
| 29 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑦 = 𝑛 → (𝑦 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁))) |
| 30 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝑄‘𝑦) = (𝑄‘𝑛)) |
| 31 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁)) |
| 32 | 30, 31 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) |
| 33 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘(𝑛 / 𝑁))) |
| 34 | 33 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))}) |
| 35 | 34 | imaeq2d 6078 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) |
| 36 | 32, 35 | eleq12d 2835 |
. . . . . . 7
⊢ (𝑦 = 𝑛 → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) |
| 37 | 29, 36 | imbi12d 344 |
. . . . . 6
⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))) |
| 38 | 37 | imbi2d 340 |
. . . . 5
⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))))) |
| 39 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑛 + 1) ∈ (0...𝑁))) |
| 40 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → (𝑄‘𝑦) = (𝑄‘(𝑛 + 1))) |
| 41 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁)) |
| 42 | 40, 41 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) |
| 43 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑛 + 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁))) |
| 44 | 43 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝑦 = (𝑛 + 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑛 + 1) / 𝑁))}) |
| 45 | 44 | imaeq2d 6078 |
. . . . . . . 8
⊢ (𝑦 = (𝑛 + 1) → (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})) |
| 46 | 42, 45 | eleq12d 2835 |
. . . . . . 7
⊢ (𝑦 = (𝑛 + 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))) |
| 47 | 39, 46 | imbi12d 344 |
. . . . . 6
⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})))) |
| 48 | 47 | imbi2d 340 |
. . . . 5
⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))))) |
| 49 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑦 = (𝑀 − 1) → (𝑦 ∈ (0...𝑁) ↔ (𝑀 − 1) ∈ (0...𝑁))) |
| 50 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = (𝑀 − 1) → (𝑄‘𝑦) = (𝑄‘(𝑀 − 1))) |
| 51 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = (𝑀 − 1) → (𝑦 / 𝑁) = ((𝑀 − 1) / 𝑁)) |
| 52 | 50, 51 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑦 = (𝑀 − 1) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) |
| 53 | | fvoveq1 7454 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑀 − 1) → (𝐺‘(𝑦 / 𝑁)) = (𝐺‘((𝑀 − 1) / 𝑁))) |
| 54 | 53 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝑦 = (𝑀 − 1) → {(𝐺‘(𝑦 / 𝑁))} = {(𝐺‘((𝑀 − 1) / 𝑁))}) |
| 55 | 54 | imaeq2d 6078 |
. . . . . . . 8
⊢ (𝑦 = (𝑀 − 1) → (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) = (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})) |
| 56 | 52, 55 | eleq12d 2835 |
. . . . . . 7
⊢ (𝑦 = (𝑀 − 1) → (((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}) ↔ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))) |
| 57 | 49, 56 | imbi12d 344 |
. . . . . 6
⊢ (𝑦 = (𝑀 − 1) → ((𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))})) ↔ ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))) |
| 58 | 57 | imbi2d 340 |
. . . . 5
⊢ (𝑦 = (𝑀 − 1) → ((𝜑 → (𝑦 ∈ (0...𝑁) → ((𝑄‘𝑦)‘(𝑦 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑦 / 𝑁))}))) ↔ (𝜑 → ((𝑀 − 1) ∈ (0...𝑁) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))))) |
| 59 | | cvmliftlem.1 |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
| 60 | | cvmliftlem.b |
. . . . . . . . . . 11
⊢ 𝐵 = ∪
𝐶 |
| 61 | | cvmliftlem.x |
. . . . . . . . . . 11
⊢ 𝑋 = ∪
𝐽 |
| 62 | | cvmliftlem.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
| 63 | | cvmliftlem.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
| 64 | | cvmliftlem.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
| 65 | | cvmliftlem.e |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0)) |
| 66 | | cvmliftlem.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪
𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))) |
| 67 | | cvmliftlem.a |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1st ‘(𝑇‘𝑘))) |
| 68 | | cvmliftlem.l |
. . . . . . . . . . 11
⊢ 𝐿 = (topGen‘ran
(,)) |
| 69 | | cvmliftlem.q |
. . . . . . . . . . 11
⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})) |
| 70 | 59, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69 | cvmliftlem4 35293 |
. . . . . . . . . 10
⊢ (𝑄‘0) = {〈0, 𝑃〉} |
| 71 | 70 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘0) = {〈0, 𝑃〉}) |
| 72 | 2 | nnne0d 12316 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ≠ 0) |
| 73 | 3, 72 | div0d 12042 |
. . . . . . . . 9
⊢ (𝜑 → (0 / 𝑁) = 0) |
| 74 | 71, 73 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = ({〈0, 𝑃〉}‘0)) |
| 75 | | 0nn0 12541 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
| 76 | | fvsng 7200 |
. . . . . . . . 9
⊢ ((0
∈ ℕ0 ∧ 𝑃 ∈ 𝐵) → ({〈0, 𝑃〉}‘0) = 𝑃) |
| 77 | 75, 64, 76 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → ({〈0, 𝑃〉}‘0) = 𝑃) |
| 78 | 74, 77 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) = 𝑃) |
| 79 | 73 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘(0 / 𝑁)) = (𝐺‘0)) |
| 80 | 65, 79 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘(0 / 𝑁))) |
| 81 | | cvmcn 35267 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
| 82 | 62, 81 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) |
| 83 | 60, 61 | cnf 23254 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋) |
| 84 | | ffn 6736 |
. . . . . . . . . 10
⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵) |
| 85 | 82, 83, 84 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐵) |
| 86 | | fniniseg 7080 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐵 → (𝑃 ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁))))) |
| 87 | 85, 86 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))}) ↔ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = (𝐺‘(0 / 𝑁))))) |
| 88 | 64, 80, 87 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))})) |
| 89 | 78, 88 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → ((𝑄‘0)‘(0 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))})) |
| 90 | 89 | a1d 25 |
. . . . 5
⊢ (𝜑 → (0 ∈ (0...𝑁) → ((𝑄‘0)‘(0 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(0 / 𝑁))}))) |
| 91 | | id 22 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
| 92 | | nn0uz 12920 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
| 93 | 91, 92 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
(ℤ≥‘0)) |
| 94 | 93 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
(ℤ≥‘0)) |
| 95 | | peano2fzr 13577 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘0) ∧ (𝑛 + 1) ∈ (0...𝑁)) → 𝑛 ∈ (0...𝑁)) |
| 96 | 95 | ex 412 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁))) |
| 97 | 94, 96 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 + 1) ∈ (0...𝑁) → 𝑛 ∈ (0...𝑁))) |
| 98 | 97 | imim1d 82 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})))) |
| 99 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) |
| 100 | | simprlr 780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (0...𝑁)) |
| 101 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ ((𝑛 + 1) ∈ (0...𝑁) → (𝑛 + 1) ≤ 𝑁) |
| 102 | 100, 101 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ≤ 𝑁) |
| 103 | | simprll 779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℕ0) |
| 104 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℕ) |
| 106 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 107 | 105, 106 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈
(ℤ≥‘1)) |
| 108 | 12 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℤ) |
| 109 | | elfz5 13556 |
. . . . . . . . . . . . 13
⊢ (((𝑛 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁)) |
| 110 | 107, 108,
109 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) ∈ (1...𝑁) ↔ (𝑛 + 1) ≤ 𝑁)) |
| 111 | 102, 110 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ (1...𝑁)) |
| 112 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) |
| 113 | 103 | nn0cnd 12589 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℂ) |
| 114 | | pncan 11514 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
| 115 | 113, 5, 114 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) − 1) = 𝑛) |
| 116 | 115 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛)) |
| 117 | 115 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁)) |
| 118 | 116, 117 | fveq12d 6913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁))) |
| 119 | 117 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺‘(((𝑛 + 1) − 1) / 𝑁)) = (𝐺‘(𝑛 / 𝑁))) |
| 120 | 119 | sneqd 4638 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))} = {(𝐺‘(𝑛 / 𝑁))}) |
| 121 | 120 | imaeq2d 6078 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}) = (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))})) |
| 122 | 112, 118,
121 | 3eltr4d 2856 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))})) |
| 123 | 59, 60, 61, 62, 63, 64, 65, 2, 66, 67, 68, 69, 99, 111, 122 | cvmliftlem6 35295 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))) |
| 124 | 123 | simpld 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵) |
| 125 | 103 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 ∈ ℝ) |
| 126 | 2 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℕ) |
| 127 | 125, 126 | nndivred 12320 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈ ℝ) |
| 128 | 127 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ∈
ℝ*) |
| 129 | | peano2re 11434 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) |
| 130 | 125, 129 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 + 1) ∈ ℝ) |
| 131 | 130, 126 | nndivred 12320 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ℝ) |
| 132 | 131 | rexrd 11311 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈
ℝ*) |
| 133 | 125 | ltp1d 12198 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑛 < (𝑛 + 1)) |
| 134 | 126 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝑁 ∈ ℝ) |
| 135 | 126 | nngt0d 12315 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 0 < 𝑁) |
| 136 | | ltdiv1 12132 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))) |
| 137 | 125, 130,
134, 135, 136 | syl112anc 1376 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))) |
| 138 | 133, 137 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)) |
| 139 | 127, 131,
138 | ltled 11409 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) |
| 140 | | ubicc2 13505 |
. . . . . . . . . . 11
⊢ (((𝑛 / 𝑁) ∈ ℝ* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
| 141 | 128, 132,
139, 140 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
| 142 | 117 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
| 143 | 141, 142 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑛 + 1) / 𝑁) ∈ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) |
| 144 | 124, 143 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵) |
| 145 | 123 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
| 146 | 142 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
| 147 | 145, 146 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) |
| 148 | 147 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁))) |
| 149 | 142 | feq2d 6722 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)) |
| 150 | 124, 149 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵) |
| 151 | | fvco3 7008 |
. . . . . . . . . 10
⊢ (((𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ ((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))) |
| 152 | 150, 141,
151 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐹 ∘ (𝑄‘(𝑛 + 1)))‘((𝑛 + 1) / 𝑁)) = (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)))) |
| 153 | | fvres 6925 |
. . . . . . . . . 10
⊢ (((𝑛 + 1) / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁))) |
| 154 | 141, 153 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))‘((𝑛 + 1) / 𝑁)) = (𝐺‘((𝑛 + 1) / 𝑁))) |
| 155 | 148, 152,
154 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁))) |
| 156 | 85 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → 𝐹 Fn 𝐵) |
| 157 | | fniniseg 7080 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐵 → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁))))) |
| 158 | 156, 157 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}) ↔ (((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁))) = (𝐺‘((𝑛 + 1) / 𝑁))))) |
| 159 | 144, 155,
158 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁)) ∧ ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))})) |
| 160 | 159 | expr 456 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧ (𝑛 + 1) ∈ (0...𝑁))) → (((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))) |
| 161 | 98, 160 | animpimp2impd 847 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 → (𝑛 ∈ (0...𝑁) → ((𝑄‘𝑛)‘(𝑛 / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘(𝑛 / 𝑁))}))) → (𝜑 → ((𝑛 + 1) ∈ (0...𝑁) → ((𝑄‘(𝑛 + 1))‘((𝑛 + 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑛 + 1) / 𝑁))}))))) |
| 162 | 28, 38, 48, 58, 90, 161 | nn0ind 12713 |
. . . 4
⊢ ((𝑀 − 1) ∈
ℕ0 → (𝜑
→ ((𝑀 − 1)
∈ (0...𝑁) →
((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})))) |
| 163 | 162 | impd 410 |
. . 3
⊢ ((𝑀 − 1) ∈
ℕ0 → ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))) |
| 164 | 18, 163 | mpcom 38 |
. 2
⊢ ((𝜑 ∧ (𝑀 − 1) ∈ (0...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})) |
| 165 | 16, 164 | syldan 591 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ (1...𝑁)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))})) |