Theorem qreccl

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

	Ref	Expression
Assertion	qreccl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		elq	⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
2		nnne0	⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
3	2	ancli	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℕ ∧ 𝑦 ≠ 0 ) )
4		neeq1	⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 ↔ ( 𝑥 / 𝑦 ) ≠ 0 ) )
5		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
6		nncn	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
7	5 6	anim12i	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
8		divne0b	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 ≠ 0 ↔ ( 𝑥 / 𝑦 ) ≠ 0 ) )
9	8	3expa	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑦 ≠ 0 ) → ( 𝑥 ≠ 0 ↔ ( 𝑥 / 𝑦 ) ≠ 0 ) )
10	7 9	sylan	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) → ( 𝑥 ≠ 0 ↔ ( 𝑥 / 𝑦 ) ≠ 0 ) )
11	10	bicomd	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) → ( ( 𝑥 / 𝑦 ) ≠ 0 ↔ 𝑥 ≠ 0 ) )
12	4 11	sylan9bbr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) → ( 𝐴 ≠ 0 ↔ 𝑥 ≠ 0 ) )
13		nnz	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
14		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
15	13 14	sylan2	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
16	15	adantr	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
17		msqznn	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) → ( 𝑥 · 𝑥 ) ∈ ℕ )
18	17	adantlr	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( 𝑥 · 𝑥 ) ∈ ℕ )
19	16 18	jca	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑥 ≠ 0 ) → ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) )
20	19	adantlr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝑥 ≠ 0 ) → ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) )
21	20	adantlr	⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) ∧ 𝑥 ≠ 0 ) → ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) )
22		oveq2	⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 1 / 𝐴 ) = ( 1 / ( 𝑥 / 𝑦 ) ) )
23		divid	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 𝑥 / 𝑥 ) = 1 )
24	23	adantr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 / 𝑥 ) = 1 )
25	24	oveq1d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑥 / 𝑥 ) / ( 𝑥 / 𝑦 ) ) = ( 1 / ( 𝑥 / 𝑦 ) ) )
26		simpll	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → 𝑥 ∈ ℂ )
27		simpl	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
28		simpr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
29		divdivdiv	⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) ) → ( ( 𝑥 / 𝑥 ) / ( 𝑥 / 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
30	26 27 27 28 29	syl22anc	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑥 / 𝑥 ) / ( 𝑥 / 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
31	25 30	eqtr3d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 1 / ( 𝑥 / 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
32	31	an4s	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ) → ( 1 / ( 𝑥 / 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
33	7 32	sylan	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ) → ( 1 / ( 𝑥 / 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
34	33	anass1rs	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝑥 ≠ 0 ) → ( 1 / ( 𝑥 / 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
35	22 34	sylan9eqr	⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝑥 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) → ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
36	35	an32s	⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) ∧ 𝑥 ≠ 0 ) → ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) )
37	21 36	jca	⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) ∧ 𝑥 ≠ 0 ) → ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) )
38	37	ex	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) → ( 𝑥 ≠ 0 → ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) ) )
39	12 38	sylbid	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) → ( 𝐴 ≠ 0 → ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) ) )
40	39	ex	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 ≠ 0 ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 → ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) ) ) )
41	40	anasss	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑦 ∈ ℕ ∧ 𝑦 ≠ 0 ) ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 → ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) ) ) )
42	3 41	sylan2	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 → ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) ) ) )
43		rspceov	⊢ ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) → ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ ( 1 / 𝐴 ) = ( 𝑧 / 𝑤 ) )
44	43	3expa	⊢ ( ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) → ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ ( 1 / 𝐴 ) = ( 𝑧 / 𝑤 ) )
45		elq	⊢ ( ( 1 / 𝐴 ) ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ ( 1 / 𝐴 ) = ( 𝑧 / 𝑤 ) )
46	44 45	sylibr	⊢ ( ( ( ( 𝑥 · 𝑦 ) ∈ ℤ ∧ ( 𝑥 · 𝑥 ) ∈ ℕ ) ∧ ( 1 / 𝐴 ) = ( ( 𝑥 · 𝑦 ) / ( 𝑥 · 𝑥 ) ) ) → ( 1 / 𝐴 ) ∈ ℚ )
47	42 46	syl8	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 → ( 1 / 𝐴 ) ∈ ℚ ) ) )
48	47	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ≠ 0 → ( 1 / 𝐴 ) ∈ ℚ ) )
49	1 48	sylbi	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 ≠ 0 → ( 1 / 𝐴 ) ∈ ℚ ) )
50	49	imp	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℚ )