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 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
constrmulcl.2 ⊢ ( 𝜑 → 𝑌 ∈ Constr )
Assertion constrmulcl ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ Constr )

Proof

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