Metamath Proof Explorer

Theorem eldioph

Description: Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion eldioph ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → 𝑁 ∈ ℕ0 )
2 simp2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
3 simp3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) )
4 eqidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } )
5 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑢 ) = ( 𝑃 ‘ 𝑢 ) )
6 5 eqeq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑢 ) = 0 ↔ ( 𝑃 ‘ 𝑢 ) = 0 ) )
7 6 anbi2d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) ) )
8 7 rexbidv ⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) ) )
9 8 abbidv ⊢ ( 𝑝 = 𝑃 → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } )
10 9 rspceeqv ⊢ ( ( 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ∧ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ) → ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
11 3 4 10 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
12 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 1 ... 𝑘 ) = ( 1 ... 𝐾 ) )
13 12 fveq2d ⊢ ( 𝑘 = 𝐾 → ( mzPoly ‘ ( 1 ... 𝑘 ) ) = ( mzPoly ‘ ( 1 ... 𝐾 ) ) )
14 12 oveq2d ⊢ ( 𝑘 = 𝐾 → ( ℕ0 ↑m ( 1 ... 𝑘 ) ) = ( ℕ0 ↑m ( 1 ... 𝐾 ) ) )
15 14 rexeqdv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ) )
16 15 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
17 16 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ↔ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
18 13 17 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
19 18 rspcev ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
20 2 11 19 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
21 eldiophb ⊢ ( { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑝 ∈ ( mzPoly ‘ ( 1 ... 𝑘 ) ) { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝑘 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
22 1 20 21 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑃 ∈ ( mzPoly ‘ ( 1 ... 𝐾 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 1 ... 𝐾 ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )