Step | Hyp | Ref
| Expression |
1 | | elmapi 7765 |
. . . . . . 7
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0) |
2 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
3 | 2 | jm2.27dlem3 36596 |
. . . . . . . 8
⊢ 2 ∈
(1...2) |
4 | | df-3 10957 |
. . . . . . . 8
⊢ 3 = (2 +
1) |
5 | 3, 4, 2 | jm2.27dlem2 36595 |
. . . . . . 7
⊢ 2 ∈
(1...3) |
6 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝑎:(1...3)⟶ℕ0 ∧ 2
∈ (1...3)) → (𝑎‘2) ∈
ℕ0) |
7 | 1, 5, 6 | sylancl 693 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → (𝑎‘2) ∈
ℕ0) |
8 | | elnn0 11171 |
. . . . . 6
⊢ ((𝑎‘2) ∈
ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) |
9 | 7, 8 | sylib 207 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) |
10 | | iba 523 |
. . . . . . 7
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) =
0)))) |
11 | | andi 907 |
. . . . . . 7
⊢ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))) |
12 | 10, 11 | syl6bb 275 |
. . . . . 6
⊢ (((𝑎‘2) ∈ ℕ ∨
(𝑎‘2) = 0) →
((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))) |
13 | 12 | anbi2d 736 |
. . . . 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
↑𝑚 (1...3)) → (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))) |
15 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈
(ℤ≥‘2)) |
16 | | nnz 11276 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘2) ∈ ℕ →
(𝑎‘2) ∈
ℤ) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈
ℤ) |
18 | | frmy 36497 |
. . . . . . . . . . . . . 14
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
19 | 18 | fovcl 6663 |
. . . . . . . . . . . . 13
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℤ) |
20 | 15, 17, 19 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℤ) |
21 | | rmy0 36512 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘1) ∈
(ℤ≥‘2) → ((𝑎‘1) Yrm 0) =
0) |
22 | 21 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) =
0) |
23 | | nngt0 10926 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎‘2) ∈ ℕ →
0 < (𝑎‘2)) |
24 | 23 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 <
(𝑎‘2)) |
25 | | 0zd 11266 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈
ℤ) |
26 | | ltrmy 36537 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎‘1) ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) →
(0 < (𝑎‘2) ↔
((𝑎‘1) Yrm
0) < ((𝑎‘1)
Yrm (𝑎‘2)))) |
27 | 15, 25, 17, 26 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 <
(𝑎‘2) ↔ ((𝑎‘1) Yrm 0) <
((𝑎‘1) Yrm
(𝑎‘2)))) |
28 | 24, 27 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) <
((𝑎‘1) Yrm
(𝑎‘2))) |
29 | 22, 28 | eqbrtrrd 4607 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 <
((𝑎‘1) Yrm
(𝑎‘2))) |
30 | | elnnz 11264 |
. . . . . . . . . . . 12
⊢ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔
(((𝑎‘1)
Yrm (𝑎‘2))
∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2)))) |
31 | 20, 29, 30 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℕ) |
32 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈
ℕ)) |
33 | 31, 32 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ)) |
34 | 33 | pm4.71rd 665 |
. . . . . . . . 9
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))))) |
35 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
(𝑎‘1) ∈
(ℤ≥‘2)) |
36 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
(𝑎‘2) ∈
ℕ) |
37 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) →
(𝑎‘3) ∈
ℕ) |
38 | | jm2.27 36593 |
. . . . . . . . . . 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 1318 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ (ℕ0
↑𝑚 (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 671 |
. . . . . . . . 9
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (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 267 |
. . . . . . . 8
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (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 449 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (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 670 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (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 6557 |
. . . . . . . . . . 11
⊢ ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm
0)) |
45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0)) |
46 | 21 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) =
0) |
47 | 45, 46 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0) |
48 | 47 | eqeq2d 2620 |
. . . . . . . 8
⊢ (((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)) |
49 | 48 | ex 449 |
. . . . . . 7
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))) |
50 | 49 | pm5.32rd 670 |
. . . . . 6
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∧ (𝑎‘1) ∈
(ℤ≥‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0))) |
51 | 43, 50 | orbi12d 742 |
. . . . 5
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (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 671 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (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 267 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (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 3161 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} = {𝑎 ∈ (ℕ0
↑𝑚 (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 11187 |
. . . 4
⊢ 3 ∈
ℕ0 |
56 | | 2z 11286 |
. . . 4
⊢ 2 ∈
ℤ |
57 | | ovex 6577 |
. . . . 5
⊢ (1...3)
∈ V |
58 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
59 | 58 | jm2.27dlem3 36596 |
. . . . . . 7
⊢ 1 ∈
(1...1) |
60 | | df-2 10956 |
. . . . . . 7
⊢ 2 = (1 +
1) |
61 | 59, 60, 58 | jm2.27dlem2 36595 |
. . . . . 6
⊢ 1 ∈
(1...2) |
62 | 61, 4, 2 | jm2.27dlem2 36595 |
. . . . 5
⊢ 1 ∈
(1...3) |
63 | | mzpproj 36318 |
. . . . 5
⊢ (((1...3)
∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘1)) ∈
(mzPoly‘(1...3))) |
64 | 57, 62, 63 | mp2an 704 |
. . . 4
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈
(mzPoly‘(1...3)) |
65 | | eluzrabdioph 36388 |
. . . 4
⊢ ((3
∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘3)) |
66 | 55, 56, 64, 65 | mp3an 1416 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘3) |
67 | | 3nn 11063 |
. . . . . . . . 9
⊢ 3 ∈
ℕ |
68 | 67 | jm2.27dlem3 36596 |
. . . . . . . 8
⊢ 3 ∈
(1...3) |
69 | | mzpproj 36318 |
. . . . . . . 8
⊢ (((1...3)
∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘3)) ∈
(mzPoly‘(1...3))) |
70 | 57, 68, 69 | mp2an 704 |
. . . . . . 7
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈
(mzPoly‘(1...3)) |
71 | | elnnrabdioph 36389 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈
(Dioph‘3)) |
72 | 55, 70, 71 | mp2an 704 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈
(Dioph‘3) |
73 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖‘8) ∈
V |
74 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖‘9) ∈
V |
75 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖‘;10) ∈ V |
76 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2)) |
77 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2)) |
78 | 77 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) |
79 | 76, 78 | oveqan12rd 6569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) −
(((𝑒↑2) − 1)
· ((𝑖‘8)↑2)))) |
80 | 79 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) −
(((𝑒↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
81 | 80 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) −
(((𝑒↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
82 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = (𝑖‘;10) → (ℎ + 1) = ((𝑖‘;10) + 1)) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑖‘;10) → ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2)))) |
84 | 83 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑖‘;10) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
85 | 84 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ ℎ = (𝑖‘;10)) → (𝑐 = ((ℎ + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
86 | 81, 85 | 3anbi12d 1392 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = (𝑖‘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 736 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = (𝑖‘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 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3))) |
89 | 88 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))) |
90 | 89 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))) |
91 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2))) |
92 | 91 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)))) |
93 | 92 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))) |
94 | 90, 93 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))) |
95 | 94 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = (𝑖‘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 743 |
. . . . . . . . . . . . . . . . 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 · (𝑎‘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 3474 |
. . . . . . . . . . . . . . . 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))))) |
98 | 97 | sbcbii 3458 |
. . . . . . . . . . . . . . 15
⊢
([(𝑖‘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 3458 |
. . . . . . . . . . . . . 14
⊢
([(𝑖‘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 3458 |
. . . . . . . . . . . . 13
⊢
([(𝑖‘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 3458 |
. . . . . . . . . . . 12
⊢
([(𝑖‘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 3458 |
. . . . . . . . . . 11
⊢
([(𝑖 ↾
(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 6113 |
. . . . . . . . . . . . . 14
⊢ (𝑖‘5) ∈
V |
104 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝑖‘6) ∈
V |
105 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝑖‘7) ∈
V |
106 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2)) |
107 | 106 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2)) |
108 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2)) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2))) |
110 | 109 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2))) |
111 | 107, 110 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2)))) |
112 | 111 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1)) |
113 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ≥‘2)
↔ (𝑖‘7) ∈
(ℤ≥‘2))) |
114 | 113 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ≥‘2)
↔ (𝑖‘7) ∈
(ℤ≥‘2))) |
115 | 112, 114 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘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 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2)) |
117 | 116 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) −
1)) |
118 | 117 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) |
119 | 118 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) =
(((𝑖‘9)↑2)
− ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) |
120 | 119 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
121 | 120 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) ·
((𝑖‘8)↑2))) = 1
↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1)) |
122 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
123 | 122 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))))) |
124 | | simp2 1055 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6)) |
125 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1))) |
126 | 125 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1))) |
127 | 124, 126 | breq12d 4596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)))) |
128 | 121, 123,
127 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = (𝑖‘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 743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑖‘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 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1)) |
131 | 130 | breq2d 4595 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 ·
(𝑎‘3)) ∥
((𝑖‘7) −
1))) |
132 | | breq1 4586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))) |
133 | 131, 132 | bi2anan9r 914 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))) |
134 | 133 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑑 = (𝑖‘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 1072 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = (𝑖‘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 743 |
. . . . . . . . . . . . . 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 · (𝑎‘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 3474 |
. . . . . . . . . . . . 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))))) |
138 | 137 | sbcbii 3458 |
. . . . . . . . . . . 12
⊢
([(𝑖‘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 3458 |
. . . . . . . . . . 11
⊢
([(𝑖 ↾
(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 3176 |
. . . . . . . . . . . . 13
⊢ 𝑖 ∈ V |
141 | 140 | resex 5363 |
. . . . . . . . . . . 12
⊢ (𝑖 ↾ (1...3)) ∈
V |
142 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑖‘4) ∈
V |
143 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2)) |
144 | 62 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1)) |
145 | 144 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2)) |
146 | 145 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) =
(((𝑖‘1)↑2)
− 1)) |
147 | 68 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3)) |
148 | 147 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2)) |
149 | 146, 148 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1)
· ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) |
150 | 143, 149 | oveqan12rd 6569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘3)↑2)))) |
151 | 150 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔
(((𝑖‘4)↑2)
− ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) =
1)) |
152 | 146 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) |
153 | 152 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) |
154 | 153 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) −
((((𝑎‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1)) |
155 | 154 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1)) |
156 | 151, 155 | 3anbi12d 1392 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑖 ↾ (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 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 ·
((𝑖‘3)↑2))) |
158 | 157 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) |
159 | 158 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))))) |
160 | 144 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1))) |
161 | 160 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))) |
162 | 159, 161 | 3anbi23d 1394 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (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 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = (𝑖 ↾ (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 743 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑖 ↾ (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 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3))) |
166 | 165 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2
· (𝑖‘3))
∥ ((𝑖‘7)
− 1))) |
167 | 147 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3))) |
168 | 167 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))) |
169 | 166, 168 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧
(𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 ·
(𝑖‘3)) ∥
((𝑖‘7) − 1)
∧ (𝑖‘6) ∥
((𝑖‘8) − (𝑖‘3))))) |
170 | 5 | jm2.27dlem1 36594 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2)) |
171 | 170 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2))) |
172 | 165, 171 | breq12d 4596 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)))) |
173 | 170, 147 | breq12d 4596 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3))) |
174 | 172, 173 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))) |
175 | 169, 174 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑖 ↾ (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 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑖 ↾ (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 743 |
. . . . . . . . . . . 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)))) ∧ (((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 3472 |
. . . . . . . . . . 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))))) |
179 | 102, 139,
178 | 3bitri 285 |
. . . . . . . . . 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)))) ↔ ((((((𝑖‘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 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 ∈ (ℕ0
↑𝑚 (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)))) ↔ ((((((𝑖‘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 | 180 | rabbiia 3161 |
. . . . . . . 8
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (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
↑𝑚 (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))))} |
182 | | 10nn0 11392 |
. . . . . . . . . . . 12
⊢ ;10 ∈
ℕ0 |
183 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(1...;10) ∈
V |
184 | | df-5 10959 |
. . . . . . . . . . . . . . . . 17
⊢ 5 = (4 +
1) |
185 | | df-6 10960 |
. . . . . . . . . . . . . . . . . 18
⊢ 6 = (5 +
1) |
186 | | df-7 10961 |
. . . . . . . . . . . . . . . . . . 19
⊢ 7 = (6 +
1) |
187 | | df-8 10962 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 8 = (7 +
1) |
188 | | df-9 10963 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 9 = (8 +
1) |
189 | | 9p1e10 11372 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (9 + 1) =
;10 |
190 | 189 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ;10 = (9 + 1) |
191 | | ssid 3587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1...;10) ⊆
(1...;10) |
192 | 190, 191 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1...9)
⊆ (1...;10) |
193 | 188, 192 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...8)
⊆ (1...;10) |
194 | 187, 193 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1...7)
⊆ (1...;10) |
195 | 186, 194 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . 18
⊢ (1...6)
⊆ (1...;10) |
196 | 185, 195 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . 17
⊢ (1...5)
⊆ (1...;10) |
197 | 184, 196 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . 16
⊢ (1...4)
⊆ (1...;10) |
198 | | 4nn 11064 |
. . . . . . . . . . . . . . . . 17
⊢ 4 ∈
ℕ |
199 | 198 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
(1...4) |
200 | 197, 199 | sselii 3565 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
(1...;10) |
201 | | mzpproj 36318 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
4 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10))) |
202 | 183, 200,
201 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)) |
203 | | 2nn0 11186 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
204 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘4)↑2)) ∈
(mzPoly‘(1...;10))) |
205 | 202, 203,
204 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘4)↑2)) ∈
(mzPoly‘(1...;10)) |
206 | | df-4 10958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 4 = (3 +
1) |
207 | 206, 197 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...3)
⊆ (1...;10) |
208 | 4, 207 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1...2)
⊆ (1...;10) |
209 | 60, 208 | jm2.27dlem5 36598 |
. . . . . . . . . . . . . . . . . 18
⊢ (1...1)
⊆ (1...;10) |
210 | 209, 59 | sselii 3565 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
(1...;10) |
211 | | mzpproj 36318 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...;10) ∈ V ∧
1 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10))) |
212 | 183, 210,
211 | mp2an 704 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)) |
213 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘1)↑2)) ∈
(mzPoly‘(1...;10))) |
214 | 212, 203,
213 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘1)↑2)) ∈
(mzPoly‘(1...;10)) |
215 | | 1z 11284 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℤ |
216 | | mzpconstmpt 36321 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
1 ∈ ℤ) → (𝑖
∈ (ℤ ↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) |
217 | 183, 215,
216 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10)) |
218 | | mzpsubmpt 36324 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘1)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (((𝑖‘1)↑2) − 1))
∈ (mzPoly‘(1...;10))) |
219 | 214, 217,
218 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈
(mzPoly‘(1...;10)) |
220 | 207, 68 | sselii 3565 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
(1...;10) |
221 | | mzpproj 36318 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
3 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10))) |
222 | 183, 220,
221 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)) |
223 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10))) |
224 | 222, 203,
223 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10)) |
225 | | mzpmulmpt 36323 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) |
226 | 219, 224,
225 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10)) |
227 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘4)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10))) |
228 | 205, 226,
227 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10)) |
229 | | eqrabdioph 36359 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1} ∈
(Dioph‘;10)) |
230 | 182, 228,
217, 229 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1} ∈
(Dioph‘;10) |
231 | | 6nn 11066 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℕ |
232 | 231 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
(1...6) |
233 | 195, 232 | sselii 3565 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
(1...;10) |
234 | | mzpproj 36318 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
6 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10))) |
235 | 183, 233,
234 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) |
236 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘6)↑2)) ∈
(mzPoly‘(1...;10))) |
237 | 235, 203,
236 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘6)↑2)) ∈
(mzPoly‘(1...;10)) |
238 | | 5nn 11065 |
. . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℕ |
239 | 238 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
(1...5) |
240 | 196, 239 | sselii 3565 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
(1...;10) |
241 | | mzpproj 36318 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
5 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10))) |
242 | 183, 240,
241 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) |
243 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘5)↑2)) ∈
(mzPoly‘(1...;10))) |
244 | 242, 203,
243 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘5)↑2)) ∈
(mzPoly‘(1...;10)) |
245 | | mzpmulmpt 36323 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘1)↑2) − 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘5)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈
(mzPoly‘(1...;10))) |
246 | 219, 244,
245 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈
(mzPoly‘(1...;10)) |
247 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘6)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) ∈
(mzPoly‘(1...;10))) |
248 | 237, 246,
247 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) ∈
(mzPoly‘(1...;10)) |
249 | | eqrabdioph 36359 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2)))) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1} ∈
(Dioph‘;10)) |
250 | 182, 248,
217, 249 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1} ∈
(Dioph‘;10) |
251 | | 7nn 11067 |
. . . . . . . . . . . . . . 15
⊢ 7 ∈
ℕ |
252 | 251 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . 14
⊢ 7 ∈
(1...7) |
253 | 194, 252 | sselii 3565 |
. . . . . . . . . . . . 13
⊢ 7 ∈
(1...;10) |
254 | | mzpproj 36318 |
. . . . . . . . . . . . 13
⊢
(((1...;10) ∈ V ∧
7 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))) |
255 | 183, 253,
254 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) |
256 | | eluzrabdioph 36388 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧ 2
∈ ℤ ∧ (𝑖
∈ (ℤ ↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘7) ∈
(ℤ≥‘2)} ∈ (Dioph‘;10)) |
257 | 182, 56, 255, 256 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘7) ∈
(ℤ≥‘2)} ∈ (Dioph‘;10) |
258 | | 3anrabdioph 36364 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘5)↑2))) = 1} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘7) ∈
(ℤ≥‘2)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2))} ∈ (Dioph‘;10)) |
259 | 230, 250,
257, 258 | mp3an 1416 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2))} ∈ (Dioph‘;10) |
260 | | 9nn 11069 |
. . . . . . . . . . . . . . . . 17
⊢ 9 ∈
ℕ |
261 | 260 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . . 16
⊢ 9 ∈
(1...9) |
262 | 261, 190,
260 | jm2.27dlem2 36595 |
. . . . . . . . . . . . . . 15
⊢ 9 ∈
(1...;10) |
263 | | mzpproj 36318 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
9 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10))) |
264 | 183, 262,
263 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)) |
265 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘9)↑2)) ∈
(mzPoly‘(1...;10))) |
266 | 264, 203,
265 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘9)↑2)) ∈
(mzPoly‘(1...;10)) |
267 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘7)↑2)) ∈
(mzPoly‘(1...;10))) |
268 | 255, 203,
267 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘7)↑2)) ∈
(mzPoly‘(1...;10)) |
269 | | mzpsubmpt 36324 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘7)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (((𝑖‘7)↑2) − 1))
∈ (mzPoly‘(1...;10))) |
270 | 268, 217,
269 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈
(mzPoly‘(1...;10)) |
271 | | 8nn 11068 |
. . . . . . . . . . . . . . . . . 18
⊢ 8 ∈
ℕ |
272 | 271 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . . . 17
⊢ 8 ∈
(1...8) |
273 | 193, 272 | sselii 3565 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
(1...;10) |
274 | | mzpproj 36318 |
. . . . . . . . . . . . . . . 16
⊢
(((1...;10) ∈ V ∧
8 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10))) |
275 | 183, 273,
274 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) |
276 | | mzpexpmpt 36326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ 2 ∈
ℕ0) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘8)↑2)) ∈
(mzPoly‘(1...;10))) |
277 | 275, 203,
276 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘8)↑2)) ∈
(mzPoly‘(1...;10)) |
278 | | mzpmulmpt 36323 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘7)↑2) − 1)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘8)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈
(mzPoly‘(1...;10))) |
279 | 270, 277,
278 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈
(mzPoly‘(1...;10)) |
280 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘9)↑2)) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2)))) ∈
(mzPoly‘(1...;10))) |
281 | 266, 279,
280 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2)))) ∈
(mzPoly‘(1...;10)) |
282 | | eqrabdioph 36359 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2)))) ∈
(mzPoly‘(1...;10)) ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 1) ∈ (mzPoly‘(1...;10))) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1} ∈
(Dioph‘;10)) |
283 | 182, 281,
217, 282 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1} ∈
(Dioph‘;10) |
284 | | 10nn 11390 |
. . . . . . . . . . . . . . . 16
⊢ ;10 ∈ ℕ |
285 | 284 | jm2.27dlem3 36596 |
. . . . . . . . . . . . . . 15
⊢ ;10 ∈ (1...;10) |
286 | | mzpproj 36318 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
;10 ∈ (1...;10)) → (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10))) |
287 | 183, 285,
286 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)) |
288 | | mzpaddmpt 36322 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘;10)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ 1) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10))) |
289 | 287, 217,
288 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10)) |
290 | | mzpconstmpt 36321 |
. . . . . . . . . . . . . . 15
⊢
(((1...;10) ∈ V ∧
2 ∈ ℤ) → (𝑖
∈ (ℤ ↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10))) |
291 | 183, 56, 290 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) |
292 | | mzpmulmpt 36323 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘3)↑2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10))) |
293 | 291, 224,
292 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (2 · ((𝑖‘3)↑2))) ∈
(mzPoly‘(1...;10)) |
294 | | mzpmulmpt 36323 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘;10) + 1)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (2 ·
((𝑖‘3)↑2)))
∈ (mzPoly‘(1...;10)))
→ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10))) |
295 | 289, 293,
294 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10)) |
296 | | eqrabdioph 36359 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈
(Dioph‘;10)) |
297 | 182, 242,
295, 296 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈
(Dioph‘;10) |
298 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (𝑖‘1)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10))) |
299 | 255, 212,
298 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...;10)) |
300 | | dvdsrabdioph 36392 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)) |
301 | 182, 235,
299, 300 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10) |
302 | | 3anrabdioph 36364 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)) |
303 | 283, 297,
301, 302 | mp3an 1416 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10) |
304 | | anrabdioph 36362 |
. . . . . . . . . 10
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1)
· ((𝑖‘3)↑2))) = 1 ∧ (((𝑖‘6)↑2) −
((((𝑖‘1)↑2)
− 1) · ((𝑖‘5)↑2))) = 1 ∧ (𝑖‘7) ∈
(ℤ≥‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1)
· ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖‘;10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (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 | 259, 303,
304 | mp2an 704 |
. . . . . . . . 9
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (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) |
306 | | mzpmulmpt 36323 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ 2) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10))) |
307 | 291, 222,
306 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) |
308 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ 1) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘7) − 1)) ∈
(mzPoly‘(1...;10))) |
309 | 255, 217,
308 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘7) − 1)) ∈
(mzPoly‘(1...;10)) |
310 | | dvdsrabdioph 36392 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘7) − 1)) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈
(Dioph‘;10)) |
311 | 182, 307,
309, 310 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈
(Dioph‘;10) |
312 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10))) |
313 | 275, 222,
312 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...;10)) |
314 | | dvdsrabdioph 36392 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)) |
315 | 182, 235,
313, 314 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10) |
316 | | anrabdioph 36362 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈
(Dioph‘;10)) |
317 | 311, 315,
316 | mp2an 704 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈
(Dioph‘;10) |
318 | 208, 3 | sselii 3565 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(1...;10) |
319 | | mzpproj 36318 |
. . . . . . . . . . . . . 14
⊢
(((1...;10) ∈ V ∧
2 ∈ (1...;10)) → (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10))) |
320 | 183, 318,
319 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)) |
321 | | mzpsubmpt 36324 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (𝑖‘2)) ∈
(mzPoly‘(1...;10))) →
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10))) |
322 | 275, 320,
321 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...;10)) |
323 | | dvdsrabdioph 36392 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10)) |
324 | 182, 307,
322, 323 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10) |
325 | | lerabdioph 36387 |
. . . . . . . . . . . 12
⊢ ((;10 ∈ ℕ0 ∧
(𝑖 ∈ (ℤ
↑𝑚 (1...;10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...;10)) ∧ (𝑖 ∈ (ℤ ↑𝑚
(1...;10)) ↦ (𝑖‘3)) ∈
(mzPoly‘(1...;10))) →
{𝑖 ∈
(ℕ0 ↑𝑚 (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)) |
326 | 182, 320,
222, 325 | mp3an 1416 |
. . . . . . . . . . 11
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10) |
327 | | anrabdioph 36362 |
. . . . . . . . . . 11
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)) |
328 | 324, 326,
327 | mp2an 704 |
. . . . . . . . . 10
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10) |
329 | | anrabdioph 36362 |
. . . . . . . . . 10
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈
(Dioph‘;10) ∧ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈
(Dioph‘;10)) |
330 | 317, 328,
329 | mp2an 704 |
. . . . . . . . 9
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈
(Dioph‘;10) |
331 | | anrabdioph 36362 |
. . . . . . . . 9
⊢ (({𝑖 ∈ (ℕ0
↑𝑚 (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
↑𝑚 (1...;10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 ·
(𝑖‘3)) ∥
((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈
(Dioph‘;10)) → {𝑖 ∈ (ℕ0
↑𝑚 (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 | 305, 330,
331 | mp2an 704 |
. . . . . . . 8
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (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) |
333 | 181, 332 | eqeltri 2684 |
. . . . . . 7
⊢ {𝑖 ∈ (ℕ0
↑𝑚 (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) |
334 | 206, 184,
185, 186, 187, 188, 190 | 7rexfrabdioph 36382 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ {𝑖 ∈ (ℕ0
↑𝑚 (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
↑𝑚 (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 | 55, 333, 334 | mp2an 704 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (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) |
336 | | anrabdioph 36362 |
. . . . . 6
⊢ (({𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈
(Dioph‘3) ∧ {𝑎
∈ (ℕ0 ↑𝑚 (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 ↑𝑚 (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 | 72, 335, 336 | mp2an 704 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (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) |
338 | | mzpproj 36318 |
. . . . . . 7
⊢ (((1...3)
∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...3))) |
339 | 57, 5, 338 | mp2an 704 |
. . . . . 6
⊢ (𝑎 ∈ (ℤ
↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈
(mzPoly‘(1...3)) |
340 | | elnnrabdioph 36389 |
. . . . . 6
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3)) |
341 | 55, 339, 340 | mp2an 704 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3) |
342 | | anrabdioph 36362 |
. . . . 5
⊢ (({𝑎 ∈ (ℕ0
↑𝑚 (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 ↑𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈
(Dioph‘3)) → {𝑎
∈ (ℕ0 ↑𝑚 (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 | 337, 341,
342 | mp2an 704 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (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) |
344 | | eq0rabdioph 36358 |
. . . . . 6
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈
(Dioph‘3)) |
345 | 55, 70, 344 | mp2an 704 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈
(Dioph‘3) |
346 | | eq0rabdioph 36358 |
. . . . . 6
⊢ ((3
∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚
(1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3)) |
347 | 55, 339, 346 | mp2an 704 |
. . . . 5
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3) |
348 | | anrabdioph 36362 |
. . . . 5
⊢ (({𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3) ∧
{𝑎 ∈
(ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈
(Dioph‘3)) → {𝑎
∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈
(Dioph‘3)) |
349 | 345, 347,
348 | mp2an 704 |
. . . 4
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈
(Dioph‘3) |
350 | | orrabdioph 36363 |
. . . 4
⊢ (({𝑎 ∈ (ℕ0
↑𝑚 (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 ↑𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈
(Dioph‘3)) → {𝑎
∈ (ℕ0 ↑𝑚 (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 | 343, 349,
350 | mp2an 704 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (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) |
352 | | anrabdioph 36362 |
. . 3
⊢ (({𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ (𝑎‘1) ∈
(ℤ≥‘2)} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0
↑𝑚 (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 ↑𝑚 (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 | 66, 351, 352 | mp2an 704 |
. 2
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (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) |
354 | 54, 353 | eqeltri 2684 |
1
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈
(ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈
(Dioph‘3) |