Step | Hyp | Ref
| Expression |
1 | | eldiophelnn0 38170 |
. 2
⊢ (𝑆 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
2 | | eldioph4b.a |
. . . . . 6
⊢ 𝑊 ∈ V |
3 | | ovex 6936 |
. . . . . 6
⊢
(1...𝑁) ∈
V |
4 | 2, 3 | unex 7215 |
. . . . 5
⊢ (𝑊 ∪ (1...𝑁)) ∈ V |
5 | 4 | jctr 522 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈
ℕ0 ∧ (𝑊 ∪ (1...𝑁)) ∈ V)) |
6 | | eldioph4b.b |
. . . . . . 7
⊢ ¬
𝑊 ∈
Fin |
7 | 6 | intnanr 483 |
. . . . . 6
⊢ ¬
(𝑊 ∈ Fin ∧
(1...𝑁) ∈
Fin) |
8 | | unfir 8496 |
. . . . . 6
⊢ ((𝑊 ∪ (1...𝑁)) ∈ Fin → (𝑊 ∈ Fin ∧ (1...𝑁) ∈ Fin)) |
9 | 7, 8 | mto 189 |
. . . . 5
⊢ ¬
(𝑊 ∪ (1...𝑁)) ∈ Fin |
10 | | ssun2 4003 |
. . . . 5
⊢
(1...𝑁) ⊆
(𝑊 ∪ (1...𝑁)) |
11 | 9, 10 | pm3.2i 464 |
. . . 4
⊢ (¬
(𝑊 ∪ (1...𝑁)) ∈ Fin ∧ (1...𝑁) ⊆ (𝑊 ∪ (1...𝑁))) |
12 | | eldioph2b 38169 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ (𝑊 ∪ (1...𝑁)) ∈ V) ∧ (¬ (𝑊 ∪ (1...𝑁)) ∈ Fin ∧ (1...𝑁) ⊆ (𝑊 ∪ (1...𝑁)))) → (𝑆 ∈ (Dioph‘𝑁) ↔ ∃𝑝 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
13 | 5, 11, 12 | sylancl 582 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑆 ∈
(Dioph‘𝑁) ↔
∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
14 | | elmapssres 8146 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (1...𝑁) ⊆ (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
15 | 10, 14 | mpan2 684 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
16 | 15 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
17 | | ssun1 4002 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 ⊆ (𝑊 ∪ (1...𝑁)) |
18 | | elmapssres 8146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ 𝑊 ⊆ (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊)) |
19 | 17, 18 | mpan2 684 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊)) |
20 | 19 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊)) |
21 | | uncom 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)) = ((𝑢 ↾ 𝑊) ∪ (𝑢 ↾ (1...𝑁))) |
22 | | resundi 5646 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ↾ (𝑊 ∪ (1...𝑁))) = ((𝑢 ↾ 𝑊) ∪ (𝑢 ↾ (1...𝑁))) |
23 | 21, 22 | eqtr4i 2851 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)) = (𝑢 ↾ (𝑊 ∪ (1...𝑁))) |
24 | | elmapi 8143 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → 𝑢:(𝑊 ∪ (1...𝑁))⟶ℕ0) |
25 | | ffn 6277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢:(𝑊 ∪ (1...𝑁))⟶ℕ0 → 𝑢 Fn (𝑊 ∪ (1...𝑁))) |
26 | | fnresdm 6232 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 Fn (𝑊 ∪ (1...𝑁)) → (𝑢 ↾ (𝑊 ∪ (1...𝑁))) = 𝑢) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ (𝑊 ∪ (1...𝑁))) = 𝑢) |
28 | 23, 27 | syl5eq 2872 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)) = 𝑢) |
29 | 28 | fveqeq2d 6440 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → ((𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0 ↔ (𝑝‘𝑢) = 0)) |
30 | 29 | biimpar 471 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0) |
31 | | uneq2 3987 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑢 ↾ 𝑊) → ((𝑢 ↾ (1...𝑁)) ∪ 𝑤) = ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) |
32 | 31 | fveqeq2d 6440 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑢 ↾ 𝑊) → ((𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0 ↔ (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0)) |
33 | 32 | rspcev 3525 |
. . . . . . . . . . . . . 14
⊢ (((𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊) ∧ (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0) → ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0) |
34 | 20, 30, 33 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0) |
35 | 16, 34 | jca 509 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0)) |
36 | | eleq1 2893 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ↔ (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)))) |
37 | | uneq1 3986 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∪ 𝑤) = ((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) |
38 | 37 | fveqeq2d 6440 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → ((𝑝‘(𝑡 ∪ 𝑤)) = 0 ↔ (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0)) |
39 | 38 | rexbidv 3261 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0 ↔ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0)) |
40 | 36, 39 | anbi12d 626 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0) ↔ ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0))) |
41 | 35, 40 | syl5ibrcom 239 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
42 | 41 | expimpd 447 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (((𝑝‘𝑢) = 0 ∧ 𝑡 = (𝑢 ↾ (1...𝑁))) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
43 | 42 | ancomsd 459 |
. . . . . . . . 9
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
44 | 43 | rexlimiv 3235 |
. . . . . . . 8
⊢
(∃𝑢 ∈
(ℕ0 ↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)) |
45 | | uncom 3983 |
. . . . . . . . . . . 12
⊢ (𝑡 ∪ 𝑤) = (𝑤 ∪ 𝑡) |
46 | | fz1ssnn 12664 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ⊆
ℕ |
47 | | sslin 4062 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...𝑁) ⊆
ℕ → (𝑊 ∩
(1...𝑁)) ⊆ (𝑊 ∩
ℕ)) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∩ (1...𝑁)) ⊆ (𝑊 ∩ ℕ) |
49 | | eldioph4b.c |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∩ ℕ) =
∅ |
50 | 48, 49 | sseqtri 3861 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∩ (1...𝑁)) ⊆ ∅ |
51 | | ss0 4198 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∩ (1...𝑁)) ⊆ ∅ → (𝑊 ∩ (1...𝑁)) = ∅) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∩ (1...𝑁)) = ∅ |
53 | 52 | reseq2i 5625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑤 ↾ ∅) |
54 | | res0 5632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ↾ ∅) =
∅ |
55 | 53, 54 | eqtri 2848 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = ∅ |
56 | 52 | reseq2i 5625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ ∅) |
57 | | res0 5632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ↾ ∅) =
∅ |
58 | 56, 57 | eqtri 2848 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ↾ (𝑊 ∩ (1...𝑁))) = ∅ |
59 | 55, 58 | eqtr4i 2851 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ (𝑊 ∩ (1...𝑁))) |
60 | | elmapresaun 38177 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ (𝑊 ∩ (1...𝑁)))) → (𝑤 ∪ 𝑡) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
61 | 59, 60 | mp3an3 1580 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → (𝑤 ∪ 𝑡) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
62 | 61 | ancoms 452 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → (𝑤 ∪ 𝑡) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
63 | 45, 62 | syl5eqel 2909 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → (𝑡 ∪ 𝑤) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
64 | 63 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → (𝑡 ∪ 𝑤) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
65 | 45 | reseq1i 5624 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∪ 𝑤) ↾ (1...𝑁)) = ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) |
66 | | elmapresaunres2 38178 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ (𝑊 ∩ (1...𝑁)))) → ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) = 𝑡) |
67 | 59, 66 | mp3an3 1580 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) = 𝑡) |
68 | 67 | ancoms 452 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) = 𝑡) |
69 | 65, 68 | syl5req 2873 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → 𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁))) |
70 | 69 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → 𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁))) |
71 | | simpr 479 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → (𝑝‘(𝑡 ∪ 𝑤)) = 0) |
72 | | reseq1 5622 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑡 ∪ 𝑤) → (𝑢 ↾ (1...𝑁)) = ((𝑡 ∪ 𝑤) ↾ (1...𝑁))) |
73 | 72 | eqeq2d 2834 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝑡 ∪ 𝑤) → (𝑡 = (𝑢 ↾ (1...𝑁)) ↔ 𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁)))) |
74 | | fveqeq2 6441 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝑡 ∪ 𝑤) → ((𝑝‘𝑢) = 0 ↔ (𝑝‘(𝑡 ∪ 𝑤)) = 0)) |
75 | 73, 74 | anbi12d 626 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝑡 ∪ 𝑤) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
76 | 75 | rspcev 3525 |
. . . . . . . . . 10
⊢ (((𝑡 ∪ 𝑤) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0)) → ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)) |
77 | 64, 70, 71, 76 | syl12anc 872 |
. . . . . . . . 9
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)) |
78 | 77 | r19.29an 3286 |
. . . . . . . 8
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0) → ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)) |
79 | 44, 78 | impbii 201 |
. . . . . . 7
⊢
(∃𝑢 ∈
(ℕ0 ↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)) |
80 | 79 | abbii 2943 |
. . . . . 6
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} = {𝑡 ∣ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)} |
81 | | df-rab 3125 |
. . . . . 6
⊢ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0} = {𝑡 ∣ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)} |
82 | 80, 81 | eqtr4i 2851 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0} |
83 | 82 | eqeq2i 2836 |
. . . 4
⊢ (𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ↔ 𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0}) |
84 | 83 | rexbii 3250 |
. . 3
⊢
(∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ↔ ∃𝑝 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0}) |
85 | 13, 84 | syl6bb 279 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑆 ∈
(Dioph‘𝑁) ↔
∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0})) |
86 | 1, 85 | biadanii 859 |
1
⊢ (𝑆 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧
∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0})) |