Step |
Hyp |
Ref |
Expression |
1 |
|
divccncf.1 |
⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) |
2 |
|
divrec2 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝑥 ) ) |
3 |
2
|
3expb |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( 𝑥 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝑥 ) ) |
4 |
3
|
ancoms |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 / 𝐴 ) = ( ( 1 / 𝐴 ) · 𝑥 ) ) |
5 |
4
|
mpteq2dva |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) ) |
6 |
1 5
|
syl5eq |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐹 = ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) ) |
7 |
|
reccl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ ) |
8 |
|
eqid |
⊢ ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) |
9 |
8
|
mulc1cncf |
⊢ ( ( 1 / 𝐴 ) ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
10 |
7 9
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( ( 1 / 𝐴 ) · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
11 |
6 10
|
eqeltrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ ( ℂ –cn→ ℂ ) ) |