Metamath Proof Explorer


Theorem cvmliftlem10

Description: Lemma for cvmlift . The function K is going to be our complete lifted path, formed by unioning together all the Q functions (each of which is defined on one segment [ ( M - 1 ) / N , M / N ] of the interval). Here we prove by induction that K is a continuous function and a lift of G by applying cvmliftlem6 , cvmliftlem7 (to show it is a function and a lift), cvmliftlem8 (to show it is continuous), and cvmliftlem9 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste gives that K is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 𝑆 = ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } )
cvmliftlem.b 𝐵 = 𝐶
cvmliftlem.x 𝑋 = 𝐽
cvmliftlem.f ( 𝜑𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftlem.g ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
cvmliftlem.p ( 𝜑𝑃𝐵 )
cvmliftlem.e ( 𝜑 → ( 𝐹𝑃 ) = ( 𝐺 ‘ 0 ) )
cvmliftlem.n ( 𝜑𝑁 ∈ ℕ )
cvmliftlem.t ( 𝜑𝑇 : ( 1 ... 𝑁 ) ⟶ 𝑗𝐽 ( { 𝑗 } × ( 𝑆𝑗 ) ) )
cvmliftlem.a ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇𝑘 ) ) )
cvmliftlem.l 𝐿 = ( topGen ‘ ran (,) )
cvmliftlem.q 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ( 𝐹 ↾ ( 𝑏 ∈ ( 2nd ‘ ( 𝑇𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
cvmliftlem.k 𝐾 = 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑘 )
cvmliftlem10.1 ( 𝜒 ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄𝑘 ) ∈ ( ( 𝐿t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) )
Assertion cvmliftlem10 ( 𝜑 → ( 𝐾 ∈ ( ( 𝐿t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) )

Proof

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 [,] ( 𝑁 / 𝑁 ) ) ) ) )