This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eftabs

Description: The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007)

Ref Expression
Assertion eftabs ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐾 ) ∈ ℂ )
2 faccl ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
3 2 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
4 3 nncnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
5 facne0 ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ≠ 0 )
6 5 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ≠ 0 )
7 1 4 6 absdivd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝐾 ) ) / ( abs ‘ ( ! ‘ 𝐾 ) ) ) )
8 absexp ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝐾 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) )
9 3 nnred ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℝ )
10 3 nnnn0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ! ‘ 𝐾 ) ∈ ℕ0 )
11 10 nn0ge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ ( ! ‘ 𝐾 ) )
12 9 11 absidd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ! ‘ 𝐾 ) ) = ( ! ‘ 𝐾 ) )
13 8 12 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( 𝐴 ↑ 𝐾 ) ) / ( abs ‘ ( ! ‘ 𝐾 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) )
14 7 13 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝐾 ) / ( ! ‘ 𝐾 ) ) )