Step | Hyp | Ref
| Expression |
1 | | eldiophelnn0 36345 |
. 2
⊢ (𝑆 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
2 | | eldioph4b.a |
. . . . . 6
⊢ 𝑊 ∈ V |
3 | | ovex 6577 |
. . . . . 6
⊢
(1...𝑁) ∈
V |
4 | 2, 3 | unex 6854 |
. . . . 5
⊢ (𝑊 ∪ (1...𝑁)) ∈ V |
5 | 4 | jctr 563 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈
ℕ0 ∧ (𝑊 ∪ (1...𝑁)) ∈ V)) |
6 | | eldioph4b.b |
. . . . . . 7
⊢ ¬
𝑊 ∈
Fin |
7 | 6 | intnanr 952 |
. . . . . 6
⊢ ¬
(𝑊 ∈ Fin ∧
(1...𝑁) ∈
Fin) |
8 | | unfir 8113 |
. . . . . 6
⊢ ((𝑊 ∪ (1...𝑁)) ∈ Fin → (𝑊 ∈ Fin ∧ (1...𝑁) ∈ Fin)) |
9 | 7, 8 | mto 187 |
. . . . 5
⊢ ¬
(𝑊 ∪ (1...𝑁)) ∈ Fin |
10 | | ssun2 3739 |
. . . . 5
⊢
(1...𝑁) ⊆
(𝑊 ∪ (1...𝑁)) |
11 | 9, 10 | pm3.2i 470 |
. . . 4
⊢ (¬
(𝑊 ∪ (1...𝑁)) ∈ Fin ∧ (1...𝑁) ⊆ (𝑊 ∪ (1...𝑁))) |
12 | | eldioph2b 36344 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ (𝑊 ∪ (1...𝑁)) ∈ V) ∧ (¬ (𝑊 ∪ (1...𝑁)) ∈ Fin ∧ (1...𝑁) ⊆ (𝑊 ∪ (1...𝑁)))) → (𝑆 ∈ (Dioph‘𝑁) ↔ ∃𝑝 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
13 | 5, 11, 12 | sylancl 693 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑆 ∈
(Dioph‘𝑁) ↔
∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
14 | | elmapssres 7768 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (1...𝑁) ⊆ (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
15 | 10, 14 | mpan2 703 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
17 | | ssun1 3738 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 ⊆ (𝑊 ∪ (1...𝑁)) |
18 | | elmapssres 7768 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ 𝑊 ⊆ (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊)) |
19 | 17, 18 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊)) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊)) |
21 | | uncom 3719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)) = ((𝑢 ↾ 𝑊) ∪ (𝑢 ↾ (1...𝑁))) |
22 | | resundi 5330 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ↾ (𝑊 ∪ (1...𝑁))) = ((𝑢 ↾ 𝑊) ∪ (𝑢 ↾ (1...𝑁))) |
23 | 21, 22 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)) = (𝑢 ↾ (𝑊 ∪ (1...𝑁))) |
24 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → 𝑢:(𝑊 ∪ (1...𝑁))⟶ℕ0) |
25 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢:(𝑊 ∪ (1...𝑁))⟶ℕ0 → 𝑢 Fn (𝑊 ∪ (1...𝑁))) |
26 | | fnresdm 5914 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 Fn (𝑊 ∪ (1...𝑁)) → (𝑢 ↾ (𝑊 ∪ (1...𝑁))) = 𝑢) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑢 ↾ (𝑊 ∪ (1...𝑁))) = 𝑢) |
28 | 23, 27 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)) = 𝑢) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = (𝑝‘𝑢)) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → ((𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0 ↔ (𝑝‘𝑢) = 0)) |
31 | 30 | biimpar 501 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0) |
32 | | uneq2 3723 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑢 ↾ 𝑊) → ((𝑢 ↾ (1...𝑁)) ∪ 𝑤) = ((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) |
33 | 32 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑢 ↾ 𝑊) → (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊)))) |
34 | 33 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑢 ↾ 𝑊) → ((𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0 ↔ (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0)) |
35 | 34 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (((𝑢 ↾ 𝑊) ∈ (ℕ0
↑𝑚 𝑊) ∧ (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ (𝑢 ↾ 𝑊))) = 0) → ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0) |
36 | 20, 31, 35 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0) |
37 | 16, 36 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0)) |
38 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ↔ (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)))) |
39 | | uneq1 3722 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∪ 𝑤) = ((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑝‘(𝑡 ∪ 𝑤)) = (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤))) |
41 | 40 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → ((𝑝‘(𝑡 ∪ 𝑤)) = 0 ↔ (𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0)) |
42 | 41 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0 ↔ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0)) |
43 | 38, 42 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0) ↔ ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘((𝑢 ↾ (1...𝑁)) ∪ 𝑤)) = 0))) |
44 | 37, 43 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑝‘𝑢) = 0) → (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
45 | 44 | expimpd 627 |
. . . . . . . . . 10
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → (((𝑝‘𝑢) = 0 ∧ 𝑡 = (𝑢 ↾ (1...𝑁))) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
46 | 45 | ancomsd 469 |
. . . . . . . . 9
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
47 | 46 | rexlimiv 3009 |
. . . . . . . 8
⊢
(∃𝑢 ∈
(ℕ0 ↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)) |
48 | | uncom 3719 |
. . . . . . . . . . . 12
⊢ (𝑡 ∪ 𝑤) = (𝑤 ∪ 𝑡) |
49 | | fz1ssnn 12243 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ⊆
ℕ |
50 | | sslin 3801 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...𝑁) ⊆
ℕ → (𝑊 ∩
(1...𝑁)) ⊆ (𝑊 ∩
ℕ)) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∩ (1...𝑁)) ⊆ (𝑊 ∩ ℕ) |
52 | | eldioph4b.c |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∩ ℕ) =
∅ |
53 | 51, 52 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∩ (1...𝑁)) ⊆ ∅ |
54 | | ss0 3926 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∩ (1...𝑁)) ⊆ ∅ → (𝑊 ∩ (1...𝑁)) = ∅) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∩ (1...𝑁)) = ∅ |
56 | 55 | reseq2i 5314 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑤 ↾ ∅) |
57 | | res0 5321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ↾ ∅) =
∅ |
58 | 56, 57 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = ∅ |
59 | 55 | reseq2i 5314 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ ∅) |
60 | | res0 5321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ↾ ∅) =
∅ |
61 | 59, 60 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ↾ (𝑊 ∩ (1...𝑁))) = ∅ |
62 | 58, 61 | eqtr4i 2635 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ (𝑊 ∩ (1...𝑁))) |
63 | | elmapresaun 36352 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ (𝑊 ∩ (1...𝑁)))) → (𝑤 ∪ 𝑡) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
64 | 62, 63 | mp3an3 1405 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → (𝑤 ∪ 𝑡) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
65 | 64 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → (𝑤 ∪ 𝑡) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
66 | 48, 65 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → (𝑡 ∪ 𝑤) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
67 | 66 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → (𝑡 ∪ 𝑤) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))) |
68 | 48 | reseq1i 5313 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∪ 𝑤) ↾ (1...𝑁)) = ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) |
69 | | elmapresaunres2 36353 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ (𝑤 ↾ (𝑊 ∩ (1...𝑁))) = (𝑡 ↾ (𝑊 ∩ (1...𝑁)))) → ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) = 𝑡) |
70 | 62, 69 | mp3an3 1405 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ (ℕ0
↑𝑚 𝑊) ∧ 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) = 𝑡) |
71 | 70 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → ((𝑤 ∪ 𝑡) ↾ (1...𝑁)) = 𝑡) |
72 | 68, 71 | syl5req 2657 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) → 𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁))) |
73 | 72 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → 𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁))) |
74 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → (𝑝‘(𝑡 ∪ 𝑤)) = 0) |
75 | | reseq1 5311 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑡 ∪ 𝑤) → (𝑢 ↾ (1...𝑁)) = ((𝑡 ∪ 𝑤) ↾ (1...𝑁))) |
76 | 75 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝑡 ∪ 𝑤) → (𝑡 = (𝑢 ↾ (1...𝑁)) ↔ 𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁)))) |
77 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑡 ∪ 𝑤) → (𝑝‘𝑢) = (𝑝‘(𝑡 ∪ 𝑤))) |
78 | 77 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝑡 ∪ 𝑤) → ((𝑝‘𝑢) = 0 ↔ (𝑝‘(𝑡 ∪ 𝑤)) = 0)) |
79 | 76, 78 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝑡 ∪ 𝑤) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0))) |
80 | 79 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝑡 ∪ 𝑤) ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁))) ∧ (𝑡 = ((𝑡 ∪ 𝑤) ↾ (1...𝑁)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0)) → ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)) |
81 | 67, 73, 74, 80 | syl12anc 1316 |
. . . . . . . . 9
⊢ (((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑤 ∈ (ℕ0
↑𝑚 𝑊)) ∧ (𝑝‘(𝑡 ∪ 𝑤)) = 0) → ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)) |
82 | 81 | r19.29an 3059 |
. . . . . . . 8
⊢ ((𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0) → ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)) |
83 | 47, 82 | impbii 198 |
. . . . . . 7
⊢
(∃𝑢 ∈
(ℕ0 ↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)) |
84 | 83 | abbii 2726 |
. . . . . 6
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} = {𝑡 ∣ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)} |
85 | | df-rab 2905 |
. . . . . 6
⊢ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0} = {𝑡 ∣ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0)} |
86 | 84, 85 | eqtr4i 2635 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0} |
87 | 86 | eqeq2i 2622 |
. . . 4
⊢ (𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ↔ 𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0}) |
88 | 87 | rexbii 3023 |
. . 3
⊢
(∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (𝑊 ∪ (1...𝑁)))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ↔ ∃𝑝 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0}) |
89 | 13, 88 | syl6bb 275 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑆 ∈
(Dioph‘𝑁) ↔
∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0})) |
90 | 1, 89 | biadan2 672 |
1
⊢ (𝑆 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧
∃𝑝 ∈
(mzPoly‘(𝑊 ∪
(1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0
↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0})) |