Step |
Hyp |
Ref |
Expression |
1 |
|
chpval |
⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) ) |
2 |
1
|
fveq2d |
⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ψ ‘ 𝐴 ) ) = ( exp ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) ) ) |
3 |
|
fzfid |
⊢ ( 𝐴 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ) |
4 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ ) |
5 |
4
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ ) |
6 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
7 |
5 6
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
8 |
|
efvmacl |
⊢ ( 𝑛 ∈ ℕ → ( exp ‘ ( Λ ‘ 𝑛 ) ) ∈ ℕ ) |
9 |
5 8
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( exp ‘ ( Λ ‘ 𝑛 ) ) ∈ ℕ ) |
10 |
3 7 9
|
efnnfsumcl |
⊢ ( 𝐴 ∈ ℝ → ( exp ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) ) ∈ ℕ ) |
11 |
2 10
|
eqeltrd |
⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ψ ‘ 𝐴 ) ) ∈ ℕ ) |