Step | Hyp | Ref
| Expression |
1 | | elmapi 7765 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0) |
2 | | 3nn 11063 |
. . . . . 6
⊢ 3 ∈
ℕ |
3 | 2 | jm2.27dlem3 36596 |
. . . . 5
⊢ 3 ∈
(1...3) |
4 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 3
∈ (1...3)) → (𝑎‘3) ∈
ℕ0) |
5 | 1, 3, 4 | sylancl 693 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → (𝑎‘3) ∈
ℕ0) |
6 | | expdiophlem1 36606 |
. . . 4
⊢ ((𝑎‘3) ∈
ℕ0 → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
∃𝑑 ∈
ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))))) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))) ↔ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
∃𝑑 ∈
ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))))) |
8 | 7 | rabbiia 3161 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} = {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
∃𝑑 ∈
ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))))} |
9 | | 3nn0 11187 |
. . 3
⊢ 3 ∈
ℕ0 |
10 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑒‘5) ∈
V |
11 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑒‘6) ∈
V |
12 | | eqeq1 2614 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑒‘5) → (𝑐 = (𝑏 Yrm (𝑎‘2)) ↔ (𝑒‘5) = (𝑏 Yrm (𝑎‘2)))) |
13 | 12 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑒‘5) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))))) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))))) |
15 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑒‘6) → (𝑑 = (𝑏 Xrm (𝑎‘2)) ↔ (𝑒‘6) = (𝑏 Xrm (𝑎‘2)))) |
16 | 15 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑒‘6) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))))) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))))) |
18 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → 𝑑 = (𝑒‘6)) |
19 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = (𝑒‘5) → ((𝑏 − (𝑎‘1)) · 𝑐) = ((𝑏 − (𝑎‘1)) · (𝑒‘5))) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 − (𝑎‘1)) · 𝑐) = ((𝑏 − (𝑎‘1)) · (𝑒‘5))) |
21 | 18, 20 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) = ((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5)))) |
22 | 21 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)) = (((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))) |
23 | 22 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)) ↔ ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥
(((𝑒‘6) −
((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))) |
24 | 23 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))) ↔ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))))) |
25 | 17, 24 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 ·
𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∧ ((((2 · 𝑏)
· (𝑎‘1))
− ((𝑎‘1)↑2)) − 1) ∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))) ↔ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 ·
𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∧ ((((2 · 𝑏)
· (𝑎‘1))
− ((𝑎‘1)↑2)) − 1) ∥
(((𝑒‘6) −
((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))))) |
26 | 14, 25 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))) ↔ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))))))) |
27 | 26 | anbi2d 736 |
. . . . . . . . . . 11
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))) ↔ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))))))) |
28 | 27 | anbi2d 736 |
. . . . . . . . . 10
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))) ↔ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))))))))) |
29 | 10, 11, 28 | sbc2ie 3472 |
. . . . . . . . 9
⊢
([(𝑒‘5)
/ 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))) ↔ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))))))) |
30 | 29 | sbcbii 3458 |
. . . . . . . 8
⊢
([(𝑒‘4)
/ 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))) ↔ [(𝑒‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))))))) |
31 | 30 | sbcbii 3458 |
. . . . . . 7
⊢
([(𝑒 ↾
(1...3)) / 𝑎][(𝑒‘4) / 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))) ↔ [(𝑒 ↾ (1...3)) / 𝑎][(𝑒‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))))))) |
32 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑒 ∈ V |
33 | 32 | resex 5363 |
. . . . . . . 8
⊢ (𝑒 ↾ (1...3)) ∈
V |
34 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑒‘4) ∈
V |
35 | | df-2 10956 |
. . . . . . . . . . . . . . 15
⊢ 2 = (1 +
1) |
36 | | df-3 10957 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
37 | | ssid 3587 |
. . . . . . . . . . . . . . . 16
⊢ (1...3)
⊆ (1...3) |
38 | 36, 37 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . 15
⊢ (1...2)
⊆ (1...3) |
39 | 35, 38 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . 14
⊢ (1...1)
⊆ (1...3) |
40 | | 1nn 10908 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ |
41 | 40 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
(1...1) |
42 | 39, 41 | sselii 3565 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1...3) |
43 | 42 | jm2.27dlem1 36594 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘1) = (𝑒‘1)) |
44 | 43 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘1) ∈
(ℤ≥‘2))) |
45 | | 2nn 11062 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
46 | 45 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(1...2) |
47 | 46, 36, 45 | jm2.27dlem2 36595 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(1...3) |
48 | 47 | jm2.27dlem1 36594 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘2) = (𝑒‘2)) |
49 | 48 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘2) ∈ ℕ ↔ (𝑒‘2) ∈
ℕ)) |
50 | 44, 49 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ))) |
51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ))) |
52 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘1) ∈
(ℤ≥‘2))) |
53 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘4) → 𝑏 = (𝑒‘4)) |
54 | 48 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘2) + 1) = ((𝑒‘2) + 1)) |
55 | 43, 54 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1) Yrm ((𝑎‘2) + 1)) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) |
56 | 53, 55 | eqeqan12rd 2628 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1)) ↔ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))) |
57 | 52, 56 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
58 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘4) → (𝑏 ∈ (ℤ≥‘2)
↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
59 | 58 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 ∈ (ℤ≥‘2)
↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
60 | 53, 48 | oveqan12rd 6569 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 Yrm (𝑎‘2)) = ((𝑒‘4) Yrm (𝑒‘2))) |
61 | 60 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘5) = (𝑏 Yrm (𝑎‘2)) ↔ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))) |
62 | 59, 61 | anbi12d 743 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))))) |
63 | 53, 48 | oveqan12rd 6569 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 Xrm (𝑎‘2)) = ((𝑒‘4) Xrm (𝑒‘2))) |
64 | 63 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘6) = (𝑏 Xrm (𝑎‘2)) ↔ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))) |
65 | 59, 64 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))))) |
66 | 3 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘3) = (𝑒‘3)) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑎‘3) = (𝑒‘3)) |
68 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑒‘4) → (2 · 𝑏) = (2 · (𝑒‘4))) |
69 | 68, 43 | oveqan12rd 6569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((2 · 𝑏) · (𝑎‘1)) = ((2 · (𝑒‘4)) · (𝑒‘1))) |
70 | 43 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑒‘1)↑2)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘1)↑2) = ((𝑒‘1)↑2)) |
72 | 69, 71 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) = (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) |
73 | 72 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) = ((((2
· (𝑒‘4))
· (𝑒‘1))
− ((𝑒‘1)↑2)) −
1)) |
74 | 67, 73 | breq12d 4596 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ↔ (𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1))) |
75 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → 𝑏 = (𝑒‘4)) |
76 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑎‘1) = (𝑒‘1)) |
77 | 75, 76 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 − (𝑎‘1)) = ((𝑒‘4) − (𝑒‘1))) |
78 | 77 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 − (𝑎‘1)) · (𝑒‘5)) = (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) |
79 | 78 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) = ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) |
80 | 79, 67 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)) = (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) |
81 | 73, 80 | breq12d 4596 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥
(((𝑒‘6) −
((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)) ↔ ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1) ∥ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3)))) |
82 | 74, 81 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))) ↔ ((𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1) ∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))) |
83 | 65, 82 | anbi12d 743 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 ·
𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∧ ((((2 · 𝑏)
· (𝑎‘1))
− ((𝑎‘1)↑2)) − 1) ∥
(((𝑒‘6) −
((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))) ↔ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))) |
84 | 62, 83 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))))) ↔ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))))) |
85 | 57, 84 | anbi12d 743 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))))) ↔ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))))) |
86 | 51, 85 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))))))) ↔ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))))))) |
87 | 33, 34, 86 | sbc2ie 3472 |
. . . . . . 7
⊢
([(𝑒 ↾
(1...3)) / 𝑎][(𝑒‘4) / 𝑏](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ (((𝑒‘6)
− ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))))))) ↔ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))))) |
88 | 31, 87 | bitri 263 |
. . . . . 6
⊢
([(𝑒 ↾
(1...3)) / 𝑎][(𝑒‘4) / 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))) ↔ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))))) |
89 | 88 | a1i 11 |
. . . . 5
⊢ (𝑒 ∈ (ℕ0
↑𝑚 (1...6)) → ([(𝑒 ↾ (1...3)) / 𝑎][(𝑒‘4) / 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3))))))) ↔ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))))))) |
90 | 89 | rabbiia 3161 |
. . . 4
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ [(𝑒 ↾ (1...3)) / 𝑎][(𝑒‘4) / 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))))} = {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))))} |
91 | | 6nn0 11190 |
. . . . . . 7
⊢ 6 ∈
ℕ0 |
92 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
93 | | ovex 6577 |
. . . . . . . 8
⊢ (1...6)
∈ V |
94 | | df-4 10958 |
. . . . . . . . . . . 12
⊢ 4 = (3 +
1) |
95 | | df-5 10959 |
. . . . . . . . . . . . 13
⊢ 5 = (4 +
1) |
96 | | df-6 10960 |
. . . . . . . . . . . . . 14
⊢ 6 = (5 +
1) |
97 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ (1...6)
⊆ (1...6) |
98 | 96, 97 | jm2.27dlem5 36598 |
. . . . . . . . . . . . 13
⊢ (1...5)
⊆ (1...6) |
99 | 95, 98 | jm2.27dlem5 36598 |
. . . . . . . . . . . 12
⊢ (1...4)
⊆ (1...6) |
100 | 94, 99 | jm2.27dlem5 36598 |
. . . . . . . . . . 11
⊢ (1...3)
⊆ (1...6) |
101 | 36, 100 | jm2.27dlem5 36598 |
. . . . . . . . . 10
⊢ (1...2)
⊆ (1...6) |
102 | 35, 101 | jm2.27dlem5 36598 |
. . . . . . . . 9
⊢ (1...1)
⊆ (1...6) |
103 | 102, 41 | sselii 3565 |
. . . . . . . 8
⊢ 1 ∈
(1...6) |
104 | | mzpproj 36318 |
. . . . . . . 8
⊢ (((1...6)
∈ V ∧ 1 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘1)) ∈
(mzPoly‘(1...6))) |
105 | 93, 103, 104 | mp2an 704 |
. . . . . . 7
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘1)) ∈
(mzPoly‘(1...6)) |
106 | | eluzrabdioph 36388 |
. . . . . . 7
⊢ ((6
∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6)))
→ {𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ (𝑒‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘6)) |
107 | 91, 92, 105, 106 | mp3an 1416 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘6) |
108 | 101, 46 | sselii 3565 |
. . . . . . . 8
⊢ 2 ∈
(1...6) |
109 | | mzpproj 36318 |
. . . . . . . 8
⊢ (((1...6)
∈ V ∧ 2 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘2)) ∈
(mzPoly‘(1...6))) |
110 | 93, 108, 109 | mp2an 704 |
. . . . . . 7
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘2)) ∈
(mzPoly‘(1...6)) |
111 | | elnnrabdioph 36389 |
. . . . . . 7
⊢ ((6
∈ ℕ0 ∧ (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘2)) ∈ (mzPoly‘(1...6)))
→ {𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ (𝑒‘2) ∈ ℕ} ∈
(Dioph‘6)) |
112 | 91, 110, 111 | mp2an 704 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘2) ∈ ℕ} ∈
(Dioph‘6) |
113 | | anrabdioph 36362 |
. . . . . 6
⊢ (({𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘6) ∧ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘2) ∈ ℕ} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ)} ∈
(Dioph‘6)) |
114 | 107, 112,
113 | mp2an 704 |
. . . . 5
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ)} ∈
(Dioph‘6) |
115 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℕ0
↑𝑚 (1...6)) → 𝑒:(1...6)⟶ℕ0) |
116 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝑒:(1...6)⟶ℕ0 ∧ 2
∈ (1...6)) → (𝑒‘2) ∈
ℕ0) |
117 | 115, 108,
116 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℕ0
↑𝑚 (1...6)) → (𝑒‘2) ∈
ℕ0) |
118 | | peano2nn0 11210 |
. . . . . . . . . 10
⊢ ((𝑒‘2) ∈
ℕ0 → ((𝑒‘2) + 1) ∈
ℕ0) |
119 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ((𝑒‘2) + 1) → ((𝑒‘1) Yrm 𝑏) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) |
120 | 119 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑏 = ((𝑒‘2) + 1) → ((𝑒‘4) = ((𝑒‘1) Yrm 𝑏) ↔ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))) |
121 | 120 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑏 = ((𝑒‘2) + 1) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
122 | 121 | ceqsrexv 3306 |
. . . . . . . . . 10
⊢ (((𝑒‘2) + 1) ∈
ℕ0 → (∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
123 | 117, 118,
122 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑒 ∈ (ℕ0
↑𝑚 (1...6)) → (∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
124 | 123 | bicomd 212 |
. . . . . . . 8
⊢ (𝑒 ∈ (ℕ0
↑𝑚 (1...6)) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ↔ ∃𝑏 ∈ ℕ0
(𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))))) |
125 | 124 | rabbiia 3161 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} = {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} |
126 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
127 | 126 | resex 5363 |
. . . . . . . . . . . 12
⊢ (𝑎 ↾ (1...6)) ∈
V |
128 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑎‘7) ∈
V |
129 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑎‘7) → 𝑏 = (𝑎‘7)) |
130 | 108 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘2) = (𝑎‘2)) |
131 | 130 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = (𝑎 ↾ (1...6)) → ((𝑒‘2) + 1) = ((𝑎‘2) + 1)) |
132 | 129, 131 | eqeqan12rd 2628 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑏 = ((𝑒‘2) + 1) ↔ (𝑎‘7) = ((𝑎‘2) + 1))) |
133 | 103 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘1) = (𝑎‘1)) |
134 | 133 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑒‘1) = (𝑎‘1)) |
135 | 134 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘1) ∈
(ℤ≥‘2) ↔ (𝑎‘1) ∈
(ℤ≥‘2))) |
136 | | 4nn 11064 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℕ |
137 | 136 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
(1...4) |
138 | 99, 137 | sselii 3565 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
(1...6) |
139 | 138 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘4) = (𝑎‘4)) |
140 | 139 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑒‘4) = (𝑎‘4)) |
141 | 133, 129 | oveqan12d 6568 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘1) Yrm 𝑏) = ((𝑎‘1) Yrm (𝑎‘7))) |
142 | 140, 141 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘4) = ((𝑒‘1) Yrm 𝑏) ↔ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))) |
143 | 135, 142 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
144 | 132, 143 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))))) |
145 | 127, 128,
144 | sbc2ie 3472 |
. . . . . . . . . . 11
⊢
([(𝑎 ↾
(1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
146 | 145 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...7)) → ([(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))))) |
147 | 146 | rabbiia 3161 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} = {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))} |
148 | | 7nn0 11191 |
. . . . . . . . . . 11
⊢ 7 ∈
ℕ0 |
149 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (1...7)
∈ V |
150 | | 7nn 11067 |
. . . . . . . . . . . . 13
⊢ 7 ∈
ℕ |
151 | 150 | jm2.27dlem3 36596 |
. . . . . . . . . . . 12
⊢ 7 ∈
(1...7) |
152 | | mzpproj 36318 |
. . . . . . . . . . . 12
⊢ (((1...7)
∈ V ∧ 7 ∈ (1...7)) → (𝑎 ∈ (ℤ ↑𝑚
(1...7)) ↦ (𝑎‘7)) ∈
(mzPoly‘(1...7))) |
153 | 149, 151,
152 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ (𝑎‘7)) ∈
(mzPoly‘(1...7)) |
154 | | df-7 10961 |
. . . . . . . . . . . . . 14
⊢ 7 = (6 +
1) |
155 | | 6nn 11066 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ |
156 | 108, 154,
155 | jm2.27dlem2 36595 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(1...7) |
157 | | mzpproj 36318 |
. . . . . . . . . . . . 13
⊢ (((1...7)
∈ V ∧ 2 ∈ (1...7)) → (𝑎 ∈ (ℤ ↑𝑚
(1...7)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...7))) |
158 | 149, 156,
157 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...7)) |
159 | | 1z 11284 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
160 | | mzpconstmpt 36321 |
. . . . . . . . . . . . 13
⊢ (((1...7)
∈ V ∧ 1 ∈ ℤ) → (𝑎 ∈ (ℤ ↑𝑚
(1...7)) ↦ 1) ∈ (mzPoly‘(1...7))) |
161 | 149, 159,
160 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ 1) ∈
(mzPoly‘(1...7)) |
162 | | mzpaddmpt 36322 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...7))
∧ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ 1) ∈ (mzPoly‘(1...7)))
→ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ ((𝑎‘2) + 1)) ∈
(mzPoly‘(1...7))) |
163 | 158, 161,
162 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ ((𝑎‘2) + 1)) ∈
(mzPoly‘(1...7)) |
164 | | eqrabdioph 36359 |
. . . . . . . . . . 11
⊢ ((7
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚
(1...7)) ↦ (𝑎‘7)) ∈ (mzPoly‘(1...7))
∧ (𝑎 ∈ (ℤ
↑𝑚 (1...7)) ↦ ((𝑎‘2) + 1)) ∈
(mzPoly‘(1...7))) → {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ (𝑎‘7) = ((𝑎‘2) + 1)} ∈
(Dioph‘7)) |
165 | 148, 153,
163, 164 | mp3an 1416 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ (𝑎‘7) = ((𝑎‘2) + 1)} ∈
(Dioph‘7) |
166 | | rmydioph 36599 |
. . . . . . . . . . 11
⊢ {𝑏 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈
(Dioph‘3) |
167 | | simp1 1054 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘1) = (𝑎‘1)) |
168 | 167 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘1) ∈
(ℤ≥‘2) ↔ (𝑎‘1) ∈
(ℤ≥‘2))) |
169 | | simp3 1056 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘3) = (𝑎‘4)) |
170 | | simp2 1055 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘2) = (𝑎‘7)) |
171 | 167, 170 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘1) Yrm (𝑏‘2)) = ((𝑎‘1) Yrm (𝑎‘7))) |
172 | 169, 171 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)) ↔ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))) |
173 | 168, 172 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
174 | 103, 154,
155 | jm2.27dlem2 36595 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...7) |
175 | 138, 154,
155 | jm2.27dlem2 36595 |
. . . . . . . . . . . 12
⊢ 4 ∈
(1...7) |
176 | 173, 174,
151, 175 | rabren3dioph 36397 |
. . . . . . . . . . 11
⊢ ((7
∈ ℕ0 ∧ {𝑏 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑𝑚 (1...7)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))} ∈
(Dioph‘7)) |
177 | 148, 166,
176 | mp2an 704 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))} ∈
(Dioph‘7) |
178 | | anrabdioph 36362 |
. . . . . . . . . 10
⊢ (({𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ (𝑎‘7) = ((𝑎‘2) + 1)} ∈ (Dioph‘7) ∧
{𝑎 ∈
(ℕ0 ↑𝑚 (1...7)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))} ∈ (Dioph‘7)) →
{𝑎 ∈
(ℕ0 ↑𝑚 (1...7)) ∣ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))} ∈
(Dioph‘7)) |
179 | 165, 177,
178 | mp2an 704 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))} ∈
(Dioph‘7) |
180 | 147, 179 | eqeltri 2684 |
. . . . . . . 8
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘7) |
181 | 154 | rexfrabdioph 36377 |
. . . . . . . 8
⊢ ((6
∈ ℕ0 ∧ {𝑎 ∈ (ℕ0
↑𝑚 (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘7)) → {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘6)) |
182 | 91, 180, 181 | mp2an 704 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘6) |
183 | 125, 182 | eqeltri 2684 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} ∈
(Dioph‘6) |
184 | | rmydioph 36599 |
. . . . . . . 8
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈
(Dioph‘3) |
185 | | simp1 1054 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘1) = (𝑒‘4)) |
186 | 185 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
187 | | simp3 1056 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘3) = (𝑒‘5)) |
188 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘2) = (𝑒‘2)) |
189 | 185, 188 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑒‘4) Yrm (𝑒‘2))) |
190 | 187, 189 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))) |
191 | 186, 190 | anbi12d 743 |
. . . . . . . . 9
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))))) |
192 | | 5nn 11065 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ |
193 | 192 | jm2.27dlem3 36596 |
. . . . . . . . . 10
⊢ 5 ∈
(1...5) |
194 | 193, 96, 192 | jm2.27dlem2 36595 |
. . . . . . . . 9
⊢ 5 ∈
(1...6) |
195 | 191, 138,
108, 194 | rabren3dioph 36397 |
. . . . . . . 8
⊢ ((6
∈ ℕ0 ∧ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)) →
{𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))} ∈
(Dioph‘6)) |
196 | 91, 184, 195 | mp2an 704 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))} ∈
(Dioph‘6) |
197 | | rmxdioph 36601 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈
(Dioph‘3) |
198 | | simp1 1054 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘1) = (𝑒‘4)) |
199 | 198 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
200 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘3) = (𝑒‘6)) |
201 | | simp2 1055 |
. . . . . . . . . . . . 13
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘2) = (𝑒‘2)) |
202 | 198, 201 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘1) Xrm (𝑎‘2)) = ((𝑒‘4) Xrm (𝑒‘2))) |
203 | 200, 202 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))) |
204 | 199, 203 | anbi12d 743 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))))) |
205 | 155 | jm2.27dlem3 36596 |
. . . . . . . . . 10
⊢ 6 ∈
(1...6) |
206 | 204, 138,
108, 205 | rabren3dioph 36397 |
. . . . . . . . 9
⊢ ((6
∈ ℕ0 ∧ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3)) →
{𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))} ∈
(Dioph‘6)) |
207 | 91, 197, 206 | mp2an 704 |
. . . . . . . 8
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))} ∈
(Dioph‘6) |
208 | 100, 3 | sselii 3565 |
. . . . . . . . . . 11
⊢ 3 ∈
(1...6) |
209 | | mzpproj 36318 |
. . . . . . . . . . 11
⊢ (((1...6)
∈ V ∧ 3 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘3)) ∈
(mzPoly‘(1...6))) |
210 | 93, 208, 209 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘3)) ∈
(mzPoly‘(1...6)) |
211 | | mzpconstmpt 36321 |
. . . . . . . . . . . . . . 15
⊢ (((1...6)
∈ V ∧ 2 ∈ ℤ) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ 2) ∈ (mzPoly‘(1...6))) |
212 | 93, 92, 211 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ 2) ∈
(mzPoly‘(1...6)) |
213 | | mzpproj 36318 |
. . . . . . . . . . . . . . 15
⊢ (((1...6)
∈ V ∧ 4 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘4)) ∈
(mzPoly‘(1...6))) |
214 | 93, 138, 213 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘4)) ∈
(mzPoly‘(1...6)) |
215 | | mzpmulmpt 36323 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ 2) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘4)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (2 · (𝑒‘4))) ∈
(mzPoly‘(1...6))) |
216 | 212, 214,
215 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (2 · (𝑒‘4))) ∈
(mzPoly‘(1...6)) |
217 | | mzpmulmpt 36323 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (2 · (𝑒‘4))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((2 · (𝑒‘4)) · (𝑒‘1))) ∈
(mzPoly‘(1...6))) |
218 | 216, 105,
217 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((2 · (𝑒‘4)) · (𝑒‘1))) ∈
(mzPoly‘(1...6)) |
219 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
220 | | mzpexpmpt 36326 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6))
∧ 2 ∈ ℕ0) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ ((𝑒‘1)↑2)) ∈
(mzPoly‘(1...6))) |
221 | 105, 219,
220 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘1)↑2)) ∈
(mzPoly‘(1...6)) |
222 | | mzpsubmpt 36324 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((2 · (𝑒‘4)) · (𝑒‘1))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘1)↑2)) ∈
(mzPoly‘(1...6))) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) ∈
(mzPoly‘(1...6))) |
223 | 218, 221,
222 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) ∈
(mzPoly‘(1...6)) |
224 | | mzpconstmpt 36321 |
. . . . . . . . . . . 12
⊢ (((1...6)
∈ V ∧ 1 ∈ ℤ) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ 1) ∈ (mzPoly‘(1...6))) |
225 | 93, 159, 224 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ 1) ∈
(mzPoly‘(1...6)) |
226 | | mzpsubmpt 36324 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) ∈
(mzPoly‘(1...6)) ∧ (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ 1) ∈ (mzPoly‘(1...6))) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6))) |
227 | 223, 225,
226 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6)) |
228 | | ltrabdioph 36390 |
. . . . . . . . . 10
⊢ ((6
∈ ℕ0 ∧ (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘3)) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6))) → {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)}
∈ (Dioph‘6)) |
229 | 91, 210, 227, 228 | mp3an 1416 |
. . . . . . . . 9
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)}
∈ (Dioph‘6) |
230 | | mzpproj 36318 |
. . . . . . . . . . . . 13
⊢ (((1...6)
∈ V ∧ 6 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘6)) ∈
(mzPoly‘(1...6))) |
231 | 93, 205, 230 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘6)) ∈
(mzPoly‘(1...6)) |
232 | | mzpsubmpt 36324 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘4)) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘4) − (𝑒‘1))) ∈
(mzPoly‘(1...6))) |
233 | 214, 105,
232 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘4) − (𝑒‘1))) ∈
(mzPoly‘(1...6)) |
234 | | mzpproj 36318 |
. . . . . . . . . . . . . 14
⊢ (((1...6)
∈ V ∧ 5 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (𝑒‘5)) ∈
(mzPoly‘(1...6))) |
235 | 93, 194, 234 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘5)) ∈
(mzPoly‘(1...6)) |
236 | | mzpmulmpt 36323 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘4) − (𝑒‘1))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘5)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) ∈
(mzPoly‘(1...6))) |
237 | 233, 235,
236 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) ∈
(mzPoly‘(1...6)) |
238 | | mzpsubmpt 36324 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘6)) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) ∈
(mzPoly‘(1...6))) |
239 | 231, 237,
238 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) ∈
(mzPoly‘(1...6)) |
240 | | mzpsubmpt 36324 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (𝑒‘3)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) ∈
(mzPoly‘(1...6))) |
241 | 239, 210,
240 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℤ
↑𝑚 (1...6)) ↦ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) ∈
(mzPoly‘(1...6)) |
242 | | dvdsrabdioph 36392 |
. . . . . . . . . 10
⊢ ((6
∈ ℕ0 ∧ (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6)) ∧ (𝑒 ∈ (ℤ ↑𝑚
(1...6)) ↦ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) ∈ (mzPoly‘(1...6)))
→ {𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1) ∥ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))} ∈
(Dioph‘6)) |
243 | 91, 227, 241, 242 | mp3an 1416 |
. . . . . . . . 9
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))} ∈
(Dioph‘6) |
244 | | anrabdioph 36362 |
. . . . . . . . 9
⊢ (({𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)}
∈ (Dioph‘6) ∧ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣ ((𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1) ∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))} ∈
(Dioph‘6)) |
245 | 229, 243,
244 | mp2an 704 |
. . . . . . . 8
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))} ∈
(Dioph‘6) |
246 | | anrabdioph 36362 |
. . . . . . . 8
⊢ (({𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))} ∈ (Dioph‘6) ∧
{𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ ((𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1) ∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣
(((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))} ∈
(Dioph‘6)) |
247 | 207, 245,
246 | mp2an 704 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))} ∈
(Dioph‘6) |
248 | | anrabdioph 36362 |
. . . . . . 7
⊢ (({𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))} ∈ (Dioph‘6) ∧
{𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣
(((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))} ∈
(Dioph‘6)) |
249 | 196, 247,
248 | mp2an 704 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))} ∈
(Dioph‘6) |
250 | | anrabdioph 36362 |
. . . . . 6
⊢ (({𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} ∈ (Dioph‘6)
∧ {𝑒 ∈
(ℕ0 ↑𝑚 (1...6)) ∣ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣
(((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))))} ∈
(Dioph‘6)) |
251 | 183, 249,
250 | mp2an 704 |
. . . . 5
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))))} ∈
(Dioph‘6) |
252 | | anrabdioph 36362 |
. . . . 5
⊢ (({𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ)} ∈
(Dioph‘6) ∧ {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣
(((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))))))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑𝑚 (1...6)) ∣
(((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))))} ∈
(Dioph‘6)) |
253 | 114, 251,
252 | mp2an 704 |
. . . 4
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ) ∧ (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))) ∧ (((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))) ∧ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))))))} ∈
(Dioph‘6) |
254 | 90, 253 | eqeltri 2684 |
. . 3
⊢ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ [(𝑒 ↾ (1...3)) / 𝑎][(𝑒‘4) / 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))))} ∈
(Dioph‘6) |
255 | 94, 95, 96 | 3rexfrabdioph 36379 |
. . 3
⊢ ((3
∈ ℕ0 ∧ {𝑒 ∈ (ℕ0
↑𝑚 (1...6)) ∣ [(𝑒 ↾ (1...3)) / 𝑎][(𝑒‘4) / 𝑏][(𝑒‘5) / 𝑐][(𝑒‘6) / 𝑑](((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))))} ∈ (Dioph‘6))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))))} ∈
(Dioph‘3)) |
256 | 9, 254, 255 | mp2an 704 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
∃𝑑 ∈
ℕ0 (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ∧ ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ∧ ((𝑏 ∈
(ℤ≥‘2) ∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ∧ ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∧ ((((2
· 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1)
∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)))))))} ∈
(Dioph‘3) |
257 | 8, 256 | eqeltri 2684 |
1
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈
(Dioph‘3) |