| Step | Hyp | Ref
| Expression |
| 1 | | elmapi 8889 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → 𝑎:(1...3)⟶ℕ0) |
| 2 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 3 | 2 | jm2.27dlem3 43023 |
. . . . . . . 8
⊢ 2 ∈
(1...2) |
| 4 | | df-3 12330 |
. . . . . . . 8
⊢ 3 = (2 +
1) |
| 5 | 3, 4, 2 | jm2.27dlem2 43022 |
. . . . . . 7
⊢ 2 ∈
(1...3) |
| 6 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2
∈ (1...3)) → (𝑎‘2) ∈
ℕ0) |
| 7 | 1, 5, 6 | sylancl 586 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (𝑎‘2) ∈
ℕ0) |
| 8 | | elnn0 12528 |
. . . . . 6
⊢ ((𝑎‘2) ∈
ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) |
| 9 | 7, 8 | sylib 218 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) |
| 10 | | iba 527 |
. . . . . . 7
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) =
0)))) |
| 11 | | andi 1010 |
. . . . . . 7
⊢ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))) |
| 12 | 10, 11 | bitrdi 287 |
. . . . . 6
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))) |
| 13 | 12 | anbi2d 630 |
. . . . 5
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
(((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))) |
| 14 | 9, 13 | syl 17 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))) |
| 15 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈
(ℤ≥‘2)) |
| 16 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘2) ∈ ℕ →
(𝑎‘2) ∈
ℤ) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈
ℤ) |
| 18 | | frmy 42926 |
. . . . . . . . . . . . . 14
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 19 | 18 | fovcl 7561 |
. . . . . . . . . . . . 13
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℤ) |
| 20 | 15, 17, 19 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℤ) |
| 21 | | rmy0 42941 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘1) ∈
(ℤ≥‘2) → ((𝑎‘1) Yrm 0) =
0) |
| 22 | 21 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) =
0) |
| 23 | | nngt0 12297 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘2) ∈ ℕ →
0 < (𝑎‘2)) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 <
(𝑎‘2)) |
| 25 | | 0zd 12625 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈
ℤ) |
| 26 | | ltrmy 42964 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) →
(0 < (𝑎‘2) ↔
((𝑎‘1) Yrm
0) < ((𝑎‘1)
Yrm (𝑎‘2)))) |
| 27 | 15, 25, 17, 26 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 <
(𝑎‘2) ↔ ((𝑎‘1) Yrm 0) <
((𝑎‘1) Yrm
(𝑎‘2)))) |
| 28 | 24, 27 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) <
((𝑎‘1) Yrm
(𝑎‘2))) |
| 29 | 22, 28 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 <
((𝑎‘1) Yrm
(𝑎‘2))) |
| 30 | | elnnz 12623 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔
(((𝑎‘1)
Yrm (𝑎‘2))
∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2)))) |
| 31 | 20, 29, 30 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℕ) |
| 32 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℕ)) |
| 33 | 31, 32 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ)) |
| 34 | 33 | pm4.71rd 562 |
. . . . . . . . 9
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))))) |
| 35 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
(𝑎‘1) ∈
(ℤ≥‘2)) |
| 36 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
(𝑎‘2) ∈
ℕ) |
| 37 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
(𝑎‘3) ∈
ℕ) |
| 38 | | jm2.27 43020 |
. . . . . . . . . . 11
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ ∧ (𝑎‘3) ∈ ℕ) →
((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))) |
| 39 | 35, 36, 37, 38 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))) |
| 40 | 39 | pm5.32da 579 |
. . . . . . . . 9
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (((𝑎‘3) ∈ ℕ ∧
(𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘3) ∈ ℕ ∧
∃𝑏 ∈
ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0
∃𝑒 ∈
ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0
∃ℎ ∈
ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))) |
| 41 | 34, 40 | bitrd 279 |
. . . . . . . 8
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))))) |
| 42 | 41 | ex 412 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → ((𝑎‘2) ∈ ℕ → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))))) |
| 43 | 42 | pm5.32rd 578 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ↔ (((𝑎‘3) ∈ ℕ ∧
∃𝑏 ∈
ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0
∃𝑒 ∈
ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0
∃ℎ ∈
ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ))) |
| 44 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm
0)) |
| 45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0)) |
| 46 | 21 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) =
0) |
| 47 | 45, 46 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0) |
| 48 | 47 | eqeq2d 2748 |
. . . . . . . 8
⊢ (((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)) |
| 49 | 48 | ex 412 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))) |
| 50 | 49 | pm5.32rd 578 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))) |
| 51 | 43, 50 | orbi12d 919 |
. . . . 5
⊢ ((𝑎 ∈ (ℕ0
↑m (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → ((((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)) ↔ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) =
0)))) |
| 52 | 51 | pm5.32da 579 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) =
0))))) |
| 53 | 14, 52 | bitrd 279 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑m (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) =
0))))) |
| 54 | 53 | rabbiia 3440 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) =
0)))} |
| 55 | | 3nn0 12544 |
. . . 4
⊢ 3 ∈
ℕ0 |
| 56 | | 2z 12649 |
. . . 4
⊢ 2 ∈
ℤ |
| 57 | | ovex 7464 |
. . . . 5
⊢ (1...3)
∈ V |
| 58 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 59 | 58 | jm2.27dlem3 43023 |
. . . . . . 7
⊢ 1 ∈
(1...1) |
| 60 | | df-2 12329 |
. . . . . . 7
⊢ 2 = (1 +
1) |
| 61 | 59, 60, 58 | jm2.27dlem2 43022 |
. . . . . 6
⊢ 1 ∈
(1...2) |
| 62 | 61, 4, 2 | jm2.27dlem2 43022 |
. . . . 5
⊢ 1 ∈
(1...3) |
| 63 | | mzpproj 42748 |
. . . . 5
⊢ (((1...3)
∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘1)) ∈
(mzPoly‘(1...3))) |
| 64 | 57, 62, 63 | mp2an 692 |
. . . 4
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ (𝑎‘1)) ∈
(mzPoly‘(1...3)) |
| 65 | | eluzrabdioph 42817 |
. . . 4
⊢ ((3
∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘1)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘3)) |
| 66 | 55, 56, 64, 65 | mp3an 1463 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘3) |
| 67 | | 3nn 12345 |
. . . . . . . . 9
⊢ 3 ∈
ℕ |
| 68 | 67 | jm2.27dlem3 43023 |
. . . . . . . 8
⊢ 3 ∈
(1...3) |
| 69 | | mzpproj 42748 |
. . . . . . . 8
⊢ (((1...3)
∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘3)) ∈
(mzPoly‘(1...3))) |
| 70 | 57, 68, 69 | mp2an 692 |
. . . . . . 7
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ (𝑎‘3)) ∈
(mzPoly‘(1...3)) |
| 71 | | elnnrabdioph 42818 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘3)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈
(Dioph‘3)) |
| 72 | 55, 70, 71 | mp2an 692 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈
(Dioph‘3) |
| 73 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖‘8) ∈
V |
| 74 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖‘9) ∈
V |
| 75 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖‘;10) ∈ V |
| 76 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2)) |
| 77 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2)) |
| 78 | 77 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) |
| 79 | 76, 78 | oveqan12rd 7451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) −
(((𝑒↑2) − 1)
· ((𝑖‘8)↑2)))) |
| 80 | 79 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) −
(((𝑒↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
| 81 | 80 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) −
(((𝑒↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
| 82 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑖‘;10) → (ℎ + 1) = ((𝑖‘;10) + 1)) |
| 83 | 82 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑖‘;10) → ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))) |
| 84 | 83 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = (𝑖‘;10) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
| 85 | 84 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
| 86 | 81, 85 | 3anbi12d 1439 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → ((((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1))))) |
| 87 | 86 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ↔ ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))))) |
| 88 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3))) |
| 89 | 88 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))) |
| 90 | 89 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))) |
| 91 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2))) |
| 92 | 91 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)))) |
| 93 | 92 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) |
| 94 | 90, 93 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 95 | 94 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 96 | 87, 95 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → ((((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))) |
| 97 | 73, 74, 75, 96 | sbc3ie 3868 |
. . . . . . . . . . . . . . 15
⊢
([(𝑖‘8)
/ 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 98 | 97 | sbcbii 3846 |
. . . . . . . . . . . . . 14
⊢
([(𝑖‘7)
/ 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 99 | 98 | sbcbii 3846 |
. . . . . . . . . . . . 13
⊢
([(𝑖‘6)
/ 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 100 | 99 | sbcbii 3846 |
. . . . . . . . . . . 12
⊢
([(𝑖‘5)
/ 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 101 | 100 | sbcbii 3846 |
. . . . . . . . . . 11
⊢
([(𝑖‘4)
/ 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 102 | 101 | sbcbii 3846 |
. . . . . . . . . 10
⊢
([(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ [(𝑖 ↾ (1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 103 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝑖‘5) ∈
V |
| 104 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝑖‘6) ∈
V |
| 105 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝑖‘7) ∈
V |
| 106 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2)) |
| 107 | 106 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2)) |
| 108 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2)) |
| 109 | 108 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2))) |
| 110 | 109 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2))) |
| 111 | 107, 110 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2)))) |
| 112 | 111 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1)) |
| 113 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ≥‘2)
↔ (𝑖‘7) ∈
(ℤ≥‘2))) |
| 114 | 113 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ≥‘2)
↔ (𝑖‘7) ∈
(ℤ≥‘2))) |
| 115 | 112, 114 | 3anbi23d 1441 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
↔ (((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)))) |
| 116 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2)) |
| 117 | 116 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) −
1)) |
| 118 | 117 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) |
| 119 | 118 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) =
(((𝑖‘9)↑2)
− ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) |
| 120 | 119 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
| 121 | 120 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
| 122 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
| 123 | 122 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
| 124 | | simp2 1138 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6)) |
| 125 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1))) |
| 126 | 125 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1))) |
| 127 | 124, 126 | breq12d 5156 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) |
| 128 | 121, 123,
127 | 3anbi123d 1438 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))) |
| 129 | 115, 128 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ↔ ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))))) |
| 130 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1)) |
| 131 | 130 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 ·
(𝑎‘3)) ∥
((𝑖‘7) −
1))) |
| 132 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))) |
| 133 | 131, 132 | bi2anan9r 639 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))) |
| 134 | 133 | anbi1d 631 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 ·
(𝑎‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 135 | 134 | 3adant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 ·
(𝑎‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 136 | 129, 135 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1)
· ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))) |
| 137 | 103, 104,
105, 136 | sbc3ie 3868 |
. . . . . . . . . . . 12
⊢
([(𝑖‘5)
/ 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1)
· ((𝑎‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 138 | 137 | sbcbii 3846 |
. . . . . . . . . . 11
⊢
([(𝑖‘4)
/ 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔
[(𝑖‘4) / 𝑏](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 139 | 138 | sbcbii 3846 |
. . . . . . . . . 10
⊢
([(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
∧ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔
[(𝑖 ↾ (1...3))
/ 𝑎][(𝑖‘4) / 𝑏](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
| 140 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑖 ∈ V |
| 141 | 140 | resex 6047 |
. . . . . . . . . . 11
⊢ (𝑖 ↾ (1...3)) ∈
V |
| 142 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑖‘4) ∈
V |
| 143 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2)) |
| 144 | 62 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1)) |
| 145 | 144 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2)) |
| 146 | 145 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) =
(((𝑖‘1)↑2)
− 1)) |
| 147 | 68 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3)) |
| 148 | 147 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2)) |
| 149 | 146, 148 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1)
· ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) |
| 150 | 143, 149 | oveqan12rd 7451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘3)↑2)))) |
| 151 | 150 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔
(((𝑖‘4)↑2)
− ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) =
1)) |
| 152 | 146 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) |
| 153 | 152 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) |
| 154 | 153 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1)) |
| 155 | 154 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1)) |
| 156 | 151, 155 | 3anbi12d 1439 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ↔ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)))) |
| 157 | 148 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 ·
((𝑖‘3)↑2))) |
| 158 | 157 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) |
| 159 | 158 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))))) |
| 160 | 144 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1))) |
| 161 | 160 | breq2d 5155 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) |
| 162 | 159, 161 | 3anbi23d 1441 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((((𝑖‘9)↑2) −
((((𝑖‘7)↑2)
− 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))) ↔ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))) |
| 164 | 156, 163 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ↔ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))))) |
| 165 | 147 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3))) |
| 166 | 165 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2
· (𝑖‘3))
∥ ((𝑖‘7)
− 1))) |
| 167 | 147 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3))) |
| 168 | 167 | breq2d 5155 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))) |
| 169 | 166, 168 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 ·
(𝑖‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑖‘3))))) |
| 170 | 5 | jm2.27dlem1 43021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2)) |
| 171 | 170 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2))) |
| 172 | 165, 171 | breq12d 5156 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)))) |
| 173 | 170, 147 | breq12d 5156 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3))) |
| 174 | 172, 173 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))) |
| 175 | 169, 174 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((2 ·
(𝑎‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 ·
(𝑖‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))) |
| 176 | 175 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 ·
(𝑖‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))) |
| 177 | 164, 176 | anbi12d 632 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ ((((((𝑖‘4)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))))) |
| 178 | 141, 142,
177 | sbc2ie 3866 |
. . . . . . . . . 10
⊢
([(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
(((𝑖‘6)↑2)
− ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ∧
(𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 ·
(𝑎‘3)) ∥
((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ ((((((𝑖‘4)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))) |
| 179 | 102, 139,
178 | 3bitri 297 |
. . . . . . . . 9
⊢
([(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) ↔ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))) |
| 180 | 179 | rabbii 3442 |
. . . . . . . 8
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ [(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} = {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))} |
| 181 | | 10nn0 12751 |
. . . . . . . . . . . 12
⊢ ;10 ∈
ℕ0 |
| 182 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢
(1...;10) ∈
V |
| 183 | | df-5 12332 |
. . . . . . . . . . . . . . . . 17
⊢ 5 = (4 +
1) |
| 184 | | df-6 12333 |
. . . . . . . . . . . . . . . . . 18
⊢ 6 = (5 +
1) |
| 185 | | df-7 12334 |
. . . . . . . . . . . . . . . . . . 19
⊢ 7 = (6 +
1) |
| 186 | | df-8 12335 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 8 = (7 +
1) |
| 187 | | df-9 12336 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 9 = (8 +
1) |
| 188 | | 9p1e10 12735 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (9 + 1) =
;10 |
| 189 | 188 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ;10 = (9 + 1) |
| 190 | | ssid 4006 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1...;10) ⊆
(1...;10) |
| 191 | 189, 190 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1...9)
⊆ (1...;10) |
| 192 | 187, 191 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...8)
⊆ (1...;10) |
| 193 | 186, 192 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1...7)
⊆ (1...;10) |
| 194 | 185, 193 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . 18
⊢ (1...6)
⊆ (1...;10) |
| 195 | 184, 194 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . 17
⊢ (1...5)
⊆ (1...;10) |
| 196 | 183, 195 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . 16
⊢ (1...4)
⊆ (1...;10) |
| 197 | | 4nn 12349 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℕ |
| 198 | 197 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
(1...4) |
| 199 | 196, 198 | sselii 3980 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
(1...;10) |
| 200 | | mzpproj 42748 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
4 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘4)) ∈
(mzPoly‘(1...;10))) |
| 201 | 182, 199,
200 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘4)) ∈
(mzPoly‘(1...;10)) |
| 202 | | 2nn0 12543 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
| 203 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘4)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘4)↑2)) ∈
(mzPoly‘(1...;10))) |
| 204 | 201, 202,
203 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘4)↑2)) ∈
(mzPoly‘(1...;10)) |
| 205 | | df-4 12331 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 = (3 +
1) |
| 206 | 205, 196 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...3)
⊆ (1...;10) |
| 207 | 4, 206 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1...2)
⊆ (1...;10) |
| 208 | 60, 207 | jm2.27dlem5 43025 |
. . . . . . . . . . . . . . . . . 18
⊢ (1...1)
⊆ (1...;10) |
| 209 | 208, 59 | sselii 3980 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
(1...;10) |
| 210 | | mzpproj 42748 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...;10) ∈ V ∧
1 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘1)) ∈
(mzPoly‘(1...;10))) |
| 211 | 182, 209,
210 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘1)) ∈
(mzPoly‘(1...;10)) |
| 212 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘1)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘1)↑2)) ∈
(mzPoly‘(1...;10))) |
| 213 | 211, 202,
212 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘1)↑2)) ∈
(mzPoly‘(1...;10)) |
| 214 | | 1z 12647 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℤ |
| 215 | | mzpconstmpt 42751 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
1 ∈ ℤ) → (𝑖
∈ (ℤ ↑m (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) |
| 216 | 182, 214,
215 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10)) |
| 217 | | mzpsubmpt 42754 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘1)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ (((𝑖‘1)↑2) − 1))
∈ (mzPoly‘(1...;10))) |
| 218 | 213, 216,
217 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘1)↑2) − 1)) ∈
(mzPoly‘(1...;10)) |
| 219 | 206, 68 | sselii 3980 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
(1...;10) |
| 220 | | mzpproj 42748 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
3 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) |
| 221 | 182, 219,
220 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10)) |
| 222 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10))) |
| 223 | 221, 202,
222 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10)) |
| 224 | | mzpmulmpt 42753 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘1)↑2) − 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) |
| 225 | 218, 223,
224 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10)) |
| 226 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘4)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10))) |
| 227 | 204, 225,
226 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10)) |
| 228 | | eqrabdioph 42788 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1} ∈
(Dioph‘;10)) |
| 229 | 181, 227,
216, 228 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1} ∈
(Dioph‘;10) |
| 230 | | 6nn 12355 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℕ |
| 231 | 230 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
(1...6) |
| 232 | 194, 231 | sselii 3980 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
(1...;10) |
| 233 | | mzpproj 42748 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
6 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘6)) ∈
(mzPoly‘(1...;10))) |
| 234 | 182, 232,
233 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘6)) ∈
(mzPoly‘(1...;10)) |
| 235 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘6)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘6)↑2)) ∈
(mzPoly‘(1...;10))) |
| 236 | 234, 202,
235 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘6)↑2)) ∈
(mzPoly‘(1...;10)) |
| 237 | | 5nn 12352 |
. . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℕ |
| 238 | 237 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
(1...5) |
| 239 | 195, 238 | sselii 3980 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
(1...;10) |
| 240 | | mzpproj 42748 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
5 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘5)) ∈
(mzPoly‘(1...;10))) |
| 241 | 182, 239,
240 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘5)) ∈
(mzPoly‘(1...;10)) |
| 242 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘5)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘5)↑2)) ∈
(mzPoly‘(1...;10))) |
| 243 | 241, 202,
242 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘5)↑2)) ∈
(mzPoly‘(1...;10)) |
| 244 | | mzpmulmpt 42753 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘1)↑2) − 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘5)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈
(mzPoly‘(1...;10))) |
| 245 | 218, 243,
244 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈
(mzPoly‘(1...;10)) |
| 246 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘6)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) ∈
(mzPoly‘(1...;10))) |
| 247 | 236, 245,
246 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) ∈
(mzPoly‘(1...;10)) |
| 248 | | eqrabdioph 42788 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1} ∈
(Dioph‘;10)) |
| 249 | 181, 247,
216, 248 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1} ∈
(Dioph‘;10) |
| 250 | | 7nn 12358 |
. . . . . . . . . . . . . . 15
⊢ 7 ∈
ℕ |
| 251 | 250 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . 14
⊢ 7 ∈
(1...7) |
| 252 | 193, 251 | sselii 3980 |
. . . . . . . . . . . . 13
⊢ 7 ∈
(1...;10) |
| 253 | | mzpproj 42748 |
. . . . . . . . . . . . 13
⊢
(((1...;10) ∈ V ∧
7 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘7)) ∈
(mzPoly‘(1...;10))) |
| 254 | 182, 252,
253 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘7)) ∈
(mzPoly‘(1...;10)) |
| 255 | | eluzrabdioph 42817 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧ 2
∈ ℤ ∧ (𝑖
∈ (ℤ ↑m (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘7) ∈
(ℤ≥‘2)} ∈ (Dioph‘;10)) |
| 256 | 181, 56, 254, 255 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘7) ∈
(ℤ≥‘2)} ∈ (Dioph‘;10) |
| 257 | | 3anrabdioph 42793 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘7) ∈
(ℤ≥‘2)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2))} ∈ (Dioph‘;10)) |
| 258 | 229, 249,
256, 257 | mp3an 1463 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2))} ∈ (Dioph‘;10) |
| 259 | | 9nn 12364 |
. . . . . . . . . . . . . . . . 17
⊢ 9 ∈
ℕ |
| 260 | 259 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . . 16
⊢ 9 ∈
(1...9) |
| 261 | 260, 189,
259 | jm2.27dlem2 43022 |
. . . . . . . . . . . . . . 15
⊢ 9 ∈
(1...;10) |
| 262 | | mzpproj 42748 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
9 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘9)) ∈
(mzPoly‘(1...;10))) |
| 263 | 182, 261,
262 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘9)) ∈
(mzPoly‘(1...;10)) |
| 264 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘9)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘9)↑2)) ∈
(mzPoly‘(1...;10))) |
| 265 | 263, 202,
264 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘9)↑2)) ∈
(mzPoly‘(1...;10)) |
| 266 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘7)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘7)↑2)) ∈
(mzPoly‘(1...;10))) |
| 267 | 254, 202,
266 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘7)↑2)) ∈
(mzPoly‘(1...;10)) |
| 268 | | mzpsubmpt 42754 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘7)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ (((𝑖‘7)↑2) − 1))
∈ (mzPoly‘(1...;10))) |
| 269 | 267, 216,
268 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘7)↑2) − 1)) ∈
(mzPoly‘(1...;10)) |
| 270 | | 8nn 12361 |
. . . . . . . . . . . . . . . . . 18
⊢ 8 ∈
ℕ |
| 271 | 270 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . . . 17
⊢ 8 ∈
(1...8) |
| 272 | 192, 271 | sselii 3980 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
(1...;10) |
| 273 | | mzpproj 42748 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
8 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘8)) ∈
(mzPoly‘(1...;10))) |
| 274 | 182, 272,
273 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘8)) ∈
(mzPoly‘(1...;10)) |
| 275 | | mzpexpmpt 42756 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘8)) ∈
(mzPoly‘(1...;10)) ∧ 2
∈ ℕ0) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘8)↑2)) ∈
(mzPoly‘(1...;10))) |
| 276 | 274, 202,
275 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)↑2)) ∈
(mzPoly‘(1...;10)) |
| 277 | | mzpmulmpt 42753 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘7)↑2) − 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈
(mzPoly‘(1...;10))) |
| 278 | 269, 276,
277 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈
(mzPoly‘(1...;10)) |
| 279 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘9)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2)))) ∈
(mzPoly‘(1...;10))) |
| 280 | 265, 278,
279 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2)))) ∈
(mzPoly‘(1...;10)) |
| 281 | | eqrabdioph 42788 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2)))) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1} ∈
(Dioph‘;10)) |
| 282 | 181, 280,
216, 281 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1} ∈
(Dioph‘;10) |
| 283 | | 10nn 12749 |
. . . . . . . . . . . . . . . 16
⊢ ;10 ∈ ℕ |
| 284 | 283 | jm2.27dlem3 43023 |
. . . . . . . . . . . . . . 15
⊢ ;10 ∈ (1...;10) |
| 285 | | mzpproj 42748 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
;10 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10))) |
| 286 | 182, 284,
285 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)) |
| 287 | | mzpaddmpt 42752 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ 1) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘;10) + 1)) ∈
(mzPoly‘(1...;10))) |
| 288 | 286, 216,
287 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘;10) + 1)) ∈
(mzPoly‘(1...;10)) |
| 289 | | mzpconstmpt 42751 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
2 ∈ ℤ) → (𝑖
∈ (ℤ ↑m (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10))) |
| 290 | 182, 56, 289 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ 2) ∈ (mzPoly‘(1...;10)) |
| 291 | | mzpmulmpt 42753 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) |
| 292 | 290, 223,
291 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10)) |
| 293 | | mzpmulmpt 42753 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘;10) + 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10))) |
| 294 | 288, 292,
293 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10)) |
| 295 | | eqrabdioph 42788 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘5)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑m (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈
(Dioph‘;10)) |
| 296 | 181, 241,
294, 295 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘5) =
(((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈
(Dioph‘;10) |
| 297 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘7)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘1)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘7)
− (𝑖‘1)))
∈ (mzPoly‘(1...;10))) |
| 298 | 254, 211,
297 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘7)
− (𝑖‘1)))
∈ (mzPoly‘(1...;10)) |
| 299 | | dvdsrabdioph 42821 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘6)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘7)
− (𝑖‘1)))
∈ (mzPoly‘(1...;10)))
→ {𝑖 ∈
(ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)) |
| 300 | 181, 234,
298, 299 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘6) ∥
((𝑖‘7) − (𝑖‘1))} ∈
(Dioph‘;10) |
| 301 | | 3anrabdioph 42793 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘5) =
(((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘6) ∥
((𝑖‘7) − (𝑖‘1))} ∈
(Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)) |
| 302 | 282, 296,
300, 301 | mp3an 1463 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10) |
| 303 | | anrabdioph 42791 |
. . . . . . . . . 10
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))} ∈ (Dioph‘;10)) |
| 304 | 258, 302,
303 | mp2an 692 |
. . . . . . . . 9
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))} ∈ (Dioph‘;10) |
| 305 | | mzpmulmpt 42753 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10))) |
| 306 | 290, 221,
305 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) |
| 307 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘7)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘7) − 1)) ∈
(mzPoly‘(1...;10))) |
| 308 | 254, 216,
307 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘7)
− 1)) ∈ (mzPoly‘(1...;10)) |
| 309 | | dvdsrabdioph 42821 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘7) − 1)) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈
(Dioph‘;10)) |
| 310 | 181, 306,
308, 309 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈
(Dioph‘;10) |
| 311 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘8)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)
− (𝑖‘3)))
∈ (mzPoly‘(1...;10))) |
| 312 | 274, 221,
311 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)
− (𝑖‘3)))
∈ (mzPoly‘(1...;10)) |
| 313 | | dvdsrabdioph 42821 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘6)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)
− (𝑖‘3)))
∈ (mzPoly‘(1...;10)))
→ {𝑖 ∈
(ℕ0 ↑m (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)) |
| 314 | 181, 234,
312, 313 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘6) ∥
((𝑖‘8) − (𝑖‘3))} ∈
(Dioph‘;10) |
| 315 | | anrabdioph 42791 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘6) ∥
((𝑖‘8) − (𝑖‘3))} ∈
(Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈
(Dioph‘;10)) |
| 316 | 310, 314,
315 | mp2an 692 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈
(Dioph‘;10) |
| 317 | 207, 3 | sselii 3980 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(1...;10) |
| 318 | | mzpproj 42748 |
. . . . . . . . . . . . . 14
⊢
(((1...;10) ∈ V ∧
2 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘2)) ∈
(mzPoly‘(1...;10))) |
| 319 | 182, 317,
318 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘2)) ∈
(mzPoly‘(1...;10)) |
| 320 | | mzpsubmpt 42754 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘8)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)
− (𝑖‘2)))
∈ (mzPoly‘(1...;10))) |
| 321 | 274, 319,
320 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑m (1...;10))
↦ ((𝑖‘8)
− (𝑖‘2)))
∈ (mzPoly‘(1...;10)) |
| 322 | | dvdsrabdioph 42821 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑m
(1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑m (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10)) |
| 323 | 181, 306,
321, 322 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10) |
| 324 | | lerabdioph 42816 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑m (1...;10))
↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑m (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)) |
| 325 | 181, 319,
221, 324 | mp3an 1463 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘2) ≤
(𝑖‘3)} ∈
(Dioph‘;10) |
| 326 | | anrabdioph 42791 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (𝑖‘2) ≤
(𝑖‘3)} ∈
(Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)) |
| 327 | 323, 325,
326 | mp2an 692 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10) |
| 328 | | anrabdioph 42791 |
. . . . . . . . . 10
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈
(Dioph‘;10)) |
| 329 | 316, 327,
328 | mp2an 692 |
. . . . . . . . 9
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈
(Dioph‘;10) |
| 330 | | anrabdioph 42791 |
. . . . . . . . 9
⊢ (({𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈
(Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))} ∈
(Dioph‘;10)) |
| 331 | 304, 329,
330 | mp2an 692 |
. . . . . . . 8
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ ((((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2)) ∧ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) ∧ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))} ∈
(Dioph‘;10) |
| 332 | 180, 331 | eqeltri 2837 |
. . . . . . 7
⊢ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ [(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘;10) |
| 333 | 205, 183,
184, 185, 186, 187, 189 | 7rexfrabdioph 42811 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ {𝑖 ∈ (ℕ0
↑m (1...;10))
∣ [(𝑖 ↾
(1...3)) / 𝑎][(𝑖‘4) / 𝑏][(𝑖‘5) / 𝑐][(𝑖‘6) / 𝑑][(𝑖‘7) / 𝑒][(𝑖‘8) / 𝑓][(𝑖‘9) / 𝑔][(𝑖‘;10) / ℎ](((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘;10)) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
∃𝑑 ∈
ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0
∃𝑔 ∈
ℕ0 ∃ℎ
∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈
(Dioph‘3)) |
| 334 | 55, 332, 333 | mp2an 692 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0 ∃𝑐 ∈ ℕ0
∃𝑑 ∈
ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0
∃𝑔 ∈
ℕ0 ∃ℎ
∈ ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈
(Dioph‘3) |
| 335 | | anrabdioph 42791 |
. . . . . 6
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈
(Dioph‘3) ∧ {𝑎
∈ (ℕ0 ↑m (1...3)) ∣ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))} ∈
(Dioph‘3)) |
| 336 | 72, 334, 335 | mp2an 692 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))} ∈
(Dioph‘3) |
| 337 | | mzpproj 42748 |
. . . . . . 7
⊢ (((1...3)
∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) |
| 338 | 57, 5, 337 | mp2an 692 |
. . . . . 6
⊢ (𝑎 ∈ (ℤ
↑m (1...3)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...3)) |
| 339 | | elnnrabdioph 42818 |
. . . . . 6
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3)) |
| 340 | 55, 338, 339 | mp2an 692 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3) |
| 341 | | anrabdioph 42791 |
. . . . 5
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3)) → {𝑎
∈ (ℕ0 ↑m (1...3)) ∣ (((𝑎‘3) ∈ ℕ ∧
∃𝑏 ∈
ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0
∃𝑒 ∈
ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0
∃ℎ ∈
ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)} ∈
(Dioph‘3)) |
| 342 | 336, 340,
341 | mp2an 692 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)} ∈
(Dioph‘3) |
| 343 | | eq0rabdioph 42787 |
. . . . . 6
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘3)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 0} ∈
(Dioph‘3)) |
| 344 | 55, 70, 343 | mp2an 692 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 0} ∈
(Dioph‘3) |
| 345 | | eq0rabdioph 42787 |
. . . . . 6
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑m (1...3))
↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3)) |
| 346 | 55, 338, 345 | mp2an 692 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3) |
| 347 | | anrabdioph 42791 |
. . . . 5
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)) →
{𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈
(Dioph‘3)) |
| 348 | 344, 346,
347 | mp2an 692 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈
(Dioph‘3) |
| 349 | | orrabdioph 42792 |
. . . 4
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ)} ∈
(Dioph‘3) ∧ {𝑎
∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈
(Dioph‘3)) → {𝑎
∈ (ℕ0 ↑m (1...3)) ∣ ((((𝑎‘3) ∈ ℕ ∧
∃𝑏 ∈
ℕ0 ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℕ0
∃𝑒 ∈
ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0
∃ℎ ∈
ℕ0 (((((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ∧
((𝑑↑2) −
((((𝑎‘1)↑2)
− 1) · (𝑐↑2))) = 1 ∧ 𝑒 ∈ (ℤ≥‘2))
∧ (((𝑔↑2) −
(((𝑒↑2) − 1)
· (𝑓↑2))) = 1
∧ 𝑐 = ((ℎ + 1) · (2 ·
((𝑎‘3)↑2)))
∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))} ∈
(Dioph‘3)) |
| 350 | 342, 348,
349 | mp2an 692 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))} ∈
(Dioph‘3) |
| 351 | | anrabdioph 42791 |
. . 3
⊢ (({𝑎 ∈ (ℕ0
↑m (1...3)) ∣ (𝑎‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))} ∈
(Dioph‘3)) → {𝑎
∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))} ∈
(Dioph‘3)) |
| 352 | 66, 350, 351 | mp2an 692 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ ((((𝑎‘3) ∈ ℕ ∧ ∃𝑏 ∈ ℕ0
∃𝑐 ∈
ℕ0 ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0
∃𝑓 ∈
ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0
(((((𝑏↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑎‘3)↑2))) = 1 ∧ ((𝑑↑2) − ((((𝑎‘1)↑2) − 1)
· (𝑐↑2))) = 1
∧ 𝑒 ∈
(ℤ≥‘2)) ∧ (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ∧ 𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ∧ 𝑑 ∥ (𝑒 − (𝑎‘1)))) ∧ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))} ∈
(Dioph‘3) |
| 353 | 54, 352 | eqeltri 2837 |
1
⊢ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈
(Dioph‘3) |