HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem qrecclt 4646
Description: Closure of reciprocal of rationals.
Assertion
Ref Expression
qrecclt |- ((A e. QQ /\ A =/= 0) -> (1 / A) e. QQ)
Proof of Theorem qrecclt
StepHypRef Expression
1 elq 4629 . . 3 |- (A e. QQ <-> E.x e. ZZ E.y e. NN A = (x / y))
2 neeq1 1194 . . . . . . . . . 10 |- (A = (x / y) -> (A =/= 0 <-> (x / y) =/= 0))
3 divneq0bt 4230 . . . . . . . . . . . 12 |- (((x e. CC /\ y e. CC) /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
4 zcnt 4568 . . . . . . . . . . . . 13 |- (x e. ZZ -> x e. CC)
5 nncnt 4428 . . . . . . . . . . . . 13 |- (y e. NN -> y e. CC)
64, 5anim12i 268 . . . . . . . . . . . 12 |- ((x e. ZZ /\ y e. NN) -> (x e. CC /\ y e. CC))
73, 6sylan 343 . . . . . . . . . . 11 |- (((x e. ZZ /\ y e. NN) /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
87bicomd 399 . . . . . . . . . 10 |- (((x e. ZZ /\ y e. NN) /\ y =/= 0) -> ((x / y) =/= 0 <-> x =/= 0))
92, 8sylan9bbr 419 . . . . . . . . 9 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) -> (A =/= 0 <-> x =/= 0))
10 zmulclt 4596 . . . . . . . . . . . . . . . 16 |- ((x e. ZZ /\ y e. ZZ) -> (x x. y) e. ZZ)
11 nnzt 4579 . . . . . . . . . . . . . . . 16 |- (y e. NN -> y e. ZZ)
1210, 11sylan2 346 . . . . . . . . . . . . . . 15 |- ((x e. ZZ /\ y e. NN) -> (x x. y) e. ZZ)
1312adantr 306 . . . . . . . . . . . . . 14 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> (x x. y) e. ZZ)
14 sqznn 4600 . . . . . . . . . . . . . . 15 |- ((x e. ZZ /\ x =/= 0) -> (x x. x) e. NN)
1514adantlr 310 . . . . . . . . . . . . . 14 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> (x x. x) e. NN)
1613, 15jca 236 . . . . . . . . . . . . 13 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
1716adantlr 310 . . . . . . . . . . . 12 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
1817adantlr 310 . . . . . . . . . . 11 |- (((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
19 opreq2 3007 . . . . . . . . . . . . 13 |- (A = (x / y) -> (1 / A) = (1 / (x / y)))
20 dividt 4256 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. CC /\ x =/= 0) -> (x / x) = 1)
2120adantrr 312 . . . . . . . . . . . . . . . . . . 19 |- ((x e. CC /\ (x =/= 0 /\ y =/= 0)) -> (x / x) = 1)
2221adantlr 310 . . . . . . . . . . . . . . . . . 18 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> (x / x) = 1)
2322opreq1d 3012 . . . . . . . . . . . . . . . . 17 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> ((x / x) / (x / y)) = (1 / (x / y)))
24 divdivdivt 4265 . . . . . . . . . . . . . . . . . 18 |- ((((x e. CC /\ x e. CC) /\ (x e. CC /\ y e. CC)) /\ (x =/= 0 /\ x =/= 0 /\ y =/= 0)) -> ((x / x) / (x / y)) = ((x x. y) / (x x. x)))
25 pm3.26 256 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. CC /\ y e. CC) -> x e. CC)
2625, 25jca 236 . . . . . . . . . . . . . . . . . . 19 |- ((x e. CC /\ y e. CC) -> (x e. CC /\ x e. CC))
2726ancri 245 . . . . . . . . . . . . . . . . . 18 |- ((x e. CC /\ y e. CC) -> ((x e. CC /\ x e. CC) /\ (x e. CC /\ y e. CC)))
28 pm3.26 256 . . . . . . . . . . . . . . . . . . 19 |- ((x =/= 0 /\ y =/= 0) -> x =/= 0)
29 pm3.27 260 . . . . . . . . . . . . . . . . . . 19 |- ((x =/= 0 /\ y =/= 0) -> y =/= 0)
3028, 28, 293jca 604 . . . . . . . . . . . . . . . . . 18 |- ((x =/= 0 /\ y =/= 0) -> (x =/= 0 /\ x =/= 0 /\ y =/= 0))
3124, 27, 30syl2an 349 . . . . . . . . . . . . . . . . 17 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> ((x / x) / (x / y)) = ((x x. y) / (x x. x)))
3223, 31eqtr3d 1130 . . . . . . . . . . . . . . . 16 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
3332, 6sylan 343 . . . . . . . . . . . . . . 15 |- (((x e. ZZ /\ y e. NN) /\ (x =/= 0 /\ y =/= 0)) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
3433anassrs 338 . . . . . . . . . . . . . 14 |- ((((x e. ZZ /\ y e. NN) /\ x =/= 0) /\ y =/= 0) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
3534an1rs 373 . . . . . . . . . . . . 13 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
3619, 35sylan9eqr 1145 . . . . . . . . . . . 12 |- (((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) /\ A = (x / y)) -> (1 / A) = ((x x. y) / (x x. x)))
3736an1rs 373 . . . . . . . . . . 11 |- (((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) /\ x =/= 0) -> (1 / A) = ((x x. y) / (x x. x)))
3818, 37jca 236 . . . . . . . . . 10 |- (((((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))))
3938exp 291 . . . . . . . . 9 |- ((((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)))))
409, 39sylbid 178 . . . . . . . 8 |- ((((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)))))
4140exp 291 . . . . . . 7 |- (((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))))))
4241anasss 337 . . . . . 6 |- ((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))))))
43 nnne0t 4444 . . . . . . 7 |- (y e. NN -> y =/= 0)
4443ancli 244 . . . . . 6 |- (y e. NN -> (y e. NN /\ y =/= 0))
4542, 44sylan2 346 . . . . 5 |- ((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))))))
46 opreq1 3006 . . . . . . . 8 |- (z = (x x. y) -> (z / w) = ((x x. y) / w))
4746cleq2d 1112 . . . . . . 7 |- (z = (x x. y) -> ((1 / A) = (z / w) <-> (1 / A) = ((x x. y) / w)))
48 opreq2 3007 . . . . . . . 8 |- (w = (x x. x) -> ((x x. y) / w) = ((x x. y) / (x x. x)))
4948cleq2d 1112 . . . . . . 7 |- (w = (x x. x) -> ((1 / A) = ((x x. y) / w) <-> (1 / A) = ((x x. y) / (x x. x))))
5047, 49rcla42ev 1405 . . . . . 6 |- ((((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))
51 elq 4629 . . . . . 6 |- ((1 / A) e. QQ <-> E.z e. ZZ E.w e. NN (1 / A) = (z / w))
5250, 51sylibr 175 . . . . 5 |- ((((x x. y) e. ZZ /\ (x x. x) e. NN) /\ (1 / A) = ((x x. y) / (x x. x))) -> (1 / A) e. QQ)
5345, 52syl8 25 . . . 4 |- ((x e. ZZ /\ y e. NN) -> (A = (x / y) -> (A =/= 0 -> (1 / A) e. QQ)))
5453r19.23aivv 1287 . . 3 |- (E.x e. ZZ E.y e. NN A = (x / y) -> (A =/= 0 -> (1 / A) e. QQ))
551, 54sylbi 174 . 2 |- (A e. QQ -> (A =/= 0 -> (1 / A) e. QQ))
5655imp 277 1 |- ((A e. QQ /\ A =/= 0) -> (1 / A) e. QQ)
Colors of variables: wff set class
Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   /\ w3a 581   = wceq 1091   e. wcel 1092   =/= wne 1190  E.wrex 1202  (class class class)co 3001  CCcc 4026  0cc0 4028  1c1 4029   x. cmulc 4032