![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > zq | GIF version |
Description: An integer is a rational number. (Contributed by NM, 9-Jan-2002.) |
Ref | Expression |
---|---|
zq | ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2179 | . . . . 5 ⊢ (𝑥 = 𝐴 ↔ 𝐴 = 𝑥) | |
2 | zcn 9234 | . . . . . . 7 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ) | |
3 | 2 | div1d 8713 | . . . . . 6 ⊢ (𝑥 ∈ ℤ → (𝑥 / 1) = 𝑥) |
4 | 3 | eqeq2d 2189 | . . . . 5 ⊢ (𝑥 ∈ ℤ → (𝐴 = (𝑥 / 1) ↔ 𝐴 = 𝑥)) |
5 | 1, 4 | bitr4id 199 | . . . 4 ⊢ (𝑥 ∈ ℤ → (𝑥 = 𝐴 ↔ 𝐴 = (𝑥 / 1))) |
6 | 1nn 8906 | . . . . 5 ⊢ 1 ∈ ℕ | |
7 | oveq2 5876 | . . . . . . 7 ⊢ (𝑦 = 1 → (𝑥 / 𝑦) = (𝑥 / 1)) | |
8 | 7 | eqeq2d 2189 | . . . . . 6 ⊢ (𝑦 = 1 → (𝐴 = (𝑥 / 𝑦) ↔ 𝐴 = (𝑥 / 1))) |
9 | 8 | rspcev 2841 | . . . . 5 ⊢ ((1 ∈ ℕ ∧ 𝐴 = (𝑥 / 1)) → ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
10 | 6, 9 | mpan 424 | . . . 4 ⊢ (𝐴 = (𝑥 / 1) → ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
11 | 5, 10 | syl6bi 163 | . . 3 ⊢ (𝑥 ∈ ℤ → (𝑥 = 𝐴 → ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))) |
12 | 11 | reximia 2572 | . 2 ⊢ (∃𝑥 ∈ ℤ 𝑥 = 𝐴 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) |
13 | risset 2505 | . 2 ⊢ (𝐴 ∈ ℤ ↔ ∃𝑥 ∈ ℤ 𝑥 = 𝐴) | |
14 | elq 9598 | . 2 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) | |
15 | 12, 13, 14 | 3imtr4i 201 | 1 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 ∃wrex 2456 (class class class)co 5868 1c1 7790 / cdiv 8605 ℕcn 8895 ℤcz 9229 ℚcq 9595 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4118 ax-pow 4171 ax-pr 4205 ax-un 4429 ax-setind 4532 ax-cnex 7880 ax-resscn 7881 ax-1cn 7882 ax-1re 7883 ax-icn 7884 ax-addcl 7885 ax-addrcl 7886 ax-mulcl 7887 ax-mulrcl 7888 ax-addcom 7889 ax-mulcom 7890 ax-addass 7891 ax-mulass 7892 ax-distr 7893 ax-i2m1 7894 ax-0lt1 7895 ax-1rid 7896 ax-0id 7897 ax-rnegex 7898 ax-precex 7899 ax-cnre 7900 ax-pre-ltirr 7901 ax-pre-ltwlin 7902 ax-pre-lttrn 7903 ax-pre-apti 7904 ax-pre-ltadd 7905 ax-pre-mulgt0 7906 ax-pre-mulext 7907 |
This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-id 4289 df-po 4292 df-iso 4293 df-xp 4628 df-rel 4629 df-cnv 4630 df-co 4631 df-dm 4632 df-rn 4633 df-res 4634 df-ima 4635 df-iota 5173 df-fun 5213 df-fn 5214 df-f 5215 df-fv 5219 df-riota 5824 df-ov 5871 df-oprab 5872 df-mpo 5873 df-1st 6134 df-2nd 6135 df-pnf 7971 df-mnf 7972 df-xr 7973 df-ltxr 7974 df-le 7975 df-sub 8107 df-neg 8108 df-reap 8509 df-ap 8516 df-div 8606 df-inn 8896 df-z 9230 df-q 9596 |
This theorem is referenced by: zssq 9603 qdivcl 9619 irrmul 9623 qbtwnz 10225 qbtwnxr 10231 flqlt 10256 flid 10257 flqltnz 10260 flqbi2 10264 flqaddz 10270 flqmulnn0 10272 ceilid 10288 flqeqceilz 10291 flqdiv 10294 modqcl 10299 mulqmod0 10303 modqfrac 10310 zmod10 10313 modqmulnn 10315 zmodcl 10317 zmodfz 10319 zmodid2 10325 q0mod 10328 q1mod 10329 modqcyc 10332 mulp1mod1 10338 modqmuladd 10339 modqmuladdim 10340 modqmuladdnn0 10341 m1modnnsub1 10343 addmodid 10345 modqm1p1mod0 10348 modqltm1p1mod 10349 modqmul1 10350 modqmul12d 10351 q2txmodxeq0 10357 modifeq2int 10359 modaddmodup 10360 modaddmodlo 10361 modqaddmulmod 10364 modqdi 10365 modqsubdir 10366 modsumfzodifsn 10369 addmodlteq 10371 qexpcl 10509 qexpclz 10514 iexpcyc 10597 qsqeqor 10603 facavg 10697 bcval 10700 qabsor 11055 modfsummodlemstep 11436 egt2lt3 11758 dvdsval3 11769 p1modz1 11772 moddvds 11777 modm1div 11778 absdvdsb 11787 dvdsabsb 11788 dvdslelemd 11819 dvdsmod 11838 mulmoddvds 11839 divalglemnn 11893 divalgmod 11902 fldivndvdslt 11910 gcdabs 11959 gcdabs1 11960 modgcd 11962 bezoutlemnewy 11967 bezoutlemstep 11968 eucalglt 12027 lcmabs 12046 sqrt2irraplemnn 12149 nn0sqrtelqelz 12176 crth 12194 phimullem 12195 eulerthlema 12200 eulerthlemh 12201 fermltl 12204 prmdiv 12205 prmdiveq 12206 odzdvds 12215 vfermltl 12221 powm2modprm 12222 modprm0 12224 modprmn0modprm0 12226 pceu 12265 pczpre 12267 pcdiv 12272 pc0 12274 pcqdiv 12277 pcrec 12278 pcexp 12279 pcxcl 12281 pcdvdstr 12296 pcgcd1 12297 pc2dvds 12299 pc11 12300 pcaddlem 12308 pcadd 12309 fldivp1 12316 qexpz 12320 4sqlem5 12350 4sqlem6 12351 4sqlem10 12355 mulgmodid 12897 2logb9irrALT 14025 2irrexpq 14027 2irrexpqap 14029 lgslem1 14034 lgsvalmod 14053 lgsneg 14058 lgsmod 14060 lgsdir2lem4 14065 lgsdirprm 14068 lgsdilem2 14070 lgsne0 14072 apdifflemr 14418 apdiff 14419 |
Copyright terms: Public domain | W3C validator |