Metamath Proof Explorer


Theorem divccncf

Description: Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007)

Ref Expression
Hypothesis divccncf.1 โŠข ๐น = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ / ๐ด ) )
Assertion divccncf ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ๐น โˆˆ ( โ„‚ โ€“cnโ†’ โ„‚ ) )

Proof

Step Hyp Ref Expression
1 divccncf.1 โŠข ๐น = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ / ๐ด ) )
2 divrec2 โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ( ๐‘ฅ / ๐ด ) = ( ( 1 / ๐ด ) ยท ๐‘ฅ ) )
3 2 3expb โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ฅ / ๐ด ) = ( ( 1 / ๐ด ) ยท ๐‘ฅ ) )
4 3 ancoms โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ / ๐ด ) = ( ( 1 / ๐ด ) ยท ๐‘ฅ ) )
5 4 mpteq2dva โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ / ๐ด ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( 1 / ๐ด ) ยท ๐‘ฅ ) ) )
6 1 5 eqtrid โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ๐น = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( 1 / ๐ด ) ยท ๐‘ฅ ) ) )
7 reccl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ( 1 / ๐ด ) โˆˆ โ„‚ )
8 eqid โŠข ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( 1 / ๐ด ) ยท ๐‘ฅ ) ) = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( 1 / ๐ด ) ยท ๐‘ฅ ) )
9 8 mulc1cncf โŠข ( ( 1 / ๐ด ) โˆˆ โ„‚ โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( 1 / ๐ด ) ยท ๐‘ฅ ) ) โˆˆ ( โ„‚ โ€“cnโ†’ โ„‚ ) )
10 7 9 syl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( 1 / ๐ด ) ยท ๐‘ฅ ) ) โˆˆ ( โ„‚ โ€“cnโ†’ โ„‚ ) )
11 6 10 eqeltrd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0 ) โ†’ ๐น โˆˆ ( โ„‚ โ€“cnโ†’ โ„‚ ) )