MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulcn2 Unicode version

Theorem mulcn2 12920
Description: Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
Assertion
Ref Expression
mulcn2
Distinct variable groups:   , , , ,   , , , ,   , , , ,

Proof of Theorem mulcn2
StepHypRef Expression
1 rphalfcl 10879 . . . 4
213ad2ant1 983 . . 3
3 abscl 12614 . . . . . 6
433ad2ant3 985 . . . . 5
5 abscl 12614 . . . . . . . . . 10
653ad2ant2 984 . . . . . . . . 9
7 1re 9264 . . . . . . . . 9
8 readdcl 9244 . . . . . . . . 9
96, 7, 8sylancl 645 . . . . . . . 8
10 absge0 12623 . . . . . . . . . 10
11 0lt1 9736 . . . . . . . . . . 11
12 addgegt0 9700 . . . . . . . . . . . 12
1312an4s 801 . . . . . . . . . . 11
147, 11, 13mpanr12 668 . . . . . . . . . 10
155, 10, 14syl2anc 644 . . . . . . . . 9
16153ad2ant2 984 . . . . . . . 8
179, 16elrpd 10889 . . . . . . 7
182, 17rpdivcld 10908 . . . . . 6
1918rpred 10891 . . . . 5
204, 19readdcld 9292 . . . 4
21 absge0 12623 . . . . . 6
22213ad2ant3 985 . . . . 5
23 elrp 10857 . . . . . 6
24 addgegt0 9700 . . . . . . 7
2524an4s 801 . . . . . 6
2623, 25sylan2b 463 . . . . 5
274, 22, 18, 26syl21anc 1191 . . . 4
2820, 27elrpd 10889 . . 3
292, 28rpdivcld 10908 . 2
30 simprl 734 . . . . . . . . . . 11
31 simpl2 966 . . . . . . . . . . 11
3230, 31subcld 9594 . . . . . . . . . 10
3332abscld 12769 . . . . . . . . 9
342adantr 453 . . . . . . . . . 10
3534rpred 10891 . . . . . . . . 9
3628adantr 453 . . . . . . . . 9
3733, 35, 36ltmuldivd 10934 . . . . . . . 8
38 simprr 735 . . . . . . . . . . . . . 14
39 simpl3 967 . . . . . . . . . . . . . 14
4038, 39abs2difd 12790 . . . . . . . . . . . . 13
4138abscld 12769 . . . . . . . . . . . . . . 15
424adantr 453 . . . . . . . . . . . . . . 15
4341, 42resubcld 9650 . . . . . . . . . . . . . 14
4438, 39subcld 9594 . . . . . . . . . . . . . . 15
4544abscld 12769 . . . . . . . . . . . . . 14
4619adantr 453 . . . . . . . . . . . . . 14
47 lelttr 9344 . . . . . . . . . . . . . 14
4843, 45, 46, 47syl3anc 1192 . . . . . . . . . . . . 13
4940, 48mpand 658 . . . . . . . . . . . 12
5041, 42, 46ltsubadd2d 9810 . . . . . . . . . . . 12
5149, 50sylibd 207 . . . . . . . . . . 11
5220adantr 453 . . . . . . . . . . . 12
53 ltle 9342 . . . . . . . . . . . 12
5441, 52, 53syl2anc 644 . . . . . . . . . . 11
5551, 54syld 43 . . . . . . . . . 10
5632absge0d 12777 . . . . . . . . . . 11
57 lemul2a 10053 . . . . . . . . . . . 12
5857ex 425 . . . . . . . . . . 11
5941, 52, 33, 56, 58syl112anc 1196 . . . . . . . . . 10
6033, 41remulcld 9293 . . . . . . . . . . . 12
6133, 52remulcld 9293 . . . . . . . . . . . 12
62 lelttr 9344 . . . . . . . . . . . 12
6360, 61, 35, 62syl3anc 1192 . . . . . . . . . . 11
6463exp3a 427 . . . . . . . . . 10
6555, 59, 643syld 54 . . . . . . . . 9
6665com23 75 . . . . . . . 8
6737, 66sylbird 228 . . . . . . 7
6867imp3a 422 . . . . . 6
6932, 38absmuld 12787 . . . . . . . 8
7030, 31, 38subdird 9675 . . . . . . . . 9
7170fveq2d 5712 . . . . . . . 8
7269, 71eqtr3d 2523 . . . . . . 7
7372breq1d 4328 . . . . . 6
7468, 73sylibd 207 . . . . 5
7517adantr 453 . . . . . . . 8
7645, 35, 75ltmuldiv2d 10935 . . . . . . 7
7731, 38, 39subdid 9674 . . . . . . . . . . 11
7877fveq2d 5712 . . . . . . . . . 10
7931, 44absmuld 12787 . . . . . . . . . 10
8078, 79eqtr3d 2523 . . . . . . . . 9
8131abscld 12769 . . . . . . . . . . 11
8281lep1d 10130 . . . . . . . . . 10
839adantr 453 . . . . . . . . . . 11
84 abscl 12614 . . . . . . . . . . . . 13
85 absge0 12623 . . . . . . . . . . . . 13
8684, 85jca 520 . . . . . . . . . . . 12
87 lemul1a 10052 . . . . . . . . . . . . 13
8887ex 425 . . . . . . . . . . . 12
8986, 88syl3an3 1227 . . . . . . . . . . 11
9081, 83, 44, 89syl3anc 1192 . . . . . . . . . 10
9182, 90mpd 15 . . . . . . . . 9
9280, 91eqbrtrd 4338 . . . . . . . 8
9331, 38mulcld 9285 . . . . . . . . . . 11
9431, 39mulcld 9285 . . . . . . . . . . 11
9593, 94subcld 9594 . . . . . . . . . 10
9695abscld 12769 . . . . . . . . 9
9783, 45remulcld 9293 . . . . . . . . 9
98 lelttr 9344 . . . . . . . . 9
9996, 97, 35, 98syl3anc 1192 . . . . . . . 8
10092, 99mpand 658 . . . . . . 7
10176, 100sylbird 228 . . . . . 6
102101adantld 455 . . . . 5
10374, 102jcad 521 . . . 4
104 mulcl 9245 . . . . . 6
105104adantl 454 . . . . 5
106 simpl1 965 . . . . . 6
107106rpred 10891 . . . . 5
108 abs3lem 12673 . . . . 5
109105, 94, 93, 107, 108syl22anc 1193 . . . 4
110103, 109syld 43 . . 3
111110ralrimivva 2852 . 2
112 breq2 4322 . . . . . 6
113112anbi1d 687 . . . . 5
114113imbi1d 310 . . . 4
1151142ralbidv 2801 . . 3
116 breq2 4322 . . . . . 6
117116anbi2d 686 . . . . 5
118117imbi1d 310 . . . 4
1191182ralbidv 2801 . . 3
120115, 119rspc2ev 3121 . 2
12129, 18, 111, 120syl3anc 1192 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  /\w3a 939  =wceq 1670  e.wcel 1732  A.wral 2759  E.wrex 2760   class class class wbr 4318  `cfv 5438  (class class class)co 6103   cc 9159   cr 9160  0cc0 9161  1c1 9162   caddc 9164   cmul 9166   clt 9297   cle 9298   cmin 9472   cdiv 9864  2c2 10237   crp 10855   cabs 12570
This theorem is referenced by:  climmul  12957  rlimmul  12969  mulcn  19912  mulc1cncf  19950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-cnex 9217  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238  ax-pre-sup 9239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rmo 2767  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6487  df-2nd 6584  df-recs 6795  df-rdg 6830  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-sup 7613  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-div 9865  df-nn 10189  df-2 10246  df-3 10247  df-n0 10446  df-z 10511  df-uz 10726  df-rp 10856  df-seq 11656  df-exp 11715  df-cj 12435  df-re 12436  df-im 12437  df-sqr 12571  df-abs 12572
  Copyright terms: Public domain W3C validator