Metamath Proof Explorer

Theorem poimirlem31

Description: Lemma for poimir , assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 and poimirlem28 . Equation (2) of Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
poimir.i ⊢ 𝐼 = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) )
poimir.r ⊢ 𝑅 = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
poimir.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) )
poimir.2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝐼 ∧ ( 𝑧 ‘ 𝑛 ) = 0 ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 )
poimirlem31.p ⊢ 𝑃 = ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f + ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
poimirlem31.3 ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
poimirlem31.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) )
poimirlem31.5 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
Assertion poimirlem31 ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ◡ ≤ } ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 poimir.0 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 poimir.i ⊢ 𝐼 = ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) )
3 poimir.r ⊢ 𝑅 = ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) )
4 poimir.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) )
5 poimir.2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝐼 ∧ ( 𝑧 ‘ 𝑛 ) = 0 ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 )
6 poimirlem31.p ⊢ 𝑃 = ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f + ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) )
7 poimirlem31.3 ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
8 poimirlem31.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) )
9 poimirlem31.5 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
10 elpri ⊢ ( 𝑟 ∈ { ≤ , ◡ ≤ } → ( 𝑟 = ≤ ∨ 𝑟 = ◡ ≤ ) )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
12 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
13 12 sseli ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( 0 ... 𝑁 ) )
14 13 anim2i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) )
15 eleq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↔ 𝑛 ∈ ( 0 ... 𝑁 ) ) )
16 15 anbi2d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) )
17 16 anbi2d ⊢ ( 𝑖 = 𝑛 → ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) ↔ ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) ) )
18 eqeq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ↔ 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
19 18 rexbidv ⊢ ( 𝑖 = 𝑛 → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
20 17 19 imbi12d ⊢ ( 𝑖 = 𝑛 → ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) ↔ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) ) )
21 20 9 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
22 elfzle1 ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 1 ≤ 𝑛 )
23 1re ⊢ 1 ∈ ℝ
24 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℤ )
25 24 zred ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℝ )
26 lenlt ⊢ ( ( 1 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 1 ≤ 𝑛 ↔ ¬ 𝑛 < 1 ) )
27 23 25 26 sylancr ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 1 ≤ 𝑛 ↔ ¬ 𝑛 < 1 ) )
28 22 27 mpbid ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ¬ 𝑛 < 1 )
29 elsni ⊢ ( 𝑛 ∈ { 0 } → 𝑛 = 0 )
30 0lt1 ⊢ 0 < 1
31 29 30 eqbrtrdi ⊢ ( 𝑛 ∈ { 0 } → 𝑛 < 1 )
32 28 31 nsyl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ¬ 𝑛 ∈ { 0 } )
33 ltso ⊢ < Or ℝ
34 snfi ⊢ { 0 } ∈ Fin
35 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
36 rabfi ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ∈ Fin )
37 35 36 ax-mp ⊢ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ∈ Fin
38 unfi ⊢ ( ( { 0 } ∈ Fin ∧ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ∈ Fin ) → ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ∈ Fin )
39 34 37 38 mp2an ⊢ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ∈ Fin
40 c0ex ⊢ 0 ∈ V
41 40 snid ⊢ 0 ∈ { 0 }
42 elun1 ⊢ ( 0 ∈ { 0 } → 0 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
43 ne0i ⊢ ( 0 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) → ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ≠ ∅ )
44 41 42 43 mp2b ⊢ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ≠ ∅
45 0re ⊢ 0 ∈ ℝ
46 snssi ⊢ ( 0 ∈ ℝ → { 0 } ⊆ ℝ )
47 45 46 ax-mp ⊢ { 0 } ⊆ ℝ
48 ssrab2 ⊢ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ⊆ ( 1 ... 𝑁 )
49 24 ssriv ⊢ ( 1 ... 𝑁 ) ⊆ ℤ
50 zssre ⊢ ℤ ⊆ ℝ
51 49 50 sstri ⊢ ( 1 ... 𝑁 ) ⊆ ℝ
52 48 51 sstri ⊢ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ⊆ ℝ
53 47 52 unssi ⊢ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ⊆ ℝ
54 39 44 53 3pm3.2i ⊢ ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ∈ Fin ∧ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ≠ ∅ ∧ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ⊆ ℝ )
55 fisupcl ⊢ ( ( < Or ℝ ∧ ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ∈ Fin ∧ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ≠ ∅ ∧ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ⊆ ℝ ) ) → sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
56 33 54 55 mp2an ⊢ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } )
57 eleq1 ⊢ ( 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( 𝑛 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ↔ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ) )
58 56 57 mpbiri ⊢ ( 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → 𝑛 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
59 elun ⊢ ( 𝑛 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ↔ ( 𝑛 ∈ { 0 } ∨ 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
60 58 59 sylib ⊢ ( 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( 𝑛 ∈ { 0 } ∨ 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
61 oveq2 ⊢ ( 𝑎 = 𝑛 → ( 1 ... 𝑎 ) = ( 1 ... 𝑛 ) )
62 61 raleqdv ⊢ ( 𝑎 = 𝑛 → ( ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
63 62 elrab ⊢ ( 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
64 elfzuz ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
65 eluzfz2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → 𝑛 ∈ ( 1 ... 𝑛 ) )
66 64 65 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( 1 ... 𝑛 ) )
67 simpl ⊢ ( ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) )
68 67 ralimi ⊢ ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → ∀ 𝑏 ∈ ( 1 ... 𝑛 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) )
69 fveq2 ⊢ ( 𝑏 = 𝑛 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) = ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
70 69 breq2d ⊢ ( 𝑏 = 𝑛 → ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ↔ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
71 70 rspcva ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑛 ) ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
72 66 68 71 syl2an ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
73 63 72 sylbi ⊢ ( 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
74 73 orim2i ⊢ ( ( 𝑛 ∈ { 0 } ∨ 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) → ( 𝑛 ∈ { 0 } ∨ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
75 60 74 syl ⊢ ( 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( 𝑛 ∈ { 0 } ∨ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
76 orel1 ⊢ ( ¬ 𝑛 ∈ { 0 } → ( ( 𝑛 ∈ { 0 } ∨ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
77 32 75 76 syl2im ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
78 77 reximdv ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑛 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
79 21 78 syl5 ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
80 14 79 sylan2i ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
81 11 80 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
82 breq ⊢ ( 𝑟 = ≤ → ( 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ↔ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
83 82 rexbidv ⊢ ( 𝑟 = ≤ → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
84 81 83 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑟 = ≤ → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
85 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
86 elfzm1b ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
87 24 85 86 syl2anr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
88 87 biimpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
89 88 ex ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) ) )
90 89 pm2.43d ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
91 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
92 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
93 91 92 syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
94 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
95 1 94 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
96 95 nn0zd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
97 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
98 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
99 96 97 98 3syl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
100 93 99 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
101 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
102 100 101 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
103 102 sseld ⊢ ( 𝜑 → ( ( 𝑛 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) )
104 90 103 syld ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) )
105 104 anim2d ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 ∈ ℕ ∧ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) ) )
106 105 imp ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑘 ∈ ℕ ∧ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) )
107 ovex ⊢ ( 𝑛 − 1 ) ∈ V
108 eleq1 ⊢ ( 𝑖 = ( 𝑛 − 1 ) → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) )
109 108 anbi2d ⊢ ( 𝑖 = ( 𝑛 − 1 ) → ( ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) ) )
110 109 anbi2d ⊢ ( 𝑖 = ( 𝑛 − 1 ) → ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) ↔ ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) ) ) )
111 eqeq1 ⊢ ( 𝑖 = ( 𝑛 − 1 ) → ( 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ↔ ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
112 111 rexbidv ⊢ ( 𝑖 = ( 𝑛 − 1 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
113 110 112 imbi12d ⊢ ( 𝑖 = ( 𝑛 − 1 ) → ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑖 = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) ↔ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) ) )
114 107 113 9 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 − 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
115 106 114 syldan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
116 eleq1 ⊢ ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ( 𝑛 − 1 ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ↔ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ) )
117 56 116 mpbiri ⊢ ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( 𝑛 − 1 ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
118 elun ⊢ ( ( 𝑛 − 1 ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ↔ ( ( 𝑛 − 1 ) ∈ { 0 } ∨ ( 𝑛 − 1 ) ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
119 107 elsn ⊢ ( ( 𝑛 − 1 ) ∈ { 0 } ↔ ( 𝑛 − 1 ) = 0 )
120 oveq2 ⊢ ( 𝑎 = ( 𝑛 − 1 ) → ( 1 ... 𝑎 ) = ( 1 ... ( 𝑛 − 1 ) ) )
121 120 raleqdv ⊢ ( 𝑎 = ( 𝑛 − 1 ) → ( ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
122 121 elrab ⊢ ( ( 𝑛 − 1 ) ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ↔ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
123 119 122 orbi12i ⊢ ( ( ( 𝑛 − 1 ) ∈ { 0 } ∨ ( 𝑛 − 1 ) ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ↔ ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) )
124 118 123 bitri ⊢ ( ( 𝑛 − 1 ) ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ↔ ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) )
125 117 124 sylib ⊢ ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) )
126 125 a1i ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) ) )
127 ltm1 ⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) < 𝑛 )
128 peano2rem ⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) ∈ ℝ )
129 ltnle ⊢ ( ( ( 𝑛 − 1 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 𝑛 − 1 ) < 𝑛 ↔ ¬ 𝑛 ≤ ( 𝑛 − 1 ) ) )
130 128 129 mpancom ⊢ ( 𝑛 ∈ ℝ → ( ( 𝑛 − 1 ) < 𝑛 ↔ ¬ 𝑛 ≤ ( 𝑛 − 1 ) ) )
131 127 130 mpbid ⊢ ( 𝑛 ∈ ℝ → ¬ 𝑛 ≤ ( 𝑛 − 1 ) )
132 25 131 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ¬ 𝑛 ≤ ( 𝑛 − 1 ) )
133 breq2 ⊢ ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( 𝑛 ≤ ( 𝑛 − 1 ) ↔ 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
134 133 notbid ⊢ ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ¬ 𝑛 ≤ ( 𝑛 − 1 ) ↔ ¬ 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
135 132 134 syl5ibcom ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ¬ 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) ) )
136 elun2 ⊢ ( 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } → 𝑛 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) )
137 fimaxre2 ⊢ ( ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ⊆ ℝ ∧ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) 𝑦 ≤ 𝑥 )
138 53 39 137 mp2an ⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) 𝑦 ≤ 𝑥
139 53 44 138 3pm3.2i ⊢ ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ⊆ ℝ ∧ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) 𝑦 ≤ 𝑥 )
140 139 suprubii ⊢ ( 𝑛 ∈ ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) → 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
141 136 140 syl ⊢ ( 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } → 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) )
142 141 con3i ⊢ ( ¬ 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ¬ 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } )
143 ianor ⊢ ( ¬ ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ↔ ( ¬ 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
144 143 63 xchnxbir ⊢ ( ¬ 𝑛 ∈ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ↔ ( ¬ 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
145 142 144 sylib ⊢ ( ¬ 𝑛 ≤ sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ¬ 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
146 135 145 syl6 ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ¬ 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) )
147 pm2.63 ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ( ( ¬ 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
148 147 orcs ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ¬ 𝑛 ∈ ( 1 ... 𝑁 ) ∨ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
149 146 148 syld ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
150 126 149 jcad ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) )
151 andir ⊢ ( ( ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ↔ ( ( ( 𝑛 − 1 ) = 0 ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ∨ ( ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) )
152 24 zcnd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℂ )
153 ax-1cn ⊢ 1 ∈ ℂ
154 0cn ⊢ 0 ∈ ℂ
155 subadd ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( 𝑛 − 1 ) = 0 ↔ ( 1 + 0 ) = 𝑛 ) )
156 153 154 155 mp3an23 ⊢ ( 𝑛 ∈ ℂ → ( ( 𝑛 − 1 ) = 0 ↔ ( 1 + 0 ) = 𝑛 ) )
157 152 156 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = 0 ↔ ( 1 + 0 ) = 𝑛 ) )
158 157 biimpa ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑛 − 1 ) = 0 ) → ( 1 + 0 ) = 𝑛 )
159 1p0e1 ⊢ ( 1 + 0 ) = 1
160 158 159 eqtr3di ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑛 − 1 ) = 0 ) → 𝑛 = 1 )
161 1z ⊢ 1 ∈ ℤ
162 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
163 161 162 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
164 oveq2 ⊢ ( 𝑛 = 1 → ( 1 ... 𝑛 ) = ( 1 ... 1 ) )
165 sneq ⊢ ( 𝑛 = 1 → { 𝑛 } = { 1 } )
166 163 164 165 3eqtr4a ⊢ ( 𝑛 = 1 → ( 1 ... 𝑛 ) = { 𝑛 } )
167 166 raleqdv ⊢ ( 𝑛 = 1 → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
168 167 notbid ⊢ ( 𝑛 = 1 → ( ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
169 168 biimpd ⊢ ( 𝑛 = 1 → ( ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
170 160 169 syl ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑛 − 1 ) = 0 ) → ( ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
171 170 expimpd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑛 − 1 ) = 0 ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
172 ralun ⊢ ( ( ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ∧ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ∀ 𝑏 ∈ ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) )
173 npcan1 ⊢ ( 𝑛 ∈ ℂ → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
174 152 173 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
175 174 64 eqeltrd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
176 peano2zm ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 − 1 ) ∈ ℤ )
177 uzid ⊢ ( ( 𝑛 − 1 ) ∈ ℤ → ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) )
178 peano2uz ⊢ ( ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) → ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) )
179 24 176 177 178 4syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) )
180 174 179 eqeltrrd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) )
181 fzsplit2 ⊢ ( ( ( ( 𝑛 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑛 − 1 ) ) ) → ( 1 ... 𝑛 ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) ) )
182 175 180 181 syl2anc ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑛 ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) ) )
183 174 oveq1d ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) = ( 𝑛 ... 𝑛 ) )
184 fzsn ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ... 𝑛 ) = { 𝑛 } )
185 24 184 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 ... 𝑛 ) = { 𝑛 } )
186 183 185 eqtrd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) = { 𝑛 } )
187 186 uneq2d ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 1 ... ( 𝑛 − 1 ) ) ∪ ( ( ( 𝑛 − 1 ) + 1 ) ... 𝑛 ) ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) )
188 182 187 eqtrd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑛 ) = ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) )
189 188 raleqdv ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ∀ 𝑏 ∈ ( ( 1 ... ( 𝑛 − 1 ) ) ∪ { 𝑛 } ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
190 172 189 syl5ibr ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ∧ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
191 190 expdimp ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ( ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
192 191 con3d ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ( ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
193 192 adantrl ⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) → ( ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
194 193 expimpd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
195 171 194 jaod ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑛 − 1 ) = 0 ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ∨ ( ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
196 151 195 syl5bi ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) )
197 fveq2 ⊢ ( 𝑏 = 𝑛 → ( 𝑃 ‘ 𝑏 ) = ( 𝑃 ‘ 𝑛 ) )
198 197 neeq1d ⊢ ( 𝑏 = 𝑛 → ( ( 𝑃 ‘ 𝑏 ) ≠ 0 ↔ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) )
199 70 198 anbi12d ⊢ ( 𝑏 = 𝑛 → ( ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) ) )
200 199 ralsng ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) ) )
201 200 notbid ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ¬ ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) ) )
202 ianor ⊢ ( ¬ ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) ↔ ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ¬ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) )
203 nne ⊢ ( ¬ ( 𝑃 ‘ 𝑛 ) ≠ 0 ↔ ( 𝑃 ‘ 𝑛 ) = 0 )
204 203 orbi2i ⊢ ( ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ¬ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) ↔ ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) )
205 202 204 bitri ⊢ ( ¬ ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ≠ 0 ) ↔ ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) )
206 201 205 bitrdi ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ¬ ∀ 𝑏 ∈ { 𝑛 } ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ↔ ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) ) )
207 196 206 sylibd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑛 − 1 ) = 0 ∨ ( ( 𝑛 − 1 ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑏 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) ) ∧ ¬ ∀ 𝑏 ∈ ( 1 ... 𝑛 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) ) → ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) ) )
208 150 207 syld ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) ) )
209 208 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) ) )
210 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
211 210 fconst6 ⊢ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top
212 pttop ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) : ( 1 ... 𝑁 ) ⟶ Top ) → ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ∈ Top )
213 35 211 212 mp2an ⊢ ( ∏t ‘ ( ( 1 ... 𝑁 ) × { ( topGen ‘ ran (,) ) } ) ) ∈ Top
214 3 213 eqeltri ⊢ 𝑅 ∈ Top
215 reex ⊢ ℝ ∈ V
216 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
217 mapss ⊢ ( ( ℝ ∈ V ∧ ( 0 [,] 1 ) ⊆ ℝ ) → ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
218 215 216 217 mp2an ⊢ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) )
219 2 218 eqsstri ⊢ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) )
220 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
221 3 220 ptuniconst ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( topGen ‘ ran (,) ) ∈ Top ) → ( ℝ ↑m ( 1 ... 𝑁 ) ) = ∪ 𝑅 )
222 35 210 221 mp2an ⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) = ∪ 𝑅
223 222 restuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝐼 ⊆ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → 𝐼 = ∪ ( 𝑅 ↾t 𝐼 ) )
224 214 219 223 mp2an ⊢ 𝐼 = ∪ ( 𝑅 ↾t 𝐼 )
225 224 222 cnf ⊢ ( 𝐹 ∈ ( ( 𝑅 ↾t 𝐼 ) Cn 𝑅 ) → 𝐹 : 𝐼 ⟶ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
226 4 225 syl ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
227 226 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐹 : 𝐼 ⟶ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
228 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
229 elfzelz ⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → 𝑥 ∈ ℤ )
230 229 zred ⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → 𝑥 ∈ ℝ )
231 230 adantr ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ℝ )
232 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
233 232 adantl ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
234 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
235 234 adantl ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ≠ 0 )
236 231 233 235 redivcld ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 / 𝑘 ) ∈ ℝ )
237 elfzle1 ⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → 0 ≤ 𝑥 )
238 230 237 jca ⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
239 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
240 239 rpregt0d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
241 divge0 ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → 0 ≤ ( 𝑥 / 𝑘 ) )
242 238 240 241 syl2an ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝑥 / 𝑘 ) )
243 elfzle2 ⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → 𝑥 ≤ 𝑘 )
244 243 adantr ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ≤ 𝑘 )
245 1red ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ )
246 239 adantl ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ+ )
247 231 245 246 ledivmuld ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 / 𝑘 ) ≤ 1 ↔ 𝑥 ≤ ( 𝑘 · 1 ) ) )
248 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
249 248 mulid1d ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · 1 ) = 𝑘 )
250 249 breq2d ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ≤ ( 𝑘 · 1 ) ↔ 𝑥 ≤ 𝑘 ) )
251 250 adantl ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ≤ ( 𝑘 · 1 ) ↔ 𝑥 ≤ 𝑘 ) )
252 247 251 bitrd ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 / 𝑘 ) ≤ 1 ↔ 𝑥 ≤ 𝑘 ) )
253 244 252 mpbird ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 / 𝑘 ) ≤ 1 )
254 elicc01 ⊢ ( ( 𝑥 / 𝑘 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝑥 / 𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 / 𝑘 ) ∧ ( 𝑥 / 𝑘 ) ≤ 1 ) )
255 236 242 253 254 syl3anbrc ⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 / 𝑘 ) ∈ ( 0 [,] 1 ) )
256 255 ancoms ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( 𝑥 / 𝑘 ) ∈ ( 0 [,] 1 ) )
257 elsni ⊢ ( 𝑦 ∈ { 𝑘 } → 𝑦 = 𝑘 )
258 257 oveq2d ⊢ ( 𝑦 ∈ { 𝑘 } → ( 𝑥 / 𝑦 ) = ( 𝑥 / 𝑘 ) )
259 258 eleq1d ⊢ ( 𝑦 ∈ { 𝑘 } → ( ( 𝑥 / 𝑦 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑥 / 𝑘 ) ∈ ( 0 [,] 1 ) ) )
260 256 259 syl5ibrcom ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( 𝑦 ∈ { 𝑘 } → ( 𝑥 / 𝑦 ) ∈ ( 0 [,] 1 ) ) )
261 260 impr ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑦 ∈ { 𝑘 } ) ) → ( 𝑥 / 𝑦 ) ∈ ( 0 [,] 1 ) )
262 228 261 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ ( 0 ... 𝑘 ) ∧ 𝑦 ∈ { 𝑘 } ) ) → ( 𝑥 / 𝑦 ) ∈ ( 0 [,] 1 ) )
263 elun ⊢ ( 𝑦 ∈ ( { 1 } ∪ { 0 } ) ↔ ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ { 0 } ) )
264 fzofzp1 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( 𝑥 + 1 ) ∈ ( 0 ... 𝑘 ) )
265 elsni ⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
266 265 oveq2d ⊢ ( 𝑦 ∈ { 1 } → ( 𝑥 + 𝑦 ) = ( 𝑥 + 1 ) )
267 266 eleq1d ⊢ ( 𝑦 ∈ { 1 } → ( ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) ↔ ( 𝑥 + 1 ) ∈ ( 0 ... 𝑘 ) ) )
268 264 267 syl5ibrcom ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( 𝑦 ∈ { 1 } → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) ) )
269 elfzonn0 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → 𝑥 ∈ ℕ0 )
270 269 nn0cnd ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → 𝑥 ∈ ℂ )
271 270 addid1d ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( 𝑥 + 0 ) = 𝑥 )
272 elfzofz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → 𝑥 ∈ ( 0 ... 𝑘 ) )
273 271 272 eqeltrd ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( 𝑥 + 0 ) ∈ ( 0 ... 𝑘 ) )
274 elsni ⊢ ( 𝑦 ∈ { 0 } → 𝑦 = 0 )
275 274 oveq2d ⊢ ( 𝑦 ∈ { 0 } → ( 𝑥 + 𝑦 ) = ( 𝑥 + 0 ) )
276 275 eleq1d ⊢ ( 𝑦 ∈ { 0 } → ( ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) ↔ ( 𝑥 + 0 ) ∈ ( 0 ... 𝑘 ) ) )
277 273 276 syl5ibrcom ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( 𝑦 ∈ { 0 } → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) ) )
278 268 277 jaod ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( ( 𝑦 ∈ { 1 } ∨ 𝑦 ∈ { 0 } ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) ) )
279 263 278 syl5bi ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) → ( 𝑦 ∈ ( { 1 } ∪ { 0 } ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) ) )
280 279 imp ⊢ ( ( 𝑥 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑦 ∈ ( { 1 } ∪ { 0 } ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) )
281 280 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ ( 0 ..^ 𝑘 ) ∧ 𝑦 ∈ ( { 1 } ∪ { 0 } ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 ... 𝑘 ) )
282 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) )
283 xp1st ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
284 elmapfn ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
285 282 283 284 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) )
286 df-f ⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) Fn ( 1 ... 𝑁 ) ∧ ran ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 0 ..^ 𝑘 ) ) )
287 285 8 286 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) )
288 287 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ..^ 𝑘 ) )
289 1ex ⊢ 1 ∈ V
290 289 fconst ⊢ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 }
291 40 fconst ⊢ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 }
292 290 291 pm3.2i ⊢ ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } )
293 xp2nd ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) × { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ) → ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
294 282 293 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } )
295 fvex ⊢ ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ V
296 f1oeq1 ⊢ ( 𝑓 = ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) → ( 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) )
297 295 296 elab ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ { 𝑓 ∣ 𝑓 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) } ↔ ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
298 294 297 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
299 dff1o3 ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ↔ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) ∧ Fun ◡ ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
300 299 simprbi ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ◡ ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) )
301 imain ⊢ ( Fun ◡ ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
302 298 300 301 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
303 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℕ0 )
304 303 nn0red ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
305 304 ltp1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
306 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
307 305 306 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) = ∅ )
308 307 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ∅ ) )
309 ima0 ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ∅ ) = ∅
310 308 309 eqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
311 302 310 sylan9req ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ )
312 fun ⊢ ( ( ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) : ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ⟶ { 1 } ∧ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) : ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ⟶ { 0 } ) ∧ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∩ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ∅ ) → ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
313 292 311 312 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) )
314 imaundi ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
315 nn0p1nn ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ )
316 303 315 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ℕ )
317 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
318 316 317 eleqtrdi ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
319 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) )
320 fzsplit2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
321 318 319 320 syl2anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) )
322 321 imaeq2d ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) )
323 f1ofo ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) )
324 foima ⊢ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) : ( 1 ... 𝑁 ) –onto→ ( 1 ... 𝑁 ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
325 298 323 324 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
326 322 325 sylan9req ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
327 326 ancoms ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 1 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
328 314 327 eqtr3id ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) = ( 1 ... 𝑁 ) )
329 328 feq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) ∪ ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) ) ⟶ ( { 1 } ∪ { 0 } ) ↔ ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) ) )
330 313 329 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ( { 1 } ∪ { 0 } ) )
331 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
332 inidm ⊢ ( ( 1 ... 𝑁 ) ∩ ( 1 ... 𝑁 ) ) = ( 1 ... 𝑁 )
333 281 288 330 331 331 332 off ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f + ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝑘 ) )
334 6 feq1i ⊢ ( 𝑃 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝑘 ) ↔ ( ( 1st ‘ ( 𝐺 ‘ 𝑘 ) ) ∘f + ( ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( 1 ... 𝑗 ) ) × { 1 } ) ∪ ( ( ( 2nd ‘ ( 𝐺 ‘ 𝑘 ) ) “ ( ( 𝑗 + 1 ) ... 𝑁 ) ) × { 0 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝑘 ) )
335 333 334 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑃 : ( 1 ... 𝑁 ) ⟶ ( 0 ... 𝑘 ) )
336 vex ⊢ 𝑘 ∈ V
337 336 fconst ⊢ ( ( 1 ... 𝑁 ) × { 𝑘 } ) : ( 1 ... 𝑁 ) ⟶ { 𝑘 }
338 337 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) × { 𝑘 } ) : ( 1 ... 𝑁 ) ⟶ { 𝑘 } )
339 262 335 338 331 331 332 off ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
340 2 eleq2i ⊢ ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ↔ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) )
341 ovex ⊢ ( 0 [,] 1 ) ∈ V
342 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
343 341 342 elmap ⊢ ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
344 340 343 bitri ⊢ ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ↔ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) : ( 1 ... 𝑁 ) ⟶ ( 0 [,] 1 ) )
345 339 344 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 )
346 227 345 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
347 elmapi ⊢ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ℝ )
348 346 347 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) : ( 1 ... 𝑁 ) ⟶ ℝ )
349 348 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∈ ℝ )
350 349 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∈ ℝ )
351 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ℝ )
352 350 351 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) < 0 ↔ ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
353 ltle ⊢ ( ( ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) < 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
354 350 45 353 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) < 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
355 352 354 sylbird ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
356 248 234 div0d ⊢ ( 𝑘 ∈ ℕ → ( 0 / 𝑘 ) = 0 )
357 oveq1 ⊢ ( ( 𝑃 ‘ 𝑛 ) = 0 → ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) = ( 0 / 𝑘 ) )
358 357 eqeq1d ⊢ ( ( 𝑃 ‘ 𝑛 ) = 0 → ( ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) = 0 ↔ ( 0 / 𝑘 ) = 0 ) )
359 356 358 syl5ibrcom ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑃 ‘ 𝑛 ) = 0 → ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) = 0 ) )
360 359 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑛 ) = 0 → ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) = 0 ) )
361 335 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑃 Fn ( 1 ... 𝑁 ) )
362 fnconstg ⊢ ( 𝑘 ∈ V → ( ( 1 ... 𝑁 ) × { 𝑘 } ) Fn ( 1 ... 𝑁 ) )
363 336 362 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) × { 𝑘 } ) Fn ( 1 ... 𝑁 ) )
364 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑛 ) = ( 𝑃 ‘ 𝑛 ) )
365 336 fvconst2 ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { 𝑘 } ) ‘ 𝑛 ) = 𝑘 )
366 365 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { 𝑘 } ) ‘ 𝑛 ) = 𝑘 )
367 361 363 331 331 332 364 366 ofval ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) )
368 367 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) )
369 368 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 ↔ ( ( 𝑃 ‘ 𝑛 ) / 𝑘 ) = 0 ) )
370 360 369 sylibrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑛 ) = 0 → ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 ) )
371 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
372 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
373 345 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 )
374 ovex ⊢ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ V
375 eleq1 ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( 𝑧 ∈ 𝐼 ↔ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 ) )
376 fveq1 ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( 𝑧 ‘ 𝑛 ) = ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) )
377 376 eqeq1d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝑧 ‘ 𝑛 ) = 0 ↔ ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 ) )
378 fveq2 ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) )
379 378 fveq1d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) = ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )
380 379 breq1d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ↔ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
381 377 380 imbi12d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( ( 𝑧 ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ↔ ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) ) )
382 375 381 imbi12d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝑧 ∈ 𝐼 → ( ( 𝑧 ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ↔ ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 → ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) ) ) )
383 382 imbi2d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑧 ∈ 𝐼 → ( ( 𝑧 ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 → ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) ) ) ) )
384 383 imbi2d ⊢ ( 𝑧 = ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) → ( ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑧 ∈ 𝐼 → ( ( 𝑧 ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 → ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) ) ) ) ) )
385 5 3exp2 ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑧 ∈ 𝐼 → ( ( 𝑧 ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑛 ) ≤ 0 ) ) ) )
386 374 384 385 vtocl ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ∈ 𝐼 → ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) ) ) )
387 371 372 373 386 syl3c ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
388 370 387 syld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑛 ) = 0 → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
389 355 388 jaod ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ¬ 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∨ ( 𝑃 ‘ 𝑛 ) = 0 ) → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
390 209 389 syld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
391 390 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
392 391 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑛 − 1 ) = sup ( ( { 0 } ∪ { 𝑎 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑏 ∈ ( 1 ... 𝑎 ) ( 0 ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑏 ) ∧ ( 𝑃 ‘ 𝑏 ) ≠ 0 ) } ) , ℝ , < ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
393 115 392 mpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 )
394 breq ⊢ ( 𝑟 = ◡ ≤ → ( 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ↔ 0 ◡ ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
395 fvex ⊢ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ∈ V
396 40 395 brcnv ⊢ ( 0 ◡ ≤ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 )
397 394 396 bitrdi ⊢ ( 𝑟 = ◡ ≤ → ( 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ↔ ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
398 397 rexbidv ⊢ ( 𝑟 = ◡ ≤ → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ≤ 0 ) )
399 393 398 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑟 = ◡ ≤ → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
400 84 399 jaod ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝑟 = ≤ ∨ 𝑟 = ◡ ≤ ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
401 10 400 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑟 ∈ { ≤ , ◡ ≤ } → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) )
402 401 exp32 ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑟 ∈ { ≤ , ◡ ≤ } → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) ) ) ) )
403 402 3imp2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ∧ 𝑟 ∈ { ≤ , ◡ ≤ } ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 0 𝑟 ( ( 𝐹 ‘ ( 𝑃 ∘f / ( ( 1 ... 𝑁 ) × { 𝑘 } ) ) ) ‘ 𝑛 ) )