Metamath Proof Explorer

Theorem constraddcl

Description: Constructive numbers are closed under complex addition. (Contributed by Thierry Arnoux, 2-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 constraddcl.1 
 |-  ( ph -> X e. Constr )
2 constraddcl.2 
 |-  ( ph -> Y e. Constr )
3 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
4 3 oveq2d 
 |-  ( ( ph /\ X = Y ) -> ( X + X ) = ( X + Y ) )
5 0nn0 
 |-  0 e. NN0
6 5 a1i 
 |-  ( ph -> 0 e. NN0 )
7 6 nn0constr 
 |-  ( ph -> 0 e. Constr )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( ph -> 2 e. RR )
10 1 constrcn 
 |-  ( ph -> X e. CC )
11 10 10 addcld 
 |-  ( ph -> ( X + X ) e. CC )
12 2cnd 
 |-  ( ph -> 2 e. CC )
13 0cnd 
 |-  ( ph -> 0 e. CC )
14 10 13 subcld 
 |-  ( ph -> ( X - 0 ) e. CC )
15 12 14 mulcld 
 |-  ( ph -> ( 2 x. ( X - 0 ) ) e. CC )
16 15 addlidd 
 |-  ( ph -> ( 0 + ( 2 x. ( X - 0 ) ) ) = ( 2 x. ( X - 0 ) ) )
17 10 subid1d 
 |-  ( ph -> ( X - 0 ) = X )
18 17 oveq2d 
 |-  ( ph -> ( 2 x. ( X - 0 ) ) = ( 2 x. X ) )
19 10 2timesd 
 |-  ( ph -> ( 2 x. X ) = ( X + X ) )
20 16 18 19 3eqtrrd 
 |-  ( ph -> ( X + X ) = ( 0 + ( 2 x. ( X - 0 ) ) ) )
21 10 10 pncand 
 |-  ( ph -> ( ( X + X ) - X ) = X )
22 21 17 eqtr4d 
 |-  ( ph -> ( ( X + X ) - X ) = ( X - 0 ) )
23 22 fveq2d 
 |-  ( ph -> ( abs ` ( ( X + X ) - X ) ) = ( abs ` ( X - 0 ) ) )
24 7 1 1 1 7 9 11 20 23 constrlccl 
 |-  ( ph -> ( X + X ) e. Constr )
25 24 adantr 
 |-  ( ( ph /\ X = Y ) -> ( X + X ) e. Constr )
26 4 25 eqeltrrd 
 |-  ( ( ph /\ X = Y ) -> ( X + Y ) e. Constr )
27 1 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. Constr )
28 2 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. Constr )
29 7 adantr 
 |-  ( ( ph /\ X =/= Y ) -> 0 e. Constr )
30 10 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. CC )
31 2 constrcn 
 |-  ( ph -> Y e. CC )
32 31 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. CC )
33 30 32 addcld 
 |-  ( ( ph /\ X =/= Y ) -> ( X + Y ) e. CC )
34 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
35 30 32 pncan2d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( X + Y ) - X ) = Y )
36 32 subid1d 
 |-  ( ( ph /\ X =/= Y ) -> ( Y - 0 ) = Y )
37 35 36 eqtr4d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( X + Y ) - X ) = ( Y - 0 ) )
38 37 fveq2d 
 |-  ( ( ph /\ X =/= Y ) -> ( abs ` ( ( X + Y ) - X ) ) = ( abs ` ( Y - 0 ) ) )
39 30 32 pncand 
 |-  ( ( ph /\ X =/= Y ) -> ( ( X + Y ) - Y ) = X )
40 30 subid1d 
 |-  ( ( ph /\ X =/= Y ) -> ( X - 0 ) = X )
41 39 40 eqtr4d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( X + Y ) - Y ) = ( X - 0 ) )
42 41 fveq2d 
 |-  ( ( ph /\ X =/= Y ) -> ( abs ` ( ( X + Y ) - Y ) ) = ( abs ` ( X - 0 ) ) )
43 27 28 29 28 27 29 33 34 38 42 constrcccl 
 |-  ( ( ph /\ X =/= Y ) -> ( X + Y ) e. Constr )
44 26 43 pm2.61dane 
 |-  ( ph -> ( X + Y ) e. Constr )