Theorem zelaz

Description: An integer is an extended integer. (Contributed by AV, 31-Oct-2026)

	Ref	Expression
Assertion	zelaz	Could not format assertion : No typesetting found for |- ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[] ` S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		azssid	Could not format ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) ) : No typesetting found for |- ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) ) with typecode |-
2	1	unssad	Could not format ( S e. CC -> ZZ C_ ( Z[] ` S ) ) : No typesetting found for |- ( S e. CC -> ZZ C_ ( Z[] ` S ) ) with typecode |-
3	2	sselda	Could not format ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[] ` S ) ) : No typesetting found for |- ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[] ` S ) ) with typecode |-