Metamath Proof Explorer

Theorem dvdsrabdioph

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

Ref Expression
Assertion dvdsrabdioph 
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 rabdiophlem1 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ )
2 rabdiophlem1 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ )
3 divides 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> E. a e. ZZ ( a x. A ) = B ) )
4 oveq1 
 |-  ( a = b -> ( a x. A ) = ( b x. A ) )
5 4 eqeq1d 
 |-  ( a = b -> ( ( a x. A ) = B <-> ( b x. A ) = B ) )
6 oveq1 
 |-  ( a = -u b -> ( a x. A ) = ( -u b x. A ) )
7 6 eqeq1d 
 |-  ( a = -u b -> ( ( a x. A ) = B <-> ( -u b x. A ) = B ) )
8 5 7 rexzrexnn0 
 |-  ( E. a e. ZZ ( a x. A ) = B <-> E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) )
9 3 8 bitrdi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) ) )
10 9 ralimi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ZZ /\ B e. ZZ ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A || B <-> E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) ) )
11 r19.26 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ZZ /\ B e. ZZ ) <-> ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ ) )
12 rabbi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A || B <-> E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) } )
13 10 11 12 3imtr3i 
 |-  ( ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) } )
14 1 2 13 syl2an 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) } )
15 14 3adant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } = { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) } )
16 nfcv 
 |-  F/_ t ( NN0 ^m ( 1 ... N ) )
17 nfcv 
 |-  F/_ a ( NN0 ^m ( 1 ... N ) )
18 nfv 
 |-  F/ a E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B )
19 nfcv 
 |-  F/_ t NN0
20 nfcv 
 |-  F/_ t b
21 nfcv 
 |-  F/_ t x.
22 nfcsb1v 
 |-  F/_ t [_ a / t ]_ A
23 20 21 22 nfov 
 |-  F/_ t ( b x. [_ a / t ]_ A )
24 nfcsb1v 
 |-  F/_ t [_ a / t ]_ B
25 23 24 nfeq 
 |-  F/ t ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B
26 nfcv 
 |-  F/_ t -u b
27 26 21 22 nfov 
 |-  F/_ t ( -u b x. [_ a / t ]_ A )
28 27 24 nfeq 
 |-  F/ t ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B
29 25 28 nfor 
 |-  F/ t ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B )
30 19 29 nfrexw 
 |-  F/ t E. b e. NN0 ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B )
31 csbeq1a 
 |-  ( t = a -> A = [_ a / t ]_ A )
32 31 oveq2d 
 |-  ( t = a -> ( b x. A ) = ( b x. [_ a / t ]_ A ) )
33 csbeq1a 
 |-  ( t = a -> B = [_ a / t ]_ B )
34 32 33 eqeq12d 
 |-  ( t = a -> ( ( b x. A ) = B <-> ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) )
35 31 oveq2d 
 |-  ( t = a -> ( -u b x. A ) = ( -u b x. [_ a / t ]_ A ) )
36 35 33 eqeq12d 
 |-  ( t = a -> ( ( -u b x. A ) = B <-> ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) )
37 34 36 orbi12d 
 |-  ( t = a -> ( ( ( b x. A ) = B \/ ( -u b x. A ) = B ) <-> ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) ) )
38 37 rexbidv 
 |-  ( t = a -> ( E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) <-> E. b e. NN0 ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) ) )
39 16 17 18 30 38 cbvrabw 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) } = { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) }
40 simp1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> N e. NN0 )
41 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
42 41 3ad2ant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( N + 1 ) e. NN0 )
43 ovex 
 |-  ( 1 ... ( N + 1 ) ) e. _V
44 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
45 elfz1end 
 |-  ( ( N + 1 ) e. NN <-> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
46 44 45 sylib 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
47 mzpproj 
 |-  ( ( ( 1 ... ( N + 1 ) ) e. _V /\ ( N + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
48 43 46 47 sylancr 
 |-  ( N e. NN0 -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
49 48 adantr 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
50 eqid 
 |-  ( N + 1 ) = ( N + 1 )
51 50 rabdiophlem2 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ A ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
52 mzpmulmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ A ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
53 49 51 52 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
54 53 3adant3 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
55 50 rabdiophlem2 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ B ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
56 55 3adant2 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ B ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
57 eqrabdioph 
 |-  ( ( ( N + 1 ) e. NN0 /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ B ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B } e. ( Dioph ` ( N + 1 ) ) )
58 42 54 56 57 syl3anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B } e. ( Dioph ` ( N + 1 ) ) )
59 mzpnegmpt 
 |-  ( ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> -u ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
60 49 59 syl 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> -u ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
61 mzpmulmpt 
 |-  ( ( ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> -u ( c ` ( N + 1 ) ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ A ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
62 60 51 61 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
63 62 3adant3 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) )
64 eqrabdioph 
 |-  ( ( ( N + 1 ) e. NN0 /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) /\ ( c e. ( ZZ ^m ( 1 ... ( N + 1 ) ) ) |-> [_ ( c |` ( 1 ... N ) ) / t ]_ B ) e. ( mzPoly ` ( 1 ... ( N + 1 ) ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B } e. ( Dioph ` ( N + 1 ) ) )
65 42 63 56 64 syl3anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B } e. ( Dioph ` ( N + 1 ) ) )
66 orrabdioph 
 |-  ( ( { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B } e. ( Dioph ` ( N + 1 ) ) /\ { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B } e. ( Dioph ` ( N + 1 ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B \/ ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B ) } e. ( Dioph ` ( N + 1 ) ) )
67 58 65 66 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B \/ ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B ) } e. ( Dioph ` ( N + 1 ) ) )
68 oveq1 
 |-  ( b = ( c ` ( N + 1 ) ) -> ( b x. [_ a / t ]_ A ) = ( ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) )
69 68 eqeq1d 
 |-  ( b = ( c ` ( N + 1 ) ) -> ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B <-> ( ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B ) )
70 negeq 
 |-  ( b = ( c ` ( N + 1 ) ) -> -u b = -u ( c ` ( N + 1 ) ) )
71 70 oveq1d 
 |-  ( b = ( c ` ( N + 1 ) ) -> ( -u b x. [_ a / t ]_ A ) = ( -u ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) )
72 71 eqeq1d 
 |-  ( b = ( c ` ( N + 1 ) ) -> ( ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B <-> ( -u ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B ) )
73 69 72 orbi12d 
 |-  ( b = ( c ` ( N + 1 ) ) -> ( ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) <-> ( ( ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u ( c ` ( N + 1 ) ) x. [_ 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 ) ) x. [_ a / t ]_ A ) = ( ( c ` ( N + 1 ) ) x. [_ ( 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 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B <-> ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B ) )
78 74 oveq2d 
 |-  ( a = ( c |` ( 1 ... N ) ) -> ( -u ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) )
79 78 76 eqeq12d 
 |-  ( a = ( c |` ( 1 ... N ) ) -> ( ( -u ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B <-> ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B ) )
80 77 79 orbi12d 
 |-  ( a = ( c |` ( 1 ... N ) ) -> ( ( ( ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u ( c ` ( N + 1 ) ) x. [_ a / t ]_ A ) = [_ a / t ]_ B ) <-> ( ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B \/ ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B ) ) )
81 50 73 80 rexrabdioph 
 |-  ( ( N e. NN0 /\ { c e. ( NN0 ^m ( 1 ... ( N + 1 ) ) ) | ( ( ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B \/ ( -u ( c ` ( N + 1 ) ) x. [_ ( c |` ( 1 ... N ) ) / t ]_ A ) = [_ ( c |` ( 1 ... N ) ) / t ]_ B ) } e. ( Dioph ` ( N + 1 ) ) ) -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) } e. ( Dioph ` N ) )
82 40 67 81 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { a e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. [_ a / t ]_ A ) = [_ a / t ]_ B \/ ( -u b x. [_ a / t ]_ A ) = [_ a / t ]_ B ) } e. ( Dioph ` N ) )
83 39 82 eqeltrid 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | E. b e. NN0 ( ( b x. A ) = B \/ ( -u b x. A ) = B ) } e. ( Dioph ` N ) )
84 15 83 eqeltrd 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } e. ( Dioph ` N ) )