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 { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 )

Proof

Step Hyp Ref Expression
1 elmapi ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ffvelcdm ⊢ ( ( 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 ∧ 2 ∈ ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) ∈ ℕ0 )
7 1 5 6 sylancl ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) ∈ ℕ0 )
8 elnn0 ⊢ ( ( 𝑎 ‘ 2 ) ∈ ℕ0 ↔ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∨ ( 𝑎 ‘ 2 ) = 0 ) )
9 7 8 sylib ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∨ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ) ) ) )
15 simplr ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) )
16 nnz ⊢ ( ( 𝑎 ‘ 2 ) ∈ ℕ → ( 𝑎 ‘ 2 ) ∈ ℤ )
17 16 adantl ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 𝑎 ‘ 2 ) ∈ ℤ )
18 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
19 18 fovcl ⊢ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℤ ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℤ )
20 15 17 19 syl2anc ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℤ )
21 rmy0 ⊢ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) = 0 )
22 21 ad2antlr ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) = 0 )
23 nngt0 ⊢ ( ( 𝑎 ‘ 2 ) ∈ ℕ → 0 < ( 𝑎 ‘ 2 ) )
24 23 adantl ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → 0 < ( 𝑎 ‘ 2 ) )
25 0zd ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 0 < ( 𝑎 ‘ 2 ) ↔ ( ( 𝑎 ‘ 1 ) Yrm 0 ) < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) )
28 24 27 mpbid ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) < ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) )
29 22 28 eqbrtrrd ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℕ )
32 eleq1 ⊢ ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) → ( ( 𝑎 ‘ 3 ) ∈ ℕ ↔ ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∈ ℕ ) )
33 31 32 syl5ibrcom ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) → ( 𝑎 ‘ 3 ) ∈ ℕ ) )
34 33 pm4.71rd ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( ( 𝑎 ‘ 3 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) ) )
35 simpllr ⊢ ( ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) )
36 simplr ⊢ ( ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) ∈ ℕ ) → ( 𝑎 ‘ 2 ) ∈ ℕ )
37 simpr ⊢ ( ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) = ( ( 𝑎 ‘ 1 ) Yrm 0 ) )
46 21 ad2antlr ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 1 ) Yrm 0 ) = 0 )
47 45 46 eqtrd ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) = 0 )
48 47 eqeq2d ⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 0 ) )
49 48 ex ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑎 ‘ 2 ) = 0 → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 0 ) ) )
50 49 pm5.32rd ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ∧ ( 𝑎 ‘ 2 ) = 0 ) ↔ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) ) )
51 43 50 orbi12d ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } = { 𝑎 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 3 ) )
66 55 56 64 65 mp3an ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) )
72 55 70 71 mp2an ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) ) } = { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) )
229 181 227 216 228 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) )
249 181 247 216 248 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 7 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 1 0 ) )
256 181 56 254 255 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 7 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 1 0 )
257 3anrabdioph ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 7 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) )
282 181 280 216 281 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 ‘ 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
296 181 241 294 295 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) } ∈ ( Dioph ‘ 1 0 ) )
300 181 234 298 299 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) } ∈ ( Dioph ‘ 1 0 )
301 3anrabdioph ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 ‘ 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 4 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) = 1 ∧ ( ( ( 𝑖 ‘ 6 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 1 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 5 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 7 ) ∈ ( ℤ≥ ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( ( 𝑖 ‘ 9 ) ↑ 2 ) − ( ( ( ( 𝑖 ‘ 7 ) ↑ 2 ) − 1 ) · ( ( 𝑖 ‘ 8 ) ↑ 2 ) ) ) = 1 ∧ ( 𝑖 ‘ 5 ) = ( ( ( 𝑖 ‘ 1 0 ) + 1 ) · ( 2 · ( ( 𝑖 ‘ 3 ) ↑ 2 ) ) ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 7 ) − ( 𝑖 ‘ 1 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) } ∈ ( Dioph ‘ 1 0 ) )
310 181 306 308 309 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) )
314 181 234 312 313 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 )
315 anrabdioph ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
316 310 314 315 mp2an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) )
323 181 306 321 322 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) } ∈ ( Dioph ‘ 1 0 ) )
325 181 319 221 324 mp3an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) } ∈ ( Dioph ‘ 1 0 )
326 anrabdioph ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) )
327 323 325 326 mp2an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 )
328 anrabdioph ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) )
329 316 327 328 mp2an ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 )
330 anrabdioph ⊢ ( ( { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 1 ... 1 0 ) ) ∣ ( ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 7 ) − 1 ) ∧ ( 𝑖 ‘ 6 ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 3 ) ) ) ∧ ( ( 2 · ( 𝑖 ‘ 3 ) ) ∥ ( ( 𝑖 ‘ 8 ) − ( 𝑖 ‘ 2 ) ) ∧ ( 𝑖 ‘ 2 ) ≤ ( 𝑖 ‘ 3 ) ) ) } ∈ ( Dioph ‘ 1 0 ) ) → { 𝑖 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ∧ { 𝑖 ∈ ( ℕ0 ↑m ( 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 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) )
340 55 338 339 mp2an ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 )
341 anrabdioph ⊢ ( ( { 𝑎 ∈ ( ℕ0 ↑m ( 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 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 ) )
344 55 70 343 mp2an ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 )
345 eq0rabdioph ⊢ ( ( 3 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 2 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 ) )
346 55 338 345 mp2an ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 )
347 anrabdioph ⊢ ( ( { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) } ∈ ( Dioph ‘ 3 ) )
348 344 346 347 mp2an ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) } ∈ ( Dioph ‘ 3 )
349 orrabdioph ⊢ ( ( { 𝑎 ∈ ( ℕ0 ↑m ( 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 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 3 ) = 0 ∧ ( 𝑎 ‘ 2 ) = 0 ) } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ( { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 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 ⊢ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) Yrm ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 )