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

Theorem rebtwn2zlemshrink 10043
 Description: Lemma for rebtwn2z 10044. 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 982 . 2
2 3simpb 979 . 2
3 oveq2 5782 . . . . . . . 8
43breq2d 3941 . . . . . . 7
54anbi2d 459 . . . . . 6
65rexbidv 2438 . . . . 5
76anbi2d 459 . . . 4
87imbi1d 230 . . 3
9 oveq2 5782 . . . . . . . 8
109breq2d 3941 . . . . . . 7
1110anbi2d 459 . . . . . 6
1211rexbidv 2438 . . . . 5
1312anbi2d 459 . . . 4
1413imbi1d 230 . . 3
15 oveq2 5782 . . . . . . . 8
1615breq2d 3941 . . . . . . 7
1716anbi2d 459 . . . . . 6
1817rexbidv 2438 . . . . 5
1918anbi2d 459 . . . 4
2019imbi1d 230 . . 3
21 oveq2 5782 . . . . . . . 8
2221breq2d 3941 . . . . . . 7
2322anbi2d 459 . . . . . 6
2423rexbidv 2438 . . . . 5
2524anbi2d 459 . . . 4
2625imbi1d 230 . . 3
27 breq1 3932 . . . . . . 7
28 oveq1 5781 . . . . . . . 8
2928breq2d 3941 . . . . . . 7
3027, 29anbi12d 464 . . . . . 6
3130cbvrexv 2655 . . . . 5
3231biimpi 119 . . . 4