Metamath Proof Explorer


Theorem rmydioph

Description: jm2.27 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Assertion rmydioph { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 )

Proof

Step Hyp Ref Expression
1 elmapi ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 )
2 2nn 2 ∈ ℕ
3 2 jm2.27dlem3 2 ∈ ( 1 ... 2 )
4 df-3 3 = ( 2 + 1 )
5 3 4 2 jm2.27dlem2 2 ∈ ( 1 ... 3 )
6 ffvelrn ( ( 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 ∧ 2 ∈ ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) ∈ ℕ0 )
7 1 5 6 sylancl ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) ∈ ℕ0 )
8 elnn0 ( ( 𝑎 ‘ 2 ) ∈ ℕ0 ↔ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) )
9 7 8 sylib ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) )
10 iba ( ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) ) ) )
11 andi ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) ) ↔ ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) )
12 10 11 bitrdi ( ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) )
13 12 anbi2d ( ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) ) )
14 9 13 syl ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) ) )
15 simplr ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) )
16 nnz ( ( 𝑎 ‘ 2 ) ∈ ℕ → ( 𝑎 ‘ 2 ) ∈ ℤ )
17 16 adantl ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 𝑎 ‘ 2 ) ∈ ℤ )
18 frmy Yrm : ( ( ℤ ‘ 2 ) × ℤ ) ⟶ ℤ
19 18 fovcl ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℤ ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℤ )
20 15 17 19 syl2anc ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℤ )
21 rmy0 ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) = 0 )
22 21 ad2antlr ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) = 0 )
23 nngt0 ( ( 𝑎 ‘ 2 ) ∈ ℕ → 0 < ( 𝑎 ‘ 2 ) )
24 23 adantl ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → 0 < ( 𝑎 ‘ 2 ) )
25 0zd ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → 0 ∈ ℤ )
26 ltrmy ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ 0 ∈ ℤ ∧ ( 𝑎 ‘ 2 ) ∈ ℤ ) → ( 0 < ( 𝑎 ‘ 2 ) ↔ ( ( 𝑎 ‘ 1 ) Yrm 0 ) < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) )
27 15 25 17 26 syl3anc ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 0 < ( 𝑎 ‘ 2 ) ↔ ( ( 𝑎 ‘ 1 ) Yrm 0 ) < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) )
28 24 27 mpbid ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) )
29 22 28 eqbrtrrd ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → 0 < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) )
30 elnnz ( ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℕ ↔ ( ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℤ ∧ 0 < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) )
31 20 29 30 sylanbrc ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℕ )
32 eleq1 ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) → ( ( 𝑎 ‘ 3 ) ∈ ℕ ↔ ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℕ ) )
33 31 32 syl5ibrcom ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) → ( 𝑎 ‘ 3 ) ∈ ℕ ) )
34 33 pm4.71rd ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ) )
35 simpllr ( ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) )
36 simplr ( ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( 𝑎 ‘ 2 ) ∈ ℕ )
37 simpr ( ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( 𝑎 ‘ 3 ) ∈ ℕ )
38 jm2.27 ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) )
39 35 36 37 38 syl3anc ( ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) )
40 39 pm5.32da ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ) )
41 34 40 bitrd ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ) )
42 41 ex ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑎 ‘ 2 ) ∈ ℕ → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ) ) )
43 42 pm5.32rd ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ‘ 2 ) = 0 → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑎 ‘ 1 ) Yrm 0 ) )
45 44 adantl ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑎 ‘ 1 ) Yrm 0 ) )
46 21 ad2antlr ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) = 0 )
47 45 46 eqtrd ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) = 0 )
48 47 eqeq2d ( ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 0 ) )
49 48 ex ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑎 ‘ 2 ) = 0 → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 0 ) ) )
50 49 pm5.32rd ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ↔ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) )
51 43 50 orbi12d ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) → ( ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ↔ ( ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) )
52 51 pm5.32da ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) ) )
53 14 52 bitrd ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) ) )
54 53 rabbiia { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } = { 𝑎 ∈ ( ℕ0m ( 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 3 ∈ ℕ0
56 2z 2 ∈ ℤ
57 ovex ( 1 ... 3 ) ∈ V
58 1nn 1 ∈ ℕ
59 58 jm2.27dlem3 1 ∈ ( 1 ... 1 )
60 df-2 2 = ( 1 + 1 )
61 59 60 58 jm2.27dlem2 1 ∈ ( 1 ... 2 )
62 61 4 2 jm2.27dlem2 1 ∈ ( 1 ... 3 )
63 mzpproj ( ( ( 1 ... 3 ) ∈ V ∧ 1 ∈ ( 1 ... 3 ) ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) )
64 57 62 63 mp2an ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) )
65 eluzrabdioph ( ( 3 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) } ∈ ( Dioph ‘ 3 ) )
66 55 56 64 65 mp3an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) } ∈ ( Dioph ‘ 3 )
67 3nn 3 ∈ ℕ
68 67 jm2.27dlem3 3 ∈ ( 1 ... 3 )
69 mzpproj ( ( ( 1 ... 3 ) ∈ V ∧ 3 ∈ ( 1 ... 3 ) ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) )
70 57 68 69 mp2an ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) )
71 elnnrabdioph ( ( 3 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) )
72 55 70 71 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) ∈ ℕ } ∈ ( Dioph ‘ 3 )
73 fvex ( 𝑖 ‘ 8 ) ∈ V
74 fvex ( 𝑖 ‘ 9 ) ∈ V
75 fvex ( 𝑖 1 0 ) ∈ V
76 oveq1 ( 𝑔 = ( 𝑖 ‘ 9 ) → ( 𝑔 ↑ 2 ) = ( ( 𝑖 ‘ 9 ) ↑ 2 ) )
77 oveq1 ( 𝑓 = ( 𝑖 ‘ 8 ) → ( 𝑓 ↑ 2 ) = ( ( 𝑖 ‘ 8 ) ↑ 2 ) )
78 77 oveq2d ( 𝑓 = ( 𝑖 ‘ 8 ) → ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) = ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) )
79 76 78 oveqan12rd ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ) → ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) )
80 79 eqeq1d ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ) → ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ) )
81 80 3adant3 ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ∧ = ( 𝑖 1 0 ) ) → ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ) )
82 oveq1 ( = ( 𝑖 1 0 ) → ( + 1 ) = ( ( 𝑖 1 0 ) + 1 ) )
83 82 oveq1d ( = ( 𝑖 1 0 ) → ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) )
84 83 eqeq2d ( = ( 𝑖 1 0 ) → ( 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ↔ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ) )
85 84 3ad2ant3 ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ∧ = ( 𝑖 1 0 ) ) → ( 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ↔ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ) )
86 81 85 3anbi12d ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ∧ = ( 𝑖 1 0 ) ) → ( ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) )
87 86 anbi2d ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ∧ = ( 𝑖 1 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 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ) )
88 oveq1 ( 𝑓 = ( 𝑖 ‘ 8 ) → ( 𝑓 − ( 𝑎 ‘ 3 ) ) = ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) )
89 88 breq2d ( 𝑓 = ( 𝑖 ‘ 8 ) → ( 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ↔ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) )
90 89 anbi2d ( 𝑓 = ( 𝑖 ‘ 8 ) → ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ↔ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ) )
91 oveq1 ( 𝑓 = ( 𝑖 ‘ 8 ) → ( 𝑓 − ( 𝑎 ‘ 2 ) ) = ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) )
92 91 breq2d ( 𝑓 = ( 𝑖 ‘ 8 ) → ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ↔ ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ) )
93 92 anbi1d ( 𝑓 = ( 𝑖 ‘ 8 ) → ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ↔ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) )
94 90 93 anbi12d ( 𝑓 = ( 𝑖 ‘ 8 ) → ( ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ↔ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
95 94 3ad2ant1 ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ∧ = ( 𝑖 1 0 ) ) → ( ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ↔ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
96 87 95 anbi12d ( ( 𝑓 = ( 𝑖 ‘ 8 ) ∧ 𝑔 = ( 𝑖 ‘ 9 ) ∧ = ( 𝑖 1 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 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) )
97 73 74 75 96 sbc3ie ( [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
98 97 sbcbii ( [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) ↔ [ ( 𝑖 ‘ 7 ) / 𝑒 ] ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
99 98 sbcbii ( [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) ↔ [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
100 99 sbcbii ( [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) ↔ [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
101 100 sbcbii ( [ ( 𝑖 ‘ 4 ) / 𝑏 ] [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) ↔ [ ( 𝑖 ‘ 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 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
102 101 sbcbii ( [ ( 𝑖 ↾ ( 1 ... 3 ) ) / 𝑎 ] [ ( 𝑖 ‘ 4 ) / 𝑏 ] [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) ↔ [ ( 𝑖 ↾ ( 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 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
103 fvex ( 𝑖 ‘ 5 ) ∈ V
104 fvex ( 𝑖 ‘ 6 ) ∈ V
105 fvex ( 𝑖 ‘ 7 ) ∈ V
106 oveq1 ( 𝑑 = ( 𝑖 ‘ 6 ) → ( 𝑑 ↑ 2 ) = ( ( 𝑖 ‘ 6 ) ↑ 2 ) )
107 106 3ad2ant2 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( 𝑑 ↑ 2 ) = ( ( 𝑖 ‘ 6 ) ↑ 2 ) )
108 oveq1 ( 𝑐 = ( 𝑖 ‘ 5 ) → ( 𝑐 ↑ 2 ) = ( ( 𝑖 ‘ 5 ) ↑ 2 ) )
109 108 oveq2d ( 𝑐 = ( 𝑖 ‘ 5 ) → ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) = ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) )
110 109 3ad2ant1 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) = ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) )
111 107 110 oveq12d ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) )
112 111 eqeq1d ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ) )
113 eleq1 ( 𝑒 = ( 𝑖 ‘ 7 ) → ( 𝑒 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) )
114 113 3ad2ant3 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( 𝑒 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) )
115 112 114 3anbi23d ( ( 𝑐 = ( 𝑖 ‘ 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 ( 𝑒 = ( 𝑖 ‘ 7 ) → ( 𝑒 ↑ 2 ) = ( ( 𝑖 ‘ 7 ) ↑ 2 ) )
117 116 oveq1d ( 𝑒 = ( 𝑖 ‘ 7 ) → ( ( 𝑒 ↑ 2 ) − 1 ) = ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) )
118 117 oveq1d ( 𝑒 = ( 𝑖 ‘ 7 ) → ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) = ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) )
119 118 oveq2d ( 𝑒 = ( 𝑖 ‘ 7 ) → ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) )
120 119 eqeq1d ( 𝑒 = ( 𝑖 ‘ 7 ) → ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ) )
121 120 3ad2ant3 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ) )
122 eqeq1 ( 𝑐 = ( 𝑖 ‘ 5 ) → ( 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ↔ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ) )
123 122 3ad2ant1 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ↔ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ) )
124 simp2 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → 𝑑 = ( 𝑖 ‘ 6 ) )
125 oveq1 ( 𝑒 = ( 𝑖 ‘ 7 ) → ( 𝑒 − ( 𝑎 ‘ 1 ) ) = ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) )
126 125 3ad2ant3 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( 𝑒 − ( 𝑎 ‘ 1 ) ) = ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) )
127 124 126 breq12d ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ↔ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) )
128 121 123 127 3anbi123d ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ) )
129 115 128 anbi12d ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ) ) )
130 oveq1 ( 𝑒 = ( 𝑖 ‘ 7 ) → ( 𝑒 − 1 ) = ( ( 𝑖 ‘ 7 ) − 1 ) )
131 130 breq2d ( 𝑒 = ( 𝑖 ‘ 7 ) → ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ↔ ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ) )
132 breq1 ( 𝑑 = ( 𝑖 ‘ 6 ) → ( 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ↔ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) )
133 131 132 bi2anan9r ( ( 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ↔ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ) )
134 133 anbi1d ( ( 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ↔ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
135 134 3adant1 ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ↔ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
136 129 135 anbi12d ( ( 𝑐 = ( 𝑖 ‘ 5 ) ∧ 𝑑 = ( 𝑖 ‘ 6 ) ∧ 𝑒 = ( 𝑖 ‘ 7 ) ) → ( ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) )
137 103 104 105 136 sbc3ie ( [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
138 137 sbcbii ( [ ( 𝑖 ‘ 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 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
139 138 sbcbii ( [ ( 𝑖 ↾ ( 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 ∧ 𝑐 = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) )
140 vex 𝑖 ∈ V
141 140 resex ( 𝑖 ↾ ( 1 ... 3 ) ) ∈ V
142 fvex ( 𝑖 ‘ 4 ) ∈ V
143 oveq1 ( 𝑏 = ( 𝑖 ‘ 4 ) → ( 𝑏 ↑ 2 ) = ( ( 𝑖 ‘ 4 ) ↑ 2 ) )
144 62 jm2.27dlem1 ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( 𝑎 ‘ 1 ) = ( 𝑖 ‘ 1 ) )
145 144 oveq1d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 1 ) ↑ 2 ) = ( ( 𝑖 ‘ 1 ) ↑ 2 ) )
146 145 oveq1d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) = ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) )
147 68 jm2.27dlem1 ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( 𝑎 ‘ 3 ) = ( 𝑖 ‘ 3 ) )
148 147 oveq1d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 3 ) ↑ 2 ) = ( ( 𝑖 ‘ 3 ) ↑ 2 ) )
149 146 148 oveq12d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) = ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) )
150 143 149 oveqan12rd ( ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑖 ‘ 4 ) ) → ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) )
151 150 eqeq1d ( ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑖 ‘ 4 ) ) → ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 ) )
152 146 oveq1d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) = ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) )
153 152 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) )
154 153 eqeq1d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ) )
155 154 adantr ( ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑖 ‘ 4 ) ) → ( ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ↔ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ) )
156 151 155 3anbi12d ( ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑖 ‘ 4 ) ) → ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) ↔ ( ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) ) )
157 148 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) = ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) )
158 157 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) )
159 158 eqeq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ↔ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) )
160 144 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) = ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) )
161 160 breq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ↔ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) )
162 159 161 3anbi23d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) )
163 162 adantr ( ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑖 ‘ 4 ) ) → ( ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑎 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) )
164 156 163 anbi12d ( ( 𝑎 = ( 𝑖 ↾ ( 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 ) = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ) )
165 147 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( 2 · ( 𝑎 ‘ 3 ) ) = ( 2 · ( 𝑖 ‘ 3 ) ) )
166 165 breq1d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ↔ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ) )
167 147 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) = ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) )
168 167 breq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ↔ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) )
169 166 168 anbi12d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ↔ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ) )
170 5 jm2.27dlem1 ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) = ( 𝑖 ‘ 2 ) )
171 170 oveq2d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) = ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) )
172 165 171 breq12d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ↔ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ) )
173 170 147 breq12d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ↔ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) )
174 172 173 anbi12d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ↔ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) )
175 169 174 anbi12d ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) → ( ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ↔ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) )
176 175 adantr ( ( 𝑎 = ( 𝑖 ↾ ( 1 ... 3 ) ) ∧ 𝑏 = ( 𝑖 ‘ 4 ) ) → ( ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ↔ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) )
177 164 176 anbi12d ( ( 𝑎 = ( 𝑖 ↾ ( 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 ) = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) ) )
178 141 142 177 sbc2ie ( [ ( 𝑖 ↾ ( 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 ) = ( ( ( 𝑖 1 0 ) + 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) )
179 102 139 178 3bitri ( [ ( 𝑖 ↾ ( 1 ... 3 ) ) / 𝑎 ] [ ( 𝑖 ‘ 4 ) / 𝑏 ] [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) ↔ ( ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) )
180 179 rabbii { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ [ ( 𝑖 ↾ ( 1 ... 3 ) ) / 𝑎 ] [ ( 𝑖 ‘ 4 ) / 𝑏 ] [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ) ) ) ) } = { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) }
181 10nn0 1 0 ∈ ℕ0
182 ovex ( 1 ... 1 0 ) ∈ V
183 df-5 5 = ( 4 + 1 )
184 df-6 6 = ( 5 + 1 )
185 df-7 7 = ( 6 + 1 )
186 df-8 8 = ( 7 + 1 )
187 df-9 9 = ( 8 + 1 )
188 9p1e10 ( 9 + 1 ) = 1 0
189 188 eqcomi 1 0 = ( 9 + 1 )
190 ssid ( 1 ... 1 0 ) ⊆ ( 1 ... 1 0 )
191 189 190 jm2.27dlem5 ( 1 ... 9 ) ⊆ ( 1 ... 1 0 )
192 187 191 jm2.27dlem5 ( 1 ... 8 ) ⊆ ( 1 ... 1 0 )
193 186 192 jm2.27dlem5 ( 1 ... 7 ) ⊆ ( 1 ... 1 0 )
194 185 193 jm2.27dlem5 ( 1 ... 6 ) ⊆ ( 1 ... 1 0 )
195 184 194 jm2.27dlem5 ( 1 ... 5 ) ⊆ ( 1 ... 1 0 )
196 183 195 jm2.27dlem5 ( 1 ... 4 ) ⊆ ( 1 ... 1 0 )
197 4nn 4 ∈ ℕ
198 197 jm2.27dlem3 4 ∈ ( 1 ... 4 )
199 196 198 sselii 4 ∈ ( 1 ... 1 0 )
200 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 4 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
201 182 199 200 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
202 2nn0 2 ∈ ℕ0
203 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 4 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 4 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
204 201 202 203 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 4 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
205 df-4 4 = ( 3 + 1 )
206 205 196 jm2.27dlem5 ( 1 ... 3 ) ⊆ ( 1 ... 1 0 )
207 4 206 jm2.27dlem5 ( 1 ... 2 ) ⊆ ( 1 ... 1 0 )
208 60 207 jm2.27dlem5 ( 1 ... 1 ) ⊆ ( 1 ... 1 0 )
209 208 59 sselii 1 ∈ ( 1 ... 1 0 )
210 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 1 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
211 182 209 210 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
212 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 1 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
213 211 202 212 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 1 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
214 1z 1 ∈ ℤ
215 mzpconstmpt ( ( ( 1 ... 1 0 ) ∈ V ∧ 1 ∈ ℤ ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
216 182 214 215 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
217 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 1 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
218 213 216 217 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
219 206 68 sselii 3 ∈ ( 1 ... 1 0 )
220 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 3 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
221 182 219 220 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
222 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
223 221 202 222 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
224 mzpmulmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
225 218 223 224 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
226 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 4 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
227 204 225 226 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
228 eqrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) )
229 181 227 216 228 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 )
230 6nn 6 ∈ ℕ
231 230 jm2.27dlem3 6 ∈ ( 1 ... 6 )
232 194 231 sselii 6 ∈ ( 1 ... 1 0 )
233 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 6 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
234 182 232 233 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
235 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 6 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
236 234 202 235 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 6 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
237 5nn 5 ∈ ℕ
238 237 jm2.27dlem3 5 ∈ ( 1 ... 5 )
239 195 238 sselii 5 ∈ ( 1 ... 1 0 )
240 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 5 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
241 182 239 240 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
242 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
243 241 202 242 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
244 mzpmulmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
245 218 243 244 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
246 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 6 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
247 236 245 246 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
248 eqrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) )
249 181 247 216 248 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 )
250 7nn 7 ∈ ℕ
251 250 jm2.27dlem3 7 ∈ ( 1 ... 7 )
252 193 251 sselii 7 ∈ ( 1 ... 1 0 )
253 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 7 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
254 182 252 253 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
255 eluzrabdioph ( ( 1 0 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) } ∈ ( Dioph ‘ 1 0 ) )
256 181 56 254 255 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) } ∈ ( Dioph ‘ 1 0 )
257 3anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) )
258 229 249 256 257 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 )
259 9nn 9 ∈ ℕ
260 259 jm2.27dlem3 9 ∈ ( 1 ... 9 )
261 260 189 259 jm2.27dlem2 9 ∈ ( 1 ... 1 0 )
262 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 9 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 9 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
263 182 261 262 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 9 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
264 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 9 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 9 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
265 263 202 264 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 9 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
266 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
267 254 202 266 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
268 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
269 267 216 268 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
270 8nn 8 ∈ ℕ
271 270 jm2.27dlem3 8 ∈ ( 1 ... 8 )
272 192 271 sselii 8 ∈ ( 1 ... 1 0 )
273 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 8 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 8 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
274 182 272 273 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 8 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
275 mzpexpmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 8 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ 2 ∈ ℕ0 ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
276 274 202 275 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
277 mzpmulmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
278 269 276 277 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
279 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 9 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
280 265 278 279 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
281 eqrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) )
282 181 280 216 281 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 )
283 10nn 1 0 ∈ ℕ
284 283 jm2.27dlem3 1 0 ∈ ( 1 ... 1 0 )
285 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 1 0 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 1 0 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
286 182 284 285 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 1 0 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
287 mzpaddmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 1 0 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 1 0 ) + 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
288 286 216 287 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 1 0 ) + 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
289 mzpconstmpt ( ( ( 1 ... 1 0 ) ∈ V ∧ 2 ∈ ℤ ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
290 182 56 289 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
291 mzpmulmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
292 290 223 291 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
293 mzpmulmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 1 0 ) + 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
294 288 292 293 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
295 eqrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 5 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
296 181 241 294 295 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) } ∈ ( Dioph ‘ 1 0 )
297 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
298 254 211 297 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
299 dvdsrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) } ∈ ( Dioph ‘ 1 0 ) )
300 181 234 298 299 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) } ∈ ( Dioph ‘ 1 0 )
301 3anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
302 282 296 300 301 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) } ∈ ( Dioph ‘ 1 0 )
303 anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 7 ) ∈ ( ℤ ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
304 258 302 303 mp2an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) } ∈ ( Dioph ‘ 1 0 )
305 mzpmulmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 2 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
306 290 221 305 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
307 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 7 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ 1 ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
308 254 216 307 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
309 dvdsrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 7 ) − 1 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) } ∈ ( Dioph ‘ 1 0 ) )
310 181 306 308 309 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) } ∈ ( Dioph ‘ 1 0 )
311 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 8 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
312 274 221 311 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
313 dvdsrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 6 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) )
314 181 234 312 313 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 )
315 anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
316 310 314 315 mp2an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 )
317 207 3 sselii 2 ∈ ( 1 ... 1 0 )
318 mzpproj ( ( ( 1 ... 1 0 ) ∈ V ∧ 2 ∈ ( 1 ... 1 0 ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
319 182 317 318 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
320 mzpsubmpt ( ( ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 8 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) )
321 274 319 320 mp2an ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) )
322 dvdsrabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 2 · ( 𝑖 ‘ 3 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) )
323 181 306 321 322 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 )
324 lerabdioph ( ( 1 0 ∈ ℕ0 ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ∧ ( 𝑖 ∈ ( ℤ ↑m ( 1 ... 1 0 ) ) ↦ ( 𝑖 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 1 0 ) ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) } ∈ ( Dioph ‘ 1 0 ) )
325 181 319 221 324 mp3an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) } ∈ ( Dioph ‘ 1 0 )
326 anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) )
327 323 325 326 mp2an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 )
328 anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
329 316 327 328 mp2an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 )
330 anrabdioph ( ( { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
331 304 329 330 mp2an { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ ( ( ( ( ( ( 𝑖 ‘ 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 ) = ( ( ( 𝑖 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) ) } ∈ ( Dioph ‘ 1 0 )
332 180 331 eqeltri { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ [ ( 𝑖 ↾ ( 1 ... 3 ) ) / 𝑎 ] [ ( 𝑖 ‘ 4 ) / 𝑏 ] [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ‘ 1 0 )
333 205 183 184 185 186 187 189 7rexfrabdioph ( ( 3 ∈ ℕ0 ∧ { 𝑖 ∈ ( ℕ0m ( 1 ... 1 0 ) ) ∣ [ ( 𝑖 ↾ ( 1 ... 3 ) ) / 𝑎 ] [ ( 𝑖 ‘ 4 ) / 𝑏 ] [ ( 𝑖 ‘ 5 ) / 𝑐 ] [ ( 𝑖 ‘ 6 ) / 𝑑 ] [ ( 𝑖 ‘ 7 ) / 𝑒 ] [ ( 𝑖 ‘ 8 ) / 𝑓 ] [ ( 𝑖 ‘ 9 ) / 𝑔 ] [ ( 𝑖 1 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 ‘ 1 0 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) } ∈ ( Dioph ‘ 3 ) )
334 55 332 333 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 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 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) } ∈ ( Dioph ‘ 3 ) )
336 72 334 335 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ( ( ( 1 ... 3 ) ∈ V ∧ 2 ∈ ( 1 ... 3 ) ) → ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) )
338 57 5 337 mp2an ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) )
339 elnnrabdioph ( ( 3 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) )
340 55 338 339 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 )
341 anrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 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 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) } ∈ ( Dioph ‘ 3 ) )
342 336 340 341 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ( ( 3 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 ) )
344 55 70 343 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 )
345 eq0rabdioph ( ( 3 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 ) )
346 55 338 345 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 )
347 anrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) } ∈ ( Dioph ‘ 3 ) )
348 344 346 347 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) } ∈ ( Dioph ‘ 3 )
349 orrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 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 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) } ∈ ( Dioph ‘ 3 ) )
350 342 348 349 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 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 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) } ∈ ( Dioph ‘ 3 ) )
352 66 350 351 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( ( ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ∃ 𝑏 ∈ ℕ0𝑐 ∈ ℕ0𝑑 ∈ ℕ0𝑒 ∈ ℕ0𝑓 ∈ ℕ0𝑔 ∈ ℕ0 ∈ ℕ0 ( ( ( ( ( 𝑏 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( 𝑑 ↑ 2 ) − ( ( ( ( 𝑎 ‘ 1 ) ↑ 2 ) − 1 ) · ( 𝑐 ↑ 2 ) ) ) = 1 ∧ 𝑒 ∈ ( ℤ ‘ 2 ) ) ∧ ( ( ( 𝑔 ↑ 2 ) − ( ( ( 𝑒 ↑ 2 ) − 1 ) · ( 𝑓 ↑ 2 ) ) ) = 1 ∧ 𝑐 = ( ( + 1 ) · ( 2 · ( ( 𝑎 ‘ 3 ) ↑ 2 ) ) ) ∧ 𝑑 ∥ ( 𝑒 − ( 𝑎 ‘ 1 ) ) ) ) ∧ ( ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑒 − 1 ) ∧ 𝑑 ∥ ( 𝑓 − ( 𝑎 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑎 ‘ 3 ) ) ∥ ( 𝑓 − ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ≤ ( 𝑎 ‘ 3 ) ) ) ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) } ∈ ( Dioph ‘ 3 )
353 54 352 eqeltri { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 )