![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > flqcld | Unicode version |
Description: The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.) |
Ref | Expression |
---|---|
flqcld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
flqcld |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flqcld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | flqcl 9743 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-13 1450 ax-14 1451 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3965 ax-pow 4017 ax-pr 4047 ax-un 4271 ax-setind 4368 ax-cnex 7499 ax-resscn 7500 ax-1cn 7501 ax-1re 7502 ax-icn 7503 ax-addcl 7504 ax-addrcl 7505 ax-mulcl 7506 ax-mulrcl 7507 ax-addcom 7508 ax-mulcom 7509 ax-addass 7510 ax-mulass 7511 ax-distr 7512 ax-i2m1 7513 ax-0lt1 7514 ax-1rid 7515 ax-0id 7516 ax-rnegex 7517 ax-precex 7518 ax-cnre 7519 ax-pre-ltirr 7520 ax-pre-ltwlin 7521 ax-pre-lttrn 7522 ax-pre-apti 7523 ax-pre-ltadd 7524 ax-pre-mulgt0 7525 ax-pre-mulext 7526 ax-arch 7527 |
This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-fal 1296 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ne 2257 df-nel 2352 df-ral 2365 df-rex 2366 df-reu 2367 df-rmo 2368 df-rab 2369 df-v 2624 df-sbc 2844 df-csb 2937 df-dif 3004 df-un 3006 df-in 3008 df-ss 3015 df-pw 3437 df-sn 3458 df-pr 3459 df-op 3461 df-uni 3662 df-int 3697 df-iun 3740 df-br 3854 df-opab 3908 df-mpt 3909 df-id 4131 df-po 4134 df-iso 4135 df-xp 4460 df-rel 4461 df-cnv 4462 df-co 4463 df-dm 4464 df-rn 4465 df-res 4466 df-ima 4467 df-iota 4995 df-fun 5032 df-fn 5033 df-f 5034 df-fv 5038 df-riota 5624 df-ov 5671 df-oprab 5672 df-mpt2 5673 df-1st 5927 df-2nd 5928 df-pnf 7587 df-mnf 7588 df-xr 7589 df-ltxr 7590 df-le 7591 df-sub 7718 df-neg 7719 df-reap 8115 df-ap 8122 df-div 8203 df-inn 8486 df-n0 8737 df-z 8814 df-q 9168 df-rp 9198 df-fl 9740 |
This theorem is referenced by: flqge 9752 flqlt 9753 flid 9754 flqltnz 9757 flqwordi 9758 flqword2 9759 flqaddz 9767 flhalf 9772 flltdivnn0lt 9774 fldiv4p1lem1div2 9775 ceiqcl 9777 ceiqge 9779 ceiqm1l 9781 intfracq 9790 flqdiv 9791 modqval 9794 modqvalr 9795 modqcl 9796 flqpmodeq 9797 modq0 9799 modqge0 9802 modqlt 9803 modqdiffl 9805 modqdifz 9806 modqmulnn 9812 modqvalp1 9813 zmodcl 9814 modqcyc 9829 modqadd1 9831 modqmuladd 9836 modqmul1 9847 modqdi 9862 modqsubdir 9863 iexpcyc 10122 facavg 10217 dvdsmod 11204 divalglemnn 11259 divalgmod 11268 flodddiv4t2lthalf 11278 modgcd 11323 hashdvds 11538 |
Copyright terms: Public domain | W3C validator |