This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / 𝐴 ) ∈ ℚ )