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 Dioph N B Dioph N A B Dioph N

Proof

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