Metamath Proof Explorer

Theorem zellaz

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

Ref Expression
Assertion zellaz 
|- ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[]l ` S ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 1 adantl 
 |-  ( ( S e. CC /\ A e. ZZ ) -> A e. CC )
3 oveq1 
 |-  ( a = A -> ( a + ( b x. S ) ) = ( A + ( b x. S ) ) )
4 3 eqeq2d 
 |-  ( a = A -> ( A = ( a + ( b x. S ) ) <-> A = ( A + ( b x. S ) ) ) )
5 oveq1 
 |-  ( b = 0 -> ( b x. S ) = ( 0 x. S ) )
6 5 oveq2d 
 |-  ( b = 0 -> ( A + ( b x. S ) ) = ( A + ( 0 x. S ) ) )
7 6 eqeq2d 
 |-  ( b = 0 -> ( A = ( A + ( b x. S ) ) <-> A = ( A + ( 0 x. S ) ) ) )
8 simpr 
 |-  ( ( S e. CC /\ A e. ZZ ) -> A e. ZZ )
9 0zd 
 |-  ( ( S e. CC /\ A e. ZZ ) -> 0 e. ZZ )
10 simpl 
 |-  ( ( S e. CC /\ A e. ZZ ) -> S e. CC )
11 10 mul02d 
 |-  ( ( S e. CC /\ A e. ZZ ) -> ( 0 x. S ) = 0 )
12 11 oveq2d 
 |-  ( ( S e. CC /\ A e. ZZ ) -> ( A + ( 0 x. S ) ) = ( A + 0 ) )
13 2 addridd 
 |-  ( ( S e. CC /\ A e. ZZ ) -> ( A + 0 ) = A )
14 12 13 eqtr2d 
 |-  ( ( S e. CC /\ A e. ZZ ) -> A = ( A + ( 0 x. S ) ) )
15 4 7 8 9 14 2rspcedvdw 
 |-  ( ( S e. CC /\ A e. ZZ ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )
16 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 ) ) ) ) )
17 16 adantr 
 |-  ( ( S e. CC /\ A e. ZZ ) -> ( A e. ( Z[]l ` S ) <-> ( A e. CC /\ E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) ) )
18 2 15 17 mpbir2and 
 |-  ( ( S e. CC /\ A e. ZZ ) -> A e. ( Z[]l ` S ) )