Metamath Proof Explorer


Theorem dvdsrabdioph

Description: Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014)

Ref Expression
Assertion dvdsrabdioph ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rabdiophlem1 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
2 rabdiophlem1 ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ )
3 divides ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴𝐵 ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · 𝐴 ) = 𝐵 ) )
4 oveq1 ( 𝑎 = 𝑏 → ( 𝑎 · 𝐴 ) = ( 𝑏 · 𝐴 ) )
5 4 eqeq1d ( 𝑎 = 𝑏 → ( ( 𝑎 · 𝐴 ) = 𝐵 ↔ ( 𝑏 · 𝐴 ) = 𝐵 ) )
6 oveq1 ( 𝑎 = - 𝑏 → ( 𝑎 · 𝐴 ) = ( - 𝑏 · 𝐴 ) )
7 6 eqeq1d ( 𝑎 = - 𝑏 → ( ( 𝑎 · 𝐴 ) = 𝐵 ↔ ( - 𝑏 · 𝐴 ) = 𝐵 ) )
8 5 7 rexzrexnn0 ( ∃ 𝑎 ∈ ℤ ( 𝑎 · 𝐴 ) = 𝐵 ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) )
9 3 8 bitrdi ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴𝐵 ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ) )
10 9 ralimi ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴𝐵 ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ) )
11 r19.26 ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) )
12 rabbi ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ( 𝐴𝐵 ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ) ↔ { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
13 10 11 12 3imtr3i ( ( ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
14 1 2 13 syl2an ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
15 14 3adant1 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } = { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
16 nfcv 𝑡 ( ℕ0m ( 1 ... 𝑁 ) )
17 nfcv 𝑎 ( ℕ0m ( 1 ... 𝑁 ) )
18 nfv 𝑎𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 )
19 nfcv 𝑡0
20 nfcv 𝑡 𝑏
21 nfcv 𝑡 ·
22 nfcsb1v 𝑡 𝑎 / 𝑡 𝐴
23 20 21 22 nfov 𝑡 ( 𝑏 · 𝑎 / 𝑡 𝐴 )
24 nfcsb1v 𝑡 𝑎 / 𝑡 𝐵
25 23 24 nfeq 𝑡 ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵
26 nfcv 𝑡 - 𝑏
27 26 21 22 nfov 𝑡 ( - 𝑏 · 𝑎 / 𝑡 𝐴 )
28 27 24 nfeq 𝑡 ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵
29 25 28 nfor 𝑡 ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 )
30 19 29 nfrex 𝑡𝑏 ∈ ℕ0 ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 )
31 csbeq1a ( 𝑡 = 𝑎𝐴 = 𝑎 / 𝑡 𝐴 )
32 31 oveq2d ( 𝑡 = 𝑎 → ( 𝑏 · 𝐴 ) = ( 𝑏 · 𝑎 / 𝑡 𝐴 ) )
33 csbeq1a ( 𝑡 = 𝑎𝐵 = 𝑎 / 𝑡 𝐵 )
34 32 33 eqeq12d ( 𝑡 = 𝑎 → ( ( 𝑏 · 𝐴 ) = 𝐵 ↔ ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) )
35 31 oveq2d ( 𝑡 = 𝑎 → ( - 𝑏 · 𝐴 ) = ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) )
36 35 33 eqeq12d ( 𝑡 = 𝑎 → ( ( - 𝑏 · 𝐴 ) = 𝐵 ↔ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) )
37 34 36 orbi12d ( 𝑡 = 𝑎 → ( ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ↔ ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) ) )
38 37 rexbidv ( 𝑡 = 𝑎 → ( ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) ) )
39 16 17 18 30 38 cbvrabw { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } = { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) }
40 simp1 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
41 peano2nn0 ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
42 41 3ad2ant1 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
43 ovex ( 1 ... ( 𝑁 + 1 ) ) ∈ V
44 nn0p1nn ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
45 elfz1end ( ( 𝑁 + 1 ) ∈ ℕ ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
46 44 45 sylib ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
47 mzpproj ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ V ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
48 43 46 47 sylancr ( 𝑁 ∈ ℕ0 → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
49 48 adantr ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
50 eqid ( 𝑁 + 1 ) = ( 𝑁 + 1 )
51 50 rabdiophlem2 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
52 mzpmulmpt ( ( ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
53 49 51 52 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
54 53 3adant3 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
55 50 rabdiophlem2 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
56 55 3adant2 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
57 eqrabdioph ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) → { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
58 42 54 56 57 syl3anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
59 mzpnegmpt ( ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ - ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
60 49 59 syl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ - ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
61 mzpmulmpt ( ( ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ - ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
62 60 51 61 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
63 62 3adant3 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
64 eqrabdioph ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) → { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
65 42 63 56 64 syl3anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
66 orrabdioph ( ( { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ∧ { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ) → { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
67 58 65 66 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
68 oveq1 ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) )
69 68 eqeq1d ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ↔ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) )
70 negeq ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → - 𝑏 = - ( 𝑐 ‘ ( 𝑁 + 1 ) ) )
71 70 oveq1d ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) )
72 71 eqeq1d ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → ( ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ↔ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) )
73 69 72 orbi12d ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → ( ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) ↔ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) ) )
74 csbeq1 ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → 𝑎 / 𝑡 𝐴 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 )
75 74 oveq2d ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) )
76 csbeq1 ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → 𝑎 / 𝑡 𝐵 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 )
77 75 76 eqeq12d ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ↔ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) )
78 74 oveq2d ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) )
79 78 76 eqeq12d ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ( ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ↔ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) )
80 77 79 orbi12d ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) ↔ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) ) )
81 50 73 80 rexrabdioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑐 ∈ ( ℕ0m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐴 ) = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 𝐵 ) } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) } ∈ ( Dioph ‘ 𝑁 ) )
82 40 67 81 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ∨ ( - 𝑏 · 𝑎 / 𝑡 𝐴 ) = 𝑎 / 𝑡 𝐵 ) } ∈ ( Dioph ‘ 𝑁 ) )
83 39 82 eqeltrid ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } ∈ ( Dioph ‘ 𝑁 ) )
84 15 83 eqeltrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0m ( 1 ... 𝑁 ) ) ∣ 𝐴𝐵 } ∈ ( Dioph ‘ 𝑁 ) )