Metamath Proof Explorer

Theorem constrmulcl

Description: Constructible numbers are closed under complex multiplication. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypotheses constrmulcl.1 
|- ( ph -> X e. Constr )
constrmulcl.2 
|- ( ph -> Y e. Constr )
Assertion constrmulcl 
|- ( ph -> ( X x. Y ) e. Constr )

Proof

Step Hyp Ref Expression
1 constrmulcl.1 
 |-  ( ph -> X e. Constr )
2 constrmulcl.2 
 |-  ( ph -> Y e. Constr )
3 1 constrcn 
 |-  ( ph -> X e. CC )
4 3 replimd 
 |-  ( ph -> X = ( ( Re ` X ) + ( _i x. ( Im ` X ) ) ) )
5 2 constrcn 
 |-  ( ph -> Y e. CC )
6 5 replimd 
 |-  ( ph -> Y = ( ( Re ` Y ) + ( _i x. ( Im ` Y ) ) ) )
7 4 6 oveq12d 
 |-  ( ph -> ( X x. Y ) = ( ( ( Re ` X ) + ( _i x. ( Im ` X ) ) ) x. ( ( Re ` Y ) + ( _i x. ( Im ` Y ) ) ) ) )
8 3 recld 
 |-  ( ph -> ( Re ` X ) e. RR )
9 8 recnd 
 |-  ( ph -> ( Re ` X ) e. CC )
10 ax-icn 
 |-  _i e. CC
11 10 a1i 
 |-  ( ph -> _i e. CC )
12 3 imcld 
 |-  ( ph -> ( Im ` X ) e. RR )
13 12 recnd 
 |-  ( ph -> ( Im ` X ) e. CC )
14 11 13 mulcld 
 |-  ( ph -> ( _i x. ( Im ` X ) ) e. CC )
15 5 recld 
 |-  ( ph -> ( Re ` Y ) e. RR )
16 15 recnd 
 |-  ( ph -> ( Re ` Y ) e. CC )
17 5 imcld 
 |-  ( ph -> ( Im ` Y ) e. RR )
18 17 recnd 
 |-  ( ph -> ( Im ` Y ) e. CC )
19 11 18 mulcld 
 |-  ( ph -> ( _i x. ( Im ` Y ) ) e. CC )
20 9 14 16 19 muladdd 
 |-  ( ph -> ( ( ( Re ` X ) + ( _i x. ( Im ` X ) ) ) x. ( ( Re ` Y ) + ( _i x. ( Im ` Y ) ) ) ) = ( ( ( ( Re ` X ) x. ( Re ` Y ) ) + ( ( _i x. ( Im ` Y ) ) x. ( _i x. ( Im ` X ) ) ) ) + ( ( ( Re ` X ) x. ( _i x. ( Im ` Y ) ) ) + ( ( Re ` Y ) x. ( _i x. ( Im ` X ) ) ) ) ) )
21 1 constrrecl 
 |-  ( ph -> ( Re ` X ) e. Constr )
22 2 constrrecl 
 |-  ( ph -> ( Re ` Y ) e. Constr )
23 21 22 8 15 constrremulcl 
 |-  ( ph -> ( ( Re ` X ) x. ( Re ` Y ) ) e. Constr )
24 11 18 11 13 mul4d 
 |-  ( ph -> ( ( _i x. ( Im ` Y ) ) x. ( _i x. ( Im ` X ) ) ) = ( ( _i x. _i ) x. ( ( Im ` Y ) x. ( Im ` X ) ) ) )
25 ixi 
 |-  ( _i x. _i ) = -u 1
26 25 oveq1i 
 |-  ( ( _i x. _i ) x. ( ( Im ` Y ) x. ( Im ` X ) ) ) = ( -u 1 x. ( ( Im ` Y ) x. ( Im ` X ) ) )
27 24 26 eqtrdi 
 |-  ( ph -> ( ( _i x. ( Im ` Y ) ) x. ( _i x. ( Im ` X ) ) ) = ( -u 1 x. ( ( Im ` Y ) x. ( Im ` X ) ) ) )
28 1zzd 
 |-  ( ph -> 1 e. ZZ )
29 28 zconstr 
 |-  ( ph -> 1 e. Constr )
30 29 constrnegcl 
 |-  ( ph -> -u 1 e. Constr )
31 2 constrimcl 
 |-  ( ph -> ( Im ` Y ) e. Constr )
32 1 constrimcl 
 |-  ( ph -> ( Im ` X ) e. Constr )
33 31 32 17 12 constrremulcl 
 |-  ( ph -> ( ( Im ` Y ) x. ( Im ` X ) ) e. Constr )
34 1red 
 |-  ( ph -> 1 e. RR )
35 34 renegcld 
 |-  ( ph -> -u 1 e. RR )
36 17 12 remulcld 
 |-  ( ph -> ( ( Im ` Y ) x. ( Im ` X ) ) e. RR )
37 30 33 35 36 constrremulcl 
 |-  ( ph -> ( -u 1 x. ( ( Im ` Y ) x. ( Im ` X ) ) ) e. Constr )
38 27 37 eqeltrd 
 |-  ( ph -> ( ( _i x. ( Im ` Y ) ) x. ( _i x. ( Im ` X ) ) ) e. Constr )
39 23 38 constraddcl 
 |-  ( ph -> ( ( ( Re ` X ) x. ( Re ` Y ) ) + ( ( _i x. ( Im ` Y ) ) x. ( _i x. ( Im ` X ) ) ) ) e. Constr )
40 9 11 18 mul12d 
 |-  ( ph -> ( ( Re ` X ) x. ( _i x. ( Im ` Y ) ) ) = ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) )
41 0zd 
 |-  ( ph -> 0 e. ZZ )
42 41 zconstr 
 |-  ( ph -> 0 e. Constr )
43 iconstr 
 |-  _i e. Constr
44 43 a1i 
 |-  ( ph -> _i e. Constr )
45 21 31 8 17 constrremulcl 
 |-  ( ph -> ( ( Re ` X ) x. ( Im ` Y ) ) e. Constr )
46 8 17 remulcld 
 |-  ( ph -> ( ( Re ` X ) x. ( Im ` Y ) ) e. RR )
47 9 18 mulcld 
 |-  ( ph -> ( ( Re ` X ) x. ( Im ` Y ) ) e. CC )
48 11 47 mulcld 
 |-  ( ph -> ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) e. CC )
49 0cnd 
 |-  ( ph -> 0 e. CC )
50 11 49 subcld 
 |-  ( ph -> ( _i - 0 ) e. CC )
51 47 50 mulcld 
 |-  ( ph -> ( ( ( Re ` X ) x. ( Im ` Y ) ) x. ( _i - 0 ) ) e. CC )
52 51 addlidd 
 |-  ( ph -> ( 0 + ( ( ( Re ` X ) x. ( Im ` Y ) ) x. ( _i - 0 ) ) ) = ( ( ( Re ` X ) x. ( Im ` Y ) ) x. ( _i - 0 ) ) )
53 11 subid1d 
 |-  ( ph -> ( _i - 0 ) = _i )
54 53 oveq2d 
 |-  ( ph -> ( ( ( Re ` X ) x. ( Im ` Y ) ) x. ( _i - 0 ) ) = ( ( ( Re ` X ) x. ( Im ` Y ) ) x. _i ) )
55 47 11 mulcomd 
 |-  ( ph -> ( ( ( Re ` X ) x. ( Im ` Y ) ) x. _i ) = ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) )
56 52 54 55 3eqtrrd 
 |-  ( ph -> ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) = ( 0 + ( ( ( Re ` X ) x. ( Im ` Y ) ) x. ( _i - 0 ) ) ) )
57 11 47 absmuld 
 |-  ( ph -> ( abs ` ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) ) = ( ( abs ` _i ) x. ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) ) )
58 absi 
 |-  ( abs ` _i ) = 1
59 58 a1i 
 |-  ( ph -> ( abs ` _i ) = 1 )
60 59 oveq1d 
 |-  ( ph -> ( ( abs ` _i ) x. ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) ) = ( 1 x. ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) ) )
61 47 abscld 
 |-  ( ph -> ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) e. RR )
62 61 recnd 
 |-  ( ph -> ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) e. CC )
63 62 mullidd 
 |-  ( ph -> ( 1 x. ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) ) = ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) )
64 57 60 63 3eqtrd 
 |-  ( ph -> ( abs ` ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) ) = ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) )
65 48 subid1d 
 |-  ( ph -> ( ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) - 0 ) = ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) )
66 65 fveq2d 
 |-  ( ph -> ( abs ` ( ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) - 0 ) ) = ( abs ` ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) ) )
67 47 subid1d 
 |-  ( ph -> ( ( ( Re ` X ) x. ( Im ` Y ) ) - 0 ) = ( ( Re ` X ) x. ( Im ` Y ) ) )
68 67 fveq2d 
 |-  ( ph -> ( abs ` ( ( ( Re ` X ) x. ( Im ` Y ) ) - 0 ) ) = ( abs ` ( ( Re ` X ) x. ( Im ` Y ) ) ) )
69 64 66 68 3eqtr4d 
 |-  ( ph -> ( abs ` ( ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) - 0 ) ) = ( abs ` ( ( ( Re ` X ) x. ( Im ` Y ) ) - 0 ) ) )
70 42 44 42 45 42 46 48 56 69 constrlccl 
 |-  ( ph -> ( _i x. ( ( Re ` X ) x. ( Im ` Y ) ) ) e. Constr )
71 40 70 eqeltrd 
 |-  ( ph -> ( ( Re ` X ) x. ( _i x. ( Im ` Y ) ) ) e. Constr )
72 16 11 13 mul12d 
 |-  ( ph -> ( ( Re ` Y ) x. ( _i x. ( Im ` X ) ) ) = ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) )
73 22 32 15 12 constrremulcl 
 |-  ( ph -> ( ( Re ` Y ) x. ( Im ` X ) ) e. Constr )
74 15 12 remulcld 
 |-  ( ph -> ( ( Re ` Y ) x. ( Im ` X ) ) e. RR )
75 16 13 mulcld 
 |-  ( ph -> ( ( Re ` Y ) x. ( Im ` X ) ) e. CC )
76 11 75 mulcld 
 |-  ( ph -> ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) e. CC )
77 75 50 mulcld 
 |-  ( ph -> ( ( ( Re ` Y ) x. ( Im ` X ) ) x. ( _i - 0 ) ) e. CC )
78 77 addlidd 
 |-  ( ph -> ( 0 + ( ( ( Re ` Y ) x. ( Im ` X ) ) x. ( _i - 0 ) ) ) = ( ( ( Re ` Y ) x. ( Im ` X ) ) x. ( _i - 0 ) ) )
79 53 oveq2d 
 |-  ( ph -> ( ( ( Re ` Y ) x. ( Im ` X ) ) x. ( _i - 0 ) ) = ( ( ( Re ` Y ) x. ( Im ` X ) ) x. _i ) )
80 75 11 mulcomd 
 |-  ( ph -> ( ( ( Re ` Y ) x. ( Im ` X ) ) x. _i ) = ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) )
81 78 79 80 3eqtrrd 
 |-  ( ph -> ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) = ( 0 + ( ( ( Re ` Y ) x. ( Im ` X ) ) x. ( _i - 0 ) ) ) )
82 11 75 absmuld 
 |-  ( ph -> ( abs ` ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) ) = ( ( abs ` _i ) x. ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) ) )
83 59 oveq1d 
 |-  ( ph -> ( ( abs ` _i ) x. ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) ) = ( 1 x. ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) ) )
84 75 abscld 
 |-  ( ph -> ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) e. RR )
85 84 recnd 
 |-  ( ph -> ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) e. CC )
86 85 mullidd 
 |-  ( ph -> ( 1 x. ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) ) = ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) )
87 82 83 86 3eqtrd 
 |-  ( ph -> ( abs ` ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) ) = ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) )
88 76 subid1d 
 |-  ( ph -> ( ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) - 0 ) = ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) )
89 88 fveq2d 
 |-  ( ph -> ( abs ` ( ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) - 0 ) ) = ( abs ` ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) ) )
90 75 subid1d 
 |-  ( ph -> ( ( ( Re ` Y ) x. ( Im ` X ) ) - 0 ) = ( ( Re ` Y ) x. ( Im ` X ) ) )
91 90 fveq2d 
 |-  ( ph -> ( abs ` ( ( ( Re ` Y ) x. ( Im ` X ) ) - 0 ) ) = ( abs ` ( ( Re ` Y ) x. ( Im ` X ) ) ) )
92 87 89 91 3eqtr4d 
 |-  ( ph -> ( abs ` ( ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) - 0 ) ) = ( abs ` ( ( ( Re ` Y ) x. ( Im ` X ) ) - 0 ) ) )
93 42 44 42 73 42 74 76 81 92 constrlccl 
 |-  ( ph -> ( _i x. ( ( Re ` Y ) x. ( Im ` X ) ) ) e. Constr )
94 72 93 eqeltrd 
 |-  ( ph -> ( ( Re ` Y ) x. ( _i x. ( Im ` X ) ) ) e. Constr )
95 71 94 constraddcl 
 |-  ( ph -> ( ( ( Re ` X ) x. ( _i x. ( Im ` Y ) ) ) + ( ( Re ` Y ) x. ( _i x. ( Im ` X ) ) ) ) e. Constr )
96 39 95 constraddcl 
 |-  ( ph -> ( ( ( ( Re ` X ) x. ( Re ` Y ) ) + ( ( _i x. ( Im ` Y ) ) x. ( _i x. ( Im ` X ) ) ) ) + ( ( ( Re ` X ) x. ( _i x. ( Im ` Y ) ) ) + ( ( Re ` Y ) x. ( _i x. ( Im ` X ) ) ) ) ) e. Constr )
97 20 96 eqeltrd 
 |-  ( ph -> ( ( ( Re ` X ) + ( _i x. ( Im ` X ) ) ) x. ( ( Re ` Y ) + ( _i x. ( Im ` Y ) ) ) ) e. Constr )
98 7 97 eqeltrd 
 |-  ( ph -> ( X x. Y ) e. Constr )