MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcnlem Structured version   Visualization version   GIF version

Theorem addcnlem 24250
Description: Lemma for addcn 24251, subcn 24252, and mulcn 24253. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
addcn.j 𝐽 = (TopOpenβ€˜β„‚fld)
addcn.2 + :(β„‚ Γ— β„‚)βŸΆβ„‚
addcn.3 ((π‘Ž ∈ ℝ+ ∧ 𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž))
Assertion
Ref Expression
addcnlem + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽)
Distinct variable groups:   π‘Ž,𝑏,𝑐,𝑒,𝑣,𝑦,𝑧,𝐽   + ,π‘Ž,𝑏,𝑐,𝑒,𝑣,𝑦,𝑧

Proof of Theorem addcnlem
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 addcn.2 . 2 + :(β„‚ Γ— β„‚)βŸΆβ„‚
2 addcn.3 . . . . 5 ((π‘Ž ∈ ℝ+ ∧ 𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž))
323coml 1128 . . . 4 ((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž))
4 ifcl 4535 . . . . . . 7 ((𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+) β†’ if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∈ ℝ+)
54adantl 483 . . . . . 6 (((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) β†’ if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∈ ℝ+)
6 simpll1 1213 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑏 ∈ β„‚)
7 simprl 770 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑒 ∈ β„‚)
8 eqid 2733 . . . . . . . . . . . . . . 15 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
98cnmetdval 24157 . . . . . . . . . . . . . 14 ((𝑏 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (𝑏(abs ∘ βˆ’ )𝑒) = (absβ€˜(𝑏 βˆ’ 𝑒)))
10 abssub 15220 . . . . . . . . . . . . . 14 ((𝑏 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (absβ€˜(𝑏 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑏)))
119, 10eqtrd 2773 . . . . . . . . . . . . 13 ((𝑏 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (𝑏(abs ∘ βˆ’ )𝑒) = (absβ€˜(𝑒 βˆ’ 𝑏)))
126, 7, 11syl2anc 585 . . . . . . . . . . . 12 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (𝑏(abs ∘ βˆ’ )𝑒) = (absβ€˜(𝑒 βˆ’ 𝑏)))
1312breq1d 5119 . . . . . . . . . . 11 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ (absβ€˜(𝑒 βˆ’ 𝑏)) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)))
147, 6subcld 11520 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (𝑒 βˆ’ 𝑏) ∈ β„‚)
1514abscld 15330 . . . . . . . . . . . 12 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (absβ€˜(𝑒 βˆ’ 𝑏)) ∈ ℝ)
16 simplrl 776 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑦 ∈ ℝ+)
1716rpred 12965 . . . . . . . . . . . 12 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑦 ∈ ℝ)
18 simplrr 777 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑧 ∈ ℝ+)
1918rpred 12965 . . . . . . . . . . . 12 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑧 ∈ ℝ)
20 ltmin 13122 . . . . . . . . . . . 12 (((absβ€˜(𝑒 βˆ’ 𝑏)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ ((absβ€˜(𝑒 βˆ’ 𝑏)) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ ((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑧)))
2115, 17, 19, 20syl3anc 1372 . . . . . . . . . . 11 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((absβ€˜(𝑒 βˆ’ 𝑏)) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ ((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑧)))
2213, 21bitrd 279 . . . . . . . . . 10 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ ((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑧)))
23 simpl 484 . . . . . . . . . 10 (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑧) β†’ (absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦)
2422, 23syl6bi 253 . . . . . . . . 9 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ (absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦))
25 simpll2 1214 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑐 ∈ β„‚)
26 simprr 772 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ 𝑣 ∈ β„‚)
278cnmetdval 24157 . . . . . . . . . . . . . 14 ((𝑐 ∈ β„‚ ∧ 𝑣 ∈ β„‚) β†’ (𝑐(abs ∘ βˆ’ )𝑣) = (absβ€˜(𝑐 βˆ’ 𝑣)))
28 abssub 15220 . . . . . . . . . . . . . 14 ((𝑐 ∈ β„‚ ∧ 𝑣 ∈ β„‚) β†’ (absβ€˜(𝑐 βˆ’ 𝑣)) = (absβ€˜(𝑣 βˆ’ 𝑐)))
2927, 28eqtrd 2773 . . . . . . . . . . . . 13 ((𝑐 ∈ β„‚ ∧ 𝑣 ∈ β„‚) β†’ (𝑐(abs ∘ βˆ’ )𝑣) = (absβ€˜(𝑣 βˆ’ 𝑐)))
3025, 26, 29syl2anc 585 . . . . . . . . . . . 12 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (𝑐(abs ∘ βˆ’ )𝑣) = (absβ€˜(𝑣 βˆ’ 𝑐)))
3130breq1d 5119 . . . . . . . . . . 11 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ (absβ€˜(𝑣 βˆ’ 𝑐)) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)))
3226, 25subcld 11520 . . . . . . . . . . . . 13 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (𝑣 βˆ’ 𝑐) ∈ β„‚)
3332abscld 15330 . . . . . . . . . . . 12 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (absβ€˜(𝑣 βˆ’ 𝑐)) ∈ ℝ)
34 ltmin 13122 . . . . . . . . . . . 12 (((absβ€˜(𝑣 βˆ’ 𝑐)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ ((absβ€˜(𝑣 βˆ’ 𝑐)) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ ((absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧)))
3533, 17, 19, 34syl3anc 1372 . . . . . . . . . . 11 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((absβ€˜(𝑣 βˆ’ 𝑐)) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ ((absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧)))
3631, 35bitrd 279 . . . . . . . . . 10 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ↔ ((absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧)))
37 simpr 486 . . . . . . . . . 10 (((absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧)
3836, 37syl6bi 253 . . . . . . . . 9 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧))
3924, 38anim12d 610 . . . . . . . 8 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)) β†’ ((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧)))
401fovcl 7488 . . . . . . . . . . . 12 ((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚) β†’ (𝑏 + 𝑐) ∈ β„‚)
416, 25, 40syl2anc 585 . . . . . . . . . . 11 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (𝑏 + 𝑐) ∈ β„‚)
421fovcl 7488 . . . . . . . . . . . 12 ((𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚) β†’ (𝑒 + 𝑣) ∈ β„‚)
4342adantl 483 . . . . . . . . . . 11 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (𝑒 + 𝑣) ∈ β„‚)
448cnmetdval 24157 . . . . . . . . . . . 12 (((𝑏 + 𝑐) ∈ β„‚ ∧ (𝑒 + 𝑣) ∈ β„‚) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) = (absβ€˜((𝑏 + 𝑐) βˆ’ (𝑒 + 𝑣))))
45 abssub 15220 . . . . . . . . . . . 12 (((𝑏 + 𝑐) ∈ β„‚ ∧ (𝑒 + 𝑣) ∈ β„‚) β†’ (absβ€˜((𝑏 + 𝑐) βˆ’ (𝑒 + 𝑣))) = (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))))
4644, 45eqtrd 2773 . . . . . . . . . . 11 (((𝑏 + 𝑐) ∈ β„‚ ∧ (𝑒 + 𝑣) ∈ β„‚) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) = (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))))
4741, 43, 46syl2anc 585 . . . . . . . . . 10 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) = (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))))
4847breq1d 5119 . . . . . . . . 9 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ (((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž ↔ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž))
4948biimprd 248 . . . . . . . 8 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž))
5039, 49imim12d 81 . . . . . . 7 ((((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) ∧ (𝑒 ∈ β„‚ ∧ 𝑣 ∈ β„‚)) β†’ ((((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž) β†’ (((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
5150ralimdvva 3198 . . . . . 6 (((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) β†’ (βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž) β†’ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
52 breq2 5113 . . . . . . . . . 10 (π‘₯ = if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ ((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ↔ (𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)))
53 breq2 5113 . . . . . . . . . 10 (π‘₯ = if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ ((𝑐(abs ∘ βˆ’ )𝑣) < π‘₯ ↔ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)))
5452, 53anbi12d 632 . . . . . . . . 9 (π‘₯ = if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) ↔ ((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧))))
5554imbi1d 342 . . . . . . . 8 (π‘₯ = if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ ((((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž) ↔ (((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
56552ralbidv 3209 . . . . . . 7 (π‘₯ = if(𝑦 ≀ 𝑧, 𝑦, 𝑧) β†’ (βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž) ↔ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
5756rspcev 3583 . . . . . 6 ((if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∈ ℝ+ ∧ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧) ∧ (𝑐(abs ∘ βˆ’ )𝑣) < if(𝑦 ≀ 𝑧, 𝑦, 𝑧)) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)) β†’ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž))
585, 51, 57syl6an 683 . . . . 5 (((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) β†’ (βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž) β†’ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
5958rexlimdvva 3202 . . . 4 ((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) β†’ (βˆƒπ‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((absβ€˜(𝑒 βˆ’ 𝑏)) < 𝑦 ∧ (absβ€˜(𝑣 βˆ’ 𝑐)) < 𝑧) β†’ (absβ€˜((𝑒 + 𝑣) βˆ’ (𝑏 + 𝑐))) < π‘Ž) β†’ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
603, 59mpd 15 . . 3 ((𝑏 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ∧ π‘Ž ∈ ℝ+) β†’ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž))
6160rgen3 3196 . 2 βˆ€π‘ ∈ β„‚ βˆ€π‘ ∈ β„‚ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)
62 cnxmet 24159 . . 3 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
63 addcn.j . . . . 5 𝐽 = (TopOpenβ€˜β„‚fld)
6463cnfldtopn 24168 . . . 4 𝐽 = (MetOpenβ€˜(abs ∘ βˆ’ ))
6564, 64, 64txmetcn 23927 . . 3 (((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)) β†’ ( + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ↔ ( + :(β„‚ Γ— β„‚)βŸΆβ„‚ ∧ βˆ€π‘ ∈ β„‚ βˆ€π‘ ∈ β„‚ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž))))
6662, 62, 62, 65mp3an 1462 . 2 ( + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽) ↔ ( + :(β„‚ Γ— β„‚)βŸΆβ„‚ ∧ βˆ€π‘ ∈ β„‚ βˆ€π‘ ∈ β„‚ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘₯ ∈ ℝ+ βˆ€π‘’ ∈ β„‚ βˆ€π‘£ ∈ β„‚ (((𝑏(abs ∘ βˆ’ )𝑒) < π‘₯ ∧ (𝑐(abs ∘ βˆ’ )𝑣) < π‘₯) β†’ ((𝑏 + 𝑐)(abs ∘ βˆ’ )(𝑒 + 𝑣)) < π‘Ž)))
671, 61, 66mpbir2an 710 1 + ∈ ((𝐽 Γ—t 𝐽) Cn 𝐽)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070  ifcif 4490   class class class wbr 5109   Γ— cxp 5635   ∘ ccom 5641  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  β„‚cc 11057  β„cr 11058   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393  β„+crp 12923  abscabs 15128  TopOpenctopn 17311  βˆžMetcxmet 20804  β„‚fldccnfld 20819   Cn ccn 22598   Γ—t ctx 22934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-z 12508  df-dec 12627  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-icc 13280  df-fz 13434  df-fzo 13577  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-struct 17027  df-sets 17044  df-slot 17062  df-ndx 17074  df-base 17092  df-ress 17121  df-plusg 17154  df-mulr 17155  df-starv 17156  df-sca 17157  df-vsca 17158  df-ip 17159  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-hom 17165  df-cco 17166  df-rest 17312  df-topn 17313  df-0g 17331  df-gsum 17332  df-topgen 17333  df-pt 17334  df-prds 17337  df-xrs 17392  df-qtop 17397  df-imas 17398  df-xps 17400  df-mre 17474  df-mrc 17475  df-acs 17477  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-submnd 18610  df-mulg 18881  df-cntz 19105  df-cmn 19572  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-cnfld 20820  df-top 22266  df-topon 22283  df-topsp 22305  df-bases 22319  df-cn 22601  df-cnp 22602  df-tx 22936  df-hmeo 23129  df-xms 23696  df-tms 23698
This theorem is referenced by:  addcn  24251  subcn  24252  mulcn  24253
  Copyright terms: Public domain W3C validator