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 ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ) )
12 eldioph2b ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( 𝐵 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) )
13 11 12 anbi12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) ) )
14 3 10 13 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) ) )
15 reeanv ⊢ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) )
16 unab ⊢ ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) = { 𝑏 ∣ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) }
17 r19.43 ⊢ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) ↔ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) )
18 andi ⊢ ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ 𝑑 ) = 0 ∨ ( 𝑐 ‘ 𝑑 ) = 0 ) ) ↔ ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) )
19 zex ⊢ ℤ ∈ V
20 nn0ssz ⊢ ℕ0 ⊆ ℤ
21 mapss ⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m ℕ ) ⊆ ( ℤ ↑m ℕ ) )
22 19 20 21 mp2an ⊢ ( ℕ0 ↑m ℕ ) ⊆ ( ℤ ↑m ℕ )
23 22 sseli ⊢ ( 𝑑 ∈ ( ℕ0 ↑m ℕ ) → 𝑑 ∈ ( ℤ ↑m ℕ ) )
24 23 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → 𝑑 ∈ ( ℤ ↑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 ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = ( ( 𝑎 ‘ 𝑑 ) · ( 𝑐 ‘ 𝑑 ) ) )
32 31 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ↔ ( ( 𝑎 ‘ 𝑑 ) · ( 𝑐 ‘ 𝑑 ) ) = 0 ) )
33 simplrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → 𝑎 ∈ ( mzPoly ‘ ℕ ) )
34 mzpf ⊢ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) → 𝑎 : ( ℤ ↑m ℕ ) ⟶ ℤ )
35 33 34 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → 𝑎 : ( ℤ ↑m ℕ ) ⟶ ℤ )
36 35 24 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( 𝑎 ‘ 𝑑 ) ∈ ℤ )
37 36 zcnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( 𝑎 ‘ 𝑑 ) ∈ ℂ )
38 simplrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → 𝑐 ∈ ( mzPoly ‘ ℕ ) )
39 mzpf ⊢ ( 𝑐 ∈ ( mzPoly ‘ ℕ ) → 𝑐 : ( ℤ ↑m ℕ ) ⟶ ℤ )
40 38 39 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → 𝑐 : ( ℤ ↑m ℕ ) ⟶ ℤ )
41 40 24 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( 𝑐 ‘ 𝑑 ) ∈ ℤ )
42 41 zcnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( 𝑐 ‘ 𝑑 ) ∈ ℂ )
43 37 42 mul0ord ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( ( 𝑎 ‘ 𝑑 ) · ( 𝑐 ‘ 𝑑 ) ) = 0 ↔ ( ( 𝑎 ‘ 𝑑 ) = 0 ∨ ( 𝑐 ‘ 𝑑 ) = 0 ) ) )
44 32 43 bitr2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( ( 𝑎 ‘ 𝑑 ) = 0 ∨ ( 𝑐 ‘ 𝑑 ) = 0 ) ↔ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) )
45 44 anbi2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ 𝑑 ) = 0 ∨ ( 𝑐 ‘ 𝑑 ) = 0 ) ) ↔ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
46 18 45 bitr3id ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) ↔ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
47 46 rexbidva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
48 17 47 bitr3id ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) ) )
49 48 abbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑏 ∣ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∨ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) ) } = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } )
50 16 49 eqtrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 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 ‘ ℕ ) ) → { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
65 51 53 63 64 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m ℕ ) ↦ ( ( 𝑎 ‘ 𝑒 ) · ( 𝑐 ‘ 𝑒 ) ) ) ‘ 𝑑 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
66 50 65 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) )
67 uneq12 ⊢ ( ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) → ( 𝐴 ∪ 𝐵 ) = ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) )
68 67 eleq1d ⊢ ( ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ↔ ( { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) ) )
69 66 68 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ℕ ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) → ( 𝐴 ∪ 𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
70 69 rexlimdvva ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑑 ) = 0 ) } ) → ( 𝐴 ∪ 𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
71 15 70 biimtrrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑏 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑑 ↾ ( 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 ‘ 𝑁 ) )