Metamath Proof Explorer

Theorem dvdsrabdioph

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

Ref Expression
Assertion dvdsrabdioph ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→t∈ℕ01…N|A∥B∈Dioph⁡N

Proof

Step Hyp Ref Expression
1 rabdiophlem1 ⊢t∈ℤ1…N⟼A∈mzPoly⁡1…N→∀t∈ℕ01…NA∈ℤ
2 rabdiophlem1 ⊢t∈ℤ1…N⟼B∈mzPoly⁡1…N→∀t∈ℕ01…NB∈ℤ
3 divides ⊢A∈ℤ∧B∈ℤ→A∥B↔∃a∈ℤa⁢A=B
4 oveq1 ⊢a=b→a⁢A=b⁢A
5 4 eqeq1d ⊢a=b→a⁢A=B↔b⁢A=B
6 oveq1 ⊢a=−b→a⁢A=−b⁢A
7 6 eqeq1d ⊢a=−b→a⁢A=B↔−b⁢A=B
8 5 7 rexzrexnn0 ⊢∃a∈ℤa⁢A=B↔∃b∈ℕ0b⁢A=B∨−b⁢A=B
9 3 8 bitrdi ⊢A∈ℤ∧B∈ℤ→A∥B↔∃b∈ℕ0b⁢A=B∨−b⁢A=B
10 9 ralimi ⊢∀t∈ℕ01…NA∈ℤ∧B∈ℤ→∀t∈ℕ01…NA∥B↔∃b∈ℕ0b⁢A=B∨−b⁢A=B
11 r19.26 ⊢∀t∈ℕ01…NA∈ℤ∧B∈ℤ↔∀t∈ℕ01…NA∈ℤ∧∀t∈ℕ01…NB∈ℤ
12 rabbi ⊢∀t∈ℕ01…NA∥B↔∃b∈ℕ0b⁢A=B∨−b⁢A=B↔t∈ℕ01…N|A∥B=t∈ℕ01…N|∃b∈ℕ0b⁢A=B∨−b⁢A=B
13 10 11 12 3imtr3i ⊢∀t∈ℕ01…NA∈ℤ∧∀t∈ℕ01…NB∈ℤ→t∈ℕ01…N|A∥B=t∈ℕ01…N|∃b∈ℕ0b⁢A=B∨−b⁢A=B
14 1 2 13 syl2an ⊢t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→t∈ℕ01…N|A∥B=t∈ℕ01…N|∃b∈ℕ0b⁢A=B∨−b⁢A=B
15 14 3adant1 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→t∈ℕ01…N|A∥B=t∈ℕ01…N|∃b∈ℕ0b⁢A=B∨−b⁢A=B
16 nfcv ⊢Ⅎ_tℕ01…N
17 nfcv ⊢Ⅎ_aℕ01…N
18 nfv ⊢Ⅎa∃b∈ℕ0b⁢A=B∨−b⁢A=B
19 nfcv ⊢Ⅎ_tℕ0
20 nfcv ⊢Ⅎ_tb
21 nfcv ⊢Ⅎ_t×
22 nfcsb1v ⊢Ⅎ_t⦋a/t⦌A
23 20 21 22 nfov ⊢Ⅎ_tb⁢⦋a/t⦌A
24 nfcsb1v ⊢Ⅎ_t⦋a/t⦌B
25 23 24 nfeq ⊢Ⅎtb⁢⦋a/t⦌A=⦋a/t⦌B
26 nfcv ⊢Ⅎ_t−b
27 26 21 22 nfov ⊢Ⅎ_t−b⁢⦋a/t⦌A
28 27 24 nfeq ⊢Ⅎt−b⁢⦋a/t⦌A=⦋a/t⦌B
29 25 28 nfor ⊢Ⅎtb⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B
30 19 29 nfrexw ⊢Ⅎt∃b∈ℕ0b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B
31 csbeq1a ⊢t=a→A=⦋a/t⦌A
32 31 oveq2d ⊢t=a→b⁢A=b⁢⦋a/t⦌A
33 csbeq1a ⊢t=a→B=⦋a/t⦌B
34 32 33 eqeq12d ⊢t=a→b⁢A=B↔b⁢⦋a/t⦌A=⦋a/t⦌B
35 31 oveq2d ⊢t=a→−b⁢A=−b⁢⦋a/t⦌A
36 35 33 eqeq12d ⊢t=a→−b⁢A=B↔−b⁢⦋a/t⦌A=⦋a/t⦌B
37 34 36 orbi12d ⊢t=a→b⁢A=B∨−b⁢A=B↔b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B
38 37 rexbidv ⊢t=a→∃b∈ℕ0b⁢A=B∨−b⁢A=B↔∃b∈ℕ0b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B
39 16 17 18 30 38 cbvrabw ⊢t∈ℕ01…N|∃b∈ℕ0b⁢A=B∨−b⁢A=B=a∈ℕ01…N|∃b∈ℕ0b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B
40 simp1 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→N∈ℕ0
41 peano2nn0 ⊢N∈ℕ0→N+1∈ℕ0
42 41 3ad2ant1 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→N+1∈ℕ0
43 ovex ⊢1…N+1∈V
44 nn0p1nn ⊢N∈ℕ0→N+1∈ℕ
45 elfz1end ⊢N+1∈ℕ↔N+1∈1…N+1
46 44 45 sylib ⊢N∈ℕ0→N+1∈1…N+1
47 mzpproj ⊢1…N+1∈V∧N+1∈1…N+1→c∈ℤ1…N+1⟼c⁡N+1∈mzPoly⁡1…N+1
48 43 46 47 sylancr ⊢N∈ℕ0→c∈ℤ1…N+1⟼c⁡N+1∈mzPoly⁡1…N+1
49 48 adantr ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→c∈ℤ1…N+1⟼c⁡N+1∈mzPoly⁡1…N+1
50 eqid ⊢N+1=N+1
51 50 rabdiophlem2 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→c∈ℤ1…N+1⟼⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
52 mzpmulmpt ⊢c∈ℤ1…N+1⟼c⁡N+1∈mzPoly⁡1…N+1∧c∈ℤ1…N+1⟼⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1→c∈ℤ1…N+1⟼c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
53 49 51 52 syl2anc ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→c∈ℤ1…N+1⟼c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
54 53 3adant3 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℤ1…N+1⟼c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
55 50 rabdiophlem2 ⊢N∈ℕ0∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℤ1…N+1⟼⦋c↾1…N/t⦌B∈mzPoly⁡1…N+1
56 55 3adant2 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℤ1…N+1⟼⦋c↾1…N/t⦌B∈mzPoly⁡1…N+1
57 eqrabdioph ⊢N+1∈ℕ0∧c∈ℤ1…N+1⟼c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1∧c∈ℤ1…N+1⟼⦋c↾1…N/t⦌B∈mzPoly⁡1…N+1→c∈ℕ01…N+1|c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1
58 42 54 56 57 syl3anc ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℕ01…N+1|c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1
59 mzpnegmpt ⊢c∈ℤ1…N+1⟼c⁡N+1∈mzPoly⁡1…N+1→c∈ℤ1…N+1⟼−c⁡N+1∈mzPoly⁡1…N+1
60 49 59 syl ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→c∈ℤ1…N+1⟼−c⁡N+1∈mzPoly⁡1…N+1
61 mzpmulmpt ⊢c∈ℤ1…N+1⟼−c⁡N+1∈mzPoly⁡1…N+1∧c∈ℤ1…N+1⟼⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1→c∈ℤ1…N+1⟼−c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
62 60 51 61 syl2anc ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N→c∈ℤ1…N+1⟼−c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
63 62 3adant3 ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℤ1…N+1⟼−c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1
64 eqrabdioph ⊢N+1∈ℕ0∧c∈ℤ1…N+1⟼−c⁡N+1⁢⦋c↾1…N/t⦌A∈mzPoly⁡1…N+1∧c∈ℤ1…N+1⟼⦋c↾1…N/t⦌B∈mzPoly⁡1…N+1→c∈ℕ01…N+1|−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1
65 42 63 56 64 syl3anc ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℕ01…N+1|−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1
66 orrabdioph ⊢c∈ℕ01…N+1|c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1∧c∈ℕ01…N+1|−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1→c∈ℕ01…N+1|c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∨−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1
67 58 65 66 syl2anc ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→c∈ℕ01…N+1|c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∨−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1
68 oveq1 ⊢b=c⁡N+1→b⁢⦋a/t⦌A=c⁡N+1⁢⦋a/t⦌A
69 68 eqeq1d ⊢b=c⁡N+1→b⁢⦋a/t⦌A=⦋a/t⦌B↔c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B
70 negeq ⊢b=c⁡N+1→−b=−c⁡N+1
71 70 oveq1d ⊢b=c⁡N+1→−b⁢⦋a/t⦌A=−c⁡N+1⁢⦋a/t⦌A
72 71 eqeq1d ⊢b=c⁡N+1→−b⁢⦋a/t⦌A=⦋a/t⦌B↔−c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B
73 69 72 orbi12d ⊢b=c⁡N+1→b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B↔c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B∨−c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B
74 csbeq1 ⊢a=c↾1…N→⦋a/t⦌A=⦋c↾1…N/t⦌A
75 74 oveq2d ⊢a=c↾1…N→c⁡N+1⁢⦋a/t⦌A=c⁡N+1⁢⦋c↾1…N/t⦌A
76 csbeq1 ⊢a=c↾1…N→⦋a/t⦌B=⦋c↾1…N/t⦌B
77 75 76 eqeq12d ⊢a=c↾1…N→c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B↔c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B
78 74 oveq2d ⊢a=c↾1…N→−c⁡N+1⁢⦋a/t⦌A=−c⁡N+1⁢⦋c↾1…N/t⦌A
79 78 76 eqeq12d ⊢a=c↾1…N→−c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B↔−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B
80 77 79 orbi12d ⊢a=c↾1…N→c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B∨−c⁡N+1⁢⦋a/t⦌A=⦋a/t⦌B↔c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∨−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B
81 50 73 80 rexrabdioph ⊢N∈ℕ0∧c∈ℕ01…N+1|c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∨−c⁡N+1⁢⦋c↾1…N/t⦌A=⦋c↾1…N/t⦌B∈Dioph⁡N+1→a∈ℕ01…N|∃b∈ℕ0b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B∈Dioph⁡N
82 40 67 81 syl2anc ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→a∈ℕ01…N|∃b∈ℕ0b⁢⦋a/t⦌A=⦋a/t⦌B∨−b⁢⦋a/t⦌A=⦋a/t⦌B∈Dioph⁡N
83 39 82 eqeltrid ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→t∈ℕ01…N|∃b∈ℕ0b⁢A=B∨−b⁢A=B∈Dioph⁡N
84 15 83 eqeltrd ⊢N∈ℕ0∧t∈ℤ1…N⟼A∈mzPoly⁡1…N∧t∈ℤ1…N⟼B∈mzPoly⁡1…N→t∈ℕ01…N|A∥B∈Dioph⁡N