Theorem rebtwn2z 10257

Description: A real number can be bounded by integers above and below which are two apart.

The proof starts by finding two integers which are less than and greater than the given real number. 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 weak linearity, and iterating until the range consists of integers which are two apart. (Contributed by Jim Kingdon, 13-Oct-2021.)

Assertion

Ref	Expression
rebtwn2z	|- ( A e. RR -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) )

Distinct variable group:   x, A

Proof of Theorem rebtwn2z

Dummy variables m n y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		btwnz 9374	. . 3 |- ( A e. RR -> ( E. m e. ZZ m < A /\ E. n e. ZZ A < n ) )
2		reeanv 2647	. . 3 |- ( E. m e. ZZ E. n e. ZZ ( m < A /\ A < n ) <-> ( E. m e. ZZ m < A /\ E. n e. ZZ A < n ) )
3	1, 2	sylibr 134	. 2 |- ( A e. RR -> E. m e. ZZ E. n e. ZZ ( m < A /\ A < n ) )
4		simpll 527	. . . . 5 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> A e. RR )
5		simplrl 535	. . . . . . . . 9 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> m e. ZZ )
6	5	zred 9377	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> m e. RR )
7		simplrr 536	. . . . . . . . 9 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> n e. ZZ )
8	7	zred 9377	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> n e. RR )
9		simprl 529	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> m < A )
10		simprr 531	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> A < n )
11	6, 4, 8, 9, 10	lttrd 8085	. . . . . . 7 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> m < n )
12		znnsub 9306	. . . . . . . 8 |- ( ( m e. ZZ /\ n e. ZZ ) -> ( m < n <-> ( n - m ) e. NN ) )
13	12	ad2antlr 489	. . . . . . 7 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( m < n <-> ( n - m ) e. NN ) )
14	11, 13	mpbid 147	. . . . . 6 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( n - m ) e. NN )
15		elnnuz 9566	. . . . . . . 8 |- ( ( n - m ) e. NN <-> ( n - m ) e. ( ZZ>= ` 1 ) )
16		eluzp1p1 9555	. . . . . . . 8 |- ( ( n - m ) e. ( ZZ>= ` 1 ) -> ( ( n - m ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
17	15, 16	sylbi 121	. . . . . . 7 |- ( ( n - m ) e. NN -> ( ( n - m ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
18		df-2 8980	. . . . . . . 8 |- 2 = ( 1 + 1 )
19	18	fveq2i 5520	. . . . . . 7 |- ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
20	17, 19	eleqtrrdi 2271	. . . . . 6 |- ( ( n - m ) e. NN -> ( ( n - m ) + 1 ) e. ( ZZ>= ` 2 ) )
21	14, 20	syl 14	. . . . 5 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( ( n - m ) + 1 ) e. ( ZZ>= ` 2 ) )
22	5	zcnd 9378	. . . . . . . . 9 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> m e. CC )
23	7	zcnd 9378	. . . . . . . . 9 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> n e. CC )
24	22, 23	pncan3d 8273	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( m + ( n - m ) ) = n )
25	24, 8	eqeltrd 2254	. . . . . . 7 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( m + ( n - m ) ) e. RR )
26	8, 6	resubcld 8340	. . . . . . . . 9 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( n - m ) e. RR )
27		1red 7974	. . . . . . . . 9 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> 1 e. RR )
28	26, 27	readdcld 7989	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( ( n - m ) + 1 ) e. RR )
29	6, 28	readdcld 7989	. . . . . . 7 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( m + ( ( n - m ) + 1 ) ) e. RR )
30	10, 24	breqtrrd 4033	. . . . . . 7 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> A < ( m + ( n - m ) ) )
31	26	ltp1d 8889	. . . . . . . 8 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( n - m ) < ( ( n - m ) + 1 ) )
32	26, 28, 6, 31	ltadd2dd 8381	. . . . . . 7 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> ( m + ( n - m ) ) < ( m + ( ( n - m ) + 1 ) ) )
33	4, 25, 29, 30, 32	lttrd 8085	. . . . . 6 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> A < ( m + ( ( n - m ) + 1 ) ) )
34		breq1 4008	. . . . . . . 8 |- ( y = m -> ( y < A <-> m < A ) )
35		oveq1 5884	. . . . . . . . 9 |- ( y = m -> ( y + ( ( n - m ) + 1 ) ) = ( m + ( ( n - m ) + 1 ) ) )
36	35	breq2d 4017	. . . . . . . 8 |- ( y = m -> ( A < ( y + ( ( n - m ) + 1 ) ) <-> A < ( m + ( ( n - m ) + 1 ) ) ) )
37	34, 36	anbi12d 473	. . . . . . 7 |- ( y = m -> ( ( y < A /\ A < ( y + ( ( n - m ) + 1 ) ) ) <-> ( m < A /\ A < ( m + ( ( n - m ) + 1 ) ) ) ) )
38	37	rspcev 2843	. . . . . 6 |- ( ( m e. ZZ /\ ( m < A /\ A < ( m + ( ( n - m ) + 1 ) ) ) ) -> E. y e. ZZ ( y < A /\ A < ( y + ( ( n - m ) + 1 ) ) ) )
39	5, 9, 33, 38	syl12anc 1236	. . . . 5 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> E. y e. ZZ ( y < A /\ A < ( y + ( ( n - m ) + 1 ) ) ) )
40		rebtwn2zlemshrink 10256	. . . . 5 |- ( ( A e. RR /\ ( ( n - m ) + 1 ) e. ( ZZ>= ` 2 ) /\ E. y e. ZZ ( y < A /\ A < ( y + ( ( n - m ) + 1 ) ) ) ) -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) )
41	4, 21, 39, 40	syl3anc 1238	. . . 4 |- ( ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( m < A /\ A < n ) ) -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) )
42	41	ex 115	. . 3 |- ( ( A e. RR /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( m < A /\ A < n ) -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) ) )
43	42	rexlimdvva 2602	. 2 |- ( A e. RR -> ( E. m e. ZZ E. n e. ZZ ( m < A /\ A < n ) -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) ) )
44	3, 43	mpd 13	1 |- ( A e. RR -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2148   E.wrex 2456   class class class wbr 4005   ` cfv 5218  (class class class)co 5877   RRcr 7812   1c1 7814   + caddc 7816   < clt 7994   - cmin 8130   NNcn 8921   2c2 8972   ZZcz 9255   ZZ>=cuz 9530

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 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-addcom 7913  ax-addass 7915  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-0id 7921  ax-rnegex 7922  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-ltadd 7929  ax-arch 7932

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-rab 2464  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-inn 8922  df-2 8980  df-n0 9179  df-z 9256  df-uz 9531

This theorem is referenced by:  qbtwnre  10259