Metamath Proof Explorer

Theorem irrapxlem6

Description: Lemma for irrapx1 . Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem6 
|- ( ( A e. RR+ /\ B e. RR+ ) -> E. x e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } ( abs ` ( x - A ) ) < B )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> a e. QQ )
2 simpr1 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> 0 < a )
3 simpr3 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) )
4 2 3 jca 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> ( 0 < a /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) )
5 breq2 
 |-  ( y = a -> ( 0 < y <-> 0 < a ) )
6 fvoveq1 
 |-  ( y = a -> ( abs ` ( y - A ) ) = ( abs ` ( a - A ) ) )
7 fveq2 
 |-  ( y = a -> ( denom ` y ) = ( denom ` a ) )
8 7 oveq1d 
 |-  ( y = a -> ( ( denom ` y ) ^ -u 2 ) = ( ( denom ` a ) ^ -u 2 ) )
9 6 8 breq12d 
 |-  ( y = a -> ( ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) <-> ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) )
10 5 9 anbi12d 
 |-  ( y = a -> ( ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) <-> ( 0 < a /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) )
11 10 elrab 
 |-  ( a e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } <-> ( a e. QQ /\ ( 0 < a /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) )
12 1 4 11 sylanbrc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> a e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } )
13 simpr2 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> ( abs ` ( a - A ) ) < B )
14 fvoveq1 
 |-  ( x = a -> ( abs ` ( x - A ) ) = ( abs ` ( a - A ) ) )
15 14 breq1d 
 |-  ( x = a -> ( ( abs ` ( x - A ) ) < B <-> ( abs ` ( a - A ) ) < B ) )
16 15 rspcev 
 |-  ( ( a e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } /\ ( abs ` ( a - A ) ) < B ) -> E. x e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } ( abs ` ( x - A ) ) < B )
17 12 13 16 syl2anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ a e. QQ ) /\ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) ) -> E. x e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } ( abs ` ( x - A ) ) < B )
18 irrapxlem5 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> E. a e. QQ ( 0 < a /\ ( abs ` ( a - A ) ) < B /\ ( abs ` ( a - A ) ) < ( ( denom ` a ) ^ -u 2 ) ) )
19 17 18 r19.29a 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> E. x e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( ( denom ` y ) ^ -u 2 ) ) } ( abs ` ( x - A ) ) < B )