Metamath Proof Explorer


Theorem abscl

Description: Real closure of absolute value. (Contributed by NM, 3-Oct-1999)

Ref Expression
Assertion abscl ( ๐ด โˆˆ โ„‚ โ†’ ( abs โ€˜ ๐ด ) โˆˆ โ„ )

Proof

Step Hyp Ref Expression
1 absval โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( abs โ€˜ ๐ด ) = ( โˆš โ€˜ ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) ) )
2 cjmulrcl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ )
3 cjmulge0 โŠข ( ๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) )
4 resqrtcl โŠข ( ( ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) โˆˆ โ„ โˆง 0 โ‰ค ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) ) โ†’ ( โˆš โ€˜ ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ )
5 2 3 4 syl2anc โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โˆš โ€˜ ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) ) ) โˆˆ โ„ )
6 1 5 eqeltrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( abs โ€˜ ๐ด ) โˆˆ โ„ )