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 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ) )
16 2 5 11 14 15 syl22anc ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 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 ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) )
27 2 18 22 25 26 syl22anc ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐵 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) )
28 16 27 anbi12d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝐵 ∈ ( Dioph ‘ 𝑁 ) ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) ) )
29 reeanv ⊢ ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) ↔ ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) )
30 inab ⊢ ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) = { 𝑐 ∣ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) }
31 reeanv ⊢ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ↔ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) )
32 simplrl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
33 simplrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → 𝑒 ∈ ( ℕ0 ↑m ℕ ) )
34 12 eqcomd ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) = ( 1 ... 𝑁 ) )
35 34 reseq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
36 35 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
37 34 reseq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
38 37 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
39 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
40 simprll ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
41 38 39 40 3eqtr2d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
42 36 41 eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) )
43 elmapresaun ⊢ ( ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ∧ ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) ) → ( 𝑑 ∪ 𝑒 ) ∈ ( ℕ0 ↑m ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) )
44 32 33 42 43 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑑 ∪ 𝑒 ) ∈ ( ℕ0 ↑m ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 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 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) = ℤ )
52 51 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ℕ0 ↑m ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) = ( ℕ0 ↑m ℤ ) )
53 52 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( ℕ0 ↑m ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∪ ℕ ) ) = ( ℕ0 ↑m ℤ ) )
54 44 53 eleqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑑 ∪ 𝑒 ) ∈ ( ℕ0 ↑m ℤ ) )
55 unidm ⊢ ( 𝑐 ∪ 𝑐 ) = 𝑐
56 40 39 uneq12d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑐 ∪ 𝑐 ) = ( ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ) )
57 55 56 eqtr3id ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → 𝑐 = ( ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ) )
58 resundir ⊢ ( ( 𝑑 ∪ 𝑒 ) ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
59 57 58 eqtr4di ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → 𝑐 = ( ( 𝑑 ∪ 𝑒 ) ↾ ( 1 ... 𝑁 ) ) )
60 uncom ⊢ ( 𝑑 ∪ 𝑒 ) = ( 𝑒 ∪ 𝑑 )
61 60 reseq1i ⊢ ( ( 𝑑 ∪ 𝑒 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( 𝑒 ∪ 𝑑 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
62 incom ⊢ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ )
63 62 34 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( 1 ... 𝑁 ) )
64 63 reseq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
65 64 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
66 63 reseq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
67 66 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) )
68 67 40 39 3eqtr2d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
69 65 68 eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) )
70 elmapresaunres2 ⊢ ( ( 𝑒 ∈ ( ℕ0 ↑m ℕ ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ ( 𝑒 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑑 ↾ ( ℕ ∩ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ) → ( ( 𝑒 ∪ 𝑑 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = 𝑑 )
71 33 32 69 70 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( ( 𝑒 ∪ 𝑑 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = 𝑑 )
72 61 71 eqtrid ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( ( 𝑑 ∪ 𝑒 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = 𝑑 )
73 72 fveq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑎 ‘ ( ( 𝑑 ∪ 𝑒 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = ( 𝑎 ‘ 𝑑 ) )
74 simprlr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑎 ‘ 𝑑 ) = 0 )
75 73 74 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑎 ‘ ( ( 𝑑 ∪ 𝑒 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 )
76 elmapresaunres2 ⊢ ( ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ∧ ( 𝑑 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) = ( 𝑒 ↾ ( ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∩ ℕ ) ) ) → ( ( 𝑑 ∪ 𝑒 ) ↾ ℕ ) = 𝑒 )
77 32 33 42 76 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( ( 𝑑 ∪ 𝑒 ) ↾ ℕ ) = 𝑒 )
78 77 fveq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑏 ‘ ( ( 𝑑 ∪ 𝑒 ) ↾ ℕ ) ) = ( 𝑏 ‘ 𝑒 ) )
79 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑏 ‘ 𝑒 ) = 0 )
80 78 79 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ( 𝑏 ‘ ( ( 𝑑 ∪ 𝑒 ) ↾ ℕ ) ) = 0 )
81 59 75 80 jca32 ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 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 ⊢ ( ( ( 𝑑 ∪ 𝑒 ) ∈ ( ℕ0 ↑m ℤ ) ∧ ( 𝑐 = ( ( 𝑑 ∪ 𝑒 ) ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( ( 𝑑 ∪ 𝑒 ) ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( ( 𝑑 ∪ 𝑒 ) ↾ ℕ ) ) = 0 ) ) ) → ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) )
91 54 81 90 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) ∧ ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) → ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) )
92 91 ex ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ) ) → ( ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) → ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
93 92 rexlimdvva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) → ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
94 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → 𝑓 ∈ ( ℕ0 ↑m ℤ ) )
95 difss ⊢ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ
96 elmapssres ⊢ ( ( 𝑓 ∈ ( ℕ0 ↑m ℤ ) ∧ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
97 94 95 96 sylancl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
98 97 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
99 nnssz ⊢ ℕ ⊆ ℤ
100 elmapssres ⊢ ( ( 𝑓 ∈ ( ℕ0 ↑m ℤ ) ∧ ℕ ⊆ ℤ ) → ( 𝑓 ↾ ℕ ) ∈ ( ℕ0 ↑m ℕ ) )
101 94 99 100 sylancl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑓 ↾ ℕ ) ∈ ( ℕ0 ↑m ℕ ) )
102 101 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑓 ↾ ℕ ) ∈ ( ℕ0 ↑m ℕ ) )
103 simprl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
104 14 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 1 ... 𝑁 ) ⊆ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
105 104 resabs1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
106 103 105 eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) )
107 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 )
108 106 107 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) )
109 resabs1 ⊢ ( ( 1 ... 𝑁 ) ⊆ ℕ → ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
110 24 109 mp1i ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) )
111 103 110 eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) )
112 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 )
113 108 111 112 jca32 ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 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 ) ) ) ) ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ ( 𝑓 ↾ ℕ ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( ( 𝑐 = ( ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ) ∧ ( 𝑐 = ( ( 𝑓 ↾ ℕ ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) )
125 98 102 113 124 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) ∧ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) → ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) )
126 125 rexlimdva2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) → ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ) )
127 93 126 impbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ) )
128 simplrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
129 mzpf ⊢ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) → 𝑎 : ( ℤ ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ⟶ ℤ )
130 128 129 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → 𝑎 : ( ℤ ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ⟶ ℤ )
131 nn0ssz ⊢ ℕ0 ⊆ ℤ
132 mapss ⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m ℤ ) ⊆ ( ℤ ↑m ℤ ) )
133 3 131 132 mp2an ⊢ ( ℕ0 ↑m ℤ ) ⊆ ( ℤ ↑m ℤ )
134 133 sseli ⊢ ( 𝑓 ∈ ( ℕ0 ↑m ℤ ) → 𝑓 ∈ ( ℤ ↑m ℤ ) )
135 elmapssres ⊢ ( ( 𝑓 ∈ ( ℤ ↑m ℤ ) ∧ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⊆ ℤ ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℤ ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
136 134 95 135 sylancl ⊢ ( 𝑓 ∈ ( ℕ0 ↑m ℤ ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℤ ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
137 136 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∈ ( ℤ ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
138 130 137 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ∈ ℤ )
139 138 zred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ∈ ℝ )
140 simplrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → 𝑏 ∈ ( mzPoly ‘ ℕ ) )
141 mzpf ⊢ ( 𝑏 ∈ ( mzPoly ‘ ℕ ) → 𝑏 : ( ℤ ↑m ℕ ) ⟶ ℤ )
142 140 141 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → 𝑏 : ( ℤ ↑m ℕ ) ⟶ ℤ )
143 elmapssres ⊢ ( ( 𝑓 ∈ ( ℤ ↑m ℤ ) ∧ ℕ ⊆ ℤ ) → ( 𝑓 ↾ ℕ ) ∈ ( ℤ ↑m ℕ ) )
144 134 99 143 sylancl ⊢ ( 𝑓 ∈ ( ℕ0 ↑m ℤ ) → ( 𝑓 ↾ ℕ ) ∈ ( ℤ ↑m ℕ ) )
145 144 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑓 ↾ ℕ ) ∈ ( ℤ ↑m ℕ ) )
146 142 145 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ∈ ℤ )
147 146 zred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ∈ ℝ )
148 sumsqeq0 ⊢ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ∈ ℝ ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ∈ ℝ ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) = 0 ) )
149 139 147 148 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) = 0 ) )
150 134 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → 𝑓 ∈ ( ℤ ↑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 ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) )
162 161 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ↔ ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) ↑ 2 ) ) = 0 ) )
163 149 162 bitr4d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ↔ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) )
164 163 anbi2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) ∧ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ) → ( ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ↔ ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
165 164 rexbidva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑎 ‘ ( 𝑓 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) = 0 ∧ ( 𝑏 ‘ ( 𝑓 ↾ ℕ ) ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
166 127 165 bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
167 31 166 bitr3id ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) ↔ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) ) )
168 167 abbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑐 ∣ ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) ∧ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) ) } = { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } )
169 30 168 eqtrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) = { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 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 ‘ ℤ ) ) → { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
193 170 175 191 192 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → { 𝑐 ∣ ∃ 𝑓 ∈ ( ℕ0 ↑m ℤ ) ( 𝑐 = ( 𝑓 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑔 ∈ ( ℤ ↑m ℤ ) ↦ ( ( ( 𝑎 ‘ ( 𝑔 ↾ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) ↑ 2 ) + ( ( 𝑏 ‘ ( 𝑔 ↾ ℕ ) ) ↑ 2 ) ) ) ‘ 𝑓 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
194 169 193 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) )
195 ineq12 ⊢ ( ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) → ( 𝐴 ∩ 𝐵 ) = ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) )
196 195 eleq1d ⊢ ( ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ↔ ( { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∩ { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) ∈ ( Dioph ‘ 𝑁 ) ) )
197 194 196 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∧ 𝑏 ∈ ( mzPoly ‘ ℕ ) ) ) → ( ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) → ( 𝐴 ∩ 𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
198 197 rexlimdvva ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) ( 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑒 ) = 0 ) } ) → ( 𝐴 ∩ 𝐵 ) ∈ ( Dioph ‘ 𝑁 ) ) )
199 29 198 biimtrrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( ∃ 𝑎 ∈ ( mzPoly ‘ ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) 𝐴 = { 𝑐 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ( 𝑐 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑎 ‘ 𝑑 ) = 0 ) } ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ℕ ) 𝐵 = { 𝑐 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑐 = ( 𝑒 ↾ ( 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 ‘ 𝑁 ) )