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 ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eldiophelnn0 ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) → 𝑁 ∈ ℕ0 )
2 nnex ℕ ∈ V
3 2 jctr ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) )
4 1z 1 ∈ ℤ
5 nnuz ℕ = ( ℤ ‘ 1 )
6 5 uzinf ( 1 ∈ ℤ → ¬ ℕ ∈ Fin )
7 4 6 ax-mp ¬ ℕ ∈ Fin
8 elfznn ( 𝑎 ∈ ( 1 ... 𝑁 ) → 𝑎 ∈ ℕ )
9 8 ssriv ( 1 ... 𝑁 ) ⊆ ℕ
10 7 9 pm3.2i ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ )
11 eldioph2b ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ) )
12 eldioph2b ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( 𝐵 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) )
13 11 12 anbi12d ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) ) )
14 3 10 13 sylancl ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) ) )
15 reeanv ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) )
16 unab ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) = { 𝑏 ∣ ( ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) }
17 r19.43 ( ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) ↔ ( ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) )
18 andi ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎𝑑 ) = 0 ∨ ( 𝑐𝑑 ) = 0 ) ) ↔ ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) )
19 zex ℤ ∈ V
20 nn0ssz 0 ⊆ ℤ
21 mapss ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0m ℕ ) ⊆ ( ℤ ↑m ℕ ) )
22 19 20 21 mp2an ( ℕ0m ℕ ) ⊆ ( ℤ ↑m ℕ )
23 22 sseli ( 𝑑 ∈ ( ℕ0m ℕ ) → 𝑑 ∈ ( ℤ ↑m ℕ ) )
24 23 adantl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → 𝑑 ∈ ( ℤ ↑m ℕ ) )
25 fveq2 ( 𝑒 = 𝑑 → ( 𝑎𝑒 ) = ( 𝑎𝑑 ) )
26 fveq2 ( 𝑒 = 𝑑 → ( 𝑐𝑒 ) = ( 𝑐𝑑 ) )
27 25 26 oveq12d ( 𝑒 = 𝑑 → ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) = ( ( 𝑎𝑑 ) · ( 𝑐𝑑 ) ) )
28 eqid ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) = ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) )
29 ovex ( ( 𝑎𝑑 ) · ( 𝑐𝑑 ) ) ∈ V
30 27 28 29 fvmpt ( 𝑑 ∈ ( ℤ ↑m ℕ ) → ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = ( ( 𝑎𝑑 ) · ( 𝑐𝑑 ) ) )
31 24 30 syl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = ( ( 𝑎𝑑 ) · ( 𝑐𝑑 ) ) )
32 31 eqeq1d ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ↔ ( ( 𝑎𝑑 ) · ( 𝑐𝑑 ) ) = 0 ) )
33 simplrl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → 𝑎 ∈ ( mzPoly ‘ ℕ ) )
34 mzpf ( 𝑎 ∈ ( mzPoly ‘ ℕ ) → 𝑎 : ( ℤ ↑m ℕ ) ⟶ ℤ )
35 33 34 syl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → 𝑎 : ( ℤ ↑m ℕ ) ⟶ ℤ )
36 35 24 ffvelrnd ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( 𝑎𝑑 ) ∈ ℤ )
37 36 zcnd ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( 𝑎𝑑 ) ∈ ℂ )
38 simplrr ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → 𝑐 ∈ ( mzPoly ‘ ℕ ) )
39 mzpf ( 𝑐 ∈ ( mzPoly ‘ ℕ ) → 𝑐 : ( ℤ ↑m ℕ ) ⟶ ℤ )
40 38 39 syl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → 𝑐 : ( ℤ ↑m ℕ ) ⟶ ℤ )
41 40 24 ffvelrnd ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( 𝑐𝑑 ) ∈ ℤ )
42 41 zcnd ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( 𝑐𝑑 ) ∈ ℂ )
43 37 42 mul0ord ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( ( ( 𝑎𝑑 ) · ( 𝑐𝑑 ) ) = 0 ↔ ( ( 𝑎𝑑 ) = 0 ∨ ( 𝑐𝑑 ) = 0 ) ) )
44 32 43 bitr2d ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( ( ( 𝑎𝑑 ) = 0 ∨ ( 𝑐𝑑 ) = 0 ) ↔ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) )
45 44 anbi2d ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎𝑑 ) = 0 ∨ ( 𝑐𝑑 ) = 0 ) ) ↔ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
46 18 45 bitr3id ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0m ℕ ) ) → ( ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) ↔ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
47 46 rexbidva ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) ↔ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
48 17 47 bitr3id ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) ↔ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
49 48 abbidv ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑏 ∣ ( ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) ) } = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } )
50 16 49 syl5eq ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } )
51 simpl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑁 ∈ ℕ0 )
52 2 9 pm3.2i ( ℕ ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ℕ )
53 52 a1i ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ℕ ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) )
54 simprl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑎 ∈ ( mzPoly ‘ ℕ ) )
55 54 34 syl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑎 : ( ℤ ↑m ℕ ) ⟶ ℤ )
56 55 feqmptd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑎 = ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( 𝑎𝑒 ) ) )
57 56 54 eqeltrrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( 𝑎𝑒 ) ) ∈ ( mzPoly ‘ ℕ ) )
58 simprr ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑐 ∈ ( mzPoly ‘ ℕ ) )
59 58 39 syl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑐 : ( ℤ ↑m ℕ ) ⟶ ℤ )
60 59 feqmptd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑐 = ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( 𝑐𝑒 ) ) )
61 60 58 eqeltrrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( 𝑐𝑒 ) ) ∈ ( mzPoly ‘ ℕ ) )
62 mzpmulmpt ( ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( 𝑎𝑒 ) ) ∈ ( mzPoly ‘ ℕ ) ∧ ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( 𝑐𝑒 ) ) ∈ ( mzPoly ‘ ℕ ) ) → ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ∈ ( mzPoly ‘ ℕ ) )
63 57 61 62 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ∈ ( mzPoly ‘ ℕ ) )
64 eldioph2 ( ( 𝑁 ∈ ℕ0 ∧ ( ℕ ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ∧ ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ∈ ( mzPoly ‘ ℕ ) ) → { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
65 51 53 63 64 syl3anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎𝑒 ) · ( 𝑐𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
66 50 65 eqeltrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) )
67 uneq12 ( ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) → ( 𝐴𝐵 ) = ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) )
68 67 eleq1d ( ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) → ( ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ↔ ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) ) )
69 66 68 syl5ibrcom ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
70 69 rexlimdvva ( 𝑁 ∈ ℕ0 → ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
71 15 70 syl5bir ( 𝑁 ∈ ℕ0 → ( ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐𝑑 ) = 0 ) } ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
72 14 71 sylbid ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
73 1 72 syl ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
74 73 anabsi5 ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) )