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

Theorem qbtwnzlemshrink 9104
 Description: Lemma for qbtwnz 9106. Shrinking the range around the given rational number. (Contributed by Jim Kingdon, 8-Oct-2021.)
Assertion
Ref Expression
qbtwnzlemshrink
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem qbtwnzlemshrink
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 905 . 2
2 3simpb 902 . 2
3 oveq2 5520 . . . . . . . 8
43breq2d 3776 . . . . . . 7
54anbi2d 437 . . . . . 6
65rexbidv 2327 . . . . 5
76anbi2d 437 . . . 4
87imbi1d 220 . . 3
9 oveq2 5520 . . . . . . . 8
109breq2d 3776 . . . . . . 7
1110anbi2d 437 . . . . . 6
1211rexbidv 2327 . . . . 5
1312anbi2d 437 . . . 4
1413imbi1d 220 . . 3
15 oveq2 5520 . . . . . . . 8
1615breq2d 3776 . . . . . . 7
1716anbi2d 437 . . . . . 6
1817rexbidv 2327 . . . . 5
1918anbi2d 437 . . . 4
2019imbi1d 220 . . 3
21 oveq2 5520 . . . . . . . 8
2221breq2d 3776 . . . . . . 7
2322anbi2d 437 . . . . . 6
2423rexbidv 2327 . . . . 5
2524anbi2d 437 . . . 4
2625imbi1d 220 . . 3
27 breq1 3767 . . . . . . 7
28 oveq1 5519 . . . . . . . 8
2928breq2d 3776 . . . . . . 7
3027, 29anbi12d 442 . . . . . 6
3130cbvrexv 2534 . . . . 5
3231biimpi 113 . . . 4