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 ⊢a∈ℕ01…3|a⁡1∈ℤ≥2∧a⁡3=a⁡1Yrma⁡2∈Dioph⁡3

Proof

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