Metamath Proof Explorer

Theorem lazcjcl

Description: The extended integers are closed under conjugation if the conjugation of the adjoined complex number is an extended integer. (Contributed by AV, 26-Oct-2026)

Ref Expression
Hypothesis laznegcl.r 
|- R = ( Z[]l ` S )
Assertion lazcjcl 
|- ( ( S e. CC /\ ( * ` S ) e. R ) -> ( A e. R -> ( * ` A ) e. R ) )

Proof

Step Hyp Ref Expression
1 laznegcl.r 
 |-  R = ( Z[]l ` S )
2 1 eleq2i 
 |-  ( A e. R <-> A e. ( Z[]l ` S ) )
3 ellazim 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )
4 3 ex 
 |-  ( S e. CC -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
5 4 adantr 
 |-  ( ( S e. CC /\ ( * ` S ) e. R ) -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
6 2 5 biimtrid 
 |-  ( ( S e. CC /\ ( * ` S ) e. R ) -> ( A e. R -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
7 fveq2 
 |-  ( A = ( a + ( b x. S ) ) -> ( * ` A ) = ( * ` ( a + ( b x. S ) ) ) )
8 zcn 
 |-  ( a e. ZZ -> a e. CC )
9 8 ad2antrl 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
10 zcn 
 |-  ( b e. ZZ -> b e. CC )
11 10 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. CC )
12 simpl 
 |-  ( ( S e. CC /\ ( * ` S ) e. R ) -> S e. CC )
13 mulcl 
 |-  ( ( b e. CC /\ S e. CC ) -> ( b x. S ) e. CC )
14 11 12 13 syl2anr 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. S ) e. CC )
15 9 14 cjaddd 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( * ` ( a + ( b x. S ) ) ) = ( ( * ` a ) + ( * ` ( b x. S ) ) ) )
16 zre 
 |-  ( a e. ZZ -> a e. RR )
17 16 ad2antrl 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. RR )
18 17 cjred 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( * ` a ) = a )
19 11 adantl 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
20 12 adantr 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC )
21 19 20 cjmuld 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( * ` ( b x. S ) ) = ( ( * ` b ) x. ( * ` S ) ) )
22 zre 
 |-  ( b e. ZZ -> b e. RR )
23 22 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. RR )
24 23 adantl 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. RR )
25 24 cjred 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( * ` b ) = b )
26 25 oveq1d 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( * ` b ) x. ( * ` S ) ) = ( b x. ( * ` S ) ) )
27 21 26 eqtrd 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( * ` ( b x. S ) ) = ( b x. ( * ` S ) ) )
28 18 27 oveq12d 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( * ` a ) + ( * ` ( b x. S ) ) ) = ( a + ( b x. ( * ` S ) ) ) )
29 15 28 eqtrd 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( * ` ( a + ( b x. S ) ) ) = ( a + ( b x. ( * ` S ) ) ) )
30 7 29 sylan9eqr 
 |-  ( ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> ( * ` A ) = ( a + ( b x. ( * ` S ) ) ) )
31 zellaz 
 |-  ( ( S e. CC /\ a e. ZZ ) -> a e. ( Z[]l ` S ) )
32 31 ad2ant2r 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ( Z[]l ` S ) )
33 32 1 eleqtrrdi 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. R )
34 simpr 
 |-  ( ( S e. CC /\ ( * ` S ) e. R ) -> ( * ` S ) e. R )
35 simpr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
36 34 35 anim12ci 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b e. ZZ /\ ( * ` S ) e. R ) )
37 1 lazmulzcl 
 |-  ( S e. CC -> ( ( b e. ZZ /\ ( * ` S ) e. R ) -> ( b x. ( * ` S ) ) e. R ) )
38 20 36 37 sylc 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b x. ( * ` S ) ) e. R )
39 33 38 jca 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a e. R /\ ( b x. ( * ` S ) ) e. R ) )
40 1 lazaddcl 
 |-  ( S e. CC -> ( ( a e. R /\ ( b x. ( * ` S ) ) e. R ) -> ( a + ( b x. ( * ` S ) ) ) e. R ) )
41 20 39 40 sylc 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. ( * ` S ) ) ) e. R )
42 41 adantr 
 |-  ( ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> ( a + ( b x. ( * ` S ) ) ) e. R )
43 30 42 eqeltrd 
 |-  ( ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ A = ( a + ( b x. S ) ) ) -> ( * ` A ) e. R )
44 43 ex 
 |-  ( ( ( S e. CC /\ ( * ` S ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> ( * ` A ) e. R ) )
45 44 rexlimdvva 
 |-  ( ( S e. CC /\ ( * ` S ) e. R ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> ( * ` A ) e. R ) )
46 6 45 syld 
 |-  ( ( S e. CC /\ ( * ` S ) e. R ) -> ( A e. R -> ( * ` A ) e. R ) )