Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  flval Structured version   Unicode version

Theorem flval 12029
 Description: Value of the floor (greatest integer) function. The floor of is the (unique) integer less than or equal to whose successor is strictly greater than . (Contributed by NM, 14-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.)
Assertion
Ref Expression
flval
Distinct variable group:   ,

Proof of Theorem flval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 breq2 4424 . . . 4
2 breq1 4423 . . . 4
31, 2anbi12d 715 . . 3
43riotabidv 6265 . 2
5 df-fl 12027 . 2
6 riotaex 6267 . 2
74, 5, 6fvmpt 5960 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1868   class class class wbr 4420  cfv 5597  crio 6262  (class class class)co 6301  cr 9538  c1 9540   caddc 9542   clt 9675   cle 9676  cz 10937  cfl 12025 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-iota 5561  df-fun 5599  df-fv 5605  df-riota 6263  df-fl 12027 This theorem is referenced by:  flcl  12030  fllelt  12032  flflp1  12042  flbi  12050  dfceil2  12067  ltflcei  31846
 Copyright terms: Public domain W3C validator