Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℕ) |
3 | | fvoveq1 7236 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))) |
4 | 3 | fveq1d 6719 |
. . . . . . . . . . . 12
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏)) |
5 | 4 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏))) |
6 | | fveq1 6716 |
. . . . . . . . . . . 12
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝‘𝑏) = (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏)) |
7 | 6 | neeq1d 3000 |
. . . . . . . . . . 11
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑏) ≠ 0 ↔ (((1st
‘𝑠)
∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)) |
8 | 5, 7 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
9 | 8 | ralbidv 3118 |
. . . . . . . . 9
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
10 | 9 | rabbidv 3390 |
. . . . . . . 8
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) |
11 | 10 | uneq2d 4077 |
. . . . . . 7
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})) |
12 | 11 | supeq1d 9062 |
. . . . . 6
⊢ (𝑝 = ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
13 | 1 | nnnn0d 12150 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
14 | | 0elfz 13209 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
16 | 15 | snssd 4722 |
. . . . . . . . 9
⊢ (𝜑 → {0} ⊆ (0...𝑁)) |
17 | | ssrab2 3993 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ⊆ (1...𝑁) |
18 | | fz1ssfz0 13208 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
(0...𝑁) |
19 | 17, 18 | sstri 3910 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ⊆ (0...𝑁) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ⊆ (0...𝑁)) |
21 | 16, 20 | unssd 4100 |
. . . . . . . 8
⊢ (𝜑 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ⊆ (0...𝑁)) |
22 | | ltso 10913 |
. . . . . . . . 9
⊢ < Or
ℝ |
23 | | snfi 8721 |
. . . . . . . . . . 11
⊢ {0}
∈ Fin |
24 | | fzfi 13545 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ∈
Fin |
25 | | rabfi 8900 |
. . . . . . . . . . . 12
⊢
((1...𝑁) ∈ Fin
→ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ∈ Fin) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ∈ Fin |
27 | | unfi 8850 |
. . . . . . . . . . 11
⊢ (({0}
∈ Fin ∧ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ∈ Fin) → ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ∈ Fin) |
28 | 23, 26, 27 | mp2an 692 |
. . . . . . . . . 10
⊢ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ∈ Fin |
29 | | c0ex 10827 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
30 | 29 | snid 4577 |
. . . . . . . . . . 11
⊢ 0 ∈
{0} |
31 | | elun1 4090 |
. . . . . . . . . . 11
⊢ (0 ∈
{0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})) |
32 | | ne0i 4249 |
. . . . . . . . . . 11
⊢ (0 ∈
({0} ∪ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ≠ ∅) |
33 | 30, 31, 32 | mp2b 10 |
. . . . . . . . . 10
⊢ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ≠ ∅ |
34 | | 0red 10836 |
. . . . . . . . . . . . 13
⊢ ((𝜑 → 𝑁 ∈ ℕ) → 0 ∈
ℝ) |
35 | 34 | snssd 4722 |
. . . . . . . . . . . 12
⊢ ((𝜑 → 𝑁 ∈ ℕ) → {0} ⊆
ℝ) |
36 | 1, 35 | ax-mp 5 |
. . . . . . . . . . 11
⊢ {0}
⊆ ℝ |
37 | | elfzelz 13112 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
38 | 37 | ssriv 3905 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
ℤ |
39 | | zssre 12183 |
. . . . . . . . . . . . 13
⊢ ℤ
⊆ ℝ |
40 | 38, 39 | sstri 3910 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
ℝ |
41 | 17, 40 | sstri 3910 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ⊆ ℝ |
42 | 36, 41 | unssi 4099 |
. . . . . . . . . 10
⊢ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ⊆ ℝ |
43 | 28, 33, 42 | 3pm3.2i 1341 |
. . . . . . . . 9
⊢ (({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ⊆ ℝ) |
44 | | fisupcl 9085 |
. . . . . . . . 9
⊢ (( <
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)})) |
45 | 22, 43, 44 | mp2an 692 |
. . . . . . . 8
⊢ sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) |
46 | | ssel 3893 |
. . . . . . . 8
⊢ (({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ⊆ (0...𝑁) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈
(0...𝑁))) |
47 | 21, 45, 46 | mpisyl 21 |
. . . . . . 7
⊢ (𝜑 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈
(0...𝑁)) |
48 | 47 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑝:(1...𝑁)⟶(0...𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈
(0...𝑁)) |
49 | | elfznn 13141 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) |
50 | | nngt0 11861 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) |
51 | 50 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) → 0 < 𝑛) |
52 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((0 ≤
((𝐹‘(𝑝 ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → (𝑝‘𝑏) ≠ 0) |
53 | 52 | ralimi 3083 |
. . . . . . . . . . . . 13
⊢
(∀𝑏 ∈
(1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑠)(𝑝‘𝑏) ≠ 0) |
54 | | elfznn 13141 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (1...𝑁) → 𝑠 ∈ ℕ) |
55 | | nnre 11837 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
56 | | nnre 11837 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℕ → 𝑠 ∈
ℝ) |
57 | | lenlt 10911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝑛 ≤ 𝑠 ↔ ¬ 𝑠 < 𝑛)) |
58 | 55, 56, 57 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛 ≤ 𝑠 ↔ ¬ 𝑠 < 𝑛)) |
59 | | elfz1b 13181 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑠) ↔ (𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛 ≤ 𝑠)) |
60 | 59 | biimpri 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛 ≤ 𝑠) → 𝑛 ∈ (1...𝑠)) |
61 | 60 | 3expia 1123 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛 ≤ 𝑠 → 𝑛 ∈ (1...𝑠))) |
62 | 58, 61 | sylbird 263 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (¬
𝑠 < 𝑛 → 𝑛 ∈ (1...𝑠))) |
63 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = 𝑛 → (𝑝‘𝑏) = (𝑝‘𝑛)) |
64 | 63 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑛 → ((𝑝‘𝑏) = 0 ↔ (𝑝‘𝑛) = 0)) |
65 | 64 | rspcev 3537 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ (1...𝑠) ∧ (𝑝‘𝑛) = 0) → ∃𝑏 ∈ (1...𝑠)(𝑝‘𝑏) = 0) |
66 | 65 | expcom 417 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘𝑛) = 0 → (𝑛 ∈ (1...𝑠) → ∃𝑏 ∈ (1...𝑠)(𝑝‘𝑏) = 0)) |
67 | 62, 66 | sylan9 511 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) ∧ (𝑝‘𝑛) = 0) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝‘𝑏) = 0)) |
68 | 67 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝‘𝑏) = 0)) |
69 | | nne 2944 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑝‘𝑏) ≠ 0 ↔ (𝑝‘𝑏) = 0) |
70 | 69 | rexbii 3170 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑏 ∈
(1...𝑠) ¬ (𝑝‘𝑏) ≠ 0 ↔ ∃𝑏 ∈ (1...𝑠)(𝑝‘𝑏) = 0) |
71 | | rexnal 3160 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑏 ∈
(1...𝑠) ¬ (𝑝‘𝑏) ≠ 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝‘𝑏) ≠ 0) |
72 | 70, 71 | bitr3i 280 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑏 ∈
(1...𝑠)(𝑝‘𝑏) = 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝‘𝑏) ≠ 0) |
73 | 68, 72 | syl6ib 254 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ¬ ∀𝑏 ∈ (1...𝑠)(𝑝‘𝑏) ≠ 0)) |
74 | 73 | con4d 115 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (∀𝑏 ∈ (1...𝑠)(𝑝‘𝑏) ≠ 0 → 𝑠 < 𝑛)) |
75 | 54, 74 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(𝑝‘𝑏) ≠ 0 → 𝑠 < 𝑛)) |
76 | 53, 75 | syl5 34 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → 𝑠 < 𝑛)) |
77 | 76 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) → ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → 𝑠 < 𝑛)) |
78 | | ralunb 4105 |
. . . . . . . . . . . 12
⊢
(∀𝑠 ∈
({0} ∪ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}𝑠 < 𝑛)) |
79 | | breq1 5056 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 0 → (𝑠 < 𝑛 ↔ 0 < 𝑛)) |
80 | 29, 79 | ralsn 4597 |
. . . . . . . . . . . . 13
⊢
(∀𝑠 ∈
{0}𝑠 < 𝑛 ↔ 0 < 𝑛) |
81 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑠 → (1...𝑎) = (1...𝑠)) |
82 | 81 | raleqdv 3325 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑠 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
83 | 82 | ralrab 3607 |
. . . . . . . . . . . . 13
⊢
(∀𝑠 ∈
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}𝑠 < 𝑛 ↔ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → 𝑠 < 𝑛)) |
84 | 80, 83 | anbi12i 630 |
. . . . . . . . . . . 12
⊢
((∀𝑠 ∈
{0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}𝑠 < 𝑛) ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → 𝑠 < 𝑛))) |
85 | 78, 84 | bitri 278 |
. . . . . . . . . . 11
⊢
(∀𝑠 ∈
({0} ∪ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → 𝑠 < 𝑛))) |
86 | 51, 77, 85 | sylanbrc 586 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) → ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑠 < 𝑛) |
87 | | breq1 5056 |
. . . . . . . . . . 11
⊢ (𝑠 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) → (𝑠 < 𝑛 ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < 𝑛)) |
88 | 87 | rspcva 3535 |
. . . . . . . . . 10
⊢
((sup(({0} ∪ {𝑎
∈ (1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ∧ ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑠 < 𝑛) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < 𝑛) |
89 | 45, 86, 88 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑝‘𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < 𝑛) |
90 | 49, 89 | sylan 583 |
. . . . . . . 8
⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑝‘𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < 𝑛) |
91 | 90 | 3adant2 1133 |
. . . . . . 7
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < 𝑛) |
92 | 91 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 0)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < 𝑛) |
93 | 37 | zred 12282 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ) |
94 | 93 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) → 𝑛 ∈ ℝ) |
95 | 94 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → 𝑛 ∈ ℝ) |
96 | | simpr1 1196 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → 𝑛 ∈ (1...𝑁)) |
97 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → 𝜑) |
98 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑘 ∈ ℕ) |
99 | | elfzelz 13112 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℤ) |
100 | 99 | zred 12282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℝ) |
101 | | nndivre 11871 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ) |
102 | 100, 101 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ) |
103 | | elfzle1 13115 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (0...𝑘) → 0 ≤ 𝑖) |
104 | 100, 103 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (0...𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖)) |
105 | | nnrp 12597 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
106 | 105 | rpregt0d 12634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
107 | | divge0 11701 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑖 ∈ ℝ ∧ 0 ≤
𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝑖 / 𝑘)) |
108 | 104, 106,
107 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘)) |
109 | | elfzle2 13116 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (0...𝑘) → 𝑖 ≤ 𝑘) |
110 | 109 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ≤ 𝑘) |
111 | 100 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ) |
112 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈
ℝ) |
113 | 105 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
114 | 111, 112,
113 | ledivmuld 12681 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1))) |
115 | | nncn 11838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
116 | 115 | mulid1d 10850 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘) |
117 | 116 | breq2d 5065 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖 ≤ 𝑘)) |
118 | 117 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖 ≤ 𝑘)) |
119 | 114, 118 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ 𝑘)) |
120 | 110, 119 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1) |
121 | | elicc01 13054 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1)) |
122 | 102, 108,
120, 121 | syl3anbrc 1345 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1)) |
123 | 122 | ancoms 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1)) |
124 | | elsni 4558 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ {𝑘} → 𝑗 = 𝑘) |
125 | 124 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘)) |
126 | 125 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1))) |
127 | 123, 126 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1))) |
128 | 127 | impr 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1)) |
129 | 98, 128 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1)) |
130 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑝:(1...𝑁)⟶(0...𝑘)) |
131 | | vex 3412 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑘 ∈ V |
132 | 131 | fconst 6605 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑁) ×
{𝑘}):(1...𝑁)⟶{𝑘} |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}) |
134 | | fzfid 13546 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (1...𝑁) ∈ Fin) |
135 | | inidm 4133 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
136 | 129, 130,
133, 134, 134, 135 | off 7486 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝 ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
137 | | poimir.i |
. . . . . . . . . . . . . . . . 17
⊢ 𝐼 = ((0[,]1) ↑m
(1...𝑁)) |
138 | 137 | eleq2i 2829 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m
(1...𝑁))) |
139 | | ovex 7246 |
. . . . . . . . . . . . . . . . 17
⊢ (0[,]1)
∈ V |
140 | | ovex 7246 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V |
141 | 139, 140 | elmap 8552 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∘f /
((1...𝑁) × {𝑘})) ∈ ((0[,]1)
↑m (1...𝑁))
↔ (𝑝
∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
142 | 138, 141 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∘f /
((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝 ∘f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1)) |
143 | 136, 142 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼) |
144 | 143 | 3adantr3 1173 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼) |
145 | | 3anass 1097 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘))) |
146 | | ancom 464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) |
147 | 145, 146 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) |
148 | | ffn 6545 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝:(1...𝑁)⟶(0...𝑘) → 𝑝 Fn (1...𝑁)) |
149 | 148 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → 𝑝 Fn (1...𝑁)) |
150 | | fnconstg 6607 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
151 | 131, 150 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁)) |
152 | | fzfid 13546 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → (1...𝑁) ∈ Fin) |
153 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑝‘𝑛) = 𝑘) |
154 | 131 | fvconst2 7019 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘) |
155 | 154 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘) |
156 | 149, 151,
152, 152, 135, 153, 155 | ofval 7479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘)) |
157 | 156 | anasss 470 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘)) |
158 | 147, 157 | sylan2b 597 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘)) |
159 | | nnne0 11864 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
160 | 115, 159 | dividd 11606 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 / 𝑘) = 1) |
161 | 160 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → (𝑘 / 𝑘) = 1) |
162 | 158, 161 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = 1) |
163 | | ovex 7246 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∘f /
((1...𝑁) × {𝑘})) ∈ V |
164 | | eleq1 2825 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → (𝑧 ∈ 𝐼 ↔ (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼)) |
165 | | fveq1 6716 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → (𝑧‘𝑛) = ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛)) |
166 | 165 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → ((𝑧‘𝑛) = 1 ↔ ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) |
167 | 164, 166 | 3anbi23d 1441 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))) |
168 | 167 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)))) |
169 | | fveq2 6717 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → (𝐹‘𝑧) = (𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))) |
170 | 169 | fveq1d 6719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛)) |
171 | 170 | breq2d 5065 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → (0 ≤ ((𝐹‘𝑧)‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛))) |
172 | 168, 171 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑝 ∘f / ((1...𝑁) × {𝑘})) → (((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) ↔ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛)))) |
173 | | poimir.3 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 1)) → 0 ≤ ((𝐹‘𝑧)‘𝑛)) |
174 | 163, 172,
173 | vtocl 3474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝 ∘f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝 ∘f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛)) |
175 | 97, 96, 144, 162, 174 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → 0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛)) |
176 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
177 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘) → (𝑝‘𝑛) = 𝑘) |
178 | | neeq1 3003 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝‘𝑛) = 𝑘 → ((𝑝‘𝑛) ≠ 0 ↔ 𝑘 ≠ 0)) |
179 | 159, 178 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → ((𝑝‘𝑛) = 𝑘 → (𝑝‘𝑛) ≠ 0)) |
180 | 179 | imp 410 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ (𝑝‘𝑛) = 𝑘) → (𝑝‘𝑛) ≠ 0) |
181 | 176, 177,
180 | syl2an 599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → (𝑝‘𝑛) ≠ 0) |
182 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑛 ∈ V |
183 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑛 → ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛)) |
184 | 183 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛))) |
185 | 63 | neeq1d 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑛 → ((𝑝‘𝑏) ≠ 0 ↔ (𝑝‘𝑛) ≠ 0)) |
186 | 184, 185 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝‘𝑛) ≠ 0))) |
187 | 182, 186 | ralsn 4597 |
. . . . . . . . . . . 12
⊢
(∀𝑏 ∈
{𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝‘𝑛) ≠ 0)) |
188 | 175, 181,
187 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) |
189 | 37 | zcnd 12283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) |
190 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ) |
191 | 189, 190 | subeq0ad 11199 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1)) |
192 | 191 | biimpcd 252 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → 𝑛 = 1)) |
193 | | 1z 12207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℤ |
194 | | fzsn 13154 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℤ → (1...1) = {1}) |
195 | 193, 194 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...1) =
{1} |
196 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (1...𝑛) = (1...1)) |
197 | | sneq 4551 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → {𝑛} = {1}) |
198 | 195, 196,
197 | 3eqtr4a 2804 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (1...𝑛) = {𝑛}) |
199 | 198 | raleqdv 3325 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
200 | 199 | biimprd 251 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
201 | 192, 200 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
202 | | ralun 4106 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑏 ∈
(1...(𝑛 − 1))(0 ≤
((𝐹‘(𝑝 ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) |
203 | | npcan1 11257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛) |
204 | 189, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛) |
205 | | elfzuz 13108 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈
(ℤ≥‘1)) |
206 | 204, 205 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈
(ℤ≥‘1)) |
207 | | peano2zm 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℤ → (𝑛 − 1) ∈
ℤ) |
208 | | uzid 12453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 − 1) ∈ ℤ
→ (𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1))) |
209 | | peano2uz 12497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈
(ℤ≥‘(𝑛 − 1))) |
210 | 37, 207, 208, 209 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈
(ℤ≥‘(𝑛 − 1))) |
211 | 204, 210 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ≥‘(𝑛 − 1))) |
212 | | fzsplit2 13137 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑛 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛))) |
213 | 206, 211,
212 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛))) |
214 | 204 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛)) |
215 | | fzsn 13154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛}) |
216 | 37, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛}) |
217 | 214, 216 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛}) |
218 | 217 | uneq2d 4077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛})) |
219 | 213, 218 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛})) |
220 | 219 | raleqdv 3325 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
221 | 202, 220 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
222 | 221 | expd 419 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
223 | 222 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑏 ∈
(1...(𝑛 − 1))(0 ≤
((𝐹‘(𝑝 ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
224 | 223 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
225 | 201, 224 | jaoi 857 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
226 | 225 | imdistand 574 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) → ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
227 | 226 | com12 32 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
228 | | elun 4063 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 1) ∈ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})) |
229 | | ovex 7246 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 − 1) ∈
V |
230 | 229 | elsn 4556 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 1) ∈ {0} ↔
(𝑛 − 1) =
0) |
231 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1))) |
232 | 231 | raleqdv 3325 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
233 | 232 | elrab 3602 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
234 | 230, 233 | orbi12i 915 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 − 1) ∈ {0} ∨
(𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
235 | 228, 234 | bitri 278 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 1) ∈ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)))) |
236 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛)) |
237 | 236 | raleqdv 3325 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
238 | 237 | elrab 3602 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0))) |
239 | 227, 235,
238 | 3imtr4g 299 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})) |
240 | | elun2 4091 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})) |
241 | 239, 240 | syl6 35 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}))) |
242 | 96, 188, 241 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}))) |
243 | | fimaxre2 11777 |
. . . . . . . . . . . . 13
⊢ ((({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ∈ Fin) → ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑗 ≤ 𝑖) |
244 | 42, 28, 243 | mp2an 692 |
. . . . . . . . . . . 12
⊢
∃𝑖 ∈
ℝ ∀𝑗 ∈
({0} ∪ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑗 ≤ 𝑖 |
245 | 42, 33, 244 | 3pm3.2i 1341 |
. . . . . . . . . . 11
⊢ (({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})𝑗 ≤ 𝑖) |
246 | 245 | suprubii 11807 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
)) |
247 | 242, 246 | syl6 35 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
248 | | ltm1 11674 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛) |
249 | | peano2rem 11145 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
250 | 42, 45 | sselii 3897 |
. . . . . . . . . . . 12
⊢ sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈
ℝ |
251 | | ltletr 10924 |
. . . . . . . . . . . 12
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ ∧
sup(({0} ∪ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ)
→ (((𝑛 − 1) <
𝑛 ∧ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
252 | 250, 251 | mp3an3 1452 |
. . . . . . . . . . 11
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ) →
(((𝑛 − 1) < 𝑛 ∧ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
253 | 249, 252 | mpancom 688 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (((𝑛 − 1) < 𝑛 ∧ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
254 | 248, 253 | mpand 695 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ → (𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
255 | 95, 247, 254 | sylsyld 61 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
256 | 250 | ltnri 10941 |
. . . . . . . . . 10
⊢ ¬
sup(({0} ∪ {𝑎 ∈
(1...𝑁) ∣
∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) |
257 | | breq1 5056 |
. . . . . . . . . 10
⊢ (sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) < sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ↔ (𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
))) |
258 | 256, 257 | mtbii 329 |
. . . . . . . . 9
⊢ (sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → ¬ (𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, <
)) |
259 | 258 | necon2ai 2970 |
. . . . . . . 8
⊢ ((𝑛 − 1) < sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) → sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)) |
260 | 255, 259 | syl6 35 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))) |
261 | | eleq1 2825 |
. . . . . . . . 9
⊢ (sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) ↔ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}))) |
262 | 45, 261 | mpbii 236 |
. . . . . . . 8
⊢ (sup(({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (𝑛 − 1) ∈ ({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)})) |
263 | 262 | necon3bi 2967 |
. . . . . . 7
⊢ (¬
(𝑛 − 1) ∈ ({0}
∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)) |
264 | 260, 263 | pm2.61d1 183 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝‘𝑛) = 𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝 ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝‘𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)) |
265 | 2, 12, 48, 92, 264, 176 | poimirlem28 35542 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
266 | | nn0ex 12096 |
. . . . . . . . . . . 12
⊢
ℕ0 ∈ V |
267 | | fzo0ssnn0 13323 |
. . . . . . . . . . . 12
⊢
(0..^𝑘) ⊆
ℕ0 |
268 | | mapss 8570 |
. . . . . . . . . . . 12
⊢
((ℕ0 ∈ V ∧ (0..^𝑘) ⊆ ℕ0) →
((0..^𝑘) ↑m
(1...𝑁)) ⊆
(ℕ0 ↑m (1...𝑁))) |
269 | 266, 267,
268 | mp2an 692 |
. . . . . . . . . . 11
⊢
((0..^𝑘)
↑m (1...𝑁))
⊆ (ℕ0 ↑m (1...𝑁)) |
270 | | xpss1 5570 |
. . . . . . . . . . 11
⊢
(((0..^𝑘)
↑m (1...𝑁))
⊆ (ℕ0 ↑m (1...𝑁)) → (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ⊆ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
271 | 269, 270 | ax-mp 5 |
. . . . . . . . . 10
⊢
(((0..^𝑘)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ⊆ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
272 | 271 | sseli 3896 |
. . . . . . . . 9
⊢ (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
273 | | xp1st 7793 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁))) |
274 | | elmapi 8530 |
. . . . . . . . . 10
⊢
((1st ‘𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)) → (1st ‘𝑠):(1...𝑁)⟶(0..^𝑘)) |
275 | | frn 6552 |
. . . . . . . . . 10
⊢
((1st ‘𝑠):(1...𝑁)⟶(0..^𝑘) → ran (1st ‘𝑠) ⊆ (0..^𝑘)) |
276 | 273, 274,
275 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ran (1st ‘𝑠) ⊆ (0..^𝑘)) |
277 | 272, 276 | jca 515 |
. . . . . . . 8
⊢ (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st ‘𝑠) ⊆ (0..^𝑘))) |
278 | 277 | anim1i 618 |
. . . . . . 7
⊢ ((𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ((𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st ‘𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
279 | | anass 472 |
. . . . . . 7
⊢ (((𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st ‘𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)))) |
280 | 278, 279 | sylib 221 |
. . . . . 6
⊢ ((𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → (𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)))) |
281 | 280 | reximi2 3167 |
. . . . 5
⊢
(∃𝑠 ∈
(((0..^𝑘)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) →
∃𝑠 ∈
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
282 | 265, 281 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
283 | 282 | ralrimiva 3105 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
284 | | nnex 11836 |
. . . 4
⊢ ℕ
∈ V |
285 | 140, 266 | ixpconst 8588 |
. . . . . . 7
⊢ X𝑛 ∈
(1...𝑁)ℕ0
= (ℕ0 ↑m (1...𝑁)) |
286 | | omelon 9261 |
. . . . . . . . . 10
⊢ ω
∈ On |
287 | | nn0ennn 13552 |
. . . . . . . . . . 11
⊢
ℕ0 ≈ ℕ |
288 | | nnenom 13553 |
. . . . . . . . . . 11
⊢ ℕ
≈ ω |
289 | 287, 288 | entr2i 8683 |
. . . . . . . . . 10
⊢ ω
≈ ℕ0 |
290 | | isnumi 9562 |
. . . . . . . . . 10
⊢ ((ω
∈ On ∧ ω ≈ ℕ0) → ℕ0
∈ dom card) |
291 | 286, 289,
290 | mp2an 692 |
. . . . . . . . 9
⊢
ℕ0 ∈ dom card |
292 | 291 | rgenw 3073 |
. . . . . . . 8
⊢
∀𝑛 ∈
(1...𝑁)ℕ0
∈ dom card |
293 | | finixpnum 35499 |
. . . . . . . 8
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑛 ∈
(1...𝑁)ℕ0
∈ dom card) → X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom
card) |
294 | 24, 292, 293 | mp2an 692 |
. . . . . . 7
⊢ X𝑛 ∈
(1...𝑁)ℕ0
∈ dom card |
295 | 285, 294 | eqeltrri 2835 |
. . . . . 6
⊢
(ℕ0 ↑m (1...𝑁)) ∈ dom card |
296 | 140, 140 | mapval 8520 |
. . . . . . . . 9
⊢
((1...𝑁)
↑m (1...𝑁))
= {𝑓 ∣ 𝑓:(1...𝑁)⟶(1...𝑁)} |
297 | | mapfi 8972 |
. . . . . . . . . 10
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑁)
↑m (1...𝑁))
∈ Fin) |
298 | 24, 24, 297 | mp2an 692 |
. . . . . . . . 9
⊢
((1...𝑁)
↑m (1...𝑁))
∈ Fin |
299 | 296, 298 | eqeltrri 2835 |
. . . . . . . 8
⊢ {𝑓 ∣ 𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin |
300 | | f1of 6661 |
. . . . . . . . 9
⊢ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑓:(1...𝑁)⟶(1...𝑁)) |
301 | 300 | ss2abi 3980 |
. . . . . . . 8
⊢ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓 ∣ 𝑓:(1...𝑁)⟶(1...𝑁)} |
302 | | ssfi 8851 |
. . . . . . . 8
⊢ (({𝑓 ∣ 𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin ∧ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓 ∣ 𝑓:(1...𝑁)⟶(1...𝑁)}) → {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin) |
303 | 299, 301,
302 | mp2an 692 |
. . . . . . 7
⊢ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin |
304 | | finnum 9564 |
. . . . . . 7
⊢ ({𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin → {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) |
305 | 303, 304 | ax-mp 5 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card |
306 | | xpnum 9567 |
. . . . . 6
⊢
(((ℕ0 ↑m (1...𝑁)) ∈ dom card ∧ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) →
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card) |
307 | 295, 305,
306 | mp2an 692 |
. . . . 5
⊢
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card |
308 | | ssrab2 3993 |
. . . . . . . 8
⊢ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
309 | 308 | rgenw 3073 |
. . . . . . 7
⊢
∀𝑘 ∈
ℕ {𝑠 ∈
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
310 | | ss2iun 4922 |
. . . . . . 7
⊢
(∀𝑘 ∈
ℕ {𝑠 ∈
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
∪ 𝑘 ∈ ℕ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
311 | 309, 310 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
∪ 𝑘 ∈ ℕ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
312 | | 1nn 11841 |
. . . . . . 7
⊢ 1 ∈
ℕ |
313 | | ne0i 4249 |
. . . . . . 7
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
314 | | iunconst 4913 |
. . . . . . 7
⊢ (ℕ
≠ ∅ → ∪ 𝑘 ∈ ℕ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
315 | 312, 313,
314 | mp2b 10 |
. . . . . 6
⊢ ∪ 𝑘 ∈ ℕ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
316 | 311, 315 | sseqtri 3937 |
. . . . 5
⊢ ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
317 | | ssnum 9653 |
. . . . 5
⊢
((((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card ∧ ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom
card) |
318 | 307, 316,
317 | mp2an 692 |
. . . 4
⊢ ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom
card |
319 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑠 = (𝑔‘𝑘) → (1st ‘𝑠) = (1st
‘(𝑔‘𝑘))) |
320 | 319 | rneqd 5807 |
. . . . . . 7
⊢ (𝑠 = (𝑔‘𝑘) → ran (1st ‘𝑠) = ran (1st
‘(𝑔‘𝑘))) |
321 | 320 | sseq1d 3932 |
. . . . . 6
⊢ (𝑠 = (𝑔‘𝑘) → (ran (1st ‘𝑠) ⊆ (0..^𝑘) ↔ ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘))) |
322 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝑔‘𝑘) → (2nd ‘𝑠) = (2nd
‘(𝑔‘𝑘))) |
323 | 322 | imaeq1d 5928 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝑔‘𝑘) → ((2nd ‘𝑠) “ (1...𝑗)) = ((2nd
‘(𝑔‘𝑘)) “ (1...𝑗))) |
324 | 323 | xpeq1d 5580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = (𝑔‘𝑘) → (((2nd ‘𝑠) “ (1...𝑗)) × {1}) =
(((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) × {1})) |
325 | 322 | imaeq1d 5928 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝑔‘𝑘) → ((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁))) |
326 | 325 | xpeq1d 5580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = (𝑔‘𝑘) → (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) |
327 | 324, 326 | uneq12d 4078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (𝑔‘𝑘) → ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪
(((2nd ‘𝑠)
“ ((𝑗 + 1)...𝑁)) × {0})) =
((((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
328 | 319, 327 | oveq12d 7231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝑔‘𝑘) → ((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(𝑔‘𝑘)) ∘f +
((((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
329 | 328 | fvoveq1d 7235 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝑔‘𝑘) → (𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))) |
330 | 329 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑔‘𝑘) → ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏)) |
331 | 330 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑔‘𝑘) → (0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏))) |
332 | 328 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝑔‘𝑘) → (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏)) |
333 | 332 | neeq1d 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (𝑔‘𝑘) → ((((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st
‘(𝑔‘𝑘)) ∘f +
((((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)) |
334 | 331, 333 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑔‘𝑘) → ((0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
335 | 334 | ralbidv 3118 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑔‘𝑘) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
336 | 335 | rabbidv 3390 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝑔‘𝑘) → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) |
337 | 336 | uneq2d 4077 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑔‘𝑘) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})) |
338 | 337 | supeq1d 9062 |
. . . . . . . . 9
⊢ (𝑠 = (𝑔‘𝑘) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
339 | 338 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑠 = (𝑔‘𝑘) → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
340 | 339 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑠 = (𝑔‘𝑘) → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔
∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
341 | 340 | ralbidv 3118 |
. . . . . 6
⊢ (𝑠 = (𝑔‘𝑘) → (∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔
∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
342 | 321, 341 | anbi12d 634 |
. . . . 5
⊢ (𝑠 = (𝑔‘𝑘) → ((ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (ran
(1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)))) |
343 | 342 | ac6num 10093 |
. . . 4
⊢ ((ℕ
∈ V ∧ ∪ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st
‘𝑠) ⊆
(0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom
card ∧ ∀𝑘 ∈
ℕ ∃𝑠 ∈
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) →
∃𝑔(𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)))) |
344 | 284, 318,
343 | mp3an12 1453 |
. . 3
⊢
(∀𝑘 ∈
ℕ ∃𝑠 ∈
((ℕ0 ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st ‘𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘𝑠) ∘f +
((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd
‘𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) →
∃𝑔(𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)))) |
345 | 283, 344 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)))) |
346 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑁 ∈
ℕ) |
347 | | poimir.r |
. . . 4
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
348 | | poimir.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
349 | 348 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝐹 ∈ ((𝑅 ↾t 𝐼) Cn 𝑅)) |
350 | | eqid 2737 |
. . . 4
⊢ ((𝐹‘(((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑛) = ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑛) |
351 | | simplr 769 |
. . . 4
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
352 | | simpl 486 |
. . . . . . 7
⊢ ((ran
(1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ran
(1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘)) |
353 | 352 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ (ran (1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) →
∀𝑘 ∈ ℕ
ran (1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘)) |
354 | 353 | adantl 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) →
∀𝑘 ∈ ℕ
ran (1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘)) |
355 | | 2fveq3 6722 |
. . . . . . . 8
⊢ (𝑘 = 𝑝 → (1st ‘(𝑔‘𝑘)) = (1st ‘(𝑔‘𝑝))) |
356 | 355 | rneqd 5807 |
. . . . . . 7
⊢ (𝑘 = 𝑝 → ran (1st ‘(𝑔‘𝑘)) = ran (1st ‘(𝑔‘𝑝))) |
357 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑘 = 𝑝 → (0..^𝑘) = (0..^𝑝)) |
358 | 356, 357 | sseq12d 3934 |
. . . . . 6
⊢ (𝑘 = 𝑝 → (ran (1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔‘𝑝)) ⊆ (0..^𝑝))) |
359 | 358 | rspccva 3536 |
. . . . 5
⊢
((∀𝑘 ∈
ℕ ran (1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ 𝑝 ∈ ℕ) → ran (1st
‘(𝑔‘𝑝)) ⊆ (0..^𝑝)) |
360 | 354, 359 | sylan 583 |
. . . 4
⊢ ((((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ 𝑝 ∈ ℕ) → ran
(1st ‘(𝑔‘𝑝)) ⊆ (0..^𝑝)) |
361 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝜑) |
362 | | poimir.2 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0) |
363 | 361, 362 | sylan 583 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0) |
364 | | eqid 2737 |
. . . . 5
⊢
((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) = ((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) |
365 | | simpr 488 |
. . . . . . . 8
⊢ ((ran
(1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) →
∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
366 | 365 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑘 ∈
ℕ (ran (1st ‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) →
∀𝑘 ∈ ℕ
∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
367 | 366 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) →
∀𝑘 ∈ ℕ
∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
368 | | 2fveq3 6722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑝 → (2nd ‘(𝑔‘𝑘)) = (2nd ‘(𝑔‘𝑝))) |
369 | 368 | imaeq1d 5928 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑝 → ((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) = ((2nd ‘(𝑔‘𝑝)) “ (1...𝑗))) |
370 | 369 | xpeq1d 5580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑝 → (((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) = (((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) ×
{1})) |
371 | 368 | imaeq1d 5928 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑝 → ((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁))) |
372 | 371 | xpeq1d 5580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑝 → (((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) |
373 | 370, 372 | uneq12d 4078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑝 → ((((2nd ‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
374 | 355, 373 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑝 → ((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
375 | | sneq 4551 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑝 → {𝑘} = {𝑝}) |
376 | 375 | xpeq2d 5581 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑝 → ((1...𝑁) × {𝑘}) = ((1...𝑁) × {𝑝})) |
377 | 374, 376 | oveq12d 7231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑝 → (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})) = (((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝}))) |
378 | 377 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑝 → (𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))) |
379 | 378 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑝 → ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏)) |
380 | 379 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑝 → (0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏))) |
381 | 374 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑝 → (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏)) |
382 | 381 | neeq1d 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑝 → ((((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)) |
383 | 380, 382 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑝 → ((0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
384 | 383 | ralbidv 3118 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑝 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
385 | 384 | rabbidv 3390 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑝 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) |
386 | 385 | uneq2d 4077 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑝 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})) |
387 | 386 | supeq1d 9062 |
. . . . . . . . 9
⊢ (𝑘 = 𝑝 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
388 | 387 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑘 = 𝑝 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
389 | 388 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑘 = 𝑝 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔
∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
390 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑖 = 𝑞 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
391 | 390 | rexbidv 3216 |
. . . . . . . 8
⊢ (𝑖 = 𝑞 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔
∃𝑗 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
392 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚)) |
393 | 392 | imaeq2d 5929 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑚 → ((2nd ‘(𝑔‘𝑝)) “ (1...𝑗)) = ((2nd ‘(𝑔‘𝑝)) “ (1...𝑚))) |
394 | 393 | xpeq1d 5580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑚 → (((2nd ‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) = (((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) ×
{1})) |
395 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑚 → (𝑗 + 1) = (𝑚 + 1)) |
396 | 395 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑚 → ((𝑗 + 1)...𝑁) = ((𝑚 + 1)...𝑁)) |
397 | 396 | imaeq2d 5929 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑚 → ((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁))) |
398 | 397 | xpeq1d 5580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑚 → (((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})) |
399 | 394, 398 | uneq12d 4078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑚 → ((((2nd ‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) |
400 | 399 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑚 → ((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))) |
401 | 400 | fvoveq1d 7235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑚 → (𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝}))) = (𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))) |
402 | 401 | fveq1d 6719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏)) |
403 | 402 | breq2d 5065 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑚 → (0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏))) |
404 | 400 | fveq1d 6719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏)) |
405 | 404 | neeq1d 3000 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑚 → ((((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st
‘(𝑔‘𝑝)) ∘f +
((((2nd ‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd
‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)) |
406 | 403, 405 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑚 → ((0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
407 | 406 | ralbidv 3118 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑚 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))) |
408 | 407 | rabbidv 3390 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑚 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) |
409 | 408 | uneq2d 4077 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})) |
410 | 409 | supeq1d 9062 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪
{𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
411 | 410 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → (𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
412 | 411 | cbvrexvw 3359 |
. . . . . . . 8
⊢
(∃𝑗 ∈
(0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔
∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
413 | 391, 412 | bitrdi 290 |
. . . . . . 7
⊢ (𝑖 = 𝑞 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔
∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
414 | 389, 413 | rspc2v 3547 |
. . . . . 6
⊢ ((𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁)) → (∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) →
∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
))) |
415 | 367, 414 | mpan9 510 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁))) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, <
)) |
416 | 346, 137,
347, 349, 363, 364, 351, 360, 415 | poimirlem31 35545 |
. . . 4
⊢ ((((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ◡ ≤ })) → ∃𝑚 ∈ (0...𝑁)0𝑟((𝐹‘(((1st ‘(𝑔‘𝑝)) ∘f + ((((2nd
‘(𝑔‘𝑝)) “ (1...𝑚)) × {1}) ∪
(((2nd ‘(𝑔‘𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑝})))‘𝑛)) |
417 | 346, 137,
347, 349, 350, 351, 360, 416 | poimirlem30 35544 |
. . 3
⊢ (((𝜑 ∧ 𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) →
∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
418 | 417 | anasss 470 |
. 2
⊢ ((𝜑 ∧ (𝑔:ℕ⟶((ℕ0
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st
‘(𝑔‘𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f /
((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔‘𝑘)) ∘f + ((((2nd
‘(𝑔‘𝑘)) “ (1...𝑗)) × {1}) ∪
(((2nd ‘(𝑔‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))) →
∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |
419 | 345, 418 | exlimddv 1943 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐼 ∀𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅 ↾t 𝐼)(𝑐 ∈ 𝑣 → ∀𝑟 ∈ { ≤ , ◡ ≤ }∃𝑧 ∈ 𝑣 0𝑟((𝐹‘𝑧)‘𝑛))) |