Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (𝑎‘1) ∈
(ℤ≥‘2)) |
2 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0) |
3 | | df-3 11080 |
. . . . . . . . . 10
⊢ 3 = (2 +
1) |
4 | | ssid 3624 |
. . . . . . . . . 10
⊢ (1...3)
⊆ (1...3) |
5 | 3, 4 | jm2.27dlem5 37580 |
. . . . . . . . 9
⊢ (1...2)
⊆ (1...3) |
6 | | 2nn 11185 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
7 | 6 | jm2.27dlem3 37578 |
. . . . . . . . 9
⊢ 2 ∈
(1...2) |
8 | 5, 7 | sselii 3600 |
. . . . . . . 8
⊢ 2 ∈
(1...3) |
9 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2
∈ (1...3)) → (𝑎‘2) ∈
ℕ0) |
10 | 2, 8, 9 | sylancl 694 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → (𝑎‘2) ∈
ℕ0) |
11 | 10 | adantr 481 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (𝑎‘2) ∈
ℕ0) |
12 | | 3nn 11186 |
. . . . . . . . 9
⊢ 3 ∈
ℕ |
13 | 12 | jm2.27dlem3 37578 |
. . . . . . . 8
⊢ 3 ∈
(1...3) |
14 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 3
∈ (1...3)) → (𝑎‘3) ∈
ℕ0) |
15 | 2, 13, 14 | sylancl 694 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → (𝑎‘3) ∈
ℕ0) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (𝑎‘3) ∈
ℕ0) |
17 | | rmxdiophlem 37582 |
. . . . . 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 1326 |
. . . . 5
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
19 | 18 | pm5.32da 673 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1)))) |
20 | | anass 681 |
. . . . . 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 3041 |
. . . . 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 3092 |
. . . . 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 265 |
. . . 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 276 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1))) |
25 | 24 | rabbiia 3185 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
1)} |
26 | | 3nn0 11310 |
. . 3
⊢ 3 ∈
ℕ0 |
27 | | vex 3203 |
. . . . . . . 8
⊢ 𝑐 ∈ V |
28 | 27 | resex 5443 |
. . . . . . 7
⊢ (𝑐 ↾ (1...3)) ∈
V |
29 | | fvex 6201 |
. . . . . . 7
⊢ (𝑐‘4) ∈
V |
30 | | df-2 11079 |
. . . . . . . . . . . . . 14
⊢ 2 = (1 +
1) |
31 | 30, 5 | jm2.27dlem5 37580 |
. . . . . . . . . . . . 13
⊢ (1...1)
⊆ (1...3) |
32 | | 1nn 11031 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ |
33 | 32 | jm2.27dlem3 37578 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1...1) |
34 | 31, 33 | sselii 3600 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...3) |
35 | 34 | jm2.27dlem1 37576 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘1) = (𝑐‘1)) |
36 | 35 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑐‘1) ∈
(ℤ≥‘2))) |
37 | 36 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑐‘1) ∈
(ℤ≥‘2))) |
38 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → 𝑏 = (𝑐‘4)) |
39 | 8 | jm2.27dlem1 37576 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘2) = (𝑐‘2)) |
40 | 35, 39 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑐‘1) Yrm (𝑐‘2))) |
41 | 40 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑐‘1) Yrm (𝑐‘2))) |
42 | 38, 41 | eqeq12d 2637 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (𝑏 = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))) |
43 | 37, 42 | anbi12d 747 |
. . . . . . . 8
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))))) |
44 | 13 | jm2.27dlem1 37576 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (𝑎‘3) = (𝑐‘3)) |
45 | 44 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2)) |
46 | 45 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((𝑎‘3)↑2) = ((𝑐‘3)↑2)) |
47 | 35 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑐 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑐‘1)↑2)) |
48 | 47 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑐 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) =
(((𝑐‘1)↑2)
− 1)) |
49 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑐‘4) → (𝑏↑2) = ((𝑐‘4)↑2)) |
50 | 48, 49 | oveqan12d 6669 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘1)↑2) − 1) · (𝑏↑2)) = ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) |
51 | 46, 50 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) =
(((𝑐‘3)↑2)
− ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2)))) |
52 | 51 | eqeq1d 2624 |
. . . . . . . 8
⊢ ((𝑎 = (𝑐 ↾ (1...3)) ∧ 𝑏 = (𝑐‘4)) → ((((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1
↔ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)) |
53 | 43, 52 | anbi12d 747 |
. . . . . . 7
⊢ ((𝑎 = (𝑐 ↾ (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 3505 |
. . . . . 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)) |
55 | 54 | a1i 11 |
. . . . 5
⊢ (𝑐 ∈ (ℕ0
↑𝑚 (1...4)) → ([(𝑐 ↾ (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))) |
56 | 55 | rabbiia 3185 |
. . . 4
⊢ {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
= {𝑐 ∈
(ℕ0 ↑𝑚 (1...4)) ∣ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)} |
57 | | 4nn0 11311 |
. . . . . 6
⊢ 4 ∈
ℕ0 |
58 | | rmydioph 37581 |
. . . . . 6
⊢ {𝑏 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈
(Dioph‘3) |
59 | | simp1 1061 |
. . . . . . . . 9
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘1) = (𝑐‘1)) |
60 | 59 | eleq1d 2686 |
. . . . . . . 8
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) ∈
(ℤ≥‘2) ↔ (𝑐‘1) ∈
(ℤ≥‘2))) |
61 | | simp3 1063 |
. . . . . . . . 9
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘3) = (𝑐‘4)) |
62 | | simp2 1062 |
. . . . . . . . . 10
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (𝑏‘2) = (𝑐‘2)) |
63 | 59, 62 | oveq12d 6668 |
. . . . . . . . 9
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘1) Yrm (𝑏‘2)) = ((𝑐‘1) Yrm (𝑐‘2))) |
64 | 61, 63 | eqeq12d 2637 |
. . . . . . . 8
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → ((𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)) ↔ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))) |
65 | 60, 64 | anbi12d 747 |
. . . . . . 7
⊢ (((𝑏‘1) = (𝑐‘1) ∧ (𝑏‘2) = (𝑐‘2) ∧ (𝑏‘3) = (𝑐‘4)) → (((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2))) ↔ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))))) |
66 | | df-4 11081 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
67 | | ssid 3624 |
. . . . . . . . . . 11
⊢ (1...4)
⊆ (1...4) |
68 | 66, 67 | jm2.27dlem5 37580 |
. . . . . . . . . 10
⊢ (1...3)
⊆ (1...4) |
69 | 3, 68 | jm2.27dlem5 37580 |
. . . . . . . . 9
⊢ (1...2)
⊆ (1...4) |
70 | 30, 69 | jm2.27dlem5 37580 |
. . . . . . . 8
⊢ (1...1)
⊆ (1...4) |
71 | 70, 33 | sselii 3600 |
. . . . . . 7
⊢ 1 ∈
(1...4) |
72 | 69, 7 | sselii 3600 |
. . . . . . 7
⊢ 2 ∈
(1...4) |
73 | | 4nn 11187 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
74 | 73 | jm2.27dlem3 37578 |
. . . . . . 7
⊢ 4 ∈
(1...4) |
75 | 65, 71, 72, 74 | rabren3dioph 37379 |
. . . . . 6
⊢ ((4
∈ ℕ0 ∧ {𝑏 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈ (Dioph‘3)) →
{𝑐 ∈
(ℕ0 ↑𝑚 (1...4)) ∣ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈
(Dioph‘4)) |
76 | 57, 58, 75 | mp2an 708 |
. . . . 5
⊢ {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈
(Dioph‘4) |
77 | | ovex 6678 |
. . . . . . . . 9
⊢ (1...4)
∈ V |
78 | 68, 13 | sselii 3600 |
. . . . . . . . 9
⊢ 3 ∈
(1...4) |
79 | | mzpproj 37300 |
. . . . . . . . 9
⊢ (((1...4)
∈ V ∧ 3 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ (𝑐‘3)) ∈
(mzPoly‘(1...4))) |
80 | 77, 78, 79 | mp2an 708 |
. . . . . . . 8
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (𝑐‘3)) ∈
(mzPoly‘(1...4)) |
81 | | 2nn0 11309 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
82 | | mzpexpmpt 37308 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (𝑐‘3)) ∈ (mzPoly‘(1...4))
∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ ((𝑐‘3)↑2)) ∈
(mzPoly‘(1...4))) |
83 | 80, 81, 82 | mp2an 708 |
. . . . . . 7
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ ((𝑐‘3)↑2)) ∈
(mzPoly‘(1...4)) |
84 | | mzpproj 37300 |
. . . . . . . . . . 11
⊢ (((1...4)
∈ V ∧ 1 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ (𝑐‘1)) ∈
(mzPoly‘(1...4))) |
85 | 77, 71, 84 | mp2an 708 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (𝑐‘1)) ∈
(mzPoly‘(1...4)) |
86 | | mzpexpmpt 37308 |
. . . . . . . . . 10
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (𝑐‘1)) ∈ (mzPoly‘(1...4))
∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ ((𝑐‘1)↑2)) ∈
(mzPoly‘(1...4))) |
87 | 85, 81, 86 | mp2an 708 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ ((𝑐‘1)↑2)) ∈
(mzPoly‘(1...4)) |
88 | | 1z 11407 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
89 | | mzpconstmpt 37303 |
. . . . . . . . . 10
⊢ (((1...4)
∈ V ∧ 1 ∈ ℤ) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) |
90 | 77, 88, 89 | mp2an 708 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ 1) ∈
(mzPoly‘(1...4)) |
91 | | mzpsubmpt 37306 |
. . . . . . . . 9
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ ((𝑐‘1)↑2)) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈
(mzPoly‘(1...4))) |
92 | 87, 90, 91 | mp2an 708 |
. . . . . . . 8
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈
(mzPoly‘(1...4)) |
93 | | mzpproj 37300 |
. . . . . . . . . 10
⊢ (((1...4)
∈ V ∧ 4 ∈ (1...4)) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ (𝑐‘4)) ∈
(mzPoly‘(1...4))) |
94 | 77, 74, 93 | mp2an 708 |
. . . . . . . . 9
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (𝑐‘4)) ∈
(mzPoly‘(1...4)) |
95 | | mzpexpmpt 37308 |
. . . . . . . . 9
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (𝑐‘4)) ∈ (mzPoly‘(1...4))
∧ 2 ∈ ℕ0) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ ((𝑐‘4)↑2)) ∈
(mzPoly‘(1...4))) |
96 | 94, 81, 95 | mp2an 708 |
. . . . . . . 8
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ ((𝑐‘4)↑2)) ∈
(mzPoly‘(1...4)) |
97 | | mzpmulmpt 37305 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (((𝑐‘1)↑2) − 1)) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ ((𝑐‘4)↑2)) ∈
(mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈
(mzPoly‘(1...4))) |
98 | 92, 96, 97 | mp2an 708 |
. . . . . . 7
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈
(mzPoly‘(1...4)) |
99 | | mzpsubmpt 37306 |
. . . . . . 7
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ ((𝑐‘3)↑2)) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ ((((𝑐‘1)↑2) − 1) · ((𝑐‘4)↑2))) ∈
(mzPoly‘(1...4))) → (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2)))) ∈
(mzPoly‘(1...4))) |
100 | 83, 98, 99 | mp2an 708 |
. . . . . 6
⊢ (𝑐 ∈ (ℤ
↑𝑚 (1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2)))) ∈
(mzPoly‘(1...4)) |
101 | | eqrabdioph 37341 |
. . . . . 6
⊢ ((4
∈ ℕ0 ∧ (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2)))) ∈
(mzPoly‘(1...4)) ∧ (𝑐 ∈ (ℤ ↑𝑚
(1...4)) ↦ 1) ∈ (mzPoly‘(1...4))) → {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1} ∈
(Dioph‘4)) |
102 | 57, 100, 90, 101 | mp3an 1424 |
. . . . 5
⊢ {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1} ∈
(Dioph‘4) |
103 | | anrabdioph 37344 |
. . . . 5
⊢ (({𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ ((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2)))} ∈ (Dioph‘4) ∧
{𝑐 ∈
(ℕ0 ↑𝑚 (1...4)) ∣ (((𝑐‘3)↑2) −
((((𝑐‘1)↑2)
− 1) · ((𝑐‘4)↑2))) = 1} ∈
(Dioph‘4)) → {𝑐
∈ (ℕ0 ↑𝑚 (1...4)) ∣
(((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)} ∈
(Dioph‘4)) |
104 | 76, 102, 103 | mp2an 708 |
. . . 4
⊢ {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ (((𝑐‘1) ∈
(ℤ≥‘2) ∧ (𝑐‘4) = ((𝑐‘1) Yrm (𝑐‘2))) ∧ (((𝑐‘3)↑2) − ((((𝑐‘1)↑2) − 1)
· ((𝑐‘4)↑2))) = 1)} ∈
(Dioph‘4) |
105 | 56, 104 | eqeltri 2697 |
. . 3
⊢ {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘4) |
106 | 66 | rexfrabdioph 37359 |
. . 3
⊢ ((3
∈ ℕ0 ∧ {𝑐 ∈ (ℕ0
↑𝑚 (1...4)) ∣ [(𝑐 ↾ (1...3)) / 𝑎][(𝑐‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘4)) → {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘3)) |
107 | 26, 105, 106 | mp2an 708 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm (𝑎‘2))) ∧ (((𝑎‘3)↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑏↑2))) = 1)}
∈ (Dioph‘3) |
108 | 25, 107 | eqeltri 2697 |
1
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈
(Dioph‘3) |