Metamath Proof Explorer

Theorem qreccl

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

Ref Expression
Assertion qreccl 
|- ( ( A e. QQ /\ A =/= 0 ) -> ( 1 / A ) e. QQ )

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
2 nnne0 
 |-  ( y e. NN -> y =/= 0 )
3 2 ancli 
 |-  ( y e. NN -> ( y e. NN /\ y =/= 0 ) )
4 neeq1 
 |-  ( A = ( x / y ) -> ( A =/= 0 <-> ( x / y ) =/= 0 ) )
5 zcn 
 |-  ( x e. ZZ -> x e. CC )
6 nncn 
 |-  ( y e. NN -> y e. CC )
7 5 6 anim12i 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( x e. CC /\ y e. CC ) )
8 divne0b 
 |-  ( ( x e. CC /\ y e. CC /\ y =/= 0 ) -> ( x =/= 0 <-> ( x / y ) =/= 0 ) )
9 8 3expa 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ y =/= 0 ) -> ( x =/= 0 <-> ( x / y ) =/= 0 ) )
10 7 9 sylan 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) -> ( x =/= 0 <-> ( x / y ) =/= 0 ) )
11 10 bicomd 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) -> ( ( x / y ) =/= 0 <-> x =/= 0 ) )
12 4 11 sylan9bbr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ A = ( x / y ) ) -> ( A =/= 0 <-> x =/= 0 ) )
13 nnz 
 |-  ( y e. NN -> y e. ZZ )
14 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
15 13 14 sylan2 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( x x. y ) e. ZZ )
16 15 adantr 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( x x. y ) e. ZZ )
17 msqznn 
 |-  ( ( x e. ZZ /\ x =/= 0 ) -> ( x x. x ) e. NN )
18 17 adantlr 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( x x. x ) e. NN )
19 16 18 jca 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) )
20 19 adantlr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ x =/= 0 ) -> ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) )
21 20 adantlr 
 |-  ( ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ A = ( x / y ) ) /\ x =/= 0 ) -> ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) )
22 oveq2 
 |-  ( A = ( x / y ) -> ( 1 / A ) = ( 1 / ( x / y ) ) )
23 divid 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( x / x ) = 1 )
24 23 adantr 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x / x ) = 1 )
25 24 oveq1d 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( ( x / x ) / ( x / y ) ) = ( 1 / ( x / y ) ) )
26 simpll 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> x e. CC )
27 simpl 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x e. CC /\ x =/= 0 ) )
28 simpr 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( y e. CC /\ y =/= 0 ) )
29 divdivdiv 
 |-  ( ( ( x e. CC /\ ( x e. CC /\ x =/= 0 ) ) /\ ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) ) -> ( ( x / x ) / ( x / y ) ) = ( ( x x. y ) / ( x x. x ) ) )
30 26 27 27 28 29 syl22anc 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( ( x / x ) / ( x / y ) ) = ( ( x x. y ) / ( x x. x ) ) )
31 25 30 eqtr3d 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( 1 / ( x / y ) ) = ( ( x x. y ) / ( x x. x ) ) )
32 31 an4s 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ ( x =/= 0 /\ y =/= 0 ) ) -> ( 1 / ( x / y ) ) = ( ( x x. y ) / ( x x. x ) ) )
33 7 32 sylan 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( x =/= 0 /\ y =/= 0 ) ) -> ( 1 / ( x / y ) ) = ( ( x x. y ) / ( x x. x ) ) )
34 33 anass1rs 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ x =/= 0 ) -> ( 1 / ( x / y ) ) = ( ( x x. y ) / ( x x. x ) ) )
35 22 34 sylan9eqr 
 |-  ( ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ x =/= 0 ) /\ A = ( x / y ) ) -> ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) )
36 35 an32s 
 |-  ( ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ A = ( x / y ) ) /\ x =/= 0 ) -> ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) )
37 21 36 jca 
 |-  ( ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ A = ( x / y ) ) /\ x =/= 0 ) -> ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) )
38 37 ex 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ A = ( x / y ) ) -> ( x =/= 0 -> ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) ) )
39 12 38 sylbid 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) /\ A = ( x / y ) ) -> ( A =/= 0 -> ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) ) )
40 39 ex 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ y =/= 0 ) -> ( A = ( x / y ) -> ( A =/= 0 -> ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) ) ) )
41 40 anasss 
 |-  ( ( x e. ZZ /\ ( y e. NN /\ y =/= 0 ) ) -> ( A = ( x / y ) -> ( A =/= 0 -> ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) ) ) )
42 3 41 sylan2 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> ( A =/= 0 -> ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) ) ) )
43 rspceov 
 |-  ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) -> E. z e. ZZ E. w e. NN ( 1 / A ) = ( z / w ) )
44 43 3expa 
 |-  ( ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) -> E. z e. ZZ E. w e. NN ( 1 / A ) = ( z / w ) )
45 elq 
 |-  ( ( 1 / A ) e. QQ <-> E. z e. ZZ E. w e. NN ( 1 / A ) = ( z / w ) )
46 44 45 sylibr 
 |-  ( ( ( ( x x. y ) e. ZZ /\ ( x x. x ) e. NN ) /\ ( 1 / A ) = ( ( x x. y ) / ( x x. x ) ) ) -> ( 1 / A ) e. QQ )
47 42 46 syl8 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> ( A =/= 0 -> ( 1 / A ) e. QQ ) ) )
48 47 rexlimivv 
 |-  ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( A =/= 0 -> ( 1 / A ) e. QQ ) )
49 1 48 sylbi 
 |-  ( A e. QQ -> ( A =/= 0 -> ( 1 / A ) e. QQ ) )
50 49 imp 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( 1 / A ) e. QQ )