Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbtwnzlemex Unicode version

Theorem exbtwnzlemex 10081
 Description: Existence of an integer so that a given real number is between the integer and its successor. The real number must satisfy the hypothesis. For example either a rational number or a number which is irrational (in the sense of being apart from any rational number) will meet this condition. The proof starts by finding two integers which are less than and greater than . Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on the hypothesis, and iterating until the range consists of two consecutive integers. (Contributed by Jim Kingdon, 8-Oct-2021.)
Hypotheses
Ref Expression
exbtwnzlemex.a
exbtwnzlemex.tri
Assertion
Ref Expression
exbtwnzlemex
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem exbtwnzlemex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exbtwnzlemex.a . . . 4
2 btwnz 9217 . . . 4
31, 2syl 14 . . 3
4 reeanv 2604 . . 3
53, 4sylibr 133 . 2
6 simplrl 525 . . . . . 6
76zred 9220 . . . . . . 7
81ad2antrr 480 . . . . . . 7
9 simprl 521 . . . . . . 7
107, 8, 9ltled 7928 . . . . . 6
11 simprr 522 . . . . . . 7
126zcnd 9221 . . . . . . . 8
13 simplrr 526 . . . . . . . . 9
1413zcnd 9221 . . . . . . . 8
1512, 14pncan3d 8123 . . . . . . 7
1611, 15breqtrrd 3965 . . . . . 6
17 breq1 3941 . . . . . . . 8
18 oveq1 5791 . . . . . . . . 9
1918breq2d 3950 . . . . . . . 8
2017, 19anbi12d 465 . . . . . . 7
2120rspcev 2794 . . . . . 6
226, 10, 16, 21syl12anc 1215 . . . . 5
2313zred 9220 . . . . . . . 8
247, 8, 23, 9, 11lttrd 7935 . . . . . . 7
25 znnsub 9152 . . . . . . . 8
2625ad2antlr 481 . . . . . . 7
2724, 26mpbid 146 . . . . . 6
28 exbtwnzlemex.tri . . . . . . . . . 10
2928ralrimiva 2509 . . . . . . . . 9
30 breq1 3941 . . . . . . . . . . 11
31 breq2 3942 . . . . . . . . . . 11
3230, 31orbi12d 783 . . . . . . . . . 10
3332cbvralv 2658 . . . . . . . . 9
3429, 33sylib 121 . . . . . . . 8
3534ad2antrr 480 . . . . . . 7
3635r19.21bi 2524 . . . . . 6
3727, 8, 36exbtwnzlemshrink 10080 . . . . 5
3822, 37mpdan 418 . . . 4
3938ex 114 . . 3
4039rexlimdvva 2561 . 2
415, 40mpd 13 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wo 698   wcel 1481  wral 2417  wrex 2418   class class class wbr 3938  (class class class)co 5784  cr 7666  c1 7668   caddc 7670   clt 7847   cle 7848   cmin 7980  cn 8767  cz 9101 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-cnex 7758  ax-resscn 7759  ax-1cn 7760  ax-1re 7761  ax-icn 7762  ax-addcl 7763  ax-addrcl 7764  ax-mulcl 7765  ax-addcom 7767  ax-addass 7769  ax-distr 7771  ax-i2m1 7772  ax-0lt1 7773  ax-0id 7775  ax-rnegex 7776  ax-cnre 7778  ax-pre-ltirr 7779  ax-pre-ltwlin 7780  ax-pre-lttrn 7781  ax-pre-ltadd 7783  ax-arch 7786 This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-br 3939  df-opab 3999  df-id 4224  df-xp 4555  df-rel 4556  df-cnv 4557  df-co 4558  df-dm 4559  df-iota 5098  df-fun 5135  df-fv 5141  df-riota 5740  df-ov 5787  df-oprab 5788  df-mpo 5789  df-pnf 7849  df-mnf 7850  df-xr 7851  df-ltxr 7852  df-le 7853  df-sub 7982  df-neg 7983  df-inn 8768  df-n0 9025  df-z 9102 This theorem is referenced by:  qbtwnz  10083  apbtwnz  10101
 Copyright terms: Public domain W3C validator