Theorem elnn0rabdioph

Description: Diophantine set builder for nonnegativity constraints. The first builder which uses a witness variable internally; an expression is nonnegative if there is a nonnegative integer equal to it. (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Assertion	elnn0rabdioph	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ℕ0 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		risset	⊢ ( 𝐴 ∈ ℕ0 ↔ ∃ 𝑏 ∈ ℕ0 𝑏 = 𝐴 )
2	1	rabbii	⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ℕ0 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = 𝐴 }
3	2	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ℕ0 } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = 𝐴 } )
4		nfcv	⊢ Ⅎ 𝑡 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
5		nfcv	⊢ Ⅎ 𝑎 ( ℕ0 ↑m ( 1 ... 𝑁 ) )
6		nfv	⊢ Ⅎ 𝑎 ∃ 𝑏 ∈ ℕ0 𝑏 = 𝐴
7		nfcv	⊢ Ⅎ 𝑡 ℕ0
8		nfcsb1v	⊢ Ⅎ 𝑡 ⦋ 𝑎 / 𝑡 ⦌ 𝐴
9	8	nfeq2	⊢ Ⅎ 𝑡 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴
10	7 9	nfrexw	⊢ Ⅎ 𝑡 ∃ 𝑏 ∈ ℕ0 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴
11		csbeq1a	⊢ ( 𝑡 = 𝑎 → 𝐴 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 )
12	11	eqeq2d	⊢ ( 𝑡 = 𝑎 → ( 𝑏 = 𝐴 ↔ 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) )
13	12	rexbidv	⊢ ( 𝑡 = 𝑎 → ( ∃ 𝑏 ∈ ℕ0 𝑏 = 𝐴 ↔ ∃ 𝑏 ∈ ℕ0 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) )
14	4 5 6 10 13	cbvrabw	⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = 𝐴 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 }
15	3 14	eqtrdi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ℕ0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 } )
16		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
17	16	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
18		ovex	⊢ ( 1 ... ( 𝑁 + 1 ) ) ∈ V
19		nn0p1nn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
20		elfz1end	⊢ ( ( 𝑁 + 1 ) ∈ ℕ ↔ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
21	19 20	sylib	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
22	21	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
23		mzpproj	⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ V ∧ ( 𝑁 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
24	18 22 23	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
25		eqid	⊢ ( 𝑁 + 1 ) = ( 𝑁 + 1 )
26	25	rabdiophlem2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
27		eqrabdioph	⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ( 𝑐 ‘ ( 𝑁 + 1 ) ) ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ∧ ( 𝑐 ∈ ( ℤ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ↦ ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( 𝑐 ‘ ( 𝑁 + 1 ) ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
28	17 24 26 27	syl3anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( 𝑐 ‘ ( 𝑁 + 1 ) ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) )
29		eqeq1	⊢ ( 𝑏 = ( 𝑐 ‘ ( 𝑁 + 1 ) ) → ( 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ↔ ( 𝑐 ‘ ( 𝑁 + 1 ) ) = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ) )
30		csbeq1	⊢ ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ⦋ 𝑎 / 𝑡 ⦌ 𝐴 = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 )
31	30	eqeq2d	⊢ ( 𝑎 = ( 𝑐 ↾ ( 1 ... 𝑁 ) ) → ( ( 𝑐 ‘ ( 𝑁 + 1 ) ) = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 ↔ ( 𝑐 ‘ ( 𝑁 + 1 ) ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 ) )
32	25 29 31	rexrabdioph	⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ ( 𝑐 ‘ ( 𝑁 + 1 ) ) = ⦋ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) / 𝑡 ⦌ 𝐴 } ∈ ( Dioph ‘ ( 𝑁 + 1 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 } ∈ ( Dioph ‘ 𝑁 ) )
33	28 32	syldan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ℕ0 𝑏 = ⦋ 𝑎 / 𝑡 ⦌ 𝐴 } ∈ ( Dioph ‘ 𝑁 ) )
34	15 33	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝐴 ∈ ℕ0 } ∈ ( Dioph ‘ 𝑁 ) )