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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
addcn.2 ⊢ + : ( ℂ × ℂ ) ⟶ ℂ
addcn.3 ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) )
Assertion addcnlem + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 addcn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 addcn.2 ⊢ + : ( ℂ × ℂ ) ⟶ ℂ
3 addcn.3 ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) )
4 3 3coml ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) )
5 ifcl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∈ ℝ+ )
6 5 adantl ⊢ ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∈ ℝ+ )
7 simpll1 ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑏 ∈ ℂ )
8 simprl ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑢 ∈ ℂ )
9 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
10 9 cnmetdval ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( 𝑏 ( abs ∘ − ) 𝑢 ) = ( abs ‘ ( 𝑏 − 𝑢 ) ) )
11 abssub ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( abs ‘ ( 𝑏 − 𝑢 ) ) = ( abs ‘ ( 𝑢 − 𝑏 ) ) )
12 10 11 eqtrd ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( 𝑏 ( abs ∘ − ) 𝑢 ) = ( abs ‘ ( 𝑢 − 𝑏 ) ) )
13 7 8 12 syl2anc ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑏 ( abs ∘ − ) 𝑢 ) = ( abs ‘ ( 𝑢 − 𝑏 ) ) )
14 13 breq1d ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( abs ‘ ( 𝑢 − 𝑏 ) ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
15 8 7 subcld ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑢 − 𝑏 ) ∈ ℂ )
16 15 abscld ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( abs ‘ ( 𝑢 − 𝑏 ) ) ∈ ℝ )
17 simplrl ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑦 ∈ ℝ+ )
18 17 rpred ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑦 ∈ ℝ )
19 simplrr ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑧 ∈ ℝ+ )
20 19 rpred ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑧 ∈ ℝ )
21 ltmin ⊢ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ) ) )
22 16 18 20 21 syl3anc ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ) ) )
23 14 22 bitrd ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ) ) )
24 simpl ⊢ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ) → ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 )
25 23 24 syl6bi ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ) )
26 simpll2 ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑐 ∈ ℂ )
27 simprr ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑣 ∈ ℂ )
28 9 cnmetdval ⊢ ( ( 𝑐 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑐 ( abs ∘ − ) 𝑣 ) = ( abs ‘ ( 𝑐 − 𝑣 ) ) )
29 abssub ⊢ ( ( 𝑐 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( abs ‘ ( 𝑐 − 𝑣 ) ) = ( abs ‘ ( 𝑣 − 𝑐 ) ) )
30 28 29 eqtrd ⊢ ( ( 𝑐 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑐 ( abs ∘ − ) 𝑣 ) = ( abs ‘ ( 𝑣 − 𝑐 ) ) )
31 26 27 30 syl2anc ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑐 ( abs ∘ − ) 𝑣 ) = ( abs ‘ ( 𝑣 − 𝑐 ) ) )
32 31 breq1d ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( abs ‘ ( 𝑣 − 𝑐 ) ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
33 27 26 subcld ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑣 − 𝑐 ) ∈ ℂ )
34 33 abscld ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( abs ‘ ( 𝑣 − 𝑐 ) ) ∈ ℝ )
35 ltmin ⊢ ( ( ( abs ‘ ( 𝑣 − 𝑐 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( abs ‘ ( 𝑣 − 𝑐 ) ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) ) )
36 34 18 20 35 syl3anc ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( abs ‘ ( 𝑣 − 𝑐 ) ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) ) )
37 32 36 bitrd ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ↔ ( ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) ) )
38 simpr ⊢ ( ( ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 )
39 37 38 syl6bi ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) )
40 25 39 anim12d ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) → ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) ) )
41 2 fovcl ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑏 + 𝑐 ) ∈ ℂ )
42 7 26 41 syl2anc ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑏 + 𝑐 ) ∈ ℂ )
43 2 fovcl ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 + 𝑣 ) ∈ ℂ )
44 43 adantl ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑢 + 𝑣 ) ∈ ℂ )
45 9 cnmetdval ⊢ ( ( ( 𝑏 + 𝑐 ) ∈ ℂ ∧ ( 𝑢 + 𝑣 ) ∈ ℂ ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) = ( abs ‘ ( ( 𝑏 + 𝑐 ) − ( 𝑢 + 𝑣 ) ) ) )
46 abssub ⊢ ( ( ( 𝑏 + 𝑐 ) ∈ ℂ ∧ ( 𝑢 + 𝑣 ) ∈ ℂ ) → ( abs ‘ ( ( 𝑏 + 𝑐 ) − ( 𝑢 + 𝑣 ) ) ) = ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) )
47 45 46 eqtrd ⊢ ( ( ( 𝑏 + 𝑐 ) ∈ ℂ ∧ ( 𝑢 + 𝑣 ) ∈ ℂ ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) = ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) )
48 42 44 47 syl2anc ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) = ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) )
49 48 breq1d ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ↔ ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) )
50 49 biimprd ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) )
51 40 50 imim12d ⊢ ( ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) → ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
52 51 ralimdvva ⊢ ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) → ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
53 breq2 ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ↔ ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
54 breq2 ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ↔ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) )
55 53 54 anbi12d ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) ↔ ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) ) )
56 55 imbi1d ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ↔ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
57 56 2ralbidv ⊢ ( 𝑥 = if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ↔ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
58 57 rspcev ⊢ ( ( if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∈ ℝ+ ∧ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < if ( 𝑦 ≤ 𝑧 , 𝑦 , 𝑧 ) ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) )
59 6 52 58 syl6an ⊢ ( ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
60 59 rexlimdvva ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝑏 + 𝑐 ) ) ) < 𝑎 ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
61 4 60 mpd ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) )
62 61 rgen3 ⊢ ∀ 𝑏 ∈ ℂ ∀ 𝑐 ∈ ℂ ∀ 𝑎 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 )
63 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
64 1 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
65 64 64 64 txmetcn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) → ( + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ↔ ( + : ( ℂ × ℂ ) ⟶ ℂ ∧ ∀ 𝑏 ∈ ℂ ∀ 𝑐 ∈ ℂ ∀ 𝑎 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) ) )
66 63 63 63 65 mp3an ⊢ ( + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ↔ ( + : ( ℂ × ℂ ) ⟶ ℂ ∧ ∀ 𝑏 ∈ ℂ ∀ 𝑐 ∈ ℂ ∀ 𝑎 ∈ ℝ+ ∃ 𝑥 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( 𝑏 ( abs ∘ − ) 𝑢 ) < 𝑥 ∧ ( 𝑐 ( abs ∘ − ) 𝑣 ) < 𝑥 ) → ( ( 𝑏 + 𝑐 ) ( abs ∘ − ) ( 𝑢 + 𝑣 ) ) < 𝑎 ) ) )
67 2 62 66 mpbir2an ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )