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 37096
 Description: jm2.27 37090 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 7831 . . . . . . 7 (𝑎 ∈ (ℕ0𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0)
2 2nn 11137 . . . . . . . . 9 2 ∈ ℕ
32jm2.27dlem3 37093 . . . . . . . 8 2 ∈ (1...2)
4 df-3 11032 . . . . . . . 8 3 = (2 + 1)
53, 4, 2jm2.27dlem2 37092 . . . . . . 7 2 ∈ (1...3)
6 ffvelrn 6318 . . . . . . 7 ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
71, 5, 6sylancl 693 . . . . . 6 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (𝑎‘2) ∈ ℕ0)
8 elnn0 11246 . . . . . 6 ((𝑎‘2) ∈ ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
97, 8sylib 208 . . . . 5 (𝑎 ∈ (ℕ0𝑚 (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
10 iba 524 . . . . . . 7 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))))
11 andi 910 . . . . . . 7 (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))
1210, 11syl6bb 276 . . . . . 6 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))
1312anbi2d 739 . . . . 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 791 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈ (ℤ‘2))
16 nnz 11351 . . . . . . . . . . . . . 14 ((𝑎‘2) ∈ ℕ → (𝑎‘2) ∈ ℤ)
1716adantl 482 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈ ℤ)
18 frmy 36994 . . . . . . . . . . . . . 14 Yrm :((ℤ‘2) × ℤ)⟶ℤ
1918fovcl 6725 . . . . . . . . . . . . 13 (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
2015, 17, 19syl2anc 692 . . . . . . . . . . . 12 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
21 rmy0 37009 . . . . . . . . . . . . . 14 ((𝑎‘1) ∈ (ℤ‘2) → ((𝑎‘1) Yrm 0) = 0)
2221ad2antlr 762 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) = 0)
23 nngt0 11001 . . . . . . . . . . . . . . 15 ((𝑎‘2) ∈ ℕ → 0 < (𝑎‘2))
2423adantl 482 . . . . . . . . . . . . . 14 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < (𝑎‘2))
25 0zd 11341 . . . . . . . . . . . . . . 15 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈ ℤ)
26 ltrmy 37034 . . . . . . . . . . . . . . 15 (((𝑎‘1) ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
2715, 25, 17, 26syl3anc 1323 . . . . . . . . . . . . . 14 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
2824, 27mpbid 222 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2)))
2922, 28eqbrtrrd 4642 . . . . . . . . . . . 12 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < ((𝑎‘1) Yrm (𝑎‘2)))
30 elnnz 11339 . . . . . . . . . . . 12 (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2))))
3120, 29, 30sylanbrc 697 . . . . . . . . . . 11 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ)
32 eleq1 2686 . . . . . . . . . . 11 ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ))
3331, 32syl5ibrcom 237 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ))
3433pm4.71rd 666 . . . . . . . . 9 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))))
35 simpllr 798 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘1) ∈ (ℤ‘2))
36 simplr 791 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘2) ∈ ℕ)
37 simpr 477 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘3) ∈ ℕ)
38 jm2.27 37090 . . . . . . . . . . 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 1323 . . . . . . . . . 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 672 . . . . . . . . 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 268 . . . . . . . 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 450 . . . . . . 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 671 . . . . . 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 6618 . . . . . . . . . . 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 762 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) = 0)
4745, 46eqtrd 2655 . . . . . . . . 9 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0)
4847eqeq2d 2631 . . . . . . . 8 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))
4948ex 450 . . . . . . 7 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)))
5049pm5.32rd 671 . . . . . 6 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))
5143, 50orbi12d 745 . . . . 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 672 . . . 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 268 . . 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 3176 . 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 11262 . . . 4 3 ∈ ℕ0
56 2z 11361 . . . 4 2 ∈ ℤ
57 ovex 6638 . . . . 5 (1...3) ∈ V
58 1nn 10983 . . . . . . . 8 1 ∈ ℕ
5958jm2.27dlem3 37093 . . . . . . 7 1 ∈ (1...1)
60 df-2 11031 . . . . . . 7 2 = (1 + 1)
6159, 60, 58jm2.27dlem2 37092 . . . . . 6 1 ∈ (1...2)
6261, 4, 2jm2.27dlem2 37092 . . . . 5 1 ∈ (1...3)
63 mzpproj 36815 . . . . 5 (((1...3) ∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
6457, 62, 63mp2an 707 . . . 4 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))
65 eluzrabdioph 36885 . . . 4 ((3 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ‘2)} ∈ (Dioph‘3))
6655, 56, 64, 65mp3an 1421 . . 3 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ‘2)} ∈ (Dioph‘3)
67 3nn 11138 . . . . . . . . 9 3 ∈ ℕ
6867jm2.27dlem3 37093 . . . . . . . 8 3 ∈ (1...3)
69 mzpproj 36815 . . . . . . . 8 (((1...3) ∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
7057, 68, 69mp2an 707 . . . . . . 7 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))
71 elnnrabdioph 36886 . . . . . . 7 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3))
7255, 70, 71mp2an 707 . . . . . 6 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3)
73 fvex 6163 . . . . . . . . . . . . . . . . 17 (𝑖‘8) ∈ V
74 fvex 6163 . . . . . . . . . . . . . . . . 17 (𝑖‘9) ∈ V
75 fvex 6163 . . . . . . . . . . . . . . . . 17 (𝑖10) ∈ V
76 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2))
77 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2))
7877oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) · ((𝑖‘8)↑2)))
7976, 78oveqan12rd 6630 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))))
8079eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
81803adant3 1079 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
82 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . 23 ( = (𝑖10) → ( + 1) = ((𝑖10) + 1))
8382oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑖10) → (( + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))))
8483eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑖10) → (𝑐 = (( + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
85843ad2ant3 1082 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → (𝑐 = (( + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
8681, 853anbi12d 1397 . . . . . . . . . . . . . . . . . . 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)))))
8786anbi2d 739 . . . . . . . . . . . . . . . . . 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 6617 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3)))
8988breq2d 4630 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))
9089anbi2d 739 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))))
91 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2)))
9291breq2d 4630 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2))))
9392anbi1d 740 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))
9490, 93anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
95943ad2ant1 1080 . . . . . . . . . . . . . . . . . 18 ((𝑓 = (𝑖‘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 746 . . . . . . . . . . . . . . . . 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))))))
9773, 74, 75, 96sbc3ie 3493 . . . . . . . . . . . . . . . 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)))))
9897sbcbii 3477 . . . . . . . . . . . . . . 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)))))
9998sbcbii 3477 . . . . . . . . . . . . . 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)))))
10099sbcbii 3477 . . . . . . . . . . . . 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)))))
101100sbcbii 3477 . . . . . . . . . . . 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)))))
102101sbcbii 3477 . . . . . . . . . . 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 6163 . . . . . . . . . . . . . 14 (𝑖‘5) ∈ V
104 fvex 6163 . . . . . . . . . . . . . 14 (𝑖‘6) ∈ V
105 fvex 6163 . . . . . . . . . . . . . 14 (𝑖‘7) ∈ V
106 oveq1 6617 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2))
1071063ad2ant2 1081 . . . . . . . . . . . . . . . . . . 19 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2))
108 oveq1 6617 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2))
109108oveq2d 6626 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
1101093ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
111107, 110oveq12d 6628 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))))
112111eqeq1d 2623 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
113 eleq1 2686 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ‘2) ↔ (𝑖‘7) ∈ (ℤ‘2)))
1141133ad2ant3 1082 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ‘2) ↔ (𝑖‘7) ∈ (ℤ‘2)))
115112, 1143anbi23d 1399 . . . . . . . . . . . . . . . 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 6617 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2))
117116oveq1d 6625 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) − 1))
118117oveq1d 6625 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))
119118oveq2d 6626 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))))
120119eqeq1d 2623 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
1211203ad2ant3 1082 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
122 eqeq1 2625 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
1231223ad2ant1 1080 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
124 simp2 1060 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6))
125 oveq1 6617 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
1261253ad2ant3 1082 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
127124, 126breq12d 4631 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))
128121, 123, 1273anbi123d 1396 . . . . . . . . . . . . . . . 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)))))
129115, 128anbi12d 746 . . . . . . . . . . . . . . 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 6617 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1))
131130breq2d 4630 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1)))
132 breq1 4621 . . . . . . . . . . . . . . . . . 18 (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))
133131, 132bi2anan9r 917 . . . . . . . . . . . . . . . . 17 ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))))
134133anbi1d 740 . . . . . . . . . . . . . . . 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)))))
1351343adant1 1077 . . . . . . . . . . . . . . 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)))))
136129, 135anbi12d 746 . . . . . . . . . . . . . 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))))))
137103, 104, 105, 136sbc3ie 3493 . . . . . . . . . . . . 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)))))
138137sbcbii 3477 . . . . . . . . . . . 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)))))
139138sbcbii 3477 . . . . . . . . . . 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 3192 . . . . . . . . . . . . 13 𝑖 ∈ V
141140resex 5407 . . . . . . . . . . . 12 (𝑖 ↾ (1...3)) ∈ V
142 fvex 6163 . . . . . . . . . . . 12 (𝑖‘4) ∈ V
143 oveq1 6617 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2))
14462jm2.27dlem1 37091 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1))
145144oveq1d 6625 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2))
146145oveq1d 6625 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑖‘1)↑2) − 1))
14768jm2.27dlem1 37091 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3))
148147oveq1d 6625 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2))
149146, 148oveq12d 6628 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))
150143, 149oveqan12rd 6630 . . . . . . . . . . . . . . . 16 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))))
151150eqeq1d 2623 . . . . . . . . . . . . . . 15 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1))
152146oveq1d 6625 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))
153152oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))))
154153eqeq1d 2623 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
155154adantr 481 . . . . . . . . . . . . . . 15 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
156151, 1553anbi12d 1397 . . . . . . . . . . . . . 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))))
157148oveq2d 6626 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 · ((𝑖‘3)↑2)))
158157oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2))))
159158eqeq2d 2631 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))))
160144oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1)))
161160breq2d 4630 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))
162159, 1613anbi23d 1399 . . . . . . . . . . . . . . 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)))))
163162adantr 481 . . . . . . . . . . . . . 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)))))
164156, 163anbi12d 746 . . . . . . . . . . . . 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))))))
165147oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3)))
166165breq1d 4628 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)))
167147oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3)))
168167breq2d 4630 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))))
169166, 168anbi12d 746 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))))
1705jm2.27dlem1 37091 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2))
171170oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2)))
172165, 171breq12d 4631 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))))
173170, 147breq12d 4631 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3)))
174172, 173anbi12d 746 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))
175169, 174anbi12d 746 . . . . . . . . . . . . . 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)))))
176175adantr 481 . . . . . . . . . . . . 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)))))
177164, 176anbi12d 746 . . . . . . . . . . . 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))))))
178141, 142, 177sbc2ie 3491 . . . . . . . . . . 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)))))
179102, 139, 1783bitri 286 . . . . . . . . . 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)))))
180179a1i 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))))))
181180rabbiia 3176 . . . . . . . 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 11468 . . . . . . . . . . . 12 10 ∈ ℕ0
183 ovex 6638 . . . . . . . . . . . . . . 15 (1...10) ∈ V
184 df-5 11034 . . . . . . . . . . . . . . . . 17 5 = (4 + 1)
185 df-6 11035 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
186 df-7 11036 . . . . . . . . . . . . . . . . . . 19 7 = (6 + 1)
187 df-8 11037 . . . . . . . . . . . . . . . . . . . 20 8 = (7 + 1)
188 df-9 11038 . . . . . . . . . . . . . . . . . . . . 21 9 = (8 + 1)
189 9p1e10 11448 . . . . . . . . . . . . . . . . . . . . . . 23 (9 + 1) = 10
190189eqcomi 2630 . . . . . . . . . . . . . . . . . . . . . 22 10 = (9 + 1)
191 ssid 3608 . . . . . . . . . . . . . . . . . . . . . 22 (1...10) ⊆ (1...10)
192190, 191jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . . . . 21 (1...9) ⊆ (1...10)
193188, 192jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . . . 20 (1...8) ⊆ (1...10)
194187, 193jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . . 19 (1...7) ⊆ (1...10)
195186, 194jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . 18 (1...6) ⊆ (1...10)
196185, 195jm2.27dlem5 37095 . . . . . . . . . . . . . . . . 17 (1...5) ⊆ (1...10)
197184, 196jm2.27dlem5 37095 . . . . . . . . . . . . . . . 16 (1...4) ⊆ (1...10)
198 4nn 11139 . . . . . . . . . . . . . . . . 17 4 ∈ ℕ
199198jm2.27dlem3 37093 . . . . . . . . . . . . . . . 16 4 ∈ (1...4)
200197, 199sselii 3584 . . . . . . . . . . . . . . 15 4 ∈ (1...10)
201 mzpproj 36815 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 4 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10)))
202183, 200, 201mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10))
203 2nn0 11261 . . . . . . . . . . . . . 14 2 ∈ ℕ0
204 mzpexpmpt 36823 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...10)))
205202, 203, 204mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...10))
206 df-4 11033 . . . . . . . . . . . . . . . . . . . . 21 4 = (3 + 1)
207206, 197jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . . . 20 (1...3) ⊆ (1...10)
2084, 207jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . . 19 (1...2) ⊆ (1...10)
20960, 208jm2.27dlem5 37095 . . . . . . . . . . . . . . . . . 18 (1...1) ⊆ (1...10)
210209, 59sselii 3584 . . . . . . . . . . . . . . . . 17 1 ∈ (1...10)
211 mzpproj 36815 . . . . . . . . . . . . . . . . 17 (((1...10) ∈ V ∧ 1 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10)))
212183, 210, 211mp2an 707 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10))
213 mzpexpmpt 36823 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10)))
214212, 203, 213mp2an 707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10))
215 1z 11359 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
216 mzpconstmpt 36818 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 1 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10)))
217183, 215, 216mp2an 707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))
218 mzpsubmpt 36821 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...10)))
219214, 217, 218mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...10))
220207, 68sselii 3584 . . . . . . . . . . . . . . . 16 3 ∈ (1...10)
221 mzpproj 36815 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 3 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10)))
222183, 220, 221mp2an 707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))
223 mzpexpmpt 36823 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10)))
224222, 203, 223mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10))
225 mzpmulmpt 36820 . . . . . . . . . . . . . 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)))
226219, 224, 225mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10))
227 mzpsubmpt 36821 . . . . . . . . . . . . 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)))
228205, 226, 227mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...10))
229 eqrabdioph 36856 . . . . . . . . . . . 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))
230182, 228, 217, 229mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘10)
231 6nn 11141 . . . . . . . . . . . . . . . . 17 6 ∈ ℕ
232231jm2.27dlem3 37093 . . . . . . . . . . . . . . . 16 6 ∈ (1...6)
233195, 232sselii 3584 . . . . . . . . . . . . . . 15 6 ∈ (1...10)
234 mzpproj 36815 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 6 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)))
235183, 233, 234mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10))
236 mzpexpmpt 36823 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...10)))
237235, 203, 236mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...10))
238 5nn 11140 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ
239238jm2.27dlem3 37093 . . . . . . . . . . . . . . . . 17 5 ∈ (1...5)
240196, 239sselii 3584 . . . . . . . . . . . . . . . 16 5 ∈ (1...10)
241 mzpproj 36815 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 5 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10)))
242183, 240, 241mp2an 707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10))
243 mzpexpmpt 36823 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...10)))
244242, 203, 243mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...10))
245 mzpmulmpt 36820 . . . . . . . . . . . . . 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)))
246219, 244, 245mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...10))
247 mzpsubmpt 36821 . . . . . . . . . . . . 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)))
248237, 246, 247mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...10))
249 eqrabdioph 36856 . . . . . . . . . . . 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))
250182, 248, 217, 249mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘10)
251 7nn 11142 . . . . . . . . . . . . . . 15 7 ∈ ℕ
252251jm2.27dlem3 37093 . . . . . . . . . . . . . 14 7 ∈ (1...7)
253194, 252sselii 3584 . . . . . . . . . . . . 13 7 ∈ (1...10)
254 mzpproj 36815 . . . . . . . . . . . . 13 (((1...10) ∈ V ∧ 7 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)))
255183, 253, 254mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10))
256 eluzrabdioph 36885 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘7) ∈ (ℤ‘2)} ∈ (Dioph‘10))
257182, 56, 255, 256mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘7) ∈ (ℤ‘2)} ∈ (Dioph‘10)
258 3anrabdioph 36861 . . . . . . . . . . 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))
259230, 250, 257, 258mp3an 1421 . . . . . . . . . 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 11144 . . . . . . . . . . . . . . . . 17 9 ∈ ℕ
261260jm2.27dlem3 37093 . . . . . . . . . . . . . . . 16 9 ∈ (1...9)
262261, 190, 260jm2.27dlem2 37092 . . . . . . . . . . . . . . 15 9 ∈ (1...10)
263 mzpproj 36815 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 9 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10)))
264183, 262, 263mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10))
265 mzpexpmpt 36823 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...10)))
266264, 203, 265mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...10))
267 mzpexpmpt 36823 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10)))
268255, 203, 267mp2an 707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10))
269 mzpsubmpt 36821 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...10)))
270268, 217, 269mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...10))
271 8nn 11143 . . . . . . . . . . . . . . . . . 18 8 ∈ ℕ
272271jm2.27dlem3 37093 . . . . . . . . . . . . . . . . 17 8 ∈ (1...8)
273193, 272sselii 3584 . . . . . . . . . . . . . . . 16 8 ∈ (1...10)
274 mzpproj 36815 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 8 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)))
275183, 273, 274mp2an 707 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10))
276 mzpexpmpt 36823 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...10)))
277275, 203, 276mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...10))
278 mzpmulmpt 36820 . . . . . . . . . . . . . 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)))
279270, 277, 278mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...10))
280 mzpsubmpt 36821 . . . . . . . . . . . . 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)))
281266, 279, 280mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...10))
282 eqrabdioph 36856 . . . . . . . . . . . 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))
283182, 281, 217, 282mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘10)
284 10nn 11466 . . . . . . . . . . . . . . . 16 10 ∈ ℕ
285284jm2.27dlem3 37093 . . . . . . . . . . . . . . 15 10 ∈ (1...10)
286 mzpproj 36815 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 10 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10)))
287183, 285, 286mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10))
288 mzpaddmpt 36819 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖10) + 1)) ∈ (mzPoly‘(1...10)))
289287, 217, 288mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖10) + 1)) ∈ (mzPoly‘(1...10))
290 mzpconstmpt 36818 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 2 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)))
291183, 56, 290mp2an 707 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10))
292 mzpmulmpt 36820 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10)))
293291, 224, 292mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10))
294 mzpmulmpt 36820 . . . . . . . . . . . . 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)))
295289, 293, 294mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...10))
296 eqrabdioph 36856 . . . . . . . . . . . 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))
297182, 242, 295, 296mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘10)
298 mzpsubmpt 36821 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10)))
299255, 212, 298mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10))
300 dvdsrabdioph 36889 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘10))
301182, 235, 299, 300mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘10)
302 3anrabdioph 36861 . . . . . . . . . . 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))
303283, 297, 301, 302mp3an 1421 . . . . . . . . . 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 36859 . . . . . . . . . 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))
305259, 303, 304mp2an 707 . . . . . . . . 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 36820 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...10)))
307291, 222, 306mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...10))
308 mzpsubmpt 36821 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...10)))
309255, 217, 308mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...10))
310 dvdsrabdioph 36889 . . . . . . . . . . . 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))
311182, 307, 309, 310mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘10)
312 mzpsubmpt 36821 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10)))
313275, 222, 312mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10))
314 dvdsrabdioph 36889 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘10))
315182, 235, 313, 314mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘10)
316 anrabdioph 36859 . . . . . . . . . . 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))
317311, 315, 316mp2an 707 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘10)
318208, 3sselii 3584 . . . . . . . . . . . . . 14 2 ∈ (1...10)
319 mzpproj 36815 . . . . . . . . . . . . . 14 (((1...10) ∈ V ∧ 2 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10)))
320183, 318, 319mp2an 707 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10))
321 mzpsubmpt 36821 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...10)))
322275, 320, 321mp2an 707 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...10))
323 dvdsrabdioph 36889 . . . . . . . . . . . 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))
324182, 307, 322, 323mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘10)
325 lerabdioph 36884 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘10))
326182, 320, 222, 325mp3an 1421 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘10)
327 anrabdioph 36859 . . . . . . . . . . 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))
328324, 326, 327mp2an 707 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘10)
329 anrabdioph 36859 . . . . . . . . . 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))
330317, 328, 329mp2an 707 . . . . . . . . 9 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘10)
331 anrabdioph 36859 . . . . . . . . 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))
332305, 330, 331mp2an 707 . . . . . . . 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)
333181, 332eqeltri 2694 . . . . . . 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)
334206, 184, 185, 186, 187, 188, 1907rexfrabdioph 36879 . . . . . . 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))
33555, 333, 334mp2an 707 . . . . . 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 36859 . . . . . 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))
33772, 335, 336mp2an 707 . . . . 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 36815 . . . . . . 7 (((1...3) ∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
33957, 5, 338mp2an 707 . . . . . 6 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))
340 elnnrabdioph 36886 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3))
34155, 339, 340mp2an 707 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)
342 anrabdioph 36859 . . . . 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))
343337, 341, 342mp2an 707 . . . 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 36855 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3))
34555, 70, 344mp2an 707 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)
346 eq0rabdioph 36855 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3))
34755, 339, 346mp2an 707 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)
348 anrabdioph 36859 . . . . 5 (({𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3) ∧ {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3))
349345, 347, 348mp2an 707 . . . 4 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)
350 orrabdioph 36860 . . . 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))
351343, 349, 350mp2an 707 . . 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 36859 . . 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))
35366, 351, 352mp2an 707 . 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)
35454, 353eqeltri 2694 1 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  ∃wrex 2908  {crab 2911  Vcvv 3189  [wsbc 3421   class class class wbr 4618   ↦ cmpt 4678   ↾ cres 5081  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610   ↑𝑚 cmap 7809  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893   < clt 10026   ≤ cle 10027   − cmin 10218  ℕcn 10972  2c2 11022  3c3 11023  4c4 11024  5c5 11025  6c6 11026  7c7 11027  8c8 11028  9c9 11029  ℕ0cn0 11244  ℤcz 11329  ;cdc 11445  ℤ≥cuz 11639  ...cfz 12276  ↑cexp 12808   ∥ cdvds 14918  mzPolycmzp 36800  Diophcdioph 36833   Yrm crmy 36980 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967  ax-mulf 9968 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-omul 7517  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7861  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fsupp 8228  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-acn 8720  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-xnn0 11316  df-z 11330  df-dec 11446  df-uz 11640  df-q 11741  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-ioo 12129  df-ioc 12130  df-ico 12131  df-icc 12132  df-fz 12277  df-fzo 12415  df-fl 12541  df-mod 12617  df-seq 12750  df-exp 12809  df-fac 13009  df-bc 13038  df-hash 13066  df-shft 13749  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-limsup 14144  df-clim 14161  df-rlim 14162  df-sum 14359  df-ef 14734  df-sin 14736  df-cos 14737  df-pi 14739  df-dvds 14919  df-gcd 15152  df-prm 15321  df-numer 15378  df-denom 15379  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-starv 15888  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-unif 15897  df-hom 15898  df-cco 15899  df-rest 16015  df-topn 16016  df-0g 16034  df-gsum 16035  df-topgen 16036  df-pt 16037  df-prds 16040  df-xrs 16094  df-qtop 16099  df-imas 16100  df-xps 16102  df-mre 16178  df-mrc 16179  df-acs 16181  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-submnd 17268  df-mulg 17473  df-cntz 17682  df-cmn 18127  df-psmet 19670  df-xmet 19671  df-met 19672  df-bl 19673  df-mopn 19674  df-fbas 19675  df-fg 19676  df-cnfld 19679  df-top 20631  df-topon 20648  df-topsp 20661  df-bases 20674  df-cld 20746  df-ntr 20747  df-cls 20748  df-nei 20825  df-lp 20863  df-perf 20864  df-cn 20954  df-cnp 20955  df-haus 21042  df-tx 21288  df-hmeo 21481  df-fil 21573  df-fm 21665  df-flim 21666  df-flf 21667  df-xms 22048  df-ms 22049  df-tms 22050  df-cncf 22604  df-limc 23553  df-dv 23554  df-log 24224  df-mzpcl 36801  df-mzp 36802  df-dioph 36834  df-squarenn 36920  df-pell1qr 36921  df-pell14qr 36922  df-pell1234qr 36923  df-pellfund 36924  df-rmx 36981  df-rmy 36982 This theorem is referenced by:  rmxdioph  37098  expdiophlem2  37104
 Copyright terms: Public domain W3C validator