Metamath Proof Explorer

Theorem addcnlem

Description: Lemma for addcn , subcn , and mulcn . (Contributed by Mario Carneiro, 5-May-2014) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses addcn.j 
|- J = ( TopOpen ` CCfld )
addcn.2 
|- .+ : ( CC X. CC ) --> CC
addcn.3 
|- ( ( 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 ) )
Assertion addcnlem 
|- .+ e. ( ( J tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 addcn.j 
 |-  J = ( TopOpen ` CCfld )
2 addcn.2 
 |-  .+ : ( CC X. CC ) --> CC
3 addcn.3 
 |-  ( ( 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 ) )
4 3 3coml 
 |-  ( ( b e. CC /\ c e. CC /\ a e. RR+ ) -> 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 ) )
5 ifcl 
 |-  ( ( y e. RR+ /\ z e. RR+ ) -> if ( y <_ z , y , z ) e. RR+ )
6 5 adantl 
 |-  ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> if ( y <_ z , y , z ) e. RR+ )
7 simpll1 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> b e. CC )
8 simprl 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> u e. CC )
9 eqid 
 |-  ( abs o. - ) = ( abs o. - )
10 9 cnmetdval 
 |-  ( ( b e. CC /\ u e. CC ) -> ( b ( abs o. - ) u ) = ( abs ` ( b - u ) ) )
11 abssub 
 |-  ( ( b e. CC /\ u e. CC ) -> ( abs ` ( b - u ) ) = ( abs ` ( u - b ) ) )
12 10 11 eqtrd 
 |-  ( ( b e. CC /\ u e. CC ) -> ( b ( abs o. - ) u ) = ( abs ` ( u - b ) ) )
13 7 8 12 syl2anc 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( b ( abs o. - ) u ) = ( abs ` ( u - b ) ) )
14 13 breq1d 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) <-> ( abs ` ( u - b ) ) < if ( y <_ z , y , z ) ) )
15 8 7 subcld 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( u - b ) e. CC )
16 15 abscld 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( abs ` ( u - b ) ) e. RR )
17 simplrl 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> y e. RR+ )
18 17 rpred 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> y e. RR )
19 simplrr 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> z e. RR+ )
20 19 rpred 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> z e. RR )
21 ltmin 
 |-  ( ( ( abs ` ( u - b ) ) e. RR /\ y e. RR /\ z e. RR ) -> ( ( abs ` ( u - b ) ) < if ( y <_ z , y , z ) <-> ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( u - b ) ) < z ) ) )
22 16 18 20 21 syl3anc 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( abs ` ( u - b ) ) < if ( y <_ z , y , z ) <-> ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( u - b ) ) < z ) ) )
23 14 22 bitrd 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) <-> ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( u - b ) ) < z ) ) )
24 simpl 
 |-  ( ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( u - b ) ) < z ) -> ( abs ` ( u - b ) ) < y )
25 23 24 syl6bi 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) -> ( abs ` ( u - b ) ) < y ) )
26 simpll2 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> c e. CC )
27 simprr 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> v e. CC )
28 9 cnmetdval 
 |-  ( ( c e. CC /\ v e. CC ) -> ( c ( abs o. - ) v ) = ( abs ` ( c - v ) ) )
29 abssub 
 |-  ( ( c e. CC /\ v e. CC ) -> ( abs ` ( c - v ) ) = ( abs ` ( v - c ) ) )
30 28 29 eqtrd 
 |-  ( ( c e. CC /\ v e. CC ) -> ( c ( abs o. - ) v ) = ( abs ` ( v - c ) ) )
31 26 27 30 syl2anc 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( c ( abs o. - ) v ) = ( abs ` ( v - c ) ) )
32 31 breq1d 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) <-> ( abs ` ( v - c ) ) < if ( y <_ z , y , z ) ) )
33 27 26 subcld 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( v - c ) e. CC )
34 33 abscld 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( abs ` ( v - c ) ) e. RR )
35 ltmin 
 |-  ( ( ( abs ` ( v - c ) ) e. RR /\ y e. RR /\ z e. RR ) -> ( ( abs ` ( v - c ) ) < if ( y <_ z , y , z ) <-> ( ( abs ` ( v - c ) ) < y /\ ( abs ` ( v - c ) ) < z ) ) )
36 34 18 20 35 syl3anc 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( abs ` ( v - c ) ) < if ( y <_ z , y , z ) <-> ( ( abs ` ( v - c ) ) < y /\ ( abs ` ( v - c ) ) < z ) ) )
37 32 36 bitrd 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) <-> ( ( abs ` ( v - c ) ) < y /\ ( abs ` ( v - c ) ) < z ) ) )
38 simpr 
 |-  ( ( ( abs ` ( v - c ) ) < y /\ ( abs ` ( v - c ) ) < z ) -> ( abs ` ( v - c ) ) < z )
39 37 38 syl6bi 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) -> ( abs ` ( v - c ) ) < z ) )
40 25 39 anim12d 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) -> ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( v - c ) ) < z ) ) )
41 2 fovcl 
 |-  ( ( b e. CC /\ c e. CC ) -> ( b .+ c ) e. CC )
42 7 26 41 syl2anc 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( b .+ c ) e. CC )
43 2 fovcl 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u .+ v ) e. CC )
44 43 adantl 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( u .+ v ) e. CC )
45 9 cnmetdval 
 |-  ( ( ( b .+ c ) e. CC /\ ( u .+ v ) e. CC ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) = ( abs ` ( ( b .+ c ) - ( u .+ v ) ) ) )
46 abssub 
 |-  ( ( ( b .+ c ) e. CC /\ ( u .+ v ) e. CC ) -> ( abs ` ( ( b .+ c ) - ( u .+ v ) ) ) = ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) )
47 45 46 eqtrd 
 |-  ( ( ( b .+ c ) e. CC /\ ( u .+ v ) e. CC ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) = ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) )
48 42 44 47 syl2anc 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) = ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) )
49 48 breq1d 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a <-> ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) < a ) )
50 49 biimprd 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) < a -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) )
51 40 50 imim12d 
 |-  ( ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ ( u e. CC /\ v e. CC ) ) -> ( ( ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( v - c ) ) < z ) -> ( abs ` ( ( u .+ v ) - ( b .+ c ) ) ) < a ) -> ( ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
52 51 ralimdvva 
 |-  ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ 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 ) -> A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
53 breq2 
 |-  ( x = if ( y <_ z , y , z ) -> ( ( b ( abs o. - ) u ) < x <-> ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) ) )
54 breq2 
 |-  ( x = if ( y <_ z , y , z ) -> ( ( c ( abs o. - ) v ) < x <-> ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) )
55 53 54 anbi12d 
 |-  ( x = if ( y <_ z , y , z ) -> ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) <-> ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) ) )
56 55 imbi1d 
 |-  ( x = if ( y <_ z , y , z ) -> ( ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) <-> ( ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
57 56 2ralbidv 
 |-  ( x = if ( y <_ z , y , z ) -> ( A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) <-> A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
58 57 rspcev 
 |-  ( ( if ( y <_ z , y , z ) e. RR+ /\ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < if ( y <_ z , y , z ) /\ ( c ( abs o. - ) v ) < if ( y <_ z , y , z ) ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) -> E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) )
59 6 52 58 syl6an 
 |-  ( ( ( b e. CC /\ c e. CC /\ a e. RR+ ) /\ ( y e. RR+ /\ 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 ) -> E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
60 59 rexlimdvva 
 |-  ( ( b e. CC /\ c e. CC /\ a e. RR+ ) -> ( 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 ) -> E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
61 4 60 mpd 
 |-  ( ( b e. CC /\ c e. CC /\ a e. RR+ ) -> E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) )
62 61 rgen3 
 |-  A. b e. CC A. c e. CC A. a e. RR+ E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a )
63 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
64 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
65 64 64 64 txmetcn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( abs o. - ) e. ( *Met ` CC ) /\ ( abs o. - ) e. ( *Met ` CC ) ) -> ( .+ e. ( ( J tX J ) Cn J ) <-> ( .+ : ( CC X. CC ) --> CC /\ A. b e. CC A. c e. CC A. a e. RR+ E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) ) )
66 63 63 63 65 mp3an 
 |-  ( .+ e. ( ( J tX J ) Cn J ) <-> ( .+ : ( CC X. CC ) --> CC /\ A. b e. CC A. c e. CC A. a e. RR+ E. x e. RR+ A. u e. CC A. v e. CC ( ( ( b ( abs o. - ) u ) < x /\ ( c ( abs o. - ) v ) < x ) -> ( ( b .+ c ) ( abs o. - ) ( u .+ v ) ) < a ) ) )
67 2 62 66 mpbir2an 
 |-  .+ e. ( ( J tX J ) Cn J )