Metamath Proof Explorer

Theorem ellazim

Description: Representation of an "extended integer". (Contributed by AV, 25-Oct-2026)

Ref Expression
Assertion ellazim 
|- ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )

Proof

Step Hyp Ref Expression
1 ellaz 
 |-  ( S e. CC -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) )
2 1 simplbda 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )