Metamath Proof Explorer

Theorem lazmulcl

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

Ref Expression
Hypothesis laznegcl.r 
|- R = ( Z[]l ` S )
Assertion lazmulcl 
|- ( ( S e. CC /\ ( S ^ 2 ) e. R ) -> ( ( A e. R /\ B e. R ) -> ( A x. B ) 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 1 eleq2i 
 |-  ( B e. R <-> B e. ( Z[]l ` S ) )
4 2 3 anbi12i 
 |-  ( ( A e. R /\ B e. R ) <-> ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) )
5 ellazim 
 |-  ( ( S e. CC /\ A e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) )
6 5 ex 
 |-  ( S e. CC -> ( A e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) ) )
7 ellazim 
 |-  ( ( S e. CC /\ B e. ( Z[]l ` S ) ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) )
8 7 ex 
 |-  ( S e. CC -> ( B e. ( Z[]l ` S ) -> E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) )
9 6 8 anim12d 
 |-  ( S e. CC -> ( ( A e. ( Z[]l ` S ) /\ B e. ( Z[]l ` S ) ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) )
10 4 9 biimtrid 
 |-  ( S e. CC -> ( ( A e. R /\ B e. R ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) )
11 10 adantr 
 |-  ( ( S e. CC /\ ( S ^ 2 ) e. R ) -> ( ( A e. R /\ B e. R ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) ) )
12 oveq12 
 |-  ( ( A = ( a + ( b x. S ) ) /\ B = ( c + ( d x. S ) ) ) -> ( A x. B ) = ( ( a + ( b x. S ) ) x. ( c + ( d x. S ) ) ) )
13 12 ancoms 
 |-  ( ( B = ( c + ( d x. S ) ) /\ A = ( a + ( b x. S ) ) ) -> ( A x. B ) = ( ( a + ( b x. S ) ) x. ( c + ( d x. S ) ) ) )
14 13 adantl 
 |-  ( ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( d x. S ) ) /\ A = ( a + ( b x. S ) ) ) ) -> ( A x. B ) = ( ( a + ( b x. S ) ) x. ( c + ( d x. S ) ) ) )
15 zcn 
 |-  ( a e. ZZ -> a e. CC )
16 15 ad2antrl 
 |-  ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
17 16 adantr 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> a e. CC )
18 zcn 
 |-  ( b e. ZZ -> b e. CC )
19 18 ad2antll 
 |-  ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
20 19 adantr 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> b e. CC )
21 simplll 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> S e. CC )
22 zcn 
 |-  ( c e. ZZ -> c e. CC )
23 22 ad2antrl 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> c e. CC )
24 zcn 
 |-  ( d e. ZZ -> d e. CC )
25 24 ad2antll 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> d e. CC )
26 17 20 21 23 25 addmuldir2d 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + ( b x. S ) ) x. ( c + ( d x. S ) ) ) = ( ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) + ( ( b x. d ) x. ( S ^ 2 ) ) ) )
27 simpl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. ZZ )
28 27 adantl 
 |-  ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
29 simpl 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> c e. ZZ )
30 zmulcl 
 |-  ( ( a e. ZZ /\ c e. ZZ ) -> ( a x. c ) e. ZZ )
31 28 29 30 syl2an 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a x. c ) e. ZZ )
32 zellaz 
 |-  ( ( S e. CC /\ ( a x. c ) e. ZZ ) -> ( a x. c ) e. ( Z[]l ` S ) )
33 21 31 32 syl2anc 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a x. c ) e. ( Z[]l ` S ) )
34 33 1 eleqtrrdi 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a x. c ) e. R )
35 simpr 
 |-  ( ( c e. ZZ /\ d e. ZZ ) -> d e. ZZ )
36 zmulcl 
 |-  ( ( a e. ZZ /\ d e. ZZ ) -> ( a x. d ) e. ZZ )
37 28 35 36 syl2an 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( a x. d ) e. ZZ )
38 simpr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. ZZ )
39 38 adantl 
 |-  ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
40 zmulcl 
 |-  ( ( c e. ZZ /\ b e. ZZ ) -> ( c x. b ) e. ZZ )
41 29 39 40 syl2anr 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( c x. b ) e. ZZ )
42 37 41 zaddcld 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a x. d ) + ( c x. b ) ) e. ZZ )
43 adcnmulzlaz 
 |-  ( ( S e. CC /\ ( ( a x. d ) + ( c x. b ) ) e. ZZ ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. ( Z[]l ` S ) )
44 21 42 43 syl2anc 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. ( Z[]l ` S ) )
45 44 1 eleqtrrdi 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. R )
46 34 45 jca 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a x. c ) e. R /\ ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. R ) )
47 1 lazaddcl 
 |-  ( S e. CC -> ( ( ( a x. c ) e. R /\ ( ( ( a x. d ) + ( c x. b ) ) x. S ) e. R ) -> ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) e. R ) )
48 21 46 47 sylc 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) e. R )
49 zmulcl 
 |-  ( ( b e. ZZ /\ d e. ZZ ) -> ( b x. d ) e. ZZ )
50 39 35 49 syl2an 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( b x. d ) e. ZZ )
51 simpllr 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( S ^ 2 ) e. R )
52 50 51 jca 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( b x. d ) e. ZZ /\ ( S ^ 2 ) e. R ) )
53 1 lazmulzcl 
 |-  ( S e. CC -> ( ( ( b x. d ) e. ZZ /\ ( S ^ 2 ) e. R ) -> ( ( b x. d ) x. ( S ^ 2 ) ) e. R ) )
54 21 52 53 sylc 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( b x. d ) x. ( S ^ 2 ) ) e. R )
55 48 54 jca 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) e. R /\ ( ( b x. d ) x. ( S ^ 2 ) ) e. R ) )
56 1 lazaddcl 
 |-  ( S e. CC -> ( ( ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) e. R /\ ( ( b x. d ) x. ( S ^ 2 ) ) e. R ) -> ( ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) + ( ( b x. d ) x. ( S ^ 2 ) ) ) e. R ) )
57 21 55 56 sylc 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( ( a x. c ) + ( ( ( a x. d ) + ( c x. b ) ) x. S ) ) + ( ( b x. d ) x. ( S ^ 2 ) ) ) e. R )
58 26 57 eqeltrd 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( ( a + ( b x. S ) ) x. ( c + ( d x. S ) ) ) e. R )
59 58 adantr 
 |-  ( ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( d x. S ) ) /\ A = ( a + ( b x. S ) ) ) ) -> ( ( a + ( b x. S ) ) x. ( c + ( d x. S ) ) ) e. R )
60 14 59 eqeltrd 
 |-  ( ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) /\ ( B = ( c + ( d x. S ) ) /\ A = ( a + ( b x. S ) ) ) ) -> ( A x. B ) e. R )
61 60 exp32 
 |-  ( ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( c e. ZZ /\ d e. ZZ ) ) -> ( B = ( c + ( d x. S ) ) -> ( A = ( a + ( b x. S ) ) -> ( A x. B ) e. R ) ) )
62 61 rexlimdvva 
 |-  ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) -> ( A = ( a + ( b x. S ) ) -> ( A x. B ) e. R ) ) )
63 62 com23 
 |-  ( ( ( S e. CC /\ ( S ^ 2 ) e. R ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( A = ( a + ( b x. S ) ) -> ( E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) -> ( A x. B ) e. R ) ) )
64 63 rexlimdvva 
 |-  ( ( S e. CC /\ ( S ^ 2 ) e. R ) -> ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) -> ( E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) -> ( A x. B ) e. R ) ) )
65 64 impd 
 |-  ( ( S e. CC /\ ( S ^ 2 ) e. R ) -> ( ( E. a e. ZZ E. b e. ZZ A = ( a + ( b x. S ) ) /\ E. c e. ZZ E. d e. ZZ B = ( c + ( d x. S ) ) ) -> ( A x. B ) e. R ) )
66 11 65 syld 
 |-  ( ( S e. CC /\ ( S ^ 2 ) e. R ) -> ( ( A e. R /\ B e. R ) -> ( A x. B ) e. R ) )