Step |
Hyp |
Ref |
Expression |
1 |
|
igamval |
⊢ ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) ) |
2 |
|
0cnd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ( ℤ ∖ ℕ ) ) → 0 ∈ ℂ ) |
3 |
|
eldif |
⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ( ℤ ∖ ℕ ) ) ) |
4 |
|
gamcl |
⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℂ ) |
5 |
|
gamne0 |
⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ≠ 0 ) |
6 |
4 5
|
reccld |
⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( 1 / ( Γ ‘ 𝐴 ) ) ∈ ℂ ) |
7 |
3 6
|
sylbir |
⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ( ℤ ∖ ℕ ) ) → ( 1 / ( Γ ‘ 𝐴 ) ) ∈ ℂ ) |
8 |
2 7
|
ifclda |
⊢ ( 𝐴 ∈ ℂ → if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) ∈ ℂ ) |
9 |
1 8
|
eqeltrd |
⊢ ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) ∈ ℂ ) |