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