Step | Hyp | Ref
| Expression |
1 | | elmapi 8530 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → 𝑎:(1...3)⟶ℕ0) |
2 | | 3nn 11909 |
. . . . . 6
⊢ 3 ∈
ℕ |
3 | 2 | jm2.27dlem3 40536 |
. . . . 5
⊢ 3 ∈
(1...3) |
4 | | ffvelrn 6902 |
. . . . 5
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 3
∈ (1...3)) → (𝑎‘3) ∈
ℕ0) |
5 | 1, 3, 4 | sylancl 589 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘3) ∈
ℕ0) |
6 | | expdiophlem1 40546 |
. . . 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 3382 |
. 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 12108 |
. . 3
⊢ 3 ∈
ℕ0 |
10 | | fvex 6730 |
. . . . . . . . 9
⊢ (𝑒‘5) ∈
V |
11 | | fvex 6730 |
. . . . . . . . 9
⊢ (𝑒‘6) ∈
V |
12 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑒‘5) → (𝑐 = (𝑏 Yrm (𝑎‘2)) ↔ (𝑒‘5) = (𝑏 Yrm (𝑎‘2)))) |
13 | 12 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑒‘5) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))))) |
14 | 13 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑐 = (𝑏 Yrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))))) |
15 | | eqeq1 2741 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝑒‘6) → (𝑑 = (𝑏 Xrm (𝑎‘2)) ↔ (𝑒‘6) = (𝑏 Xrm (𝑎‘2)))) |
16 | 15 | anbi2d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑒‘6) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))))) |
17 | 16 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 ∈ (ℤ≥‘2)
∧ 𝑑 = (𝑏 Xrm (𝑎‘2))) ↔ (𝑏 ∈
(ℤ≥‘2) ∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))))) |
18 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → 𝑑 = (𝑒‘6)) |
19 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑒‘5) → ((𝑏 − (𝑎‘1)) · 𝑐) = ((𝑏 − (𝑎‘1)) · (𝑒‘5))) |
20 | 19 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑏 − (𝑎‘1)) · 𝑐) = ((𝑏 − (𝑎‘1)) · (𝑒‘5))) |
21 | 18, 20 | oveq12d 7231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) = ((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5)))) |
22 | 21 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)) = (((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3))) |
23 | 22 | breq2d 5065 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = (𝑒‘5) ∧ 𝑑 = (𝑒‘6)) → (((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥ ((𝑑 − ((𝑏 − (𝑎‘1)) · 𝑐)) − (𝑎‘3)) ↔ ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ∥
(((𝑒‘6) −
((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)))) |
24 | 23 | anbi2d 632 |
. . . . . . . . . . . . 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 634 |
. . . . . . . . . . . 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 634 |
. . . . . . . . . . 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 632 |
. . . . . . . . . 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 632 |
. . . . . . . . 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 3778 |
. . . . . . . 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 3755 |
. . . . . . 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 3755 |
. . . . . 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 3412 |
. . . . . . . 8
⊢ 𝑒 ∈ V |
33 | 32 | resex 5899 |
. . . . . . 7
⊢ (𝑒 ↾ (1...3)) ∈
V |
34 | | fvex 6730 |
. . . . . . 7
⊢ (𝑒‘4) ∈
V |
35 | | df-2 11893 |
. . . . . . . . . . . . . 14
⊢ 2 = (1 +
1) |
36 | | df-3 11894 |
. . . . . . . . . . . . . . 15
⊢ 3 = (2 +
1) |
37 | | ssid 3923 |
. . . . . . . . . . . . . . 15
⊢ (1...3)
⊆ (1...3) |
38 | 36, 37 | jm2.27dlem5 40538 |
. . . . . . . . . . . . . 14
⊢ (1...2)
⊆ (1...3) |
39 | 35, 38 | jm2.27dlem5 40538 |
. . . . . . . . . . . . 13
⊢ (1...1)
⊆ (1...3) |
40 | | 1nn 11841 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ |
41 | 40 | jm2.27dlem3 40536 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1...1) |
42 | 39, 41 | sselii 3897 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...3) |
43 | 42 | jm2.27dlem1 40534 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘1) = (𝑒‘1)) |
44 | 43 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘1) ∈
(ℤ≥‘2))) |
45 | | 2nn 11903 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
46 | 45 | jm2.27dlem3 40536 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(1...2) |
47 | 46, 36, 45 | jm2.27dlem2 40535 |
. . . . . . . . . . . 12
⊢ 2 ∈
(1...3) |
48 | 47 | jm2.27dlem1 40534 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘2) = (𝑒‘2)) |
49 | 48 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘2) ∈ ℕ ↔ (𝑒‘2) ∈
ℕ)) |
50 | 44, 49 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ))) |
51 | 50 | adantr 484 |
. . . . . . . 8
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘2) ∈ ℕ))) |
52 | 44 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘1) ∈
(ℤ≥‘2))) |
53 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑒‘4) → 𝑏 = (𝑒‘4)) |
54 | 48 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘2) + 1) = ((𝑒‘2) + 1)) |
55 | 43, 54 | oveq12d 7231 |
. . . . . . . . . . 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 634 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 𝑏 = ((𝑎‘1) Yrm ((𝑎‘2) + 1))) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
58 | | eleq1 2825 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘4) → (𝑏 ∈ (ℤ≥‘2)
↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
59 | 58 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 ∈ (ℤ≥‘2)
↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
60 | 53, 48 | oveqan12rd 7233 |
. . . . . . . . . . . 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 634 |
. . . . . . . . . 10
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘5) = (𝑏 Yrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))))) |
63 | 53, 48 | oveqan12rd 7233 |
. . . . . . . . . . . . 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 634 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 ∈ (ℤ≥‘2)
∧ (𝑒‘6) = (𝑏 Xrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))))) |
66 | 3 | jm2.27dlem1 40534 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑒 ↾ (1...3)) → (𝑎‘3) = (𝑒‘3)) |
67 | 66 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑎‘3) = (𝑒‘3)) |
68 | | oveq2 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑒‘4) → (2 · 𝑏) = (2 · (𝑒‘4))) |
69 | 68, 43 | oveqan12rd 7233 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((2 · 𝑏) · (𝑎‘1)) = ((2 · (𝑒‘4)) · (𝑒‘1))) |
70 | 43 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑒 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑒‘1)↑2)) |
71 | 70 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘1)↑2) = ((𝑒‘1)↑2)) |
72 | 69, 71 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) = (((2 · (𝑒‘4)) · (𝑒‘1)) − ((𝑒‘1)↑2))) |
73 | 72 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) = ((((2
· (𝑒‘4))
· (𝑒‘1))
− ((𝑒‘1)↑2)) −
1)) |
74 | 67, 73 | breq12d 5066 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑎‘3) < ((((2 · 𝑏) · (𝑎‘1)) − ((𝑎‘1)↑2)) − 1) ↔ (𝑒‘3) < ((((2 ·
(𝑒‘4)) ·
(𝑒‘1)) −
((𝑒‘1)↑2))
− 1))) |
75 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → 𝑏 = (𝑒‘4)) |
76 | 43 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑎‘1) = (𝑒‘1)) |
77 | 75, 76 | oveq12d 7231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (𝑏 − (𝑎‘1)) = ((𝑒‘4) − (𝑒‘1))) |
78 | 77 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑏 − (𝑎‘1)) · (𝑒‘5)) = (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) |
79 | 78 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → ((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) = ((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5)))) |
80 | 79, 67 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑒 ↾ (1...3)) ∧ 𝑏 = (𝑒‘4)) → (((𝑒‘6) − ((𝑏 − (𝑎‘1)) · (𝑒‘5))) − (𝑎‘3)) = (((𝑒‘6) − (((𝑒‘4) − (𝑒‘1)) · (𝑒‘5))) − (𝑒‘3))) |
81 | 73, 80 | breq12d 5066 |
. . . . . . . . . . . 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 634 |
. . . . . . . . . . 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 634 |
. . . . . . . . . 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 634 |
. . . . . . . . 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 634 |
. . . . . . . 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 634 |
. . . . . . 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 3778 |
. . . . . 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 278 |
. . . . 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 3383 |
. . . 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 12111 |
. . . . . . 7
⊢ 6 ∈
ℕ0 |
91 | | 2z 12209 |
. . . . . . 7
⊢ 2 ∈
ℤ |
92 | | ovex 7246 |
. . . . . . . 8
⊢ (1...6)
∈ V |
93 | | df-4 11895 |
. . . . . . . . . . . 12
⊢ 4 = (3 +
1) |
94 | | df-5 11896 |
. . . . . . . . . . . . 13
⊢ 5 = (4 +
1) |
95 | | df-6 11897 |
. . . . . . . . . . . . . 14
⊢ 6 = (5 +
1) |
96 | | ssid 3923 |
. . . . . . . . . . . . . 14
⊢ (1...6)
⊆ (1...6) |
97 | 95, 96 | jm2.27dlem5 40538 |
. . . . . . . . . . . . 13
⊢ (1...5)
⊆ (1...6) |
98 | 94, 97 | jm2.27dlem5 40538 |
. . . . . . . . . . . 12
⊢ (1...4)
⊆ (1...6) |
99 | 93, 98 | jm2.27dlem5 40538 |
. . . . . . . . . . 11
⊢ (1...3)
⊆ (1...6) |
100 | 36, 99 | jm2.27dlem5 40538 |
. . . . . . . . . 10
⊢ (1...2)
⊆ (1...6) |
101 | 35, 100 | jm2.27dlem5 40538 |
. . . . . . . . 9
⊢ (1...1)
⊆ (1...6) |
102 | 101, 41 | sselii 3897 |
. . . . . . . 8
⊢ 1 ∈
(1...6) |
103 | | mzpproj 40262 |
. . . . . . . 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 40331 |
. . . . . . 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 3897 |
. . . . . . . 8
⊢ 2 ∈
(1...6) |
108 | | mzpproj 40262 |
. . . . . . . 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 40332 |
. . . . . . 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 40305 |
. . . . . 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 8530 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → 𝑒:(1...6)⟶ℕ0) |
115 | | ffvelrn 6902 |
. . . . . . . . . . 11
⊢ ((𝑒:(1...6)⟶ℕ0 ∧ 2
∈ (1...6)) → (𝑒‘2) ∈
ℕ0) |
116 | 114, 107,
115 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → (𝑒‘2) ∈
ℕ0) |
117 | | peano2nn0 12130 |
. . . . . . . . . 10
⊢ ((𝑒‘2) ∈
ℕ0 → ((𝑒‘2) + 1) ∈
ℕ0) |
118 | | oveq2 7221 |
. . . . . . . . . . . . 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 632 |
. . . . . . . . . . 11
⊢ (𝑏 = ((𝑒‘2) + 1) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)) ↔ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))))) |
121 | 120 | ceqsrexv 3563 |
. . . . . . . . . 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 226 |
. . . . . . . 8
⊢ (𝑒 ∈ (ℕ0
↑m (1...6)) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1))) ↔ ∃𝑏 ∈ ℕ0
(𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))))) |
124 | 123 | rabbiia 3382 |
. . . . . . 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 3412 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
126 | 125 | resex 5899 |
. . . . . . . . . . 11
⊢ (𝑎 ↾ (1...6)) ∈
V |
127 | | fvex 6730 |
. . . . . . . . . . 11
⊢ (𝑎‘7) ∈
V |
128 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑎‘7) → 𝑏 = (𝑎‘7)) |
129 | 107 | jm2.27dlem1 40534 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘2) = (𝑎‘2)) |
130 | 129 | oveq1d 7228 |
. . . . . . . . . . . . 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 40534 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘1) = (𝑎‘1)) |
133 | 132 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑒‘1) = (𝑎‘1)) |
134 | 133 | eleq1d 2822 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → ((𝑒‘1) ∈
(ℤ≥‘2) ↔ (𝑎‘1) ∈
(ℤ≥‘2))) |
135 | | 4nn 11913 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 ∈
ℕ |
136 | 135 | jm2.27dlem3 40536 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
(1...4) |
137 | 98, 136 | sselii 3897 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
(1...6) |
138 | 137 | jm2.27dlem1 40534 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝑎 ↾ (1...6)) → (𝑒‘4) = (𝑎‘4)) |
139 | 138 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (𝑒‘4) = (𝑎‘4)) |
140 | 132, 128 | oveqan12d 7232 |
. . . . . . . . . . . . . 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 634 |
. . . . . . . . . . . 12
⊢ ((𝑒 = (𝑎 ↾ (1...6)) ∧ 𝑏 = (𝑎‘7)) → (((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
143 | 131, 142 | anbi12d 634 |
. . . . . . . . . . 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 3778 |
. . . . . . . . . 10
⊢
([(𝑎 ↾
(1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏))) ↔ ((𝑎‘7) = ((𝑎‘2) + 1) ∧ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘4) = ((𝑎‘1) Yrm (𝑎‘7))))) |
145 | 144 | rabbii 3383 |
. . . . . . . . 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 12112 |
. . . . . . . . . . 11
⊢ 7 ∈
ℕ0 |
147 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ (1...7)
∈ V |
148 | | 7nn 11922 |
. . . . . . . . . . . . 13
⊢ 7 ∈
ℕ |
149 | 148 | jm2.27dlem3 40536 |
. . . . . . . . . . . 12
⊢ 7 ∈
(1...7) |
150 | | mzpproj 40262 |
. . . . . . . . . . . 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 11898 |
. . . . . . . . . . . . . 14
⊢ 7 = (6 +
1) |
153 | | 6nn 11919 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ |
154 | 107, 152,
153 | jm2.27dlem2 40535 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(1...7) |
155 | | mzpproj 40262 |
. . . . . . . . . . . . 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 12207 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
158 | | mzpconstmpt 40265 |
. . . . . . . . . . . . 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 40266 |
. . . . . . . . . . . 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 40302 |
. . . . . . . . . . 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 40539 |
. . . . . . . . . . 11
⊢ {𝑏 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑏‘1) ∈
(ℤ≥‘2) ∧ (𝑏‘3) = ((𝑏‘1) Yrm (𝑏‘2)))} ∈
(Dioph‘3) |
165 | | simp1 1138 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘1) = (𝑎‘1)) |
166 | 165 | eleq1d 2822 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → ((𝑏‘1) ∈
(ℤ≥‘2) ↔ (𝑎‘1) ∈
(ℤ≥‘2))) |
167 | | simp3 1140 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘3) = (𝑎‘4)) |
168 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏‘1) = (𝑎‘1) ∧ (𝑏‘2) = (𝑎‘7) ∧ (𝑏‘3) = (𝑎‘4)) → (𝑏‘2) = (𝑎‘7)) |
169 | 165, 168 | oveq12d 7231 |
. . . . . . . . . . . . . 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 634 |
. . . . . . . . . . . 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 40535 |
. . . . . . . . . . . 12
⊢ 1 ∈
(1...7) |
173 | 137, 152,
153 | jm2.27dlem2 40535 |
. . . . . . . . . . . 12
⊢ 4 ∈
(1...7) |
174 | 171, 172,
149, 173 | rabren3dioph 40340 |
. . . . . . . . . . 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 40305 |
. . . . . . . . . 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 2834 |
. . . . . . . 8
⊢ {𝑎 ∈ (ℕ0
↑m (1...7)) ∣ [(𝑎 ↾ (1...6)) / 𝑒][(𝑎‘7) / 𝑏](𝑏 = ((𝑒‘2) + 1) ∧ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm 𝑏)))} ∈ (Dioph‘7) |
179 | 152 | rexfrabdioph 40320 |
. . . . . . . 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 2834 |
. . . . . 6
⊢ {𝑒 ∈ (ℕ0
↑m (1...6)) ∣ ((𝑒‘1) ∈
(ℤ≥‘2) ∧ (𝑒‘4) = ((𝑒‘1) Yrm ((𝑒‘2) + 1)))} ∈
(Dioph‘6) |
182 | | rmydioph 40539 |
. . . . . . . 8
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈
(Dioph‘3) |
183 | | simp1 1138 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘1) = (𝑒‘4)) |
184 | 183 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
185 | | simp3 1140 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘3) = (𝑒‘5)) |
186 | | simp2 1139 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (𝑎‘2) = (𝑒‘2)) |
187 | 183, 186 | oveq12d 7231 |
. . . . . . . . . . 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 634 |
. . . . . . . . 9
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘5)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘5) = ((𝑒‘4) Yrm (𝑒‘2))))) |
190 | | 5nn 11916 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ |
191 | 190 | jm2.27dlem3 40536 |
. . . . . . . . . 10
⊢ 5 ∈
(1...5) |
192 | 191, 95, 190 | jm2.27dlem2 40535 |
. . . . . . . . 9
⊢ 5 ∈
(1...6) |
193 | 189, 137,
107, 192 | rabren3dioph 40340 |
. . . . . . . 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 40541 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈
(Dioph‘3) |
196 | | simp1 1138 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘1) = (𝑒‘4)) |
197 | 196 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → ((𝑎‘1) ∈
(ℤ≥‘2) ↔ (𝑒‘4) ∈
(ℤ≥‘2))) |
198 | | simp3 1140 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘3) = (𝑒‘6)) |
199 | | simp2 1139 |
. . . . . . . . . . . . 13
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (𝑎‘2) = (𝑒‘2)) |
200 | 196, 199 | oveq12d 7231 |
. . . . . . . . . . . 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 634 |
. . . . . . . . . 10
⊢ (((𝑎‘1) = (𝑒‘4) ∧ (𝑎‘2) = (𝑒‘2) ∧ (𝑎‘3) = (𝑒‘6)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2))) ↔ ((𝑒‘4) ∈
(ℤ≥‘2) ∧ (𝑒‘6) = ((𝑒‘4) Xrm (𝑒‘2))))) |
203 | 153 | jm2.27dlem3 40536 |
. . . . . . . . . 10
⊢ 6 ∈
(1...6) |
204 | 202, 137,
107, 203 | rabren3dioph 40340 |
. . . . . . . . 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 3897 |
. . . . . . . . . . 11
⊢ 3 ∈
(1...6) |
207 | | mzpproj 40262 |
. . . . . . . . . . 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 40265 |
. . . . . . . . . . . . . . 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 40262 |
. . . . . . . . . . . . . . 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 40267 |
. . . . . . . . . . . . . 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 40267 |
. . . . . . . . . . . . 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 12107 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
218 | | mzpexpmpt 40270 |
. . . . . . . . . . . . 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 40268 |
. . . . . . . . . . . 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 40265 |
. . . . . . . . . . . 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 40268 |
. . . . . . . . . . 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 40333 |
. . . . . . . . . 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 40262 |
. . . . . . . . . . . . 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 40268 |
. . . . . . . . . . . . . 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 40262 |
. . . . . . . . . . . . . 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 40267 |
. . . . . . . . . . . . 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 40268 |
. . . . . . . . . . . 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 40268 |
. . . . . . . . . . 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 40335 |
. . . . . . . . . 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 40305 |
. . . . . . . . 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 40305 |
. . . . . . . 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 40305 |
. . . . . . 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 40305 |
. . . . . 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 40305 |
. . . . 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 2834 |
. . 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 40322 |
. . 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 2834 |
1
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈
(Dioph‘3) |