Metamath Proof Explorer

Theorem constrremulcl

Description: If two real numbers X and Y are constructible, then, so is their product. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses constrremulcl.1 
|- ( ph -> X e. Constr )
constrremulcl.2 
|- ( ph -> Y e. Constr )
constrremulcl.3 
|- ( ph -> X e. RR )
constrremulcl.4 
|- ( ph -> Y e. RR )
Assertion constrremulcl 
|- ( ph -> ( X x. Y ) e. Constr )

Proof

Step Hyp Ref Expression
1 constrremulcl.1 
 |-  ( ph -> X e. Constr )
2 constrremulcl.2 
 |-  ( ph -> Y e. Constr )
3 constrremulcl.3 
 |-  ( ph -> X e. RR )
4 constrremulcl.4 
 |-  ( ph -> Y e. RR )
5 simpr 
 |-  ( ( ph /\ X = 0 ) -> X = 0 )
6 5 oveq1d 
 |-  ( ( ph /\ X = 0 ) -> ( X x. Y ) = ( 0 x. Y ) )
7 4 recnd 
 |-  ( ph -> Y e. CC )
8 7 adantr 
 |-  ( ( ph /\ X = 0 ) -> Y e. CC )
9 8 mul02d 
 |-  ( ( ph /\ X = 0 ) -> ( 0 x. Y ) = 0 )
10 6 9 eqtrd 
 |-  ( ( ph /\ X = 0 ) -> ( X x. Y ) = 0 )
11 0nn0 
 |-  0 e. NN0
12 11 a1i 
 |-  ( ph -> 0 e. NN0 )
13 12 nn0constr 
 |-  ( ph -> 0 e. Constr )
14 13 adantr 
 |-  ( ( ph /\ X = 0 ) -> 0 e. Constr )
15 10 14 eqeltrd 
 |-  ( ( ph /\ X = 0 ) -> ( X x. Y ) e. Constr )
16 13 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> 0 e. Constr )
17 1 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> X e. Constr )
18 iconstr 
 |-  _i e. Constr
19 18 a1i 
 |-  ( ph -> _i e. Constr )
20 19 constrcn 
 |-  ( ph -> _i e. CC )
21 20 7 mulcld 
 |-  ( ph -> ( _i x. Y ) e. CC )
22 20 subid1d 
 |-  ( ph -> ( _i - 0 ) = _i )
23 22 oveq2d 
 |-  ( ph -> ( Y x. ( _i - 0 ) ) = ( Y x. _i ) )
24 22 20 eqeltrd 
 |-  ( ph -> ( _i - 0 ) e. CC )
25 7 24 mulcld 
 |-  ( ph -> ( Y x. ( _i - 0 ) ) e. CC )
26 25 addlidd 
 |-  ( ph -> ( 0 + ( Y x. ( _i - 0 ) ) ) = ( Y x. ( _i - 0 ) ) )
27 20 7 mulcomd 
 |-  ( ph -> ( _i x. Y ) = ( Y x. _i ) )
28 23 26 27 3eqtr4rd 
 |-  ( ph -> ( _i x. Y ) = ( 0 + ( Y x. ( _i - 0 ) ) ) )
29 20 7 absmuld 
 |-  ( ph -> ( abs ` ( _i x. Y ) ) = ( ( abs ` _i ) x. ( abs ` Y ) ) )
30 absi 
 |-  ( abs ` _i ) = 1
31 30 a1i 
 |-  ( ph -> ( abs ` _i ) = 1 )
32 31 oveq1d 
 |-  ( ph -> ( ( abs ` _i ) x. ( abs ` Y ) ) = ( 1 x. ( abs ` Y ) ) )
33 7 abscld 
 |-  ( ph -> ( abs ` Y ) e. RR )
34 33 recnd 
 |-  ( ph -> ( abs ` Y ) e. CC )
35 34 mullidd 
 |-  ( ph -> ( 1 x. ( abs ` Y ) ) = ( abs ` Y ) )
36 29 32 35 3eqtrd 
 |-  ( ph -> ( abs ` ( _i x. Y ) ) = ( abs ` Y ) )
37 21 subid1d 
 |-  ( ph -> ( ( _i x. Y ) - 0 ) = ( _i x. Y ) )
38 37 fveq2d 
 |-  ( ph -> ( abs ` ( ( _i x. Y ) - 0 ) ) = ( abs ` ( _i x. Y ) ) )
39 7 subid1d 
 |-  ( ph -> ( Y - 0 ) = Y )
40 39 fveq2d 
 |-  ( ph -> ( abs ` ( Y - 0 ) ) = ( abs ` Y ) )
41 36 38 40 3eqtr4d 
 |-  ( ph -> ( abs ` ( ( _i x. Y ) - 0 ) ) = ( abs ` ( Y - 0 ) ) )
42 13 19 13 2 13 4 21 28 41 constrlccl 
 |-  ( ph -> ( _i x. Y ) e. Constr )
43 42 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> ( _i x. Y ) e. Constr )
44 3 recnd 
 |-  ( ph -> X e. CC )
45 44 20 negsubd 
 |-  ( ph -> ( X + -u _i ) = ( X - _i ) )
46 19 constrnegcl 
 |-  ( ph -> -u _i e. Constr )
47 1 46 constraddcl 
 |-  ( ph -> ( X + -u _i ) e. Constr )
48 45 47 eqeltrrd 
 |-  ( ph -> ( X - _i ) e. Constr )
49 48 42 constraddcl 
 |-  ( ph -> ( ( X - _i ) + ( _i x. Y ) ) e. Constr )
50 49 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> ( ( X - _i ) + ( _i x. Y ) ) e. Constr )
51 4 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> Y e. RR )
52 44 7 mulcld 
 |-  ( ph -> ( X x. Y ) e. CC )
53 52 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> ( X x. Y ) e. CC )
54 44 subid1d 
 |-  ( ph -> ( X - 0 ) = X )
55 54 oveq2d 
 |-  ( ph -> ( Y x. ( X - 0 ) ) = ( Y x. X ) )
56 54 44 eqeltrd 
 |-  ( ph -> ( X - 0 ) e. CC )
57 7 56 mulcld 
 |-  ( ph -> ( Y x. ( X - 0 ) ) e. CC )
58 57 addlidd 
 |-  ( ph -> ( 0 + ( Y x. ( X - 0 ) ) ) = ( Y x. ( X - 0 ) ) )
59 44 7 mulcomd 
 |-  ( ph -> ( X x. Y ) = ( Y x. X ) )
60 55 58 59 3eqtr4rd 
 |-  ( ph -> ( X x. Y ) = ( 0 + ( Y x. ( X - 0 ) ) ) )
61 60 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> ( X x. Y ) = ( 0 + ( Y x. ( X - 0 ) ) ) )
62 44 20 subcld 
 |-  ( ph -> ( X - _i ) e. CC )
63 62 21 pncand 
 |-  ( ph -> ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) = ( X - _i ) )
64 63 oveq2d 
 |-  ( ph -> ( Y x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) = ( Y x. ( X - _i ) ) )
65 64 oveq2d 
 |-  ( ph -> ( ( _i x. Y ) + ( Y x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) = ( ( _i x. Y ) + ( Y x. ( X - _i ) ) ) )
66 7 44 20 subdid 
 |-  ( ph -> ( Y x. ( X - _i ) ) = ( ( Y x. X ) - ( Y x. _i ) ) )
67 59 27 oveq12d 
 |-  ( ph -> ( ( X x. Y ) - ( _i x. Y ) ) = ( ( Y x. X ) - ( Y x. _i ) ) )
68 66 67 eqtr4d 
 |-  ( ph -> ( Y x. ( X - _i ) ) = ( ( X x. Y ) - ( _i x. Y ) ) )
69 68 oveq2d 
 |-  ( ph -> ( ( _i x. Y ) + ( Y x. ( X - _i ) ) ) = ( ( _i x. Y ) + ( ( X x. Y ) - ( _i x. Y ) ) ) )
70 21 52 pncan3d 
 |-  ( ph -> ( ( _i x. Y ) + ( ( X x. Y ) - ( _i x. Y ) ) ) = ( X x. Y ) )
71 65 69 70 3eqtrrd 
 |-  ( ph -> ( X x. Y ) = ( ( _i x. Y ) + ( Y x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) )
72 71 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> ( X x. Y ) = ( ( _i x. Y ) + ( Y x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) )
73 54 fveq2d 
 |-  ( ph -> ( * ` ( X - 0 ) ) = ( * ` X ) )
74 3 cjred 
 |-  ( ph -> ( * ` X ) = X )
75 73 74 eqtrd 
 |-  ( ph -> ( * ` ( X - 0 ) ) = X )
76 63 45 eqtr4d 
 |-  ( ph -> ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) = ( X + -u _i ) )
77 75 76 oveq12d 
 |-  ( ph -> ( ( * ` ( X - 0 ) ) x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) = ( X x. ( X + -u _i ) ) )
78 20 negcld 
 |-  ( ph -> -u _i e. CC )
79 44 44 78 adddid 
 |-  ( ph -> ( X x. ( X + -u _i ) ) = ( ( X x. X ) + ( X x. -u _i ) ) )
80 44 78 mulcomd 
 |-  ( ph -> ( X x. -u _i ) = ( -u _i x. X ) )
81 mulneg12 
 |-  ( ( _i e. CC /\ X e. CC ) -> ( -u _i x. X ) = ( _i x. -u X ) )
82 20 44 81 syl2anc 
 |-  ( ph -> ( -u _i x. X ) = ( _i x. -u X ) )
83 80 82 eqtrd 
 |-  ( ph -> ( X x. -u _i ) = ( _i x. -u X ) )
84 83 oveq2d 
 |-  ( ph -> ( ( X x. X ) + ( X x. -u _i ) ) = ( ( X x. X ) + ( _i x. -u X ) ) )
85 77 79 84 3eqtrd 
 |-  ( ph -> ( ( * ` ( X - 0 ) ) x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) = ( ( X x. X ) + ( _i x. -u X ) ) )
86 85 fveq2d 
 |-  ( ph -> ( Im ` ( ( * ` ( X - 0 ) ) x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) = ( Im ` ( ( X x. X ) + ( _i x. -u X ) ) ) )
87 3 3 remulcld 
 |-  ( ph -> ( X x. X ) e. RR )
88 3 renegcld 
 |-  ( ph -> -u X e. RR )
89 87 88 crimd 
 |-  ( ph -> ( Im ` ( ( X x. X ) + ( _i x. -u X ) ) ) = -u X )
90 86 89 eqtrd 
 |-  ( ph -> ( Im ` ( ( * ` ( X - 0 ) ) x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) = -u X )
91 90 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> ( Im ` ( ( * ` ( X - 0 ) ) x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) = -u X )
92 44 adantr 
 |-  ( ( ph /\ X =/= 0 ) -> X e. CC )
93 simpr 
 |-  ( ( ph /\ X =/= 0 ) -> X =/= 0 )
94 92 93 negne0d 
 |-  ( ( ph /\ X =/= 0 ) -> -u X =/= 0 )
95 91 94 eqnetrd 
 |-  ( ( ph /\ X =/= 0 ) -> ( Im ` ( ( * ` ( X - 0 ) ) x. ( ( ( X - _i ) + ( _i x. Y ) ) - ( _i x. Y ) ) ) ) =/= 0 )
96 16 17 43 50 51 51 53 61 72 95 constrllcl 
 |-  ( ( ph /\ X =/= 0 ) -> ( X x. Y ) e. Constr )
97 15 96 pm2.61dane 
 |-  ( ph -> ( X x. Y ) e. Constr )