Metamath Proof Explorer


Theorem recoscl

Description: The cosine of a real number is real. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion recoscl ( ๐ด โˆˆ โ„ โ†’ ( cos โ€˜ ๐ด ) โˆˆ โ„ )

Proof

Step Hyp Ref Expression
1 recosval โŠข ( ๐ด โˆˆ โ„ โ†’ ( cos โ€˜ ๐ด ) = ( โ„œ โ€˜ ( exp โ€˜ ( i ยท ๐ด ) ) ) )
2 ax-icn โŠข i โˆˆ โ„‚
3 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
4 mulcl โŠข ( ( i โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( i ยท ๐ด ) โˆˆ โ„‚ )
5 2 3 4 sylancr โŠข ( ๐ด โˆˆ โ„ โ†’ ( i ยท ๐ด ) โˆˆ โ„‚ )
6 efcl โŠข ( ( i ยท ๐ด ) โˆˆ โ„‚ โ†’ ( exp โ€˜ ( i ยท ๐ด ) ) โˆˆ โ„‚ )
7 5 6 syl โŠข ( ๐ด โˆˆ โ„ โ†’ ( exp โ€˜ ( i ยท ๐ด ) ) โˆˆ โ„‚ )
8 7 recld โŠข ( ๐ด โˆˆ โ„ โ†’ ( โ„œ โ€˜ ( exp โ€˜ ( i ยท ๐ด ) ) ) โˆˆ โ„ )
9 1 8 eqeltrd โŠข ( ๐ด โˆˆ โ„ โ†’ ( cos โ€˜ ๐ด ) โˆˆ โ„ )