Theorem zq 9517

Description: An integer is a rational number. (Contributed by NM, 9-Jan-2002.)

Assertion

Ref	Expression
zq	|- ( A e. ZZ -> A e. QQ )

Proof of Theorem zq

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqcom 2159	. . . . 5 |- ( x = A <-> A = x )
2		zcn 9155	. . . . . . 7 |- ( x e. ZZ -> x e. CC )
3	2	div1d 8636	. . . . . 6 |- ( x e. ZZ -> ( x / 1 ) = x )
4	3	eqeq2d 2169	. . . . 5 |- ( x e. ZZ -> ( A = ( x / 1 ) <-> A = x ) )
5	1, 4	bitr4id 198	. . . 4 |- ( x e. ZZ -> ( x = A <-> A = ( x / 1 ) ) )
6		1nn 8827	. . . . 5 |- 1 e. NN
7		oveq2 5826	. . . . . . 7 |- ( y = 1 -> ( x / y ) = ( x / 1 ) )
8	7	eqeq2d 2169	. . . . . 6 |- ( y = 1 -> ( A = ( x / y ) <-> A = ( x / 1 ) ) )
9	8	rspcev 2816	. . . . 5 |- ( ( 1 e. NN /\ A = ( x / 1 ) ) -> E. y e. NN A = ( x / y ) )
10	6, 9	mpan 421	. . . 4 |- ( A = ( x / 1 ) -> E. y e. NN A = ( x / y ) )
11	5, 10	syl6bi 162	. . 3 |- ( x e. ZZ -> ( x = A -> E. y e. NN A = ( x / y ) ) )
12	11	reximia 2552	. 2 |- ( E. x e. ZZ x = A -> E. x e. ZZ E. y e. NN A = ( x / y ) )
13		risset 2485	. 2 |- ( A e. ZZ <-> E. x e. ZZ x = A )
14		elq 9513	. 2 |- ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
15	12, 13, 14	3imtr4i 200	1 |- ( A e. ZZ -> A e. QQ )

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128   E.wrex 2436  (class class class)co 5818   1c1 7716   / cdiv 8528   NNcn 8816   ZZcz 9150   QQcq 9510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-cnex 7806  ax-resscn 7807  ax-1cn 7808  ax-1re 7809  ax-icn 7810  ax-addcl 7811  ax-addrcl 7812  ax-mulcl 7813  ax-mulrcl 7814  ax-addcom 7815  ax-mulcom 7816  ax-addass 7817  ax-mulass 7818  ax-distr 7819  ax-i2m1 7820  ax-0lt1 7821  ax-1rid 7822  ax-0id 7823  ax-rnegex 7824  ax-precex 7825  ax-cnre 7826  ax-pre-ltirr 7827  ax-pre-ltwlin 7828  ax-pre-lttrn 7829  ax-pre-apti 7830  ax-pre-ltadd 7831  ax-pre-mulgt0 7832  ax-pre-mulext 7833

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4252  df-po 4255  df-iso 4256  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-riota 5774  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-pnf 7897  df-mnf 7898  df-xr 7899  df-ltxr 7900  df-le 7901  df-sub 8031  df-neg 8032  df-reap 8433  df-ap 8440  df-div 8529  df-inn 8817  df-z 9151  df-q 9511

This theorem is referenced by:  zssq  9518  qdivcl  9534  irrmul  9538  qbtwnz  10133  qbtwnxr  10139  flqlt  10164  flid  10165  flqltnz  10168  flqbi2  10172  flqaddz  10178  flqmulnn0  10180  ceilid  10196  flqeqceilz  10199  flqdiv  10202  modqcl  10207  mulqmod0  10211  modqfrac  10218  zmod10  10221  modqmulnn  10223  zmodcl  10225  zmodfz  10227  zmodid2  10233  q0mod  10236  q1mod  10237  modqcyc  10240  mulp1mod1  10246  modqmuladd  10247  modqmuladdim  10248  modqmuladdnn0  10249  m1modnnsub1  10251  addmodid  10253  modqm1p1mod0  10256  modqltm1p1mod  10257  modqmul1  10258  modqmul12d  10259  q2txmodxeq0  10265  modifeq2int  10267  modaddmodup  10268  modaddmodlo  10269  modqaddmulmod  10272  modqdi  10273  modqsubdir  10274  modsumfzodifsn  10277  addmodlteq  10279  qexpcl  10417  qexpclz  10422  iexpcyc  10505  facavg  10602  bcval  10605  qabsor  10957  modfsummodlemstep  11336  egt2lt3  11658  dvdsval3  11669  p1modz1  11672  moddvds  11677  absdvdsb  11686  dvdsabsb  11687  dvdslelemd  11716  dvdsmod  11735  mulmoddvds  11736  divalglemnn  11790  divalgmod  11799  fldivndvdslt  11807  gcdabs  11852  gcdabs1  11853  modgcd  11855  bezoutlemnewy  11860  bezoutlemstep  11861  eucalglt  11914  lcmabs  11933  sqrt2irraplemnn  12033  nn0sqrtelqelz  12060  crth  12076  phimullem  12077  eulerthlema  12082  eulerthlemh  12083  fermltl  12086  prmdiv  12087  prmdiveq  12088  2logb9irrALT  13251  2irrexpq  13253  2irrexpqap  13255  apdifflemr  13580  apdiff  13581