Theorem qrecclt 6211

Description: Closure of reciprocal of rationals.

Assertion

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

Proof of Theorem qrecclt

Step	Hyp	Ref	Expression
1		elq 6195	. . 3 |- (A e. QQ <-> E.x e. ZZ E.y e. NN A = (x / y))
2		neeq1 1582	. . . . . . . . . 10 |- (A = (x / y) -> (A =/= 0 <-> (x / y) =/= 0))
3		divne0bt 5691	. . . . . . . . . . . . 13 |- ((x e. CC /\ y e. CC /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
4	3	3expa 831	. . . . . . . . . . . 12 |- (((x e. CC /\ y e. CC) /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
5		zcnt 6087	. . . . . . . . . . . . 13 |- (x e. ZZ -> x e. CC)
6		nncnt 5878	. . . . . . . . . . . . 13 |- (y e. NN -> y e. CC)
7	5, 6	anim12i 333	. . . . . . . . . . . 12 |- ((x e. ZZ /\ y e. NN) -> (x e. CC /\ y e. CC))
8	4, 7	sylan 448	. . . . . . . . . . 11 |- (((x e. ZZ /\ y e. NN) /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
9	8	bicomd 519	. . . . . . . . . 10 |- (((x e. ZZ /\ y e. NN) /\ y =/= 0) -> ((x / y) =/= 0 <-> x =/= 0))
10	2, 9	sylan9bbr 539	. . . . . . . . 9 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) -> (A =/= 0 <-> x =/= 0))
11		zmulclt 6127	. . . . . . . . . . . . . . . 16 |- ((x e. ZZ /\ y e. ZZ) -> (x x. y) e. ZZ)
12		nnzt 6100	. . . . . . . . . . . . . . . 16 |- (y e. NN -> y e. ZZ)
13	11, 12	sylan2 451	. . . . . . . . . . . . . . 15 |- ((x e. ZZ /\ y e. NN) -> (x x. y) e. ZZ)
14	13	adantr 389	. . . . . . . . . . . . . 14 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> (x x. y) e. ZZ)
15		msqznn 6143	. . . . . . . . . . . . . . 15 |- ((x e. ZZ /\ x =/= 0) -> (x x. x) e. NN)
16	15	adantlr 393	. . . . . . . . . . . . . 14 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> (x x. x) e. NN)
17	14, 16	jca 288	. . . . . . . . . . . . 13 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
18	17	adantlr 393	. . . . . . . . . . . 12 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
19	18	adantlr 393	. . . . . . . . . . 11 |- (((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
20		opreq2 3954	. . . . . . . . . . . . 13 |- (A = (x / y) -> (1 / A) = (1 / (x / y)))
21		dividt 5722	. . . . . . . . . . . . . . . . . . 19 |- ((x e. CC /\ x =/= 0) -> (x / x) = 1)
22	21	ad2ant2r 409	. . . . . . . . . . . . . . . . . 18 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> (x / x) = 1)
23	22	opreq1d 3960	. . . . . . . . . . . . . . . . 17 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> ((x / x) / (x / y)) = (1 / (x / y)))
24		divdivdivt 5741	. . . . . . . . . . . . . . . . . 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 319	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. CC /\ y e. CC) -> x e. CC)
26	25, 25	jca 288	. . . . . . . . . . . . . . . . . . 19 |- ((x e. CC /\ y e. CC) -> (x e. CC /\ x e. CC))
27	26	ancri 297	. . . . . . . . . . . . . . . . . 18 |- ((x e. CC /\ y e. CC) -> ((x e. CC /\ x e. CC) /\ (x e. CC /\ y e. CC)))
28		id 59	. . . . . . . . . . . . . . . . . . 19 |- ((x =/= 0 /\ x =/= 0 /\ y =/= 0) -> (x =/= 0 /\ x =/= 0 /\ y =/= 0))
29	28	3anidm12 879	. . . . . . . . . . . . . . . . . 18 |- ((x =/= 0 /\ y =/= 0) -> (x =/= 0 /\ x =/= 0 /\ y =/= 0))
30	24, 27, 29	syl2an 454	. . . . . . . . . . . . . . . . 17 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> ((x / x) / (x / y)) = ((x x. y) / (x x. x)))
31	23, 30	eqtr3d 1501	. . . . . . . . . . . . . . . 16 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
32	31, 7	sylan 448	. . . . . . . . . . . . . . 15 |- (((x e. ZZ /\ y e. NN) /\ (x =/= 0 /\ y =/= 0)) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
33	32	anassrs 441	. . . . . . . . . . . . . 14 |- ((((x e. ZZ /\ y e. NN) /\ x =/= 0) /\ y =/= 0) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
34	33	an1rs 488	. . . . . . . . . . . . 13 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
35	20, 34	sylan9eqr 1521	. . . . . . . . . . . 12 |- (((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) /\ A = (x / y)) -> (1 / A) = ((x x. y) / (x x. x)))
36	35	an1rs 488	. . . . . . . . . . 11 |- (((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) /\ x =/= 0) -> (1 / A) = ((x x. y) / (x x. x)))
37	19, 36	jca 288	. . . . . . . . . 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))))
38	37	ex 373	. . . . . . . . 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)))))
39	10, 38	sylbid 203	. . . . . . . 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)))))
40	39	ex 373	. . . . . . 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))))))
41	40	anasss 440	. . . . . 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))))))
42		nnne0t 5897	. . . . . . 7 |- (y e. NN -> y =/= 0)
43	42	ancli 296	. . . . . 6 |- (y e. NN -> (y e. NN /\ y =/= 0))
44	41, 43	sylan2 451	. . . . 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))))))
45		rcla4eopr 3975	. . . . . . 7 |- (((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))
46	45	3expa 831	. . . . . 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))
47		elq 6195	. . . . . 6 |- ((1 / A) e. QQ <-> E.z e. ZZ E.w e. NN (1 / A) = (z / w))
48	46, 47	sylibr 200	. . . . 5 |- ((((x x. y) e. ZZ /\ (x x. x) e. NN) /\ (1 / A) = ((x x. y) / (x x. x))) -> (1 / A) e. QQ)
49	44, 48	syl8 24	. . . 4 |- ((x e. ZZ /\ y e. NN) -> (A = (x / y) -> (A =/= 0 -> (1 / A) e. QQ)))
50	49	r19.23aivv 1740	. . 3 |- (E.x e. ZZ E.y e. NN A = (x / y) -> (A =/= 0 -> (1 / A) e. QQ))
51	1, 50	sylbi 199	. 2 |- (A e. QQ -> (A =/= 0 -> (1 / A) e. QQ))
52	51	imp 350	1 |- ((A e. QQ /\ A =/= 0) -> (1 / A) e. QQ)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 773   = wceq 953   e. wcel 955   =/= wne 1577  E.wrex 1638  (class class class)co 3948  CCcc 5204  0cc0 5206  1c1 5207   x. cmul 5211   / cdiv 5266  NNcn 5268  ZZcz 5270  QQcq 5271

This theorem is referenced by:  qdivclt 6212

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136