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 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∥ 𝐵 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rabdiophlem1 ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
2 rabdiophlem1 ⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 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 ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∥ 𝐵 ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ) )
11 r19.26 ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ↔ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) )
12 rabbi ⊢ ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ( 𝐴 ∥ 𝐵 ↔ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) ) ↔ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∥ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
13 10 11 12 3imtr3i ⊢ ( ( ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ∧ ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐵 ∈ ℤ ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∥ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
14 1 2 13 syl2an ⊢ ( ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∥ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
15 14 3adant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∥ 𝐵 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } )
16 nfcv ⊢ Ⅎ 𝑡 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
17 nfcv ⊢ Ⅎ 𝑎 ( ℕ0 ↑m ( 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 nfrexw ⊢ Ⅎ 𝑡 ∃ 𝑏 ∈ ℕ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 ⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } = { 𝑎 ∈ ( ℕ0 ↑m ( 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 ) ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
58 42 54 56 57 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 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 ) ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
65 42 63 56 64 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
66 orrabdioph ⊢ ( ( { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ∧ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 ) } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
67 58 65 66 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 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 ∧ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 ∨ ( - ( 𝑐 ‘ ( 𝑁 + 1 ) ) · ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐵 ) } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) = ⦋ 𝑎 / 𝑡 ⦌ 𝐵 ∨ ( - 𝑏 · ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) = ⦋ 𝑎 / 𝑡 ⦌ 𝐵 ) } ∈ ( Dioph ‘ 𝑁 ) )
82 40 67 81 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) = ⦋ 𝑎 / 𝑡 ⦌ 𝐵 ∨ ( - 𝑏 · ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) = ⦋ 𝑎 / 𝑡 ⦌ 𝐵 ) } ∈ ( Dioph ‘ 𝑁 ) )
83 39 82 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 ( ( 𝑏 · 𝐴 ) = 𝐵 ∨ ( - 𝑏 · 𝐴 ) = 𝐵 ) } ∈ ( Dioph ‘ 𝑁 ) )
84 15 83 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐵 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∥ 𝐵 } ∈ ( Dioph ‘ 𝑁 ) )