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 38100
Description: jm2.27 38094 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 8124 . . . . . . 7 (𝑎 ∈ (ℕ0𝑚 (1...3)) → 𝑎:(1...3)⟶ℕ0)
2 2nn 11386 . . . . . . . . 9 2 ∈ ℕ
32jm2.27dlem3 38097 . . . . . . . 8 2 ∈ (1...2)
4 df-3 11377 . . . . . . . 8 3 = (2 + 1)
53, 4, 2jm2.27dlem2 38096 . . . . . . 7 2 ∈ (1...3)
6 ffvelrn 6589 . . . . . . 7 ((𝑎:(1...3)⟶ℕ0 ∧ 2 ∈ (1...3)) → (𝑎‘2) ∈ ℕ0)
71, 5, 6sylancl 576 . . . . . 6 (𝑎 ∈ (ℕ0𝑚 (1...3)) → (𝑎‘2) ∈ ℕ0)
8 elnn0 11581 . . . . . 6 ((𝑎‘2) ∈ ℕ0 ↔ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
97, 8sylib 209 . . . . 5 (𝑎 ∈ (ℕ0𝑚 (1...3)) → ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))
10 iba 519 . . . . . . 7 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0))))
11 andi 1021 . . . . . . 7 (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ ((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0)))
1210, 11syl6bb 278 . . . . . 6 (((𝑎‘2) ∈ ℕ ∨ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) ∈ ℕ) ∨ ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0))))
1312anbi2d 616 . . . . 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 776 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘1) ∈ (ℤ‘2))
16 nnz 11685 . . . . . . . . . . . . . 14 ((𝑎‘2) ∈ ℕ → (𝑎‘2) ∈ ℤ)
1716adantl 469 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (𝑎‘2) ∈ ℤ)
18 frmy 37998 . . . . . . . . . . . . . 14 Yrm :((ℤ‘2) × ℤ)⟶ℤ
1918fovcl 7005 . . . . . . . . . . . . 13 (((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘2) ∈ ℤ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
2015, 17, 19syl2anc 575 . . . . . . . . . . . 12 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ)
21 rmy0 38013 . . . . . . . . . . . . . 14 ((𝑎‘1) ∈ (ℤ‘2) → ((𝑎‘1) Yrm 0) = 0)
2221ad2antlr 709 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) = 0)
23 nngt0 11347 . . . . . . . . . . . . . . 15 ((𝑎‘2) ∈ ℕ → 0 < (𝑎‘2))
2423adantl 469 . . . . . . . . . . . . . 14 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < (𝑎‘2))
25 0zd 11675 . . . . . . . . . . . . . . 15 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 ∈ ℤ)
26 ltrmy 38038 . . . . . . . . . . . . . . 15 (((𝑎‘1) ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (𝑎‘2) ∈ ℤ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
2715, 25, 17, 26syl3anc 1483 . . . . . . . . . . . . . 14 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → (0 < (𝑎‘2) ↔ ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2))))
2824, 27mpbid 223 . . . . . . . . . . . . 13 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm 0) < ((𝑎‘1) Yrm (𝑎‘2)))
2922, 28eqbrtrrd 4879 . . . . . . . . . . . 12 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → 0 < ((𝑎‘1) Yrm (𝑎‘2)))
30 elnnz 11673 . . . . . . . . . . . 12 (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ ↔ (((𝑎‘1) Yrm (𝑎‘2)) ∈ ℤ ∧ 0 < ((𝑎‘1) Yrm (𝑎‘2))))
3120, 29, 30sylanbrc 574 . . . . . . . . . . 11 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ)
32 eleq1 2884 . . . . . . . . . . 11 ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → ((𝑎‘3) ∈ ℕ ↔ ((𝑎‘1) Yrm (𝑎‘2)) ∈ ℕ))
3331, 32syl5ibrcom 238 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) → (𝑎‘3) ∈ ℕ))
3433pm4.71rd 554 . . . . . . . . 9 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ ((𝑎‘3) ∈ ℕ ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))))
35 simpllr 784 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘1) ∈ (ℤ‘2))
36 simplr 776 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘2) ∈ ℕ)
37 simpr 473 . . . . . . . . . . 11 ((((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) ∈ ℕ) → (𝑎‘3) ∈ ℕ)
38 jm2.27 38094 . . . . . . . . . . 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 1483 . . . . . . . . . 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 570 . . . . . . . . 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 270 . . . . . . . 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 399 . . . . . . 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 569 . . . . . 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 6892 . . . . . . . . . . 11 ((𝑎‘2) = 0 → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
4544adantl 469 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = ((𝑎‘1) Yrm 0))
4621ad2antlr 709 . . . . . . . . . 10 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm 0) = 0)
4745, 46eqtrd 2851 . . . . . . . . 9 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘1) Yrm (𝑎‘2)) = 0)
4847eqeq2d 2827 . . . . . . . 8 (((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) ∧ (𝑎‘2) = 0) → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0))
4948ex 399 . . . . . . 7 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → ((𝑎‘2) = 0 → ((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ↔ (𝑎‘3) = 0)))
5049pm5.32rd 569 . . . . . 6 ((𝑎 ∈ (ℕ0𝑚 (1...3)) ∧ (𝑎‘1) ∈ (ℤ‘2)) → (((𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)) ∧ (𝑎‘2) = 0) ↔ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)))
5143, 50orbi12d 933 . . . . 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 570 . . . 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 270 . . 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 3385 . 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 11597 . . . 4 3 ∈ ℕ0
56 2z 11695 . . . 4 2 ∈ ℤ
57 ovex 6916 . . . . 5 (1...3) ∈ V
58 1nn 11328 . . . . . . . 8 1 ∈ ℕ
5958jm2.27dlem3 38097 . . . . . . 7 1 ∈ (1...1)
60 df-2 11376 . . . . . . 7 2 = (1 + 1)
6159, 60, 58jm2.27dlem2 38096 . . . . . 6 1 ∈ (1...2)
6261, 4, 2jm2.27dlem2 38096 . . . . 5 1 ∈ (1...3)
63 mzpproj 37820 . . . . 5 (((1...3) ∈ V ∧ 1 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3)))
6457, 62, 63mp2an 675 . . . 4 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))
65 eluzrabdioph 37890 . . . 4 ((3 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘1)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ‘2)} ∈ (Dioph‘3))
6655, 56, 64, 65mp3an 1578 . . 3 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘1) ∈ (ℤ‘2)} ∈ (Dioph‘3)
67 3nn 11392 . . . . . . . . 9 3 ∈ ℕ
6867jm2.27dlem3 38097 . . . . . . . 8 3 ∈ (1...3)
69 mzpproj 37820 . . . . . . . 8 (((1...3) ∈ V ∧ 3 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3)))
7057, 68, 69mp2an 675 . . . . . . 7 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))
71 elnnrabdioph 37891 . . . . . . 7 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3))
7255, 70, 71mp2an 675 . . . . . 6 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) ∈ ℕ} ∈ (Dioph‘3)
73 fvex 6431 . . . . . . . . . . . . . . . 16 (𝑖‘8) ∈ V
74 fvex 6431 . . . . . . . . . . . . . . . 16 (𝑖‘9) ∈ V
75 fvex 6431 . . . . . . . . . . . . . . . 16 (𝑖10) ∈ V
76 oveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = (𝑖‘9) → (𝑔↑2) = ((𝑖‘9)↑2))
77 oveq1 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = (𝑖‘8) → (𝑓↑2) = ((𝑖‘8)↑2))
7877oveq2d 6900 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = (𝑖‘8) → (((𝑒↑2) − 1) · (𝑓↑2)) = (((𝑒↑2) − 1) · ((𝑖‘8)↑2)))
7976, 78oveqan12rd 6904 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → ((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))))
8079eqeq1d 2819 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
81803adant3 1155 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → (((𝑔↑2) − (((𝑒↑2) − 1) · (𝑓↑2))) = 1 ↔ (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1))
82 oveq1 6891 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑖10) → ( + 1) = ((𝑖10) + 1))
8382oveq1d 6899 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑖10) → (( + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))))
8483eqeq2d 2827 . . . . . . . . . . . . . . . . . . . 20 ( = (𝑖10) → (𝑐 = (( + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
85843ad2ant3 1158 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = (𝑖‘8) ∧ 𝑔 = (𝑖‘9) ∧ = (𝑖10)) → (𝑐 = (( + 1) · (2 · ((𝑎‘3)↑2))) ↔ 𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
8681, 853anbi12d 1554 . . . . . . . . . . . . . . . . . 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 616 . . . . . . . . . . . . . . . . 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 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘3)) = ((𝑖‘8) − (𝑎‘3)))
8988breq2d 4867 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑖‘8) → (𝑑 ∥ (𝑓 − (𝑎‘3)) ↔ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))))
9089anbi2d 616 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3)))))
91 oveq1 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑖‘8) → (𝑓 − (𝑎‘2)) = ((𝑖‘8) − (𝑎‘2)))
9291breq2d 4867 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑖‘8) → ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2))))
9392anbi1d 617 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑖‘8) → (((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))))
9490, 93anbi12d 618 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑖‘8) → ((((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ (𝑓 − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ (𝑓 − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3))) ↔ (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ∧ ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)))))
95943ad2ant1 1156 . . . . . . . . . . . . . . . . 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 618 . . . . . . . . . . . . . . . 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 3714 . . . . . . . . . . . . . . 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 3700 . . . . . . . . . . . . . 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 3700 . . . . . . . . . . . . 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 3700 . . . . . . . . . . . 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 3700 . . . . . . . . . . 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 3700 . . . . . . . . . 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 6431 . . . . . . . . . . . . 13 (𝑖‘5) ∈ V
104 fvex 6431 . . . . . . . . . . . . 13 (𝑖‘6) ∈ V
105 fvex 6431 . . . . . . . . . . . . 13 (𝑖‘7) ∈ V
106 oveq1 6891 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑖‘6) → (𝑑↑2) = ((𝑖‘6)↑2))
1071063ad2ant2 1157 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑↑2) = ((𝑖‘6)↑2))
108 oveq1 6891 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (𝑖‘5) → (𝑐↑2) = ((𝑖‘5)↑2))
109108oveq2d 6900 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (𝑖‘5) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
1101093ad2ant1 1156 . . . . . . . . . . . . . . . . . 18 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑎‘1)↑2) − 1) · (𝑐↑2)) = ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)))
111107, 110oveq12d 6902 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))))
112111eqeq1d 2819 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((𝑑↑2) − ((((𝑎‘1)↑2) − 1) · (𝑐↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
113 eleq1 2884 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖‘7) → (𝑒 ∈ (ℤ‘2) ↔ (𝑖‘7) ∈ (ℤ‘2)))
1141133ad2ant3 1158 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 ∈ (ℤ‘2) ↔ (𝑖‘7) ∈ (ℤ‘2)))
115112, 1143anbi23d 1556 . . . . . . . . . . . . . . 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 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = (𝑖‘7) → (𝑒↑2) = ((𝑖‘7)↑2))
117116oveq1d 6899 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝑖‘7) → ((𝑒↑2) − 1) = (((𝑖‘7)↑2) − 1))
118117oveq1d 6899 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑖‘7) → (((𝑒↑2) − 1) · ((𝑖‘8)↑2)) = ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))
119118oveq2d 6900 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))))
120119eqeq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖‘7) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
1211203ad2ant3 1158 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → ((((𝑖‘9)↑2) − (((𝑒↑2) − 1) · ((𝑖‘8)↑2))) = 1 ↔ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1))
122 eqeq1 2821 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑖‘5) → (𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
1231223ad2ant1 1156 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑐 = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2)))))
124 simp2 1160 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → 𝑑 = (𝑖‘6))
125 oveq1 6891 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
1261253ad2ant3 1158 . . . . . . . . . . . . . . . . 17 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑒 − (𝑎‘1)) = ((𝑖‘7) − (𝑎‘1)))
127124, 126breq12d 4868 . . . . . . . . . . . . . . . 16 ((𝑐 = (𝑖‘5) ∧ 𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (𝑑 ∥ (𝑒 − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1))))
128121, 123, 1273anbi123d 1553 . . . . . . . . . . . . . . 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 618 . . . . . . . . . . . . . 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 6891 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑖‘7) → (𝑒 − 1) = ((𝑖‘7) − 1))
131130breq2d 4867 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑖‘7) → ((2 · (𝑎‘3)) ∥ (𝑒 − 1) ↔ (2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1)))
132 breq1 4858 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝑖‘6) → (𝑑 ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))))
133131, 132bi2anan9r 623 . . . . . . . . . . . . . . . 16 ((𝑑 = (𝑖‘6) ∧ 𝑒 = (𝑖‘7)) → (((2 · (𝑎‘3)) ∥ (𝑒 − 1) ∧ 𝑑 ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)))))
134133anbi1d 617 . . . . . . . . . . . . . . 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 1153 . . . . . . . . . . . . . 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 618 . . . . . . . . . . . . 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 3714 . . . . . . . . . . . 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 3700 . . . . . . . . . . 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 3700 . . . . . . . . . 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 3405 . . . . . . . . . . . 12 𝑖 ∈ V
141140resex 5662 . . . . . . . . . . 11 (𝑖 ↾ (1...3)) ∈ V
142 fvex 6431 . . . . . . . . . . 11 (𝑖‘4) ∈ V
143 oveq1 6891 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑖‘4) → (𝑏↑2) = ((𝑖‘4)↑2))
14462jm2.27dlem1 38095 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘1) = (𝑖‘1))
145144oveq1d 6899 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘1)↑2) = ((𝑖‘1)↑2))
146145oveq1d 6899 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑎‘1)↑2) − 1) = (((𝑖‘1)↑2) − 1))
14768jm2.27dlem1 38095 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘3) = (𝑖‘3))
148147oveq1d 6899 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘3)↑2) = ((𝑖‘3)↑2))
149146, 148oveq12d 6902 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))
150143, 149oveqan12rd 6904 . . . . . . . . . . . . . . 15 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))))
151150eqeq1d 2819 . . . . . . . . . . . . . 14 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → (((𝑏↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑎‘3)↑2))) = 1 ↔ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1))
152146oveq1d 6899 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2)) = ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))
153152oveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))))
154153eqeq1d 2819 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
155154adantr 468 . . . . . . . . . . . . . 14 ((𝑎 = (𝑖 ↾ (1...3)) ∧ 𝑏 = (𝑖‘4)) → ((((𝑖‘6)↑2) − ((((𝑎‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1 ↔ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1))
156151, 1553anbi12d 1554 . . . . . . . . . . . . 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 6900 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (2 · ((𝑎‘3)↑2)) = (2 · ((𝑖‘3)↑2)))
158157oveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2))))
159158eqeq2d 2827 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑎‘3)↑2))) ↔ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))))
160144oveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘7) − (𝑎‘1)) = ((𝑖‘7) − (𝑖‘1)))
161160breq2d 4867 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘7) − (𝑎‘1)) ↔ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))))
162159, 1613anbi23d 1556 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 618 . . . . . . . . . . . 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 6900 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → (2 · (𝑎‘3)) = (2 · (𝑖‘3)))
166165breq1d 4865 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)))
167147oveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘3)) = ((𝑖‘8) − (𝑖‘3)))
168167breq2d 4867 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3)) ↔ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))))
169166, 168anbi12d 618 . . . . . . . . . . . . . 14 (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑎‘3))) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))))
1705jm2.27dlem1 38095 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 ↾ (1...3)) → (𝑎‘2) = (𝑖‘2))
171170oveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑖‘8) − (𝑎‘2)) = ((𝑖‘8) − (𝑖‘2)))
172165, 171breq12d 4868 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ↔ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))))
173170, 147breq12d 4868 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 ↾ (1...3)) → ((𝑎‘2) ≤ (𝑎‘3) ↔ (𝑖‘2) ≤ (𝑖‘3)))
174172, 173anbi12d 618 . . . . . . . . . . . . . 14 (𝑎 = (𝑖 ↾ (1...3)) → (((2 · (𝑎‘3)) ∥ ((𝑖‘8) − (𝑎‘2)) ∧ (𝑎‘2) ≤ (𝑎‘3)) ↔ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))))
175169, 174anbi12d 618 . . . . . . . . . . . . 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 468 . . . . . . . . . . . 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 618 . . . . . . . . . . 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 3712 . . . . . . . . . 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 288 . . . . . . . . 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 3386 . . . . . . . 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 11797 . . . . . . . . . . . 12 10 ∈ ℕ0
182 ovex 6916 . . . . . . . . . . . . . . 15 (1...10) ∈ V
183 df-5 11379 . . . . . . . . . . . . . . . . 17 5 = (4 + 1)
184 df-6 11380 . . . . . . . . . . . . . . . . . 18 6 = (5 + 1)
185 df-7 11381 . . . . . . . . . . . . . . . . . . 19 7 = (6 + 1)
186 df-8 11382 . . . . . . . . . . . . . . . . . . . 20 8 = (7 + 1)
187 df-9 11383 . . . . . . . . . . . . . . . . . . . . 21 9 = (8 + 1)
188 9p1e10 11781 . . . . . . . . . . . . . . . . . . . . . . 23 (9 + 1) = 10
189188eqcomi 2826 . . . . . . . . . . . . . . . . . . . . . 22 10 = (9 + 1)
190 ssid 3831 . . . . . . . . . . . . . . . . . . . . . 22 (1...10) ⊆ (1...10)
191189, 190jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . . . . 21 (1...9) ⊆ (1...10)
192187, 191jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . . . 20 (1...8) ⊆ (1...10)
193186, 192jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . . 19 (1...7) ⊆ (1...10)
194185, 193jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . 18 (1...6) ⊆ (1...10)
195184, 194jm2.27dlem5 38099 . . . . . . . . . . . . . . . . 17 (1...5) ⊆ (1...10)
196183, 195jm2.27dlem5 38099 . . . . . . . . . . . . . . . 16 (1...4) ⊆ (1...10)
197 4nn 11397 . . . . . . . . . . . . . . . . 17 4 ∈ ℕ
198197jm2.27dlem3 38097 . . . . . . . . . . . . . . . 16 4 ∈ (1...4)
199196, 198sselii 3806 . . . . . . . . . . . . . . 15 4 ∈ (1...10)
200 mzpproj 37820 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 4 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10)))
201182, 199, 200mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10))
202 2nn0 11596 . . . . . . . . . . . . . 14 2 ∈ ℕ0
203 mzpexpmpt 37828 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘4)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...10)))
204201, 202, 203mp2an 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘4)↑2)) ∈ (mzPoly‘(1...10))
205 df-4 11378 . . . . . . . . . . . . . . . . . . . . 21 4 = (3 + 1)
206205, 196jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . . . 20 (1...3) ⊆ (1...10)
2074, 206jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . . 19 (1...2) ⊆ (1...10)
20860, 207jm2.27dlem5 38099 . . . . . . . . . . . . . . . . . 18 (1...1) ⊆ (1...10)
209208, 59sselii 3806 . . . . . . . . . . . . . . . . 17 1 ∈ (1...10)
210 mzpproj 37820 . . . . . . . . . . . . . . . . 17 (((1...10) ∈ V ∧ 1 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10)))
211182, 209, 210mp2an 675 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10))
212 mzpexpmpt 37828 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10)))
213211, 202, 212mp2an 675 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘1)↑2)) ∈ (mzPoly‘(1...10))
214 1z 11693 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
215 mzpconstmpt 37823 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 1 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10)))
216182, 214, 215mp2an 675 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))
217 mzpsubmpt 37826 . . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘1)↑2) − 1)) ∈ (mzPoly‘(1...10))
219206, 68sselii 3806 . . . . . . . . . . . . . . . 16 3 ∈ (1...10)
220 mzpproj 37820 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 3 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10)))
221182, 219, 220mp2an 675 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))
222 mzpexpmpt 37828 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10)))
223221, 202, 222mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘3)↑2)) ∈ (mzPoly‘(1...10))
224 mzpmulmpt 37825 . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10))
226 mzpsubmpt 37826 . . . . . . . . . . . . 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 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...10))
228 eqrabdioph 37861 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘4)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘3)↑2))) = 1} ∈ (Dioph‘10)
230 6nn 11405 . . . . . . . . . . . . . . . . 17 6 ∈ ℕ
231230jm2.27dlem3 38097 . . . . . . . . . . . . . . . 16 6 ∈ (1...6)
232194, 231sselii 3806 . . . . . . . . . . . . . . 15 6 ∈ (1...10)
233 mzpproj 37820 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 6 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)))
234182, 232, 233mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10))
235 mzpexpmpt 37828 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘6)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...10)))
236234, 202, 235mp2an 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘6)↑2)) ∈ (mzPoly‘(1...10))
237 5nn 11401 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ
238237jm2.27dlem3 38097 . . . . . . . . . . . . . . . . 17 5 ∈ (1...5)
239195, 238sselii 3806 . . . . . . . . . . . . . . . 16 5 ∈ (1...10)
240 mzpproj 37820 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 5 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10)))
241182, 239, 240mp2an 675 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10))
242 mzpexpmpt 37828 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘5)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...10)))
243241, 202, 242mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘5)↑2)) ∈ (mzPoly‘(1...10))
244 mzpmulmpt 37825 . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) ∈ (mzPoly‘(1...10))
246 mzpsubmpt 37826 . . . . . . . . . . . . 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 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2)))) ∈ (mzPoly‘(1...10))
248 eqrabdioph 37861 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘6)↑2) − ((((𝑖‘1)↑2) − 1) · ((𝑖‘5)↑2))) = 1} ∈ (Dioph‘10)
250 7nn 11409 . . . . . . . . . . . . . . 15 7 ∈ ℕ
251250jm2.27dlem3 38097 . . . . . . . . . . . . . 14 7 ∈ (1...7)
252193, 251sselii 3806 . . . . . . . . . . . . 13 7 ∈ (1...10)
253 mzpproj 37820 . . . . . . . . . . . . 13 (((1...10) ∈ V ∧ 7 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)))
254182, 252, 253mp2an 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10))
255 eluzrabdioph 37890 . . . . . . . . . . . 12 ((10 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10))) → {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘7) ∈ (ℤ‘2)} ∈ (Dioph‘10))
256181, 56, 254, 255mp3an 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘7) ∈ (ℤ‘2)} ∈ (Dioph‘10)
257 3anrabdioph 37866 . . . . . . . . . . 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 1578 . . . . . . . . . 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 11417 . . . . . . . . . . . . . . . . 17 9 ∈ ℕ
260259jm2.27dlem3 38097 . . . . . . . . . . . . . . . 16 9 ∈ (1...9)
261260, 189, 259jm2.27dlem2 38096 . . . . . . . . . . . . . . 15 9 ∈ (1...10)
262 mzpproj 37820 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 9 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10)))
263182, 261, 262mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10))
264 mzpexpmpt 37828 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘9)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...10)))
265263, 202, 264mp2an 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘9)↑2)) ∈ (mzPoly‘(1...10))
266 mzpexpmpt 37828 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10)))
267254, 202, 266mp2an 675 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7)↑2)) ∈ (mzPoly‘(1...10))
268 mzpsubmpt 37826 . . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘7)↑2) − 1)) ∈ (mzPoly‘(1...10))
270 8nn 11413 . . . . . . . . . . . . . . . . . 18 8 ∈ ℕ
271270jm2.27dlem3 38097 . . . . . . . . . . . . . . . . 17 8 ∈ (1...8)
272192, 271sselii 3806 . . . . . . . . . . . . . . . 16 8 ∈ (1...10)
273 mzpproj 37820 . . . . . . . . . . . . . . . 16 (((1...10) ∈ V ∧ 8 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)))
274182, 272, 273mp2an 675 . . . . . . . . . . . . . . 15 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10))
275 mzpexpmpt 37828 . . . . . . . . . . . . . . 15 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ 2 ∈ ℕ0) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...10)))
276274, 202, 275mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8)↑2)) ∈ (mzPoly‘(1...10))
277 mzpmulmpt 37825 . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) ∈ (mzPoly‘(1...10))
279 mzpsubmpt 37826 . . . . . . . . . . . . 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 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2)))) ∈ (mzPoly‘(1...10))
281 eqrabdioph 37861 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((𝑖‘9)↑2) − ((((𝑖‘7)↑2) − 1) · ((𝑖‘8)↑2))) = 1} ∈ (Dioph‘10)
283 10nn 11795 . . . . . . . . . . . . . . . 16 10 ∈ ℕ
284283jm2.27dlem3 38097 . . . . . . . . . . . . . . 15 10 ∈ (1...10)
285 mzpproj 37820 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 10 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10)))
286182, 284, 285mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10))
287 mzpaddmpt 37824 . . . . . . . . . . . . . 14 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖10)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖10) + 1)) ∈ (mzPoly‘(1...10)))
288286, 216, 287mp2an 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖10) + 1)) ∈ (mzPoly‘(1...10))
289 mzpconstmpt 37823 . . . . . . . . . . . . . . 15 (((1...10) ∈ V ∧ 2 ∈ ℤ) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)))
290182, 56, 289mp2an 675 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10))
291 mzpmulmpt 37825 . . . . . . . . . . . . . 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 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · ((𝑖‘3)↑2))) ∈ (mzPoly‘(1...10))
293 mzpmulmpt 37825 . . . . . . . . . . . . 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 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))) ∈ (mzPoly‘(1...10))
295 eqrabdioph 37861 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘5) = (((𝑖10) + 1) · (2 · ((𝑖‘3)↑2)))} ∈ (Dioph‘10)
297 mzpsubmpt 37826 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘1)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10)))
298254, 211, 297mp2an 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − (𝑖‘1))) ∈ (mzPoly‘(1...10))
299 dvdsrabdioph 37894 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘7) − (𝑖‘1))} ∈ (Dioph‘10)
301 3anrabdioph 37866 . . . . . . . . . . 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 1578 . . . . . . . . . 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 37864 . . . . . . . . . 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 675 . . . . . . . . 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 37825 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 2) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...10)))
306290, 221, 305mp2an 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (2 · (𝑖‘3))) ∈ (mzPoly‘(1...10))
307 mzpsubmpt 37826 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘7)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ 1) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...10)))
308254, 216, 307mp2an 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘7) − 1)) ∈ (mzPoly‘(1...10))
309 dvdsrabdioph 37894 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1)} ∈ (Dioph‘10)
311 mzpsubmpt 37826 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘3)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10)))
312274, 221, 311mp2an 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘3))) ∈ (mzPoly‘(1...10))
313 dvdsrabdioph 37894 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))} ∈ (Dioph‘10)
315 anrabdioph 37864 . . . . . . . . . . 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 675 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3)))} ∈ (Dioph‘10)
317207, 3sselii 3806 . . . . . . . . . . . . . 14 2 ∈ (1...10)
318 mzpproj 37820 . . . . . . . . . . . . . 14 (((1...10) ∈ V ∧ 2 ∈ (1...10)) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10)))
319182, 317, 318mp2an 675 . . . . . . . . . . . . 13 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10))
320 mzpsubmpt 37826 . . . . . . . . . . . . 13 (((𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘8)) ∈ (mzPoly‘(1...10)) ∧ (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ (𝑖‘2)) ∈ (mzPoly‘(1...10))) → (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...10)))
321274, 319, 320mp2an 675 . . . . . . . . . . . 12 (𝑖 ∈ (ℤ ↑𝑚 (1...10)) ↦ ((𝑖‘8) − (𝑖‘2))) ∈ (mzPoly‘(1...10))
322 dvdsrabdioph 37894 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2))} ∈ (Dioph‘10)
324 lerabdioph 37889 . . . . . . . . . . . 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 1578 . . . . . . . . . . 11 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (𝑖‘2) ≤ (𝑖‘3)} ∈ (Dioph‘10)
326 anrabdioph 37864 . . . . . . . . . . 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 675 . . . . . . . . . 10 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3))} ∈ (Dioph‘10)
328 anrabdioph 37864 . . . . . . . . . 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 675 . . . . . . . . 9 {𝑖 ∈ (ℕ0𝑚 (1...10)) ∣ (((2 · (𝑖‘3)) ∥ ((𝑖‘7) − 1) ∧ (𝑖‘6) ∥ ((𝑖‘8) − (𝑖‘3))) ∧ ((2 · (𝑖‘3)) ∥ ((𝑖‘8) − (𝑖‘2)) ∧ (𝑖‘2) ≤ (𝑖‘3)))} ∈ (Dioph‘10)
330 anrabdioph 37864 . . . . . . . . 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 675 . . . . . . . 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 2892 . . . . . . 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 37884 . . . . . . 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 675 . . . . . 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 37864 . . . . . 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 675 . . . . 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 37820 . . . . . . 7 (((1...3) ∈ V ∧ 2 ∈ (1...3)) → (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3)))
33857, 5, 337mp2an 675 . . . . . 6 (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))
339 elnnrabdioph 37891 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3))
34055, 338, 339mp2an 675 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) ∈ ℕ} ∈ (Dioph‘3)
341 anrabdioph 37864 . . . . 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 675 . . . 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 37860 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘3)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3))
34455, 70, 343mp2an 675 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘3) = 0} ∈ (Dioph‘3)
345 eq0rabdioph 37860 . . . . . 6 ((3 ∈ ℕ0 ∧ (𝑎 ∈ (ℤ ↑𝑚 (1...3)) ↦ (𝑎‘2)) ∈ (mzPoly‘(1...3))) → {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3))
34655, 338, 345mp2an 675 . . . . 5 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ (𝑎‘2) = 0} ∈ (Dioph‘3)
347 anrabdioph 37864 . . . . 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 675 . . . 4 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘3) = 0 ∧ (𝑎‘2) = 0)} ∈ (Dioph‘3)
349 orrabdioph 37865 . . . 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 675 . . 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 37864 . . 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 675 . 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 2892 1 {𝑎 ∈ (ℕ0𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2157  wrex 3108  {crab 3111  Vcvv 3402  [wsbc 3644   class class class wbr 4855  cmpt 4934  cres 5326  wf 6107  cfv 6111  (class class class)co 6884  𝑚 cmap 8102  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236   < clt 10369  cle 10370  cmin 10561  cn 11315  2c2 11368  3c3 11369  4c4 11370  5c5 11371  6c6 11372  7c7 11373  8c8 11374  9c9 11375  0cn0 11579  cz 11663  cdc 11779  cuz 11924  ...cfz 12569  cexp 13103  cdvds 15223  mzPolycmzp 37805  Diophcdioph 37838   Yrm crmy 37985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-inf2 8795  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309  ax-addf 10310  ax-mulf 10311
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-of 7137  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-2o 7807  df-oadd 7810  df-omul 7811  df-er 7989  df-map 8104  df-pm 8105  df-ixp 8156  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-fi 8566  df-sup 8597  df-inf 8598  df-oi 8664  df-card 9058  df-acn 9061  df-cda 9285  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-xnn0 11650  df-z 11664  df-dec 11780  df-uz 11925  df-q 12028  df-rp 12067  df-xneg 12182  df-xadd 12183  df-xmul 12184  df-ioo 12417  df-ioc 12418  df-ico 12419  df-icc 12420  df-fz 12570  df-fzo 12710  df-fl 12837  df-mod 12913  df-seq 13045  df-exp 13104  df-fac 13301  df-bc 13330  df-hash 13358  df-shft 14050  df-cj 14082  df-re 14083  df-im 14084  df-sqrt 14218  df-abs 14219  df-limsup 14445  df-clim 14462  df-rlim 14463  df-sum 14660  df-ef 15038  df-sin 15040  df-cos 15041  df-pi 15043  df-dvds 15224  df-gcd 15456  df-prm 15624  df-numer 15680  df-denom 15681  df-struct 16090  df-ndx 16091  df-slot 16092  df-base 16094  df-sets 16095  df-ress 16096  df-plusg 16186  df-mulr 16187  df-starv 16188  df-sca 16189  df-vsca 16190  df-ip 16191  df-tset 16192  df-ple 16193  df-ds 16195  df-unif 16196  df-hom 16197  df-cco 16198  df-rest 16308  df-topn 16309  df-0g 16327  df-gsum 16328  df-topgen 16329  df-pt 16330  df-prds 16333  df-xrs 16387  df-qtop 16392  df-imas 16393  df-xps 16395  df-mre 16471  df-mrc 16472  df-acs 16474  df-mgm 17467  df-sgrp 17509  df-mnd 17520  df-submnd 17561  df-mulg 17766  df-cntz 17971  df-cmn 18416  df-psmet 19966  df-xmet 19967  df-met 19968  df-bl 19969  df-mopn 19970  df-fbas 19971  df-fg 19972  df-cnfld 19975  df-top 20933  df-topon 20950  df-topsp 20972  df-bases 20985  df-cld 21058  df-ntr 21059  df-cls 21060  df-nei 21137  df-lp 21175  df-perf 21176  df-cn 21266  df-cnp 21267  df-haus 21354  df-tx 21600  df-hmeo 21793  df-fil 21884  df-fm 21976  df-flim 21977  df-flf 21978  df-xms 22359  df-ms 22360  df-tms 22361  df-cncf 22915  df-limc 23867  df-dv 23868  df-log 24540  df-mzpcl 37806  df-mzp 37807  df-dioph 37839  df-squarenn 37925  df-pell1qr 37926  df-pell14qr 37927  df-pell1234qr 37928  df-pellfund 37929  df-rmx 37986  df-rmy 37987
This theorem is referenced by:  rmxdioph  38102  expdiophlem2  38108
  Copyright terms: Public domain W3C validator