| Step | Hyp | Ref
| Expression |
| 1 | | elmapi 8889 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → 𝑎:(1...3)⟶ℕ0) |
| 2 | | 3nn 12345 |
. . . . . 6
⊢ 3 ∈
ℕ |
| 3 | 2 | jm2.27dlem3 43023 |
. . . . 5
⊢ 3 ∈
(1...3) |
| 4 | | ffvelcdm 7101 |
. . . . 5
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 3
∈ (1...3)) → (𝑎‘3) ∈
ℕ0) |
| 5 | 1, 3, 4 | sylancl 586 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘3) ∈
ℕ0) |
| 6 | | expdiophlem1 43033 |
. . . 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
↑m (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 3440 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} = {𝑎 ∈ (ℕ0
↑m (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 12544 |
. . 3
⊢ 3 ∈
ℕ0 |
| 10 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑒‘5) ∈
V |
| 11 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑒‘6) ∈
V |
| 12 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑒‘5) → (𝑐 = (𝑏 Yrm (𝑎‘2)) ↔ (𝑒‘5) = (𝑏 Yrm (𝑎‘2)))) |
| 13 | 12 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑒‘5) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))))) |
| 14 | 13 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))))) |
| 15 | | eqeq1 2741 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑒‘6) → (𝑑 = (𝑏 Xrm (𝑎‘2)) ↔ (𝑒‘6) = (𝑏 Xrm (𝑎‘2)))) |
| 16 | 15 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑒‘6) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))))) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))))) |
| 18 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → 𝑑 = (𝑒‘6)) |
| 19 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑒‘5) → ((𝑏 − (𝑎‘1)) · 𝑐) = ((𝑏 − (𝑎‘1)) · (𝑒‘5))) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 − (𝑎‘1)) · 𝑐) = ((𝑏 − (𝑎‘1)) · (𝑒‘5))) |
| 21 | 18, 20 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) = ((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5)))) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)) = (((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))) |
| 23 | 22 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)) ↔ ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥
(((𝑒‘6) −
((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))) |
| 24 | 23 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = (𝑒‘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 632 |
. . . . . . . . . . . 12
⊢ ((𝑐 = (𝑒‘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 632 |
. . . . . . . . . . 11
⊢ ((𝑐 = (𝑒‘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 630 |
. . . . . . . . . 10
⊢ ((𝑐 = (𝑒‘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 630 |
. . . . . . . . 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))))))))) |
| 29 | 10, 11, 28 | sbc2ie 3866 |
. . . . . . . 8
⊢
([(𝑒‘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 3846 |
. . . . . . 7
⊢
([(𝑒‘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 3846 |
. . . . . 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...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 3484 |
. . . . . . . 8
⊢ 𝑒 ∈ V |
| 33 | 32 | resex 6047 |
. . . . . . 7
⊢ (𝑒 ↾ (1...3)) ∈
V |
| 34 | | fvex 6919 |
. . . . . . 7
⊢ (𝑒‘4) ∈
V |
| 35 | | df-2 12329 |
. . . . . . . . . . . . . 14
⊢ 2 = (1 +
1) |
| 36 | | df-3 12330 |
. . . . . . . . . . . . . . 15
⊢ 3 = (2 +
1) |
| 37 | | ssid 4006 |
. . . . . . . . . . . . . . 15
⊢ (1...3)
⊆ (1...3) |
| 38 | 36, 37 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . 14
⊢ (1...2)
⊆ (1...3) |
| 39 | 35, 38 | jm2.27dlem5 43025 |
. . . . . . . . . . . . 13
⊢ (1...1)
⊆ (1...3) |
| 40 | | 1nn 12277 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ |
| 41 | 40 | jm2.27dlem3 43023 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1...1) |
| 42 | 39, 41 | sselii 3980 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...3) |
| 43 | 42 | jm2.27dlem1 43021 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘1) = (𝑒‘1)) |
| 44 | 43 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘1) ∈
(ℤ≥‘2))) |
| 45 | | 2nn 12339 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
| 46 | 45 | jm2.27dlem3 43023 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(1...2) |
| 47 | 46, 36, 45 | jm2.27dlem2 43022 |
. . . . . . . . . . . 12
⊢ 2 ∈
(1...3) |
| 48 | 47 | jm2.27dlem1 43021 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘2) = (𝑒‘2)) |
| 49 | 48 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘2) ∈ ℕ ↔ (𝑒‘2) ∈
ℕ)) |
| 50 | 44, 49 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ))) |
| 51 | 50 | adantr 480 |
. . . . . . . 8
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ))) |
| 52 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘1) ∈
(ℤ≥‘2))) |
| 53 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑒‘4) → 𝑏 = (𝑒‘4)) |
| 54 | 48 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘2) + 1) = ((𝑒‘2) + 1)) |
| 55 | 43, 54 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1) Yrm ((𝑎‘2) + 1)) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) |
| 56 | 53, 55 | eqeqan12rd 2752 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1)) ↔ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))) |
| 57 | 52, 56 | anbi12d 632 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
| 58 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘4) → (𝑏 ∈ (ℤ≥‘2)
↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 ∈ (ℤ≥‘2)
↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
| 60 | 53, 48 | oveqan12rd 7451 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 Yrm (𝑎‘2)) = ((𝑒‘4) Yrm (𝑒‘2))) |
| 61 | 60 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘5) = (𝑏 Yrm (𝑎‘2)) ↔ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))) |
| 62 | 59, 61 | anbi12d 632 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))))) |
| 63 | 53, 48 | oveqan12rd 7451 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 Xrm (𝑎‘2)) = ((𝑒‘4) Xrm (𝑒‘2))) |
| 64 | 63 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘6) = (𝑏 Xrm (𝑎‘2)) ↔ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))) |
| 65 | 59, 64 | anbi12d 632 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))))) |
| 66 | 3 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘3) = (𝑒‘3)) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑎‘3) = (𝑒‘3)) |
| 68 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑒‘4) → (2 · 𝑏) = (2 · (𝑒‘4))) |
| 69 | 68, 43 | oveqan12rd 7451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((2 · 𝑏) · (𝑎‘1)) = ((2 · (𝑒‘4)) · (𝑒‘1))) |
| 70 | 43 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑒‘1)↑2)) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘1)↑2) = ((𝑒‘1)↑2)) |
| 72 | 69, 71 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) = (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) |
| 73 | 72 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) = ((((2
· (𝑒‘4))
· (𝑒‘1))
− ((𝑒‘1)↑2)) −
1)) |
| 74 | 67, 73 | breq12d 5156 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ↔ (𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1))) |
| 75 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → 𝑏 = (𝑒‘4)) |
| 76 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑎‘1) = (𝑒‘1)) |
| 77 | 75, 76 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 − (𝑎‘1)) = ((𝑒‘4) − (𝑒‘1))) |
| 78 | 77 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 − (𝑎‘1)) · (𝑒‘5)) = (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) |
| 79 | 78 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) = ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) |
| 80 | 79, 67 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)) = (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) |
| 81 | 73, 80 | breq12d 5156 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (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 632 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (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 632 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (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 632 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑒 ↾ (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 632 |
. . . . . . . 8
⊢ ((𝑎 = (𝑒 ↾ (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 632 |
. . . . . . 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))))))))) |
| 87 | 33, 34, 86 | sbc2ie 3866 |
. . . . . 6
⊢
([(𝑒 ↾
(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 275 |
. . . . 5
⊢
([(𝑒 ↾
(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 | rabbii 3442 |
. . . 4
⊢ {𝑒 ∈ (ℕ0
↑m (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
↑m (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)))))))} |
| 90 | | 6nn0 12547 |
. . . . . . 7
⊢ 6 ∈
ℕ0 |
| 91 | | 2z 12649 |
. . . . . . 7
⊢ 2 ∈
ℤ |
| 92 | | ovex 7464 |
. . . . . . . 8
⊢ (1...6)
∈ V |
| 93 | | df-4 12331 |
. . . . . . . . . . . 12
⊢ 4 = (3 +
1) |
| 94 | | df-5 12332 |
. . . . . . . . . . . . 13
⊢ 5 = (4 +
1) |
| 95 | | df-6 12333 |
. . . . . . . . . . . . . 14
⊢ 6 = (5 +
1) |
| 96 | | ssid 4006 |
. . . . . . . . . . . . . 14
⊢ (1...6)
⊆ (1...6) |
| 97 | 95, 96 | jm2.27dlem5 43025 |
. . . . . . . . . . . . 13
⊢ (1...5)
⊆ (1...6) |
| 98 | 94, 97 | jm2.27dlem5 43025 |
. . . . . . . . . . . 12
⊢ (1...4)
⊆ (1...6) |
| 99 | 93, 98 | jm2.27dlem5 43025 |
. . . . . . . . . . 11
⊢ (1...3)
⊆ (1...6) |
| 100 | 36, 99 | jm2.27dlem5 43025 |
. . . . . . . . . 10
⊢ (1...2)
⊆ (1...6) |
| 101 | 35, 100 | jm2.27dlem5 43025 |
. . . . . . . . 9
⊢ (1...1)
⊆ (1...6) |
| 102 | 101, 41 | sselii 3980 |
. . . . . . . 8
⊢ 1 ∈
(1...6) |
| 103 | | mzpproj 42748 |
. . . . . . . 8
⊢ (((1...6)
∈ V ∧ 1 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘1)) ∈
(mzPoly‘(1...6))) |
| 104 | 92, 102, 103 | mp2an 692 |
. . . . . . 7
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘1)) ∈
(mzPoly‘(1...6)) |
| 105 | | eluzrabdioph 42817 |
. . . . . . 7
⊢ ((6
∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘1)) ∈
(mzPoly‘(1...6))) → {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘6)) |
| 106 | 90, 91, 104, 105 | mp3an 1463 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘6) |
| 107 | 100, 46 | sselii 3980 |
. . . . . . . 8
⊢ 2 ∈
(1...6) |
| 108 | | mzpproj 42748 |
. . . . . . . 8
⊢ (((1...6)
∈ V ∧ 2 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘2)) ∈
(mzPoly‘(1...6))) |
| 109 | 92, 107, 108 | mp2an 692 |
. . . . . . 7
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘2)) ∈
(mzPoly‘(1...6)) |
| 110 | | elnnrabdioph 42818 |
. . . . . . 7
⊢ ((6
∈ ℕ0 ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘2)) ∈
(mzPoly‘(1...6))) → {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘2) ∈ ℕ} ∈
(Dioph‘6)) |
| 111 | 90, 109, 110 | mp2an 692 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘2) ∈ ℕ} ∈
(Dioph‘6) |
| 112 | | anrabdioph 42791 |
. . . . . 6
⊢ (({𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘6) ∧ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘2) ∈ ℕ} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ)} ∈
(Dioph‘6)) |
| 113 | 106, 111,
112 | mp2an 692 |
. . . . 5
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ)} ∈
(Dioph‘6) |
| 114 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → 𝑒:(1...6)⟶ℕ0) |
| 115 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝑒:(1...6)⟶ℕ0 ∧ 2
∈ (1...6)) → (𝑒‘2) ∈
ℕ0) |
| 116 | 114, 107,
115 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → (𝑒‘2) ∈
ℕ0) |
| 117 | | peano2nn0 12566 |
. . . . . . . . . 10
⊢ ((𝑒‘2) ∈
ℕ0 → ((𝑒‘2) + 1) ∈
ℕ0) |
| 118 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ((𝑒‘2) + 1) → ((𝑒‘1) Yrm 𝑏) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) |
| 119 | 118 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑏 = ((𝑒‘2) + 1) → ((𝑒‘4) = ((𝑒‘1) Yrm 𝑏) ↔ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))) |
| 120 | 119 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑏 = ((𝑒‘2) + 1) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
| 121 | 120 | ceqsrexv 3655 |
. . . . . . . . . 10
⊢ (((𝑒‘2) + 1) ∈
ℕ0 → (∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
| 122 | 116, 117,
121 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → (∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
| 123 | 122 | bicomd 223 |
. . . . . . . 8
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ↔ ∃𝑏 ∈ ℕ0
(𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))))) |
| 124 | 123 | rabbiia 3440 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} = {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} |
| 125 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
| 126 | 125 | resex 6047 |
. . . . . . . . . . 11
⊢ (𝑎 ↾ (1...6)) ∈
V |
| 127 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑎‘7) ∈
V |
| 128 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑎‘7) → 𝑏 = (𝑎‘7)) |
| 129 | 107 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘2) = (𝑎‘2)) |
| 130 | 129 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑒 = (𝑎 ↾ (1...6)) → ((𝑒‘2) + 1) = ((𝑎‘2) + 1)) |
| 131 | 128, 130 | eqeqan12rd 2752 |
. . . . . . . . . . . 12
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑏 = ((𝑒‘2) + 1) ↔ (𝑎‘7) = ((𝑎‘2) + 1))) |
| 132 | 102 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘1) = (𝑎‘1)) |
| 133 | 132 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑒‘1) = (𝑎‘1)) |
| 134 | 133 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘1) ∈
(ℤ≥‘2) ↔ (𝑎‘1) ∈
(ℤ≥‘2))) |
| 135 | | 4nn 12349 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
| 136 | 135 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
(1...4) |
| 137 | 98, 136 | sselii 3980 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
(1...6) |
| 138 | 137 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘4) = (𝑎‘4)) |
| 139 | 138 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑒‘4) = (𝑎‘4)) |
| 140 | 132, 128 | oveqan12d 7450 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘1) Yrm 𝑏) = ((𝑎‘1) Yrm (𝑎‘7))) |
| 141 | 139, 140 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘4) = ((𝑒‘1) Yrm 𝑏) ↔ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))) |
| 142 | 134, 141 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
| 143 | 131, 142 | anbi12d 632 |
. . . . . . . . . . 11
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))))) |
| 144 | 126, 127,
143 | sbc2ie 3866 |
. . . . . . . . . 10
⊢
([(𝑎 ↾
(1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
| 145 | 144 | rabbii 3442 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} = {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))} |
| 146 | | 7nn0 12548 |
. . . . . . . . . . 11
⊢ 7 ∈
ℕ0 |
| 147 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (1...7)
∈ V |
| 148 | | 7nn 12358 |
. . . . . . . . . . . . 13
⊢ 7 ∈
ℕ |
| 149 | 148 | jm2.27dlem3 43023 |
. . . . . . . . . . . 12
⊢ 7 ∈
(1...7) |
| 150 | | mzpproj 42748 |
. . . . . . . . . . . 12
⊢ (((1...7)
∈ V ∧ 7 ∈ (1...7)) → (𝑎 ∈ (ℤ ↑m (1...7))
↦ (𝑎‘7)) ∈
(mzPoly‘(1...7))) |
| 151 | 147, 149,
150 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℤ
↑m (1...7)) ↦ (𝑎‘7)) ∈
(mzPoly‘(1...7)) |
| 152 | | df-7 12334 |
. . . . . . . . . . . . . 14
⊢ 7 = (6 +
1) |
| 153 | | 6nn 12355 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ |
| 154 | 107, 152,
153 | jm2.27dlem2 43022 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(1...7) |
| 155 | | mzpproj 42748 |
. . . . . . . . . . . . 13
⊢ (((1...7)
∈ V ∧ 2 ∈ (1...7)) → (𝑎 ∈ (ℤ ↑m (1...7))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...7))) |
| 156 | 147, 154,
155 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℤ
↑m (1...7)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...7)) |
| 157 | | 1z 12647 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
| 158 | | mzpconstmpt 42751 |
. . . . . . . . . . . . 13
⊢ (((1...7)
∈ V ∧ 1 ∈ ℤ) → (𝑎 ∈ (ℤ ↑m (1...7))
↦ 1) ∈ (mzPoly‘(1...7))) |
| 159 | 147, 157,
158 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℤ
↑m (1...7)) ↦ 1) ∈
(mzPoly‘(1...7)) |
| 160 | | mzpaddmpt 42752 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (ℤ
↑m (1...7)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...7))
∧ (𝑎 ∈ (ℤ
↑m (1...7)) ↦ 1) ∈ (mzPoly‘(1...7))) →
(𝑎 ∈ (ℤ
↑m (1...7)) ↦ ((𝑎‘2) + 1)) ∈
(mzPoly‘(1...7))) |
| 161 | 156, 159,
160 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (ℤ
↑m (1...7)) ↦ ((𝑎‘2) + 1)) ∈
(mzPoly‘(1...7)) |
| 162 | | eqrabdioph 42788 |
. . . . . . . . . . 11
⊢ ((7
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...7))
↦ (𝑎‘7)) ∈
(mzPoly‘(1...7)) ∧ (𝑎 ∈ (ℤ ↑m (1...7))
↦ ((𝑎‘2) + 1))
∈ (mzPoly‘(1...7))) → {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ (𝑎‘7) = ((𝑎‘2) + 1)} ∈
(Dioph‘7)) |
| 163 | 146, 151,
161, 162 | mp3an 1463 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ (𝑎‘7) = ((𝑎‘2) + 1)} ∈
(Dioph‘7) |
| 164 | | rmydioph 43026 |
. . . . . . . . . . 11
⊢ {𝑏 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈
(Dioph‘3) |
| 165 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘1) = (𝑎‘1)) |
| 166 | 165 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘1) ∈
(ℤ≥‘2) ↔ (𝑎‘1) ∈
(ℤ≥‘2))) |
| 167 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘3) = (𝑎‘4)) |
| 168 | | simp2 1138 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘2) = (𝑎‘7)) |
| 169 | 165, 168 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘1) Yrm (𝑏‘2)) = ((𝑎‘1) Yrm (𝑎‘7))) |
| 170 | 167, 169 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)) ↔ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))) |
| 171 | 166, 170 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
| 172 | 102, 152,
153 | jm2.27dlem2 43022 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...7) |
| 173 | 137, 152,
153 | jm2.27dlem2 43022 |
. . . . . . . . . . . 12
⊢ 4 ∈
(1...7) |
| 174 | 171, 172,
149, 173 | rabren3dioph 42826 |
. . . . . . . . . . 11
⊢ ((7
∈ ℕ0 ∧ {𝑏 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...7)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))} ∈
(Dioph‘7)) |
| 175 | 146, 164,
174 | mp2an 692 |
. . . . . . . . . 10
⊢ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))} ∈
(Dioph‘7) |
| 176 | | anrabdioph 42791 |
. . . . . . . . . 10
⊢ (({𝑎 ∈ (ℕ0
↑m (1...7)) ∣ (𝑎‘7) = ((𝑎‘2) + 1)} ∈ (Dioph‘7) ∧
{𝑎 ∈
(ℕ0 ↑m (1...7)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7)))} ∈ (Dioph‘7)) →
{𝑎 ∈
(ℕ0 ↑m (1...7)) ∣ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))} ∈
(Dioph‘7)) |
| 177 | 163, 175,
176 | mp2an 692 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))} ∈
(Dioph‘7) |
| 178 | 145, 177 | eqeltri 2837 |
. . . . . . . 8
⊢ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘7) |
| 179 | 152 | rexfrabdioph 42806 |
. . . . . . . 8
⊢ ((6
∈ ℕ0 ∧ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘7)) → {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘6)) |
| 180 | 90, 178, 179 | mp2an 692 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ∃𝑏 ∈ ℕ0 (𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘6) |
| 181 | 124, 180 | eqeltri 2837 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} ∈
(Dioph‘6) |
| 182 | | rmydioph 43026 |
. . . . . . . 8
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈
(Dioph‘3) |
| 183 | | simp1 1137 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘1) = (𝑒‘4)) |
| 184 | 183 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
| 185 | | simp3 1139 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘3) = (𝑒‘5)) |
| 186 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘2) = (𝑒‘2)) |
| 187 | 183, 186 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑒‘4) Yrm (𝑒‘2))) |
| 188 | 185, 187 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))) |
| 189 | 184, 188 | anbi12d 632 |
. . . . . . . . 9
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))))) |
| 190 | | 5nn 12352 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ |
| 191 | 190 | jm2.27dlem3 43023 |
. . . . . . . . . 10
⊢ 5 ∈
(1...5) |
| 192 | 191, 95, 190 | jm2.27dlem2 43022 |
. . . . . . . . 9
⊢ 5 ∈
(1...6) |
| 193 | 189, 137,
107, 192 | rabren3dioph 42826 |
. . . . . . . 8
⊢ ((6
∈ ℕ0 ∧ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)) →
{𝑒 ∈
(ℕ0 ↑m (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))} ∈
(Dioph‘6)) |
| 194 | 90, 182, 193 | mp2an 692 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))} ∈
(Dioph‘6) |
| 195 | | rmxdioph 43028 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈
(Dioph‘3) |
| 196 | | simp1 1137 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘1) = (𝑒‘4)) |
| 197 | 196 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
| 198 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘3) = (𝑒‘6)) |
| 199 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘2) = (𝑒‘2)) |
| 200 | 196, 199 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘1) Xrm (𝑎‘2)) = ((𝑒‘4) Xrm (𝑒‘2))) |
| 201 | 198, 200 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)) ↔ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))) |
| 202 | 197, 201 | anbi12d 632 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))))) |
| 203 | 153 | jm2.27dlem3 43023 |
. . . . . . . . . 10
⊢ 6 ∈
(1...6) |
| 204 | 202, 137,
107, 203 | rabren3dioph 42826 |
. . . . . . . . 9
⊢ ((6
∈ ℕ0 ∧ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3)) →
{𝑒 ∈
(ℕ0 ↑m (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))} ∈
(Dioph‘6)) |
| 205 | 90, 195, 204 | mp2an 692 |
. . . . . . . 8
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))} ∈
(Dioph‘6) |
| 206 | 99, 3 | sselii 3980 |
. . . . . . . . . . 11
⊢ 3 ∈
(1...6) |
| 207 | | mzpproj 42748 |
. . . . . . . . . . 11
⊢ (((1...6)
∈ V ∧ 3 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘3)) ∈
(mzPoly‘(1...6))) |
| 208 | 92, 206, 207 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘3)) ∈
(mzPoly‘(1...6)) |
| 209 | | mzpconstmpt 42751 |
. . . . . . . . . . . . . . 15
⊢ (((1...6)
∈ V ∧ 2 ∈ ℤ) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ 2) ∈ (mzPoly‘(1...6))) |
| 210 | 92, 91, 209 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ 2) ∈
(mzPoly‘(1...6)) |
| 211 | | mzpproj 42748 |
. . . . . . . . . . . . . . 15
⊢ (((1...6)
∈ V ∧ 4 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘4)) ∈
(mzPoly‘(1...6))) |
| 212 | 92, 137, 211 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘4)) ∈
(mzPoly‘(1...6)) |
| 213 | | mzpmulmpt 42753 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ 2) ∈ (mzPoly‘(1...6)) ∧
(𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘4)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (2 · (𝑒‘4))) ∈
(mzPoly‘(1...6))) |
| 214 | 210, 212,
213 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (2 · (𝑒‘4))) ∈
(mzPoly‘(1...6)) |
| 215 | | mzpmulmpt 42753 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ (2 · (𝑒‘4))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((2 · (𝑒‘4)) · (𝑒‘1))) ∈
(mzPoly‘(1...6))) |
| 216 | 214, 104,
215 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((2 · (𝑒‘4)) · (𝑒‘1))) ∈
(mzPoly‘(1...6)) |
| 217 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 218 | | mzpexpmpt 42756 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6))
∧ 2 ∈ ℕ0) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ ((𝑒‘1)↑2)) ∈
(mzPoly‘(1...6))) |
| 219 | 104, 217,
218 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘1)↑2)) ∈
(mzPoly‘(1...6)) |
| 220 | | mzpsubmpt 42754 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((2 · (𝑒‘4)) · (𝑒‘1))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘1)↑2)) ∈
(mzPoly‘(1...6))) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) ∈
(mzPoly‘(1...6))) |
| 221 | 216, 219,
220 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) ∈
(mzPoly‘(1...6)) |
| 222 | | mzpconstmpt 42751 |
. . . . . . . . . . . 12
⊢ (((1...6)
∈ V ∧ 1 ∈ ℤ) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ 1) ∈ (mzPoly‘(1...6))) |
| 223 | 92, 157, 222 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ 1) ∈
(mzPoly‘(1...6)) |
| 224 | | mzpsubmpt 42754 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) ∈
(mzPoly‘(1...6)) ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ 1) ∈ (mzPoly‘(1...6))) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6))) |
| 225 | 221, 223,
224 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6)) |
| 226 | | ltrabdioph 42819 |
. . . . . . . . . 10
⊢ ((6
∈ ℕ0 ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘3)) ∈
(mzPoly‘(1...6)) ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6))) → {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)}
∈ (Dioph‘6)) |
| 227 | 90, 208, 225, 226 | mp3an 1463 |
. . . . . . . . 9
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)}
∈ (Dioph‘6) |
| 228 | | mzpproj 42748 |
. . . . . . . . . . . . 13
⊢ (((1...6)
∈ V ∧ 6 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘6)) ∈
(mzPoly‘(1...6))) |
| 229 | 92, 203, 228 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘6)) ∈
(mzPoly‘(1...6)) |
| 230 | | mzpsubmpt 42754 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘4)) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘1)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘4) − (𝑒‘1))) ∈
(mzPoly‘(1...6))) |
| 231 | 212, 104,
230 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘4) − (𝑒‘1))) ∈
(mzPoly‘(1...6)) |
| 232 | | mzpproj 42748 |
. . . . . . . . . . . . . 14
⊢ (((1...6)
∈ V ∧ 5 ∈ (1...6)) → (𝑒 ∈ (ℤ ↑m (1...6))
↦ (𝑒‘5)) ∈
(mzPoly‘(1...6))) |
| 233 | 92, 192, 232 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘5)) ∈
(mzPoly‘(1...6)) |
| 234 | | mzpmulmpt 42753 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘4) − (𝑒‘1))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘5)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) ∈
(mzPoly‘(1...6))) |
| 235 | 231, 233,
234 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) ∈
(mzPoly‘(1...6)) |
| 236 | | mzpsubmpt 42754 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘6)) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) ∈
(mzPoly‘(1...6))) |
| 237 | 229, 235,
236 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) ∈
(mzPoly‘(1...6)) |
| 238 | | mzpsubmpt 42754 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ (ℤ
↑m (1...6)) ↦ ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) ∈ (mzPoly‘(1...6))
∧ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (𝑒‘3)) ∈ (mzPoly‘(1...6)))
→ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) ∈
(mzPoly‘(1...6))) |
| 239 | 237, 208,
238 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℤ
↑m (1...6)) ↦ (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) ∈
(mzPoly‘(1...6)) |
| 240 | | dvdsrabdioph 42821 |
. . . . . . . . . 10
⊢ ((6
∈ ℕ0 ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)) ∈
(mzPoly‘(1...6)) ∧ (𝑒 ∈ (ℤ ↑m (1...6))
↦ (((𝑒‘6)
− (((𝑒‘4)
− (𝑒‘1))
· (𝑒‘5)))
− (𝑒‘3)))
∈ (mzPoly‘(1...6))) → {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))} ∈
(Dioph‘6)) |
| 241 | 90, 225, 239, 240 | mp3an 1463 |
. . . . . . . . 9
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))} ∈
(Dioph‘6) |
| 242 | | anrabdioph 42791 |
. . . . . . . . 9
⊢ (({𝑒 ∈ (ℕ0
↑m (1...6)) ∣ (𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)}
∈ (Dioph‘6) ∧ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑m (1...6)) ∣ ((𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1) ∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))} ∈
(Dioph‘6)) |
| 243 | 227, 241,
242 | mp2an 692 |
. . . . . . . 8
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))} ∈
(Dioph‘6) |
| 244 | | anrabdioph 42791 |
. . . . . . . 8
⊢ (({𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2)))} ∈ (Dioph‘6) ∧
{𝑒 ∈
(ℕ0 ↑m (1...6)) ∣ ((𝑒‘3) < ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1)
∧ ((((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2)) − 1) ∥
(((𝑒‘6) −
(((𝑒‘4) −
(𝑒‘1)) ·
(𝑒‘5))) −
(𝑒‘3)))} ∈
(Dioph‘6)) → {𝑒
∈ (ℕ0 ↑m (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)) |
| 245 | 205, 243,
244 | mp2an 692 |
. . . . . . 7
⊢ {𝑒 ∈ (ℕ0
↑m (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) |
| 246 | | anrabdioph 42791 |
. . . . . . 7
⊢ (({𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2)))} ∈ (Dioph‘6) ∧
{𝑒 ∈
(ℕ0 ↑m (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 ↑m (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)) |
| 247 | 194, 245,
246 | mp2an 692 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑m (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) |
| 248 | | anrabdioph 42791 |
. . . . . 6
⊢ (({𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} ∈ (Dioph‘6)
∧ {𝑒 ∈
(ℕ0 ↑m (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 ↑m (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)) |
| 249 | 181, 247,
248 | mp2an 692 |
. . . . 5
⊢ {𝑒 ∈ (ℕ0
↑m (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) |
| 250 | | anrabdioph 42791 |
. . . . 5
⊢ (({𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ)} ∈
(Dioph‘6) ∧ {𝑒
∈ (ℕ0 ↑m (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 ↑m (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)) |
| 251 | 113, 249,
250 | mp2an 692 |
. . . 4
⊢ {𝑒 ∈ (ℕ0
↑m (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) |
| 252 | 89, 251 | eqeltri 2837 |
. . 3
⊢ {𝑒 ∈ (ℕ0
↑m (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) |
| 253 | 93, 94, 95 | 3rexfrabdioph 42808 |
. . 3
⊢ ((3
∈ ℕ0 ∧ {𝑒 ∈ (ℕ0
↑m (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 ↑m (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)) |
| 254 | 9, 252, 253 | mp2an 692 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (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) |
| 255 | 8, 254 | eqeltri 2837 |
1
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈
(Dioph‘3) |