Metamath Proof Explorer

Theorem eldiophelnn0

Description: Remove antecedent on B from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	eldiophelnn0	\|- ( A e. ( Dioph ` B ) -> B e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		eldiophb	\|- ( A e. ( Dioph ` B ) <-> ( B e. NN0 /\ E. b e. ( ZZ>= ` B ) E. a e. ( mzPoly ` ( 1 ... b ) ) A = { c \| E. d e. ( NN0 ^m ( 1 ... b ) ) ( c = ( d \|` ( 1 ... B ) ) /\ ( a ` d ) = 0 ) } ) )
2	1	simplbi	\|- ( A e. ( Dioph ` B ) -> B e. NN0 )

Step

Hyp

Ref

Expression

eldiophb

 |-  ( A e. ( Dioph ` B ) <-> ( B e. NN0 /\ E. b e. ( ZZ>= ` B ) E. a e. ( mzPoly ` ( 1 ... b ) ) A = { c | E. d e. ( NN0 ^m ( 1 ... b ) ) ( c = ( d |` ( 1 ... B ) ) /\ ( a ` d ) = 0 ) } ) )

simplbi

 |-  ( A e. ( Dioph ` B ) -> B e. NN0 )