Metamath Proof Explorer

Theorem addcn2

Description: Complex number addition is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion addcn2 
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )

Proof

Step Hyp Ref Expression
1 rphalfcl 
 |-  ( A e. RR+ -> ( A / 2 ) e. RR+ )
2 1 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> ( A / 2 ) e. RR+ )
3 simprl 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> u e. CC )
4 simpl2 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> B e. CC )
5 simprr 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> v e. CC )
6 3 4 5 pnpcan2d 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( u + v ) - ( B + v ) ) = ( u - B ) )
7 6 fveq2d 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( abs ` ( ( u + v ) - ( B + v ) ) ) = ( abs ` ( u - B ) ) )
8 7 breq1d 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( abs ` ( ( u + v ) - ( B + v ) ) ) < ( A / 2 ) <-> ( abs ` ( u - B ) ) < ( A / 2 ) ) )
9 simpl3 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> C e. CC )
10 4 5 9 pnpcand 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( B + v ) - ( B + C ) ) = ( v - C ) )
11 10 fveq2d 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( abs ` ( ( B + v ) - ( B + C ) ) ) = ( abs ` ( v - C ) ) )
12 11 breq1d 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( abs ` ( ( B + v ) - ( B + C ) ) ) < ( A / 2 ) <-> ( abs ` ( v - C ) ) < ( A / 2 ) ) )
13 8 12 anbi12d 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( ( abs ` ( ( u + v ) - ( B + v ) ) ) < ( A / 2 ) /\ ( abs ` ( ( B + v ) - ( B + C ) ) ) < ( A / 2 ) ) <-> ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) ) )
14 addcl 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u + v ) e. CC )
15 14 adantl 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( u + v ) e. CC )
16 4 9 addcld 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( B + C ) e. CC )
17 4 5 addcld 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( B + v ) e. CC )
18 simpl1 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> A e. RR+ )
19 18 rpred 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> A e. RR )
20 abs3lem 
 |-  ( ( ( ( u + v ) e. CC /\ ( B + C ) e. CC ) /\ ( ( B + v ) e. CC /\ A e. RR ) ) -> ( ( ( abs ` ( ( u + v ) - ( B + v ) ) ) < ( A / 2 ) /\ ( abs ` ( ( B + v ) - ( B + C ) ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
21 15 16 17 19 20 syl22anc 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( ( abs ` ( ( u + v ) - ( B + v ) ) ) < ( A / 2 ) /\ ( abs ` ( ( B + v ) - ( B + C ) ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
22 13 21 sylbird 
 |-  ( ( ( A e. RR+ /\ B e. CC /\ C e. CC ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
23 22 ralrimivva 
 |-  ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
24 breq2 
 |-  ( y = ( A / 2 ) -> ( ( abs ` ( u - B ) ) < y <-> ( abs ` ( u - B ) ) < ( A / 2 ) ) )
25 24 anbi1d 
 |-  ( y = ( A / 2 ) -> ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) <-> ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < z ) ) )
26 25 imbi1d 
 |-  ( y = ( A / 2 ) -> ( ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) <-> ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) ) )
27 26 2ralbidv 
 |-  ( y = ( A / 2 ) -> ( A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) <-> A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) ) )
28 breq2 
 |-  ( z = ( A / 2 ) -> ( ( abs ` ( v - C ) ) < z <-> ( abs ` ( v - C ) ) < ( A / 2 ) ) )
29 28 anbi2d 
 |-  ( z = ( A / 2 ) -> ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < z ) <-> ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) ) )
30 29 imbi1d 
 |-  ( z = ( A / 2 ) -> ( ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) <-> ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) ) )
31 30 2ralbidv 
 |-  ( z = ( A / 2 ) -> ( A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) <-> A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) ) )
32 27 31 rspc2ev 
 |-  ( ( ( A / 2 ) e. RR+ /\ ( A / 2 ) e. RR+ /\ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < ( A / 2 ) /\ ( abs ` ( v - C ) ) < ( A / 2 ) ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
33 2 2 23 32 syl3anc 
 |-  ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )