divccncf

Description: Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007)

		Ref	Expression
	Hypothesis	divccncf.1	$⊢ F = (x \in ℂ ⟼ \frac{x}{A})$
	Assertion	divccncf	$⊢ (A \in ℂ \land A \neq 0) \to F : ℂ \underset{cn}{⟶} ℂ$

Step	Hyp	Ref	Expression
1		divccncf.1	$⊢ F = (x \in ℂ ⟼ \frac{x}{A})$
2		divrec2	$⊢ (x \in ℂ \land A \in ℂ \land A \neq 0) \to \frac{x}{A} = (\frac{1}{A}) x$
3	2	3expb	$⊢ (x \in ℂ \land (A \in ℂ \land A \neq 0)) \to \frac{x}{A} = (\frac{1}{A}) x$
4	3	ancoms	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℂ) \to \frac{x}{A} = (\frac{1}{A}) x$
5	4	mpteq2dva	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ \frac{x}{A}) = (x \in ℂ ⟼ (\frac{1}{A}) x)$
6	1 5	eqtrid	$⊢ (A \in ℂ \land A \neq 0) \to F = (x \in ℂ ⟼ (\frac{1}{A}) x)$
7		reccl	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \in ℂ$
8		eqid	$⊢ (x \in ℂ ⟼ (\frac{1}{A}) x) = (x \in ℂ ⟼ (\frac{1}{A}) x)$
9	8	mulc1cncf	$⊢ \frac{1}{A} \in ℂ \to (x \in ℂ ⟼ (\frac{1}{A}) x) : ℂ \underset{cn}{⟶} ℂ$
10	7 9	syl	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ (\frac{1}{A}) x) : ℂ \underset{cn}{⟶} ℂ$
11	6 10	eqeltrd	$⊢ (A \in ℂ \land A \neq 0) \to F : ℂ \underset{cn}{⟶} ℂ$

Metamath Proof Explorer