quotcl2

Description: Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014)

		Ref	Expression
	Assertion	quotcl2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to F quot G \in Poly (ℂ)$

Step	Hyp	Ref	Expression
1		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
2	1	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
3		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
4	3	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \land (x \in ℂ \land y \in ℂ)) \to x y \in ℂ$
5		reccl	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \in ℂ$
6	5	adantl	$⊢ ((F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \land (x \in ℂ \land x \neq 0)) \to \frac{1}{x} \in ℂ$
7		neg1cn	$⊢ - 1 \in ℂ$
8	7	a1i	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to - 1 \in ℂ$
9		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
10		simp1	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to F \in Poly (S)$
11	9 10	sselid	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to F \in Poly (ℂ)$
12		simp2	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to G \in Poly (S)$
13	9 12	sselid	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to G \in Poly (ℂ)$
14		simp3	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to G \neq 0_{𝑝}$
15	2 4 6 8 11 13 14	quotcl	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to F quot G \in Poly (ℂ)$

Metamath Proof Explorer