Step | Hyp | Ref
| Expression |
1 | | simpr 489 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (𝑎‘1) ∈
(ℤ≥‘2)) |
2 | | elmapi 8431 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → 𝑎:(1...3)⟶ℕ0) |
3 | | df-3 11723 |
. . . . . . . . . 10
⊢ 3 = (2 +
1) |
4 | | ssid 3910 |
. . . . . . . . . 10
⊢ (1...3)
⊆ (1...3) |
5 | 3, 4 | jm2.27dlem5 40312 |
. . . . . . . . 9
⊢ (1...2)
⊆ (1...3) |
6 | | 2nn 11732 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
7 | 6 | jm2.27dlem3 40310 |
. . . . . . . . 9
⊢ 2 ∈
(1...2) |
8 | 5, 7 | sselii 3885 |
. . . . . . . 8
⊢ 2 ∈
(1...3) |
9 | | ffvelrn 6833 |
. . . . . . . 8
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2
∈ (1...3)) → (𝑎‘2) ∈
ℕ0) |
10 | 2, 8, 9 | sylancl 590 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘2) ∈
ℕ0) |
11 | 10 | adantr 485 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (𝑎‘2) ∈
ℕ0) |
12 | | 3nn 11738 |
. . . . . . . . 9
⊢ 3 ∈
ℕ |
13 | 12 | jm2.27dlem3 40310 |
. . . . . . . 8
⊢ 3 ∈
(1...3) |
14 | | ffvelrn 6833 |
. . . . . . . 8
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 3
∈ (1...3)) → (𝑎‘3) ∈
ℕ0) |
15 | 2, 13, 14 | sylancl 590 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘3) ∈
ℕ0) |
16 | 15 | adantr 485 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (𝑎‘3) ∈
ℕ0) |
17 | | rmxdiophlem 40314 |
. . . . . 6
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ0 ∧
(𝑎‘3) ∈
ℕ0) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
18 | 1, 11, 16, 17 | syl3anc 1369 |
. . . . 5
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
19 | 18 | pm5.32da 583 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1)))) |
20 | | anass 473 |
. . . . . 6
⊢ ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)
↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
21 | 20 | rexbii 3173 |
. . . . 5
⊢
(∃𝑏 ∈
ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)
↔ ∃𝑏 ∈
ℕ0 ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
22 | | r19.42v 3266 |
. . . . 5
⊢
(∃𝑏 ∈
ℕ0 ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1))
↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
23 | 21, 22 | bitr2i 279 |
. . . 4
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1))
↔ ∃𝑏 ∈
ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1)) |
24 | 19, 23 | syl6bb 291 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
25 | 24 | rabbiia 3382 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1)} |
26 | | 3nn0 11937 |
. . 3
⊢ 3 ∈
ℕ0 |
27 | | vex 3411 |
. . . . . . 7
⊢ 𝑐 ∈ V |
28 | 27 | resex 5864 |
. . . . . 6
⊢ (𝑐 ↾ (1...3)) ∈
V |
29 | | fvex 6664 |
. . . . . 6
⊢ (𝑐‘4) ∈
V |
30 | | df-2 11722 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
31 | 30, 5 | jm2.27dlem5 40312 |
. . . . . . . . . . . 12
⊢ (1...1)
⊆ (1...3) |
32 | | 1nn 11670 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
33 | 32 | jm2.27dlem3 40310 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...1) |
34 | 31, 33 | sselii 3885 |
. . . . . . . . . . 11
⊢ 1 ∈
(1...3) |
35 | 34 | jm2.27dlem1 40308 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘1) = (𝑐‘1)) |
36 | 35 | eleq1d 2835 |
. . . . . . . . 9
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑐‘1) ∈
(ℤ≥‘2))) |
37 | 36 | adantr 485 |
. . . . . . . 8
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑐‘1) ∈
(ℤ≥‘2))) |
38 | | simpr 489 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → 𝑏 = (𝑐‘4)) |
39 | 8 | jm2.27dlem1 40308 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘2) = (𝑐‘2)) |
40 | 35, 39 | oveq12d 7161 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑐‘1) Yrm (𝑐‘2))) |
41 | 40 | adantr 485 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑐‘1) Yrm (𝑐‘2))) |
42 | 38, 41 | eqeq12d 2775 |
. . . . . . . 8
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))) |
43 | 37, 42 | anbi12d 634 |
. . . . . . 7
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))))) |
44 | 13 | jm2.27dlem1 40308 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘3) = (𝑐‘3)) |
45 | 44 | oveq1d 7158 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2)) |
46 | 45 | adantr 485 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2)) |
47 | 35 | oveq1d 7158 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑐‘1)↑2)) |
48 | 47 | oveq1d 7158 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) =
(((𝑐‘1)↑2)
− 1)) |
49 | | oveq1 7150 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑐‘4) → (𝑏↑2) = ((𝑐‘4)↑2)) |
50 | 48, 49 | oveqan12d 7162 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1)↑2) − 1) · (𝑏↑2)) = ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) |
51 | 46, 50 | oveq12d 7161 |
. . . . . . . 8
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
(((𝑐‘3)↑2)
− ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) |
52 | 51 | eqeq1d 2761 |
. . . . . . 7
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1
↔ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)) |
53 | 43, 52 | anbi12d 634 |
. . . . . 6
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)
↔ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1))) |
54 | 28, 29, 53 | sbc2ie 3769 |
. . . . 5
⊢
([(𝑐 ↾
(1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)
↔ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)) |
55 | 54 | rabbii 3383 |
. . . 4
⊢ {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
= {𝑐 ∈
(ℕ0 ↑m (1...4)) ∣ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)} |
56 | | 4nn0 11938 |
. . . . . 6
⊢ 4 ∈
ℕ0 |
57 | | rmydioph 40313 |
. . . . . 6
⊢ {𝑏 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈
(Dioph‘3) |
58 | | simp1 1134 |
. . . . . . . . 9
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘1) = (𝑐‘1)) |
59 | 58 | eleq1d 2835 |
. . . . . . . 8
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) ∈
(ℤ≥‘2) ↔ (𝑐‘1) ∈
(ℤ≥‘2))) |
60 | | simp3 1136 |
. . . . . . . . 9
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘3) = (𝑐‘4)) |
61 | | simp2 1135 |
. . . . . . . . . 10
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘2) = (𝑐‘2)) |
62 | 58, 61 | oveq12d 7161 |
. . . . . . . . 9
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) Yrm (𝑏‘2)) = ((𝑐‘1) Yrm (𝑐‘2))) |
63 | 60, 62 | eqeq12d 2775 |
. . . . . . . 8
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))) |
64 | 59, 63 | anbi12d 634 |
. . . . . . 7
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2))) ↔ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))))) |
65 | | df-4 11724 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
66 | | ssid 3910 |
. . . . . . . . . . 11
⊢ (1...4)
⊆ (1...4) |
67 | 65, 66 | jm2.27dlem5 40312 |
. . . . . . . . . 10
⊢ (1...3)
⊆ (1...4) |
68 | 3, 67 | jm2.27dlem5 40312 |
. . . . . . . . 9
⊢ (1...2)
⊆ (1...4) |
69 | 30, 68 | jm2.27dlem5 40312 |
. . . . . . . 8
⊢ (1...1)
⊆ (1...4) |
70 | 69, 33 | sselii 3885 |
. . . . . . 7
⊢ 1 ∈
(1...4) |
71 | 68, 7 | sselii 3885 |
. . . . . . 7
⊢ 2 ∈
(1...4) |
72 | | 4nn 11742 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
73 | 72 | jm2.27dlem3 40310 |
. . . . . . 7
⊢ 4 ∈
(1...4) |
74 | 64, 70, 71, 73 | rabren3dioph 40114 |
. . . . . 6
⊢ ((4
∈ ℕ0 ∧ {𝑏 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈ (Dioph‘3)) →
{𝑐 ∈
(ℕ0 ↑m (1...4)) ∣ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈
(Dioph‘4)) |
75 | 56, 57, 74 | mp2an 692 |
. . . . 5
⊢ {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈
(Dioph‘4) |
76 | | ovex 7176 |
. . . . . . . . 9
⊢ (1...4)
∈ V |
77 | 67, 13 | sselii 3885 |
. . . . . . . . 9
⊢ 3 ∈
(1...4) |
78 | | mzpproj 40036 |
. . . . . . . . 9
⊢ (((1...4)
∈ V ∧ 3 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ (𝑐‘3)) ∈
(mzPoly‘(1...4))) |
79 | 76, 77, 78 | mp2an 692 |
. . . . . . . 8
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ (𝑐‘3)) ∈
(mzPoly‘(1...4)) |
80 | | 2nn0 11936 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
81 | | mzpexpmpt 40044 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑m (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4))
∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ ((𝑐‘3)↑2)) ∈
(mzPoly‘(1...4))) |
82 | 79, 80, 81 | mp2an 692 |
. . . . . . 7
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ ((𝑐‘3)↑2)) ∈
(mzPoly‘(1...4)) |
83 | | mzpproj 40036 |
. . . . . . . . . . 11
⊢ (((1...4)
∈ V ∧ 1 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ (𝑐‘1)) ∈
(mzPoly‘(1...4))) |
84 | 76, 70, 83 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ (𝑐‘1)) ∈
(mzPoly‘(1...4)) |
85 | | mzpexpmpt 40044 |
. . . . . . . . . 10
⊢ (((𝑐 ∈ (ℤ
↑m (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4))
∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ ((𝑐‘1)↑2)) ∈
(mzPoly‘(1...4))) |
86 | 84, 80, 85 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ ((𝑐‘1)↑2)) ∈
(mzPoly‘(1...4)) |
87 | | 1z 12036 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
88 | | mzpconstmpt 40039 |
. . . . . . . . . 10
⊢ (((1...4)
∈ V ∧ 1 ∈ ℤ) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ 1) ∈ (mzPoly‘(1...4))) |
89 | 76, 87, 88 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ 1) ∈
(mzPoly‘(1...4)) |
90 | | mzpsubmpt 40042 |
. . . . . . . . 9
⊢ (((𝑐 ∈ (ℤ
↑m (1...4)) ↦ ((𝑐‘1)↑2)) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑m (1...4))
↦ 1) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ (((𝑐‘1)↑2) − 1)) ∈
(mzPoly‘(1...4))) |
91 | 86, 89, 90 | mp2an 692 |
. . . . . . . 8
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈
(mzPoly‘(1...4)) |
92 | | mzpproj 40036 |
. . . . . . . . . 10
⊢ (((1...4)
∈ V ∧ 4 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ (𝑐‘4)) ∈
(mzPoly‘(1...4))) |
93 | 76, 73, 92 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ (𝑐‘4)) ∈
(mzPoly‘(1...4)) |
94 | | mzpexpmpt 40044 |
. . . . . . . . 9
⊢ (((𝑐 ∈ (ℤ
↑m (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4))
∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ ((𝑐‘4)↑2)) ∈
(mzPoly‘(1...4))) |
95 | 93, 80, 94 | mp2an 692 |
. . . . . . . 8
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ ((𝑐‘4)↑2)) ∈
(mzPoly‘(1...4)) |
96 | | mzpmulmpt 40041 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑m (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑m (1...4))
↦ ((𝑐‘4)↑2)) ∈
(mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈
(mzPoly‘(1...4))) |
97 | 91, 95, 96 | mp2an 692 |
. . . . . . 7
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈
(mzPoly‘(1...4)) |
98 | | mzpsubmpt 40042 |
. . . . . . 7
⊢ (((𝑐 ∈ (ℤ
↑m (1...4)) ↦ ((𝑐‘3)↑2)) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑m (1...4))
↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈
(mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑m (1...4))
↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2)))) ∈
(mzPoly‘(1...4))) |
99 | 82, 97, 98 | mp2an 692 |
. . . . . 6
⊢ (𝑐 ∈ (ℤ
↑m (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2)))) ∈
(mzPoly‘(1...4)) |
100 | | eqrabdioph 40076 |
. . . . . 6
⊢ ((4
∈ ℕ0 ∧ (𝑐 ∈ (ℤ ↑m (1...4))
↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2)))) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑m (1...4))
↦ 1) ∈ (mzPoly‘(1...4))) → {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1} ∈
(Dioph‘4)) |
101 | 56, 99, 89, 100 | mp3an 1459 |
. . . . 5
⊢ {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1} ∈
(Dioph‘4) |
102 | | anrabdioph 40079 |
. . . . 5
⊢ (({𝑐 ∈ (ℕ0
↑m (1...4)) ∣ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈ (Dioph‘4) ∧
{𝑐 ∈
(ℕ0 ↑m (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1} ∈
(Dioph‘4)) → {𝑐
∈ (ℕ0 ↑m (1...4)) ∣ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)} ∈
(Dioph‘4)) |
103 | 75, 101, 102 | mp2an 692 |
. . . 4
⊢ {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)} ∈
(Dioph‘4) |
104 | 55, 103 | eqeltri 2847 |
. . 3
⊢ {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘4) |
105 | 65 | rexfrabdioph 40094 |
. . 3
⊢ ((3
∈ ℕ0 ∧ {𝑐 ∈ (ℕ0
↑m (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘4)) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘3)) |
106 | 26, 104, 105 | mp2an 692 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘3) |
107 | 25, 106 | eqeltri 2847 |
1
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈
(Dioph‘3) |