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

Theorem rebtwn2zlemshrink 9329
 Description: Lemma for rebtwn2z 9330. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.)
Assertion
Ref Expression
rebtwn2zlemshrink
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem rebtwn2zlemshrink
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 940 . 2
2 3simpb 937 . 2
3 2z 8449 . . 3
4 oveq2 5545 . . . . . . . 8
54breq2d 3799 . . . . . . 7
65anbi2d 452 . . . . . 6
76rexbidv 2370 . . . . 5
87anbi2d 452 . . . 4
98imbi1d 229 . . 3
10 oveq2 5545 . . . . . . . 8
1110breq2d 3799 . . . . . . 7
1211anbi2d 452 . . . . . 6
1312rexbidv 2370 . . . . 5
1413anbi2d 452 . . . 4
1514imbi1d 229 . . 3
16 oveq2 5545 . . . . . . . 8
1716breq2d 3799 . . . . . . 7
1817anbi2d 452 . . . . . 6
1918rexbidv 2370 . . . . 5
2019anbi2d 452 . . . 4
2120imbi1d 229 . . 3
22 oveq2 5545 . . . . . . . 8
2322breq2d 3799 . . . . . . 7
2423anbi2d 452 . . . . . 6
2524rexbidv 2370 . . . . 5
2625anbi2d 452 . . . 4
2726imbi1d 229 . . 3
28 breq1 3790 . . . . . . 7
29 oveq1 5544 . . . . . . . 8
3029breq2d 3799 . . . . . . 7
3128, 30anbi12d 457 . . . . . 6
3231cbvrexv 2579 . . . . 5
3332biimpi 118 . . . 4