Theorem qrecclt 6274

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 6258	. . 3 |- (A e. QQ <-> E.x e. ZZ E.y e. NN A = (x / y))
2		neeq1 1593	. . . . . . . . . 10 |- (A = (x / y) -> (A =/= 0 <-> (x / y) =/= 0))
3		divne0bt 5735	. . . . . . . . . . . . 13 |- ((x e. CC /\ y e. CC /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
4	3	3expa 835	. . . . . . . . . . . 12 |- (((x e. CC /\ y e. CC) /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
5		zcnt 6142	. . . . . . . . . . . . 13 |- (x e. ZZ -> x e. CC)
6		nncnt 5932	. . . . . . . . . . . . 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 450	. . . . . . . . . . 11 |- (((x e. ZZ /\ y e. NN) /\ y =/= 0) -> (x =/= 0 <-> (x / y) =/= 0))
9	8	bicomd 523	. . . . . . . . . 10 |- (((x e. ZZ /\ y e. NN) /\ y =/= 0) -> ((x / y) =/= 0 <-> x =/= 0))
10	2, 9	sylan9bbr 543	. . . . . . . . 9 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ A = (x / y)) -> (A =/= 0 <-> x =/= 0))
11		zmulclt 6182	. . . . . . . . . . . . . . . 16 |- ((x e. ZZ /\ y e. ZZ) -> (x x. y) e. ZZ)
12		nnzt 6155	. . . . . . . . . . . . . . . 16 |- (y e. NN -> y e. ZZ)
13	11, 12	sylan2 453	. . . . . . . . . . . . . . 15 |- ((x e. ZZ /\ y e. NN) -> (x x. y) e. ZZ)
14	13	adantr 391	. . . . . . . . . . . . . 14 |- (((x e. ZZ /\ y e. NN) /\ x =/= 0) -> (x x. y) e. ZZ)
15		msqznn 6198	. . . . . . . . . . . . . . 15 |- ((x e. ZZ /\ x =/= 0) -> (x x. x) e. NN)
16	15	adantlr 395	. . . . . . . . . . . . . 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 395	. . . . . . . . . . . 12 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) -> ((x x. y) e. ZZ /\ (x x. x) e. NN))
19	18	adantlr 395	. . . . . . . . . . 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 3975	. . . . . . . . . . . . 13 |- (A = (x / y) -> (1 / A) = (1 / (x / y)))
21		dividt 5767	. . . . . . . . . . . . . . . . . . 19 |- ((x e. CC /\ x =/= 0) -> (x / x) = 1)
22	21	ad2ant2r 411	. . . . . . . . . . . . . . . . . 18 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> (x / x) = 1)
23	22	opreq1d 3981	. . . . . . . . . . . . . . . . 17 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> ((x / x) / (x / y)) = (1 / (x / y)))
24		divdivdivt 5787	. . . . . . . . . . . . . . . . . 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 884	. . . . . . . . . . . . . . . . . 18 |- ((x =/= 0 /\ y =/= 0) -> (x =/= 0 /\ x =/= 0 /\ y =/= 0))
30	24, 27, 29	syl2an 456	. . . . . . . . . . . . . . . . 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 1512	. . . . . . . . . . . . . . . 16 |- (((x e. CC /\ y e. CC) /\ (x =/= 0 /\ y =/= 0)) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
32	31, 7	sylan 450	. . . . . . . . . . . . . . 15 |- (((x e. ZZ /\ y e. NN) /\ (x =/= 0 /\ y =/= 0)) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
33	32	anassrs 443	. . . . . . . . . . . . . 14 |- ((((x e. ZZ /\ y e. NN) /\ x =/= 0) /\ y =/= 0) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
34	33	an1rs 491	. . . . . . . . . . . . 13 |- ((((x e. ZZ /\ y e. NN) /\ y =/= 0) /\ x =/= 0) -> (1 / (x / y)) = ((x x. y) / (x x. x)))
35	20, 34	sylan9eqr 1532	. . . . . . . . . . . 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 491	. . . . . . . . . . 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 442	. . . . . 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 5951	. . . . . . 7 |- (y e. NN -> y =/= 0)
43	42	ancli 296	. . . . . 6 |- (y e. NN -> (y e. NN /\ y =/= 0))
44	41, 43	sylan2 453	. . . . 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 3996	. . . . . . 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 835	. . . . . 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 6258	. . . . . 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 1751	. . 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 777   = wceq 958   e. wcel 960   =/= wne 1588  E.wrex 1649  (class class class)co 3969  CCcc 5244  0cc0 5246  1c1 5247   x. cmul 5251   / cdiv 5306  NNcn 5308  ZZcz 5310  QQcq 5311

This theorem is referenced by:  qdivclt 6275

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  a