Metamath Proof Explorer


Theorem diophin

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

Ref Expression
Assertion diophin ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eldiophelnn0 ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) → 𝑁 ∈ ℕ0 )
2 id ( 𝑁 ∈ ℕ0𝑁 ∈ ℕ0 )
3 zex ℤ ∈ V
4 difexg ( ℤ ∈ V → ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ V )
5 3 4 mp1i ( 𝑁 ∈ ℕ0 → ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ V )
6 ominf ¬ ω ∈ Fin
7 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
8 lzenom ( 𝑁 ∈ ℤ → ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ≈ ω )
9 enfi ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ≈ ω → ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ Fin ↔ ω ∈ Fin ) )
10 7 8 9 3syl ( 𝑁 ∈ ℕ0 → ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ Fin ↔ ω ∈ Fin ) )
11 6 10 mtbiri ( 𝑁 ∈ ℕ0 → ¬ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ Fin )
12 fz1eqin ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) = ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) )
13 inss1 ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ⊆ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) )
14 12 13 eqsstrdi ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ⊆ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
15 eldioph2b ( ( ( 𝑁 ∈ ℕ0 ∧ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ V ) ∧ ( ¬ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ) )
16 2 5 11 14 15 syl22anc ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ) )
17 nnex ℕ ∈ V
18 17 a1i ( 𝑁 ∈ ℕ0 → ℕ ∈ V )
19 1z 1 ∈ ℤ
20 nnuz ℕ = ( ℤ ‘ 1 )
21 20 uzinf ( 1 ∈ ℤ → ¬ ℕ ∈ Fin )
22 19 21 mp1i ( 𝑁 ∈ ℕ0 → ¬ ℕ ∈ Fin )
23 elfznn ( 𝑎 ∈ ( 1 ... 𝑁 ) → 𝑎 ∈ ℕ )
24 23 ssriv ( 1 ... 𝑁 ) ⊆ ℕ
25 24 a1i ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ⊆ ℕ )
26 eldioph2b ( ( ( 𝑁 ∈ ℕ0 ∧ ℕ ∈ V ) ∧ ( ¬ ℕ ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ℕ ) ) → ( 𝐵 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) )
27 2 18 22 25 26 syl22anc ( 𝑁 ∈ ℕ0 → ( 𝐵 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) )
28 16 27 anbi12d ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) ) )
29 reeanv ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) )
30 inab ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) = { 𝑐 ∣ ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) }
31 reeanv ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ↔ ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) )
32 simplrl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
33 simplrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → 𝑒 ∈ ( ℕ0m ℕ ) )
34 12 eqcomd ( 𝑁 ∈ ℕ0 → ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) = ( 1 ... 𝑁 ) )
35 34 reseq2d ( 𝑁 ∈ ℕ0 → ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
36 35 ad3antrrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
37 34 reseq2d ( 𝑁 ∈ ℕ0 → ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
38 37 ad3antrrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
39 simprrl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
40 simprll ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
41 38 39 40 3eqtr2d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
42 36 41 eqtr4d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) )
43 elmapresaun ( ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ∧ ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) ) → ( 𝑑𝑒 ) ∈ ( ℕ0m ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) )
44 32 33 42 43 syl3anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑑𝑒 ) ∈ ( ℕ0m ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) )
45 20 uneq2i ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) = ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ( ℤ ‘ 1 ) )
46 19 a1i ( 𝑁 ∈ ℕ0 → 1 ∈ ℤ )
47 nn0p1nn ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
48 47 nnge1d ( 𝑁 ∈ ℕ0 → 1 ≤ ( 𝑁 + 1 ) )
49 lzunuz ( ( 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ ( 𝑁 + 1 ) ) → ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ( ℤ ‘ 1 ) ) = ℤ )
50 7 46 48 49 syl3anc ( 𝑁 ∈ ℕ0 → ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ( ℤ ‘ 1 ) ) = ℤ )
51 45 50 syl5eq ( 𝑁 ∈ ℕ0 → ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) = ℤ )
52 51 oveq2d ( 𝑁 ∈ ℕ0 → ( ℕ0m ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) = ( ℕ0m ℤ ) )
53 52 ad3antrrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( ℕ0m ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) = ( ℕ0m ℤ ) )
54 44 53 eleqtrd ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑑𝑒 ) ∈ ( ℕ0m ℤ ) )
55 unidm ( 𝑐𝑐 ) = 𝑐
56 40 39 uneq12d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑐𝑐 ) = ( ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ) )
57 55 56 eqtr3id ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → 𝑐 = ( ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ) )
58 resundir ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
59 57 58 eqtr4di ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → 𝑐 = ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) )
60 uncom ( 𝑑𝑒 ) = ( 𝑒𝑑 )
61 60 reseq1i ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( 𝑒𝑑 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
62 incom ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ )
63 62 34 syl5eq ( 𝑁 ∈ ℕ0 → ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = ( 1 ... 𝑁 ) )
64 63 reseq2d ( 𝑁 ∈ ℕ0 → ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
65 64 ad3antrrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
66 63 reseq2d ( 𝑁 ∈ ℕ0 → ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
67 66 ad3antrrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
68 67 40 39 3eqtr2d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
69 65 68 eqtr4d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) )
70 elmapresaunres2 ( ( 𝑒 ∈ ( ℕ0m ℕ ) ∧ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ) → ( ( 𝑒𝑑 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = 𝑑 )
71 33 32 69 70 syl3anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( ( 𝑒𝑑 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = 𝑑 )
72 61 71 syl5eq ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = 𝑑 )
73 72 fveq2d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑎𝑑 ) )
74 simprlr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑎𝑑 ) = 0 )
75 73 74 eqtrd ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 )
76 elmapresaunres2 ( ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ∧ ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) ) → ( ( 𝑑𝑒 ) ↾ ℕ ) = 𝑒 )
77 32 33 42 76 syl3anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( ( 𝑑𝑒 ) ↾ ℕ ) = 𝑒 )
78 77 fveq2d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = ( 𝑏𝑒 ) )
79 simprrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑏𝑒 ) = 0 )
80 78 79 eqtrd ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = 0 )
81 59 75 80 jca32 ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ( 𝑐 = ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = 0 ) ) )
82 reseq1 ( 𝑓 = ( 𝑑𝑒 ) → ( 𝑓 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) )
83 82 eqeq2d ( 𝑓 = ( 𝑑𝑒 ) → ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑐 = ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) ) )
84 reseq1 ( 𝑓 = ( 𝑑𝑒 ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
85 84 fveqeq2d ( 𝑓 = ( 𝑑𝑒 ) → ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ↔ ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) )
86 reseq1 ( 𝑓 = ( 𝑑𝑒 ) → ( 𝑓 ↾ ℕ ) = ( ( 𝑑𝑒 ) ↾ ℕ ) )
87 86 fveqeq2d ( 𝑓 = ( 𝑑𝑒 ) → ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ↔ ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = 0 ) )
88 85 87 anbi12d ( 𝑓 = ( 𝑑𝑒 ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = 0 ) ) )
89 83 88 anbi12d ( 𝑓 = ( 𝑑𝑒 ) → ( ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ↔ ( 𝑐 = ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = 0 ) ) ) )
90 89 rspcev ( ( ( 𝑑𝑒 ) ∈ ( ℕ0m ℤ ) ∧ ( 𝑐 = ( ( 𝑑𝑒 ) ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( ( 𝑑𝑒 ) ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( ( 𝑑𝑒 ) ↾ ℕ ) ) = 0 ) ) ) → ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) )
91 54 81 90 syl2anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) → ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) )
92 91 ex ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0m ℕ ) ) ) → ( ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) → ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
93 92 rexlimdvva ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) → ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
94 simpr ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → 𝑓 ∈ ( ℕ0m ℤ ) )
95 difss ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ
96 elmapssres ( ( 𝑓 ∈ ( ℕ0m ℤ ) ∧ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
97 94 95 96 sylancl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
98 97 adantr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
99 nnssz ℕ ⊆ ℤ
100 elmapssres ( ( 𝑓 ∈ ( ℕ0m ℤ ) ∧ ℕ ⊆ ℤ ) → ( 𝑓 ↾ ℕ ) ∈ ( ℕ0m ℕ ) )
101 94 99 100 sylancl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑓 ↾ ℕ ) ∈ ( ℕ0m ℕ ) )
102 101 adantr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑓 ↾ ℕ ) ∈ ( ℕ0m ℕ ) )
103 simprl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
104 14 ad3antrrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 1 ... 𝑁 ) ⊆ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) )
105 104 resabs1d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
106 103 105 eqtr4d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) )
107 simprrl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 )
108 106 107 jca ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) )
109 resabs1 ( ( 1 ... 𝑁 ) ⊆ ℕ → ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
110 24 109 mp1i ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
111 103 110 eqtr4d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) )
112 simprrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 )
113 108 111 112 jca32 ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ∧ ( 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) )
114 reseq1 ( 𝑑 = ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑑 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) )
115 114 eqeq2d ( 𝑑 = ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) → ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ) )
116 fveqeq2 ( 𝑑 = ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) → ( ( 𝑎𝑑 ) = 0 ↔ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) )
117 115 116 anbi12d ( 𝑑 = ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) → ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ↔ ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ) )
118 117 anbi1d ( 𝑑 = ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) → ( ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ↔ ( ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) )
119 reseq1 ( 𝑒 = ( 𝑓 ↾ ℕ ) → ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) )
120 119 eqeq2d ( 𝑒 = ( 𝑓 ↾ ℕ ) → ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) ) )
121 fveqeq2 ( 𝑒 = ( 𝑓 ↾ ℕ ) → ( ( 𝑏𝑒 ) = 0 ↔ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) )
122 120 121 anbi12d ( 𝑒 = ( 𝑓 ↾ ℕ ) → ( ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ↔ ( 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) )
123 122 anbi2d ( 𝑒 = ( 𝑓 ↾ ℕ ) → ( ( ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ↔ ( ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ∧ ( 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
124 118 123 rspc2ev ( ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ ( 𝑓 ↾ ℕ ) ∈ ( ℕ0m ℕ ) ∧ ( ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ∧ ( 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) )
125 98 102 113 124 syl3anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) )
126 125 rexlimdva2 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) → ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ) )
127 93 126 impbid ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
128 simplrl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
129 mzpf ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) → 𝑎 : ( ℤ ↑m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ⟶ ℤ )
130 128 129 syl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → 𝑎 : ( ℤ ↑m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ⟶ ℤ )
131 nn0ssz 0 ⊆ ℤ
132 mapss ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0m ℤ ) ⊆ ( ℤ ↑m ℤ ) )
133 3 131 132 mp2an ( ℕ0m ℤ ) ⊆ ( ℤ ↑m ℤ )
134 133 sseli ( 𝑓 ∈ ( ℕ0m ℤ ) → 𝑓 ∈ ( ℤ ↑m ℤ ) )
135 elmapssres ( ( 𝑓 ∈ ( ℤ ↑m ℤ ) ∧ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℤ ↑m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
136 134 95 135 sylancl ( 𝑓 ∈ ( ℕ0m ℤ ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℤ ↑m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
137 136 adantl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℤ ↑m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
138 130 137 ffvelrnd ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ∈ ℤ )
139 138 zred ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ∈ ℝ )
140 simplrr ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → 𝑏 ∈ ( mzPoly ‘ ℕ ) )
141 mzpf ( 𝑏 ∈ ( mzPoly ‘ ℕ ) → 𝑏 : ( ℤ ↑m ℕ ) ⟶ ℤ )
142 140 141 syl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → 𝑏 : ( ℤ ↑m ℕ ) ⟶ ℤ )
143 elmapssres ( ( 𝑓 ∈ ( ℤ ↑m ℤ ) ∧ ℕ ⊆ ℤ ) → ( 𝑓 ↾ ℕ ) ∈ ( ℤ ↑m ℕ ) )
144 134 99 143 sylancl ( 𝑓 ∈ ( ℕ0m ℤ ) → ( 𝑓 ↾ ℕ ) ∈ ( ℤ ↑m ℕ ) )
145 144 adantl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑓 ↾ ℕ ) ∈ ( ℤ ↑m ℕ ) )
146 142 145 ffvelrnd ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ∈ ℤ )
147 146 zred ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ∈ ℝ )
148 sumsqeq0 ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ∈ ℝ ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ∈ ℝ ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) = 0 ) )
149 139 147 148 syl2anc ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) = 0 ) )
150 134 adantl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → 𝑓 ∈ ( ℤ ↑m ℤ ) )
151 reseq1 ( 𝑔 = 𝑓 → ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) = ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
152 151 fveq2d ( 𝑔 = 𝑓 → ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) )
153 152 oveq1d ( 𝑔 = 𝑓 → ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) = ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) )
154 reseq1 ( 𝑔 = 𝑓 → ( 𝑔 ↾ ℕ ) = ( 𝑓 ↾ ℕ ) )
155 154 fveq2d ( 𝑔 = 𝑓 → ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) = ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) )
156 155 oveq1d ( 𝑔 = 𝑓 → ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) = ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) )
157 153 156 oveq12d ( 𝑔 = 𝑓 → ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) = ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) )
158 eqid ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) = ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) )
159 ovex ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) ∈ V
160 157 158 159 fvmpt ( 𝑓 ∈ ( ℤ ↑m ℤ ) → ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) )
161 150 160 syl ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) )
162 161 eqeq1d ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ↔ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) = 0 ) )
163 149 162 bitr4d ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) )
164 163 anbi2d ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0m ℤ ) ) → ( ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ↔ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
165 164 rexbidva ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
166 127 165 bitrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
167 31 166 bitr3id ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
168 167 abbidv ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑐 ∣ ( ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) ) } = { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } )
169 30 168 syl5eq ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) = { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } )
170 simpl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑁 ∈ ℕ0 )
171 fzssuz ( 1 ... 𝑁 ) ⊆ ( ℤ ‘ 1 )
172 uzssz ( ℤ ‘ 1 ) ⊆ ℤ
173 171 172 sstri ( 1 ... 𝑁 ) ⊆ ℤ
174 3 173 pm3.2i ( ℤ ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ℤ )
175 174 a1i ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ℤ ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ℤ ) )
176 3 a1i ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ℤ ∈ V )
177 95 a1i ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ )
178 simprl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) )
179 mzpresrename ( ( ℤ ∈ V ∧ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ ∧ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ) ∈ ( mzPoly ‘ ℤ ) )
180 176 177 178 179 syl3anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ) ∈ ( mzPoly ‘ ℤ ) )
181 2nn0 2 ∈ ℕ0
182 mzpexpmpt ( ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ) ∈ ( mzPoly ‘ ℤ ) ∧ 2 ∈ ℕ0 ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) ) ∈ ( mzPoly ‘ ℤ ) )
183 180 181 182 sylancl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) ) ∈ ( mzPoly ‘ ℤ ) )
184 99 a1i ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ℕ ⊆ ℤ )
185 simprr ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → 𝑏 ∈ ( mzPoly ‘ ℕ ) )
186 mzpresrename ( ( ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ) ∈ ( mzPoly ‘ ℤ ) )
187 176 184 185 186 syl3anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ) ∈ ( mzPoly ‘ ℤ ) )
188 mzpexpmpt ( ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ) ∈ ( mzPoly ‘ ℤ ) ∧ 2 ∈ ℕ0 ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ∈ ( mzPoly ‘ ℤ ) )
189 187 181 188 sylancl ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ∈ ( mzPoly ‘ ℤ ) )
190 mzpaddmpt ( ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) ) ∈ ( mzPoly ‘ ℤ ) ∧ ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ∈ ( mzPoly ‘ ℤ ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ℤ ) )
191 183 189 190 syl2anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ℤ ) )
192 eldioph2 ( ( 𝑁 ∈ ℕ0 ∧ ( ℤ ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ℤ ) ∧ ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ∈ ( mzPoly ‘ ℤ ) ) → { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
193 170 175 191 192 syl3anc ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
194 169 193 eqeltrd ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) )
195 ineq12 ( ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) → ( 𝐴𝐵 ) = ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) )
196 195 eleq1d ( ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) → ( ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ↔ ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) ) )
197 194 196 syl5ibrcom ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
198 197 rexlimdvva ( 𝑁 ∈ ℕ0 → ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
199 29 198 syl5bir ( 𝑁 ∈ ℕ0 → ( ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0m ( ℤ ∖ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎𝑑 ) = 0 ) } ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏𝑒 ) = 0 ) } ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
200 28 199 sylbid ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
201 1 200 syl ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
202 201 anabsi5 ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) → ( 𝐴𝐵 ) ∈ ( Dioph ‘ 𝑁 ) )