Metamath Proof Explorer

Theorem diophun

Description: If two sets are Diophantine, so is their union. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Assertion diophun 
|- ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A u. B ) e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 eldiophelnn0 
 |-  ( A e. ( Dioph ` N ) -> N e. NN0 )
2 nnex 
 |-  NN e. _V
3 2 jctr 
 |-  ( N e. NN0 -> ( N e. NN0 /\ NN e. _V ) )
4 1z 
 |-  1 e. ZZ
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 5 uzinf 
 |-  ( 1 e. ZZ -> -. NN e. Fin )
7 4 6 ax-mp 
 |-  -. NN e. Fin
8 elfznn 
 |-  ( a e. ( 1 ... N ) -> a e. NN )
9 8 ssriv 
 |-  ( 1 ... N ) C_ NN
10 7 9 pm3.2i 
 |-  ( -. NN e. Fin /\ ( 1 ... N ) C_ NN )
11 eldioph2b 
 |-  ( ( ( N e. NN0 /\ NN e. _V ) /\ ( -. NN e. Fin /\ ( 1 ... N ) C_ NN ) ) -> ( A e. ( Dioph ` N ) <-> E. a e. ( mzPoly ` NN ) A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } ) )
12 eldioph2b 
 |-  ( ( ( N e. NN0 /\ NN e. _V ) /\ ( -. NN e. Fin /\ ( 1 ... N ) C_ NN ) ) -> ( B e. ( Dioph ` N ) <-> E. c e. ( mzPoly ` NN ) B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) )
13 11 12 anbi12d 
 |-  ( ( ( N e. NN0 /\ NN e. _V ) /\ ( -. NN e. Fin /\ ( 1 ... N ) C_ NN ) ) -> ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) <-> ( E. a e. ( mzPoly ` NN ) A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ E. c e. ( mzPoly ` NN ) B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) ) )
14 3 10 13 sylancl 
 |-  ( N e. NN0 -> ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) <-> ( E. a e. ( mzPoly ` NN ) A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ E. c e. ( mzPoly ` NN ) B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) ) )
15 reeanv 
 |-  ( E. a e. ( mzPoly ` NN ) E. c e. ( mzPoly ` NN ) ( A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) <-> ( E. a e. ( mzPoly ` NN ) A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ E. c e. ( mzPoly ` NN ) B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) )
16 unab 
 |-  ( { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } u. { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) = { b | ( E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) }
17 r19.43 
 |-  ( E. d e. ( NN0 ^m NN ) ( ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) <-> ( E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) )
18 andi 
 |-  ( ( b = ( d |` ( 1 ... N ) ) /\ ( ( a ` d ) = 0 \/ ( c ` d ) = 0 ) ) <-> ( ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) )
19 zex 
 |-  ZZ e. _V
20 nn0ssz 
 |-  NN0 C_ ZZ
21 mapss 
 |-  ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m NN ) C_ ( ZZ ^m NN ) )
22 19 20 21 mp2an 
 |-  ( NN0 ^m NN ) C_ ( ZZ ^m NN )
23 22 sseli 
 |-  ( d e. ( NN0 ^m NN ) -> d e. ( ZZ ^m NN ) )
24 23 adantl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> d e. ( ZZ ^m NN ) )
25 fveq2 
 |-  ( e = d -> ( a ` e ) = ( a ` d ) )
26 fveq2 
 |-  ( e = d -> ( c ` e ) = ( c ` d ) )
27 25 26 oveq12d 
 |-  ( e = d -> ( ( a ` e ) x. ( c ` e ) ) = ( ( a ` d ) x. ( c ` d ) ) )
28 eqid 
 |-  ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) = ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) )
29 ovex 
 |-  ( ( a ` d ) x. ( c ` d ) ) e. _V
30 27 28 29 fvmpt 
 |-  ( d e. ( ZZ ^m NN ) -> ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = ( ( a ` d ) x. ( c ` d ) ) )
31 24 30 syl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = ( ( a ` d ) x. ( c ` d ) ) )
32 31 eqeq1d 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 <-> ( ( a ` d ) x. ( c ` d ) ) = 0 ) )
33 simplrl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> a e. ( mzPoly ` NN ) )
34 mzpf 
 |-  ( a e. ( mzPoly ` NN ) -> a : ( ZZ ^m NN ) --> ZZ )
35 33 34 syl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> a : ( ZZ ^m NN ) --> ZZ )
36 35 24 ffvelcdmd 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( a ` d ) e. ZZ )
37 36 zcnd 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( a ` d ) e. CC )
38 simplrr 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> c e. ( mzPoly ` NN ) )
39 mzpf 
 |-  ( c e. ( mzPoly ` NN ) -> c : ( ZZ ^m NN ) --> ZZ )
40 38 39 syl 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> c : ( ZZ ^m NN ) --> ZZ )
41 40 24 ffvelcdmd 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( c ` d ) e. ZZ )
42 41 zcnd 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( c ` d ) e. CC )
43 37 42 mul0ord 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( ( ( a ` d ) x. ( c ` d ) ) = 0 <-> ( ( a ` d ) = 0 \/ ( c ` d ) = 0 ) ) )
44 32 43 bitr2d 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( ( ( a ` d ) = 0 \/ ( c ` d ) = 0 ) <-> ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) )
45 44 anbi2d 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( ( b = ( d |` ( 1 ... N ) ) /\ ( ( a ` d ) = 0 \/ ( c ` d ) = 0 ) ) <-> ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) ) )
46 18 45 bitr3id 
 |-  ( ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) /\ d e. ( NN0 ^m NN ) ) -> ( ( ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) <-> ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) ) )
47 46 rexbidva 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( E. d e. ( NN0 ^m NN ) ( ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) <-> E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) ) )
48 17 47 bitr3id 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( ( E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) <-> E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) ) )
49 48 abbidv 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> { b | ( E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) \/ E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) ) } = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) } )
50 16 49 eqtrid 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } u. { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) } )
51 simpl 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> N e. NN0 )
52 2 9 pm3.2i 
 |-  ( NN e. _V /\ ( 1 ... N ) C_ NN )
53 52 a1i 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( NN e. _V /\ ( 1 ... N ) C_ NN ) )
54 simprl 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> a e. ( mzPoly ` NN ) )
55 54 34 syl 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> a : ( ZZ ^m NN ) --> ZZ )
56 55 feqmptd 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> a = ( e e. ( ZZ ^m NN ) |-> ( a ` e ) ) )
57 56 54 eqeltrrd 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( e e. ( ZZ ^m NN ) |-> ( a ` e ) ) e. ( mzPoly ` NN ) )
58 simprr 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> c e. ( mzPoly ` NN ) )
59 58 39 syl 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> c : ( ZZ ^m NN ) --> ZZ )
60 59 feqmptd 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> c = ( e e. ( ZZ ^m NN ) |-> ( c ` e ) ) )
61 60 58 eqeltrrd 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( e e. ( ZZ ^m NN ) |-> ( c ` e ) ) e. ( mzPoly ` NN ) )
62 mzpmulmpt 
 |-  ( ( ( e e. ( ZZ ^m NN ) |-> ( a ` e ) ) e. ( mzPoly ` NN ) /\ ( e e. ( ZZ ^m NN ) |-> ( c ` e ) ) e. ( mzPoly ` NN ) ) -> ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) e. ( mzPoly ` NN ) )
63 57 61 62 syl2anc 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) e. ( mzPoly ` NN ) )
64 eldioph2 
 |-  ( ( N e. NN0 /\ ( NN e. _V /\ ( 1 ... N ) C_ NN ) /\ ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) e. ( mzPoly ` NN ) ) -> { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) } e. ( Dioph ` N ) )
65 51 53 63 64 syl3anc 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( ( e e. ( ZZ ^m NN ) |-> ( ( a ` e ) x. ( c ` e ) ) ) ` d ) = 0 ) } e. ( Dioph ` N ) )
66 50 65 eqeltrd 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } u. { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) e. ( Dioph ` N ) )
67 uneq12 
 |-  ( ( A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) -> ( A u. B ) = ( { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } u. { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) )
68 67 eleq1d 
 |-  ( ( A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) -> ( ( A u. B ) e. ( Dioph ` N ) <-> ( { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } u. { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) e. ( Dioph ` N ) ) )
69 66 68 syl5ibrcom 
 |-  ( ( N e. NN0 /\ ( a e. ( mzPoly ` NN ) /\ c e. ( mzPoly ` NN ) ) ) -> ( ( A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) -> ( A u. B ) e. ( Dioph ` N ) ) )
70 69 rexlimdvva 
 |-  ( N e. NN0 -> ( E. a e. ( mzPoly ` NN ) E. c e. ( mzPoly ` NN ) ( A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) -> ( A u. B ) e. ( Dioph ` N ) ) )
71 15 70 biimtrrid 
 |-  ( N e. NN0 -> ( ( E. a e. ( mzPoly ` NN ) A = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( a ` d ) = 0 ) } /\ E. c e. ( mzPoly ` NN ) B = { b | E. d e. ( NN0 ^m NN ) ( b = ( d |` ( 1 ... N ) ) /\ ( c ` d ) = 0 ) } ) -> ( A u. B ) e. ( Dioph ` N ) ) )
72 14 71 sylbid 
 |-  ( N e. NN0 -> ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A u. B ) e. ( Dioph ` N ) ) )
73 1 72 syl 
 |-  ( A e. ( Dioph ` N ) -> ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A u. B ) e. ( Dioph ` N ) ) )
74 73 anabsi5 
 |-  ( ( A e. ( Dioph ` N ) /\ B e. ( Dioph ` N ) ) -> ( A u. B ) e. ( Dioph ` N ) )