Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rmydioph Structured version   Visualization version   GIF version

Theorem rmydioph 39096
Description: jm2.27 39090 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
Assertion
Ref Expression
rmydioph {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)

Proof of Theorem rmydioph
Dummy variables 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmapi 8278 . . . . . . 7 (𝑎 ∈ (ℕ0𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0)
2 2nn 11558 . . . . . . . . 9 2 ∈ ℕ
32jm2.27dlem3 39093 . . . . . . . 8 2 ∈ (1...2)
4 df-3 11549 . . . . . . . 8 3 = (2 + 1)
53, 4, 2jm2.27dlem2 39092 . . . . . . 7 2 ∈ (1...3)
6 ffvelrn 6714 . . . . . . 7 ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
71, 5, 6sylancl 586 . . . . . 6 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (𝑎‘2) ∈ ℕ0)
8 elnn0 11747 . . . . . 6 ((𝑎‘2) ∈ ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
97, 8sylib 219 . . . . 5 (𝑎 ∈ (ℕ0𝑚 (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
10 iba 528 . . . . . . 7 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))))
11 andi 1002 . . . . . . 7 (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))
1210, 11syl6bb 288 . . . . . 6 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))
1312anbi2d 628 . . . . 5 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2))) ↔ ((𝑎‘1) ∈ (ℤ‘2) ∧ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))))
149, 13syl 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 765 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈ (ℤ‘2))
16 nnz 11853 . . . . . . . . . . . . . 14 ((𝑎‘2) ∈ ℕ → (𝑎‘2) ∈ ℤ)
1716adantl 482 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈ ℤ)
18 frmy 38996 . . . . . . . . . . . . . 14 Yrm :((ℤ‘2) × ℤ)⟶ℤ
1918fovcl 7135 . . . . . . . . . . . . 13 (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
2015, 17, 19syl2anc 584 . . . . . . . . . . . 12 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
21 rmy0 39011 . . . . . . . . . . . . . 14 ((𝑎‘1) ∈ (ℤ‘2) → ((𝑎‘1) Yrm 0) = 0)
2221ad2antlr 723 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) = 0)
23 nngt0 11516 . . . . . . . . . . . . . . 15 ((𝑎‘2) ∈ ℕ → 0 < (𝑎‘2))
2423adantl 482 . . . . . . . . . . . . . 14 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < (𝑎‘2))
25 0zd 11841 . . . . . . . . . . . . . . 15 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈ ℤ)
26 ltrmy 39034 . . . . . . . . . . . . . . 15 (((𝑎‘1) ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
2715, 25, 17, 26syl3anc 1364 . . . . . . . . . . . . . 14 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
2824, 27mpbid 233 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2)))
2922, 28eqbrtrrd 4986 . . . . . . . . . . . 12 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < ((𝑎‘1) Yrm (𝑎‘2)))
30 elnnz 11839 . . . . . . . . . . . 12 (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2))))
3120, 29, 30sylanbrc 583 . . . . . . . . . . 11 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ)
32 eleq1 2870 . . . . . . . . . . 11 ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ))
3331, 32syl5ibrcom 248 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ))
3433pm4.71rd 563 . . . . . . . . 9 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))))
35 simpllr 772 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘1) ∈ (ℤ‘2))
36 simplr 765 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘2) ∈ ℕ)
37 simpr 485 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘3) ∈ ℕ)
38 jm2.27 39090 . . . . . . . . . . 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))))))
3935, 36, 37, 38syl3anc 1364 . . . . . . . . . 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))))))
4039pm5.32da 579 . . . . . . . . 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)))))))
4134, 40bitrd 280 . . . . . . . 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)))))))
4241ex 413 . . . . . . 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))))))))
4342pm5.32rd 578 . . . . . 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 7024 . . . . . . . . . . 11 ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
4544adantl 482 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
4621ad2antlr 723 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) = 0)
4745, 46eqtrd 2831 . . . . . . . . 9 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0)
4847eqeq2d 2805 . . . . . . . 8 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))
4948ex 413 . . . . . . 7 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)))
5049pm5.32rd 578 . . . . . 6 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))
5143, 50orbi12d 913 . . . . 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))))
5251pm5.32da 579 . . . 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)))))
5314, 52bitrd 280 . . 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)))))
5453rabbiia 3418 . 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 11763 . . . 4 3 ∈ ℕ0
56 2z 11863 . . . 4 2 ∈ ℤ
57 ovex 7048 . . . . 5 (1...3) ∈ V
58 1nn 11497 . . . . . . . 8 1 ∈ ℕ
5958jm2.27dlem3 39093 . . . . . . 7 1 ∈ (1...1)
60 df-2 11548 . . . . . . 7 2 = (1 + 1)
6159, 60, 58jm2.27dlem2 39092 . . . . . 6 1 ∈ (1...2)
6261, 4, 2jm2.27dlem2 39092 . . . . 5 1 ∈ (1...3)
63 mzpproj 38819 . . . . 5 (((1...3) ∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
6457, 62, 63mp2an 688 . . . 4 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))
65 eluzrabdioph 38888 . . . 4 ((3 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ‘2)} ∈ (Dioph‘3))
6655, 56, 64, 65mp3an 1453 . . 3 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ‘2)} ∈ (Dioph‘3)
67 3nn 11564 . . . . . . . . 9 3 ∈ ℕ
6867jm2.27dlem3 39093 . . . . . . . 8 3 ∈ (1...3)
69 mzpproj 38819 . . . . . . . 8 (((1...3) ∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
7057, 68, 69mp2an 688 . . . . . . 7 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))
71 elnnrabdioph 38889 . . . . . . 7 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3))
7255, 70, 71mp2an 688 . . . . . 6 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3)
73 fvex 6551 . . . . . . . . . . . . . . . 16 (𝑖‘8) ∈ V
74 fvex 6551 . . . . . . . . . . . . . . . 16 (𝑖‘9) ∈ V
75 fvex 6551 . . . . . . . . . . . . . . . 16 (𝑖10) ∈ V
76 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2))
77 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2))
7877oveq2d 7032 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) · ((𝑖‘8)↑2)))
7976, 78oveqan12rd 7036 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))))
8079eqeq1d 2797 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
81803adant3 1125 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
82 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑖10) → ( + 1) = ((𝑖10) + 1))
8382oveq1d 7031 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑖10) → (( + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))))
8483eqeq2d 2805 . . . . . . . . . . . . . . . . . . . 20 ( = (𝑖10) → (𝑐 = (( + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
85843ad2ant3 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → (𝑐 = (( + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
8681, 853anbi12d 1429 . . . . . . . . . . . . . . . . . 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)))))
8786anbi2d 628 . . . . . . . . . . . . . . . . 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 7023 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3)))
8988breq2d 4974 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))
9089anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))))
91 oveq1 7023 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2)))
9291breq2d 4974 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2))))
9392anbi1d 629 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))
9490, 93anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
95943ad2ant1 1126 . . . . . . . . . . . . . . . . 17 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
9687, 95anbi12d 630 . . . . . . . . . . . . . . . 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))))))
9773, 74, 75, 96sbc3ie 3780 . . . . . . . . . . . . . . 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)))))
9897sbcbii 3757 . . . . . . . . . . . . . 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)))))
9998sbcbii 3757 . . . . . . . . . . . . 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)))))
10099sbcbii 3757 . . . . . . . . . . . 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)))))
101100sbcbii 3757 . . . . . . . . . . 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)))))
102101sbcbii 3757 . . . . . . . . . 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 6551 . . . . . . . . . . . . 13 (𝑖‘5) ∈ V
104 fvex 6551 . . . . . . . . . . . . 13 (𝑖‘6) ∈ V
105 fvex 6551 . . . . . . . . . . . . 13 (𝑖‘7) ∈ V
106 oveq1 7023 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2))
1071063ad2ant2 1127 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2))
108 oveq1 7023 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2))
109108oveq2d 7032 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
1101093ad2ant1 1126 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
111107, 110oveq12d 7034 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))))
112111eqeq1d 2797 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
113 eleq1 2870 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ‘2) ↔ (𝑖‘7) ∈ (ℤ‘2)))
1141133ad2ant3 1128 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ‘2) ↔ (𝑖‘7) ∈ (ℤ‘2)))
115112, 1143anbi23d 1431 . . . . . . . . . . . . . . 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 7023 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2))
117116oveq1d 7031 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) − 1))
118117oveq1d 7031 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))
119118oveq2d 7032 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))))
120119eqeq1d 2797 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
1211203ad2ant3 1128 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
122 eqeq1 2799 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
1231223ad2ant1 1126 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
124 simp2 1130 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6))
125 oveq1 7023 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
1261253ad2ant3 1128 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
127124, 126breq12d 4975 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))
128121, 123, 1273anbi123d 1428 . . . . . . . . . . . . . . 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)))))
129115, 128anbi12d 630 . . . . . . . . . . . . . 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 7023 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1))
131130breq2d 4974 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1)))
132 breq1 4965 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))
133131, 132bi2anan9r 636 . . . . . . . . . . . . . . . 16 ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))))
134133anbi1d 629 . . . . . . . . . . . . . . 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)))))
1351343adant1 1123 . . . . . . . . . . . . . 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)))))
136129, 135anbi12d 630 . . . . . . . . . . . . 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))))))
137103, 104, 105, 136sbc3ie 3780 . . . . . . . . . . . 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)))))
138137sbcbii 3757 . . . . . . . . . . 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)))))
139138sbcbii 3757 . . . . . . . . . 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 3440 . . . . . . . . . . . 12 𝑖 ∈ V
141140resex 5780 . . . . . . . . . . 11 (𝑖 ↾ (1...3)) ∈ V
142 fvex 6551 . . . . . . . . . . 11 (𝑖‘4) ∈ V
143 oveq1 7023 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2))
14462jm2.27dlem1 39091 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1))
145144oveq1d 7031 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2))
146145oveq1d 7031 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑖‘1)↑2) − 1))
14768jm2.27dlem1 39091 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3))
148147oveq1d 7031 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2))
149146, 148oveq12d 7034 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))
150143, 149oveqan12rd 7036 . . . . . . . . . . . . . . 15 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))))
151150eqeq1d 2797 . . . . . . . . . . . . . 14 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1))
152146oveq1d 7031 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))
153152oveq2d 7032 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))))
154153eqeq1d 2797 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
155154adantr 481 . . . . . . . . . . . . . 14 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
156151, 1553anbi12d 1429 . . . . . . . . . . . . 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))))
157148oveq2d 7032 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 · ((𝑖‘3)↑2)))
158157oveq2d 7032 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2))))
159158eqeq2d 2805 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))))
160144oveq2d 7032 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1)))
161160breq2d 4974 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))
162159, 1613anbi23d 1431 . . . . . . . . . . . . . 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)))))
163162adantr 481 . . . . . . . . . . . . 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)))))
164156, 163anbi12d 630 . . . . . . . . . . . 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))))))
165147oveq2d 7032 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3)))
166165breq1d 4972 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)))
167147oveq2d 7032 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3)))
168167breq2d 4974 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))))
169166, 168anbi12d 630 . . . . . . . . . . . . . 14 (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))))
1705jm2.27dlem1 39091 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2))
171170oveq2d 7032 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2)))
172165, 171breq12d 4975 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))))
173170, 147breq12d 4975 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3)))
174172, 173anbi12d 630 . . . . . . . . . . . . . 14 (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))
175169, 174anbi12d 630 . . . . . . . . . . . . 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)))))
176175adantr 481 . . . . . . . . . . . 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)))))
177164, 176anbi12d 630 . . . . . . . . . . 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))))))
178141, 142, 177sbc2ie 3778 . . . . . . . . . 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)))))
179102, 139, 1783bitri 298 . . . . . . . . 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)))))
180179rabbii 3419 . . . . . . . 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))))}
181 10nn0 11965 . . . . . . . . . . . 12 10 ∈ ℕ0
182 ovex 7048 . . . . . . . . . . . . . . 15 (1...10) ∈ V
183 df-5 11551 . . . . . . . . . . . . . . . . 17 5 = (4 + 1)
184 df-6 11552 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
185 df-7 11553 . . . . . . . . . . . . . . . . . . 19 7 = (6 + 1)
186 df-8 11554 . . . . . . . . . . . . . . . . . . . 20 8 = (7 + 1)
187 df-9 11555 . . . . . . . . . . . . . . . . . . . . 21 9 = (8 + 1)
188 9p1e10 11949 . . . . . . . . . . . . . . . . . . . . . . 23 (9 + 1) = 10
189188eqcomi 2804 . . . . . . . . . . . . . . . . . . . . . 22 10 = (9 + 1)
190 ssid 3910 . . . . . . . . . . . . . . . . . . . . . 22 (1...10) ⊆ (1...10)
191189, 190jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . . . . 21 (1...9) ⊆ (1...10)
192187, 191jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . . . 20 (1...8) ⊆ (1...10)
193186, 192jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . . 19 (1...7) ⊆ (1...10)
194185, 193jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . 18 (1...6) ⊆ (1...10)
195184, 194jm2.27dlem5 39095 . . . . . . . . . . . . . . . . 17 (1...5) ⊆ (1...10)
196183, 195jm2.27dlem5 39095 . . . . . . . . . . . . . . . 16 (1...4) ⊆ (1...10)
197 4nn 11568 . . . . . . . . . . . . . . . . 17 4 ∈ ℕ
198197jm2.27dlem3 39093 . . . . . . . . . . . . . . . 16 4 ∈ (1...4)
199196, 198sselii 3886 . . . . . . . . . . . . . . 15 4 ∈ (1...10)
200 mzpproj 38819 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 4 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10)))
201182, 199, 200mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10))
202 2nn0 11762 . . . . . . . . . . . . . 14 2 ∈ ℕ0
203 mzpexpmpt 38827 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...10)))
204201, 202, 203mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...10))
205 df-4 11550 . . . . . . . . . . . . . . . . . . . . 21 4 = (3 + 1)
206205, 196jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . . . 20 (1...3) ⊆ (1...10)
2074, 206jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . . 19 (1...2) ⊆ (1...10)
20860, 207jm2.27dlem5 39095 . . . . . . . . . . . . . . . . . 18 (1...1) ⊆ (1...10)
209208, 59sselii 3886 . . . . . . . . . . . . . . . . 17 1 ∈ (1...10)
210 mzpproj 38819 . . . . . . . . . . . . . . . . 17 (((1...10) ∈ V ∧ 1 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10)))
211182, 209, 210mp2an 688 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10))
212 mzpexpmpt 38827 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10)))
213211, 202, 212mp2an 688 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10))
214 1z 11861 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
215 mzpconstmpt 38822 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 1 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10)))
216182, 214, 215mp2an 688 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))
217 mzpsubmpt 38825 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...10)))
218213, 216, 217mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...10))
219206, 68sselii 3886 . . . . . . . . . . . . . . . 16 3 ∈ (1...10)
220 mzpproj 38819 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 3 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10)))
221182, 219, 220mp2an 688 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))
222 mzpexpmpt 38827 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10)))
223221, 202, 222mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10))
224 mzpmulmpt 38824 . . . . . . . . . . . . . 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)))
225218, 223, 224mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10))
226 mzpsubmpt 38825 . . . . . . . . . . . . 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)))
227204, 225, 226mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...10))
228 eqrabdioph 38859 . . . . . . . . . . . 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))
229181, 227, 216, 228mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘10)
230 6nn 11574 . . . . . . . . . . . . . . . . 17 6 ∈ ℕ
231230jm2.27dlem3 39093 . . . . . . . . . . . . . . . 16 6 ∈ (1...6)
232194, 231sselii 3886 . . . . . . . . . . . . . . 15 6 ∈ (1...10)
233 mzpproj 38819 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 6 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)))
234182, 232, 233mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10))
235 mzpexpmpt 38827 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...10)))
236234, 202, 235mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...10))
237 5nn 11571 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ
238237jm2.27dlem3 39093 . . . . . . . . . . . . . . . . 17 5 ∈ (1...5)
239195, 238sselii 3886 . . . . . . . . . . . . . . . 16 5 ∈ (1...10)
240 mzpproj 38819 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 5 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10)))
241182, 239, 240mp2an 688 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10))
242 mzpexpmpt 38827 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...10)))
243241, 202, 242mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...10))
244 mzpmulmpt 38824 . . . . . . . . . . . . . 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)))
245218, 243, 244mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...10))
246 mzpsubmpt 38825 . . . . . . . . . . . . 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)))
247236, 245, 246mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...10))
248 eqrabdioph 38859 . . . . . . . . . . . 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))
249181, 247, 216, 248mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘10)
250 7nn 11577 . . . . . . . . . . . . . . 15 7 ∈ ℕ
251250jm2.27dlem3 39093 . . . . . . . . . . . . . 14 7 ∈ (1...7)
252193, 251sselii 3886 . . . . . . . . . . . . 13 7 ∈ (1...10)
253 mzpproj 38819 . . . . . . . . . . . . 13 (((1...10) ∈ V ∧ 7 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)))
254182, 252, 253mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10))
255 eluzrabdioph 38888 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘7) ∈ (ℤ‘2)} ∈ (Dioph‘10))
256181, 56, 254, 255mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘7) ∈ (ℤ‘2)} ∈ (Dioph‘10)
257 3anrabdioph 38864 . . . . . . . . . . 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))
258229, 249, 256, 257mp3an 1453 . . . . . . . . . 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 9nn 11583 . . . . . . . . . . . . . . . . 17 9 ∈ ℕ
260259jm2.27dlem3 39093 . . . . . . . . . . . . . . . 16 9 ∈ (1...9)
261260, 189, 259jm2.27dlem2 39092 . . . . . . . . . . . . . . 15 9 ∈ (1...10)
262 mzpproj 38819 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 9 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10)))
263182, 261, 262mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10))
264 mzpexpmpt 38827 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...10)))
265263, 202, 264mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...10))
266 mzpexpmpt 38827 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10)))
267254, 202, 266mp2an 688 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10))
268 mzpsubmpt 38825 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...10)))
269267, 216, 268mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...10))
270 8nn 11580 . . . . . . . . . . . . . . . . . 18 8 ∈ ℕ
271270jm2.27dlem3 39093 . . . . . . . . . . . . . . . . 17 8 ∈ (1...8)
272192, 271sselii 3886 . . . . . . . . . . . . . . . 16 8 ∈ (1...10)
273 mzpproj 38819 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 8 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)))
274182, 272, 273mp2an 688 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10))
275 mzpexpmpt 38827 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...10)))
276274, 202, 275mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...10))
277 mzpmulmpt 38824 . . . . . . . . . . . . . 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)))
278269, 276, 277mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...10))
279 mzpsubmpt 38825 . . . . . . . . . . . . 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)))
280265, 278, 279mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...10))
281 eqrabdioph 38859 . . . . . . . . . . . 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))
282181, 280, 216, 281mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘10)
283 10nn 11963 . . . . . . . . . . . . . . . 16 10 ∈ ℕ
284283jm2.27dlem3 39093 . . . . . . . . . . . . . . 15 10 ∈ (1...10)
285 mzpproj 38819 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 10 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10)))
286182, 284, 285mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10))
287 mzpaddmpt 38823 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖10) + 1)) ∈ (mzPoly‘(1...10)))
288286, 216, 287mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖10) + 1)) ∈ (mzPoly‘(1...10))
289 mzpconstmpt 38822 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 2 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)))
290182, 56, 289mp2an 688 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10))
291 mzpmulmpt 38824 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10)))
292290, 223, 291mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10))
293 mzpmulmpt 38824 . . . . . . . . . . . . 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)))
294288, 292, 293mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...10))
295 eqrabdioph 38859 . . . . . . . . . . . 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))
296181, 241, 294, 295mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘10)
297 mzpsubmpt 38825 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10)))
298254, 211, 297mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10))
299 dvdsrabdioph 38892 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘10))
300181, 234, 298, 299mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘10)
301 3anrabdioph 38864 . . . . . . . . . . 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))
302282, 296, 300, 301mp3an 1453 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1 ∧ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2))) ∧ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1)))} ∈ (Dioph‘10)
303 anrabdioph 38862 . . . . . . . . . 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))
304258, 302, 303mp2an 688 . . . . . . . . 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)
305 mzpmulmpt 38824 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...10)))
306290, 221, 305mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...10))
307 mzpsubmpt 38825 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...10)))
308254, 216, 307mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...10))
309 dvdsrabdioph 38892 . . . . . . . . . . . 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))
310181, 306, 308, 309mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘10)
311 mzpsubmpt 38825 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10)))
312274, 221, 311mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10))
313 dvdsrabdioph 38892 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘10))
314181, 234, 312, 313mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘10)
315 anrabdioph 38862 . . . . . . . . . . 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))
316310, 314, 315mp2an 688 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘10)
317207, 3sselii 3886 . . . . . . . . . . . . . 14 2 ∈ (1...10)
318 mzpproj 38819 . . . . . . . . . . . . . 14 (((1...10) ∈ V ∧ 2 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10)))
319182, 317, 318mp2an 688 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10))
320 mzpsubmpt 38825 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...10)))
321274, 319, 320mp2an 688 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...10))
322 dvdsrabdioph 38892 . . . . . . . . . . . 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))
323181, 306, 321, 322mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘10)
324 lerabdioph 38887 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘10))
325181, 319, 221, 324mp3an 1453 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘10)
326 anrabdioph 38862 . . . . . . . . . . 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))
327323, 325, 326mp2an 688 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘10)
328 anrabdioph 38862 . . . . . . . . . 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))
329316, 327, 328mp2an 688 . . . . . . . . 9 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘10)
330 anrabdioph 38862 . . . . . . . . 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))
331304, 329, 330mp2an 688 . . . . . . . 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)
332180, 331eqeltri 2879 . . . . . . 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)
333205, 183, 184, 185, 186, 187, 1897rexfrabdioph 38882 . . . . . . 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))
33455, 332, 333mp2an 688 . . . . . 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)
335 anrabdioph 38862 . . . . . 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))
33672, 334, 335mp2an 688 . . . . 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)
337 mzpproj 38819 . . . . . . 7 (((1...3) ∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
33857, 5, 337mp2an 688 . . . . . 6 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))
339 elnnrabdioph 38889 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3))
34055, 338, 339mp2an 688 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)
341 anrabdioph 38862 . . . . 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))
342336, 340, 341mp2an 688 . . . 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)
343 eq0rabdioph 38858 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3))
34455, 70, 343mp2an 688 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)
345 eq0rabdioph 38858 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3))
34655, 338, 345mp2an 688 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)
347 anrabdioph 38862 . . . . 5 (({𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3))
348344, 346, 347mp2an 688 . . . 4 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)
349 orrabdioph 38863 . . . 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))
350342, 348, 349mp2an 688 . . 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 anrabdioph 38862 . . 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))
35266, 350, 351mp2an 688 . 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)
35354, 352eqeltri 2879 1 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wo 842  w3a 1080   = wceq 1522  wcel 2081  wrex 3106  {crab 3109  Vcvv 3437  [wsbc 3706   class class class wbr 4962  cmpt 5041  cres 5445  wf 6221  cfv 6225  (class class class)co 7016  𝑚 cmap 8256  0cc0 10383  1c1 10384   + caddc 10386   · cmul 10388   < clt 10521  cle 10522  cmin 10717  cn 11486  2c2 11540  3c3 11541  4c4 11542  5c5 11543  6c6 11544  7c7 11545  8c8 11546  9c9 11547  0cn0 11745  cz 11829  cdc 11947  cuz 12093  ...cfz 12742  cexp 13279  cdvds 15440  mzPolycmzp 38804  Diophcdioph 38837   Yrm crmy 38983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461  ax-addf 10462  ax-mulf 10463
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-of 7267  df-om 7437  df-1st 7545  df-2nd 7546  df-supp 7682  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-2o 7954  df-oadd 7957  df-omul 7958  df-er 8139  df-map 8258  df-pm 8259  df-ixp 8311  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-fsupp 8680  df-fi 8721  df-sup 8752  df-inf 8753  df-oi 8820  df-dju 9176  df-card 9214  df-acn 9217  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-7 11553  df-8 11554  df-9 11555  df-n0 11746  df-xnn0 11816  df-z 11830  df-dec 11948  df-uz 12094  df-q 12198  df-rp 12240  df-xneg 12357  df-xadd 12358  df-xmul 12359  df-ioo 12592  df-ioc 12593  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-fl 13012  df-mod 13088  df-seq 13220  df-exp 13280  df-fac 13484  df-bc 13513  df-hash 13541  df-shft 14260  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-limsup 14662  df-clim 14679  df-rlim 14680  df-sum 14877  df-ef 15254  df-sin 15256  df-cos 15257  df-pi 15259  df-dvds 15441  df-gcd 15677  df-prm 15845  df-numer 15904  df-denom 15905  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-sets 16319  df-ress 16320  df-plusg 16407  df-mulr 16408  df-starv 16409  df-sca 16410  df-vsca 16411  df-ip 16412  df-tset 16413  df-ple 16414  df-ds 16416  df-unif 16417  df-hom 16418  df-cco 16419  df-rest 16525  df-topn 16526  df-0g 16544  df-gsum 16545  df-topgen 16546  df-pt 16547  df-prds 16550  df-xrs 16604  df-qtop 16609  df-imas 16610  df-xps 16612  df-mre 16686  df-mrc 16687  df-acs 16689  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-submnd 17775  df-mulg 17982  df-cntz 18188  df-cmn 18635  df-psmet 20219  df-xmet 20220  df-met 20221  df-bl 20222  df-mopn 20223  df-fbas 20224  df-fg 20225  df-cnfld 20228  df-top 21186  df-topon 21203  df-topsp 21225  df-bases 21238  df-cld 21311  df-ntr 21312  df-cls 21313  df-nei 21390  df-lp 21428  df-perf 21429  df-cn 21519  df-cnp 21520  df-haus 21607  df-tx 21854  df-hmeo 22047  df-fil 22138  df-fm 22230  df-flim 22231  df-flf 22232  df-xms 22613  df-ms 22614  df-tms 22615  df-cncf 23169  df-limc 24147  df-dv 24148  df-log 24821  df-mzpcl 38805  df-mzp 38806  df-dioph 38838  df-squarenn 38923  df-pell1qr 38924  df-pell14qr 38925  df-pell1234qr 38926  df-pellfund 38927  df-rmx 38984  df-rmy 38985
This theorem is referenced by:  rmxdioph  39098  expdiophlem2  39104
  Copyright terms: Public domain W3C validator