Metamath Proof Explorer


Theorem reexplog

Description: Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion reexplog ( ( ๐ด โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด โ†‘ ๐‘ ) = ( exp โ€˜ ( ๐‘ ยท ( log โ€˜ ๐ด ) ) ) )

Proof

Step Hyp Ref Expression
1 relogcl โŠข ( ๐ด โˆˆ โ„+ โ†’ ( log โ€˜ ๐ด ) โˆˆ โ„ )
2 1 recnd โŠข ( ๐ด โˆˆ โ„+ โ†’ ( log โ€˜ ๐ด ) โˆˆ โ„‚ )
3 efexp โŠข ( ( ( log โ€˜ ๐ด ) โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( exp โ€˜ ( ๐‘ ยท ( log โ€˜ ๐ด ) ) ) = ( ( exp โ€˜ ( log โ€˜ ๐ด ) ) โ†‘ ๐‘ ) )
4 2 3 sylan โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( exp โ€˜ ( ๐‘ ยท ( log โ€˜ ๐ด ) ) ) = ( ( exp โ€˜ ( log โ€˜ ๐ด ) ) โ†‘ ๐‘ ) )
5 reeflog โŠข ( ๐ด โˆˆ โ„+ โ†’ ( exp โ€˜ ( log โ€˜ ๐ด ) ) = ๐ด )
6 5 oveq1d โŠข ( ๐ด โˆˆ โ„+ โ†’ ( ( exp โ€˜ ( log โ€˜ ๐ด ) ) โ†‘ ๐‘ ) = ( ๐ด โ†‘ ๐‘ ) )
7 6 adantr โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( exp โ€˜ ( log โ€˜ ๐ด ) ) โ†‘ ๐‘ ) = ( ๐ด โ†‘ ๐‘ ) )
8 4 7 eqtr2d โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด โ†‘ ๐‘ ) = ( exp โ€˜ ( ๐‘ ยท ( log โ€˜ ๐ด ) ) ) )