qreccl

Description: Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004)

		Ref	Expression
	Assertion	qreccl	$⊢ (A \in ℚ \land A \neq 0) \to \frac{1}{A} \in ℚ$

Proof

Step	Hyp	Ref	Expression
1		elq	$⊢ A \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
2		nnne0	$⊢ y \in ℕ \to y \neq 0$
3	2	ancli	$⊢ y \in ℕ \to (y \in ℕ \land y \neq 0)$
4		neeq1	$⊢ A = \frac{x}{y} \to (A \neq 0 \leftrightarrow \frac{x}{y} \neq 0)$
5		zcn	$⊢ x \in ℤ \to x \in ℂ$
6		nncn	$⊢ y \in ℕ \to y \in ℂ$
7	5 6	anim12i	$⊢ (x \in ℤ \land y \in ℕ) \to (x \in ℂ \land y \in ℂ)$
8		divne0b	$⊢ (x \in ℂ \land y \in ℂ \land y \neq 0) \to (x \neq 0 \leftrightarrow \frac{x}{y} \neq 0)$
9	8	3expa	$⊢ ((x \in ℂ \land y \in ℂ) \land y \neq 0) \to (x \neq 0 \leftrightarrow \frac{x}{y} \neq 0)$
10	7 9	sylan	$⊢ ((x \in ℤ \land y \in ℕ) \land y \neq 0) \to (x \neq 0 \leftrightarrow \frac{x}{y} \neq 0)$
11	10	bicomd	$⊢ ((x \in ℤ \land y \in ℕ) \land y \neq 0) \to (\frac{x}{y} \neq 0 \leftrightarrow x \neq 0)$
12	4 11	sylan9bbr	$⊢ (((x \in ℤ \land y \in ℕ) \land y \neq 0) \land A = \frac{x}{y}) \to (A \neq 0 \leftrightarrow x \neq 0)$
13		nnz	$⊢ y \in ℕ \to y \in ℤ$
14		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
15	13 14	sylan2	$⊢ (x \in ℤ \land y \in ℕ) \to x y \in ℤ$
16	15	adantr	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to x y \in ℤ$
17		msqznn	$⊢ (x \in ℤ \land x \neq 0) \to x x \in ℕ$
18	17	adantlr	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to x x \in ℕ$
19	16 18	jca	$⊢ ((x \in ℤ \land y \in ℕ) \land x \neq 0) \to (x y \in ℤ \land x x \in ℕ)$
20	19	adantlr	$⊢ (((x \in ℤ \land y \in ℕ) \land y \neq 0) \land x \neq 0) \to (x y \in ℤ \land x x \in ℕ)$
21	20	adantlr	$⊢ ((((x \in ℤ \land y \in ℕ) \land y \neq 0) \land A = \frac{x}{y}) \land x \neq 0) \to (x y \in ℤ \land x x \in ℕ)$
22		oveq2	$⊢ A = \frac{x}{y} \to \frac{1}{A} = \frac{1}{\frac{x}{y}}$
23		divid	$⊢ (x \in ℂ \land x \neq 0) \to \frac{x}{x} = 1$
24	23	adantr	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \frac{x}{x} = 1$
25	24	oveq1d	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \frac{\frac{x}{x}}{\frac{x}{y}} = \frac{1}{\frac{x}{y}}$
26		simpll	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x \in ℂ$
27		simpl	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to (x \in ℂ \land x \neq 0)$
28		simpr	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to (y \in ℂ \land y \neq 0)$
29		divdivdiv	$⊢ ((x \in ℂ \land (x \in ℂ \land x \neq 0)) \land ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0))) \to \frac{\frac{x}{x}}{\frac{x}{y}} = \frac{x y}{x x}$
30	26 27 27 28 29	syl22anc	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \frac{\frac{x}{x}}{\frac{x}{y}} = \frac{x y}{x x}$
31	25 30	eqtr3d	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to \frac{1}{\frac{x}{y}} = \frac{x y}{x x}$
32	31	an4s	$⊢ ((x \in ℂ \land y \in ℂ) \land (x \neq 0 \land y \neq 0)) \to \frac{1}{\frac{x}{y}} = \frac{x y}{x x}$
33	7 32	sylan	$⊢ ((x \in ℤ \land y \in ℕ) \land (x \neq 0 \land y \neq 0)) \to \frac{1}{\frac{x}{y}} = \frac{x y}{x x}$
34	33	anass1rs	$⊢ (((x \in ℤ \land y \in ℕ) \land y \neq 0) \land x \neq 0) \to \frac{1}{\frac{x}{y}} = \frac{x y}{x x}$
35	22 34	sylan9eqr	$⊢ ((((x \in ℤ \land y \in ℕ) \land y \neq 0) \land x \neq 0) \land A = \frac{x}{y}) \to \frac{1}{A} = \frac{x y}{x x}$
36	35	an32s	$⊢ ((((x \in ℤ \land y \in ℕ) \land y \neq 0) \land A = \frac{x}{y}) \land x \neq 0) \to \frac{1}{A} = \frac{x y}{x x}$
37	21 36	jca	$⊢ ((((x \in ℤ \land y \in ℕ) \land y \neq 0) \land A = \frac{x}{y}) \land x \neq 0) \to ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x})$
38	37	ex	$⊢ (((x \in ℤ \land y \in ℕ) \land y \neq 0) \land A = \frac{x}{y}) \to (x \neq 0 \to ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x}))$
39	12 38	sylbid	$⊢ (((x \in ℤ \land y \in ℕ) \land y \neq 0) \land A = \frac{x}{y}) \to (A \neq 0 \to ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x}))$
40	39	ex	$⊢ ((x \in ℤ \land y \in ℕ) \land y \neq 0) \to (A = \frac{x}{y} \to (A \neq 0 \to ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x})))$
41	40	anasss	$⊢ (x \in ℤ \land (y \in ℕ \land y \neq 0)) \to (A = \frac{x}{y} \to (A \neq 0 \to ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x})))$
42	3 41	sylan2	$⊢ (x \in ℤ \land y \in ℕ) \to (A = \frac{x}{y} \to (A \neq 0 \to ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x})))$
43		rspceov	$⊢ (x y \in ℤ \land x x \in ℕ \land \frac{1}{A} = \frac{x y}{x x}) \to \exists z \in ℤ \exists w \in ℕ \frac{1}{A} = \frac{z}{w}$
44	43	3expa	$⊢ ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x}) \to \exists z \in ℤ \exists w \in ℕ \frac{1}{A} = \frac{z}{w}$
45		elq	$⊢ \frac{1}{A} \in ℚ \leftrightarrow \exists z \in ℤ \exists w \in ℕ \frac{1}{A} = \frac{z}{w}$
46	44 45	sylibr	$⊢ ((x y \in ℤ \land x x \in ℕ) \land \frac{1}{A} = \frac{x y}{x x}) \to \frac{1}{A} \in ℚ$
47	42 46	syl8	$⊢ (x \in ℤ \land y \in ℕ) \to (A = \frac{x}{y} \to (A \neq 0 \to \frac{1}{A} \in ℚ))$
48	47	rexlimivv	$⊢ \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \to (A \neq 0 \to \frac{1}{A} \in ℚ)$
49	1 48	sylbi	$⊢ A \in ℚ \to (A \neq 0 \to \frac{1}{A} \in ℚ)$
50	49	imp	$⊢ (A \in ℚ \land A \neq 0) \to \frac{1}{A} \in ℚ$

Metamath Proof Explorer

Theorem qreccl

Proof