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 ‘ 𝑁 ) )