Metamath Proof Explorer

Theorem ltflcei

Description: Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017)

Ref Expression
Assertion ltflcei 
|- ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B <-> A < -u ( |_ ` -u B ) ) )

Proof

Step Hyp Ref Expression
1 flltp1 
 |-  ( A e. RR -> A < ( ( |_ ` A ) + 1 ) )
2 1 ad3antrrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> A < ( ( |_ ` A ) + 1 ) )
3 renegcl 
 |-  ( B e. RR -> -u B e. RR )
4 flval 
 |-  ( -u B e. RR -> ( |_ ` -u B ) = ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) )
5 3 4 syl 
 |-  ( B e. RR -> ( |_ ` -u B ) = ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) )
6 5 ad3antlr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( |_ ` -u B ) = ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) )
7 fllep1 
 |-  ( A e. RR -> A <_ ( ( |_ ` A ) + 1 ) )
8 7 adantl 
 |-  ( ( B e. RR /\ A e. RR ) -> A <_ ( ( |_ ` A ) + 1 ) )
9 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
10 peano2re 
 |-  ( ( |_ ` A ) e. RR -> ( ( |_ ` A ) + 1 ) e. RR )
11 9 10 syl 
 |-  ( A e. RR -> ( ( |_ ` A ) + 1 ) e. RR )
12 11 adantl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( |_ ` A ) + 1 ) e. RR )
13 letr 
 |-  ( ( B e. RR /\ A e. RR /\ ( ( |_ ` A ) + 1 ) e. RR ) -> ( ( B <_ A /\ A <_ ( ( |_ ` A ) + 1 ) ) -> B <_ ( ( |_ ` A ) + 1 ) ) )
14 12 13 mpd3an3 
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( B <_ A /\ A <_ ( ( |_ ` A ) + 1 ) ) -> B <_ ( ( |_ ` A ) + 1 ) ) )
15 8 14 mpan2d 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B <_ A -> B <_ ( ( |_ ` A ) + 1 ) ) )
16 leneg 
 |-  ( ( B e. RR /\ ( ( |_ ` A ) + 1 ) e. RR ) -> ( B <_ ( ( |_ ` A ) + 1 ) <-> -u ( ( |_ ` A ) + 1 ) <_ -u B ) )
17 11 16 sylan2 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B <_ ( ( |_ ` A ) + 1 ) <-> -u ( ( |_ ` A ) + 1 ) <_ -u B ) )
18 15 17 sylibd 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B <_ A -> -u ( ( |_ ` A ) + 1 ) <_ -u B ) )
19 18 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B <_ A -> -u ( ( |_ ` A ) + 1 ) <_ -u B ) )
20 ltneg 
 |-  ( ( ( |_ ` A ) e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B <-> -u B < -u ( |_ ` A ) ) )
21 9 20 sylan 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B <-> -u B < -u ( |_ ` A ) ) )
22 9 recnd 
 |-  ( A e. RR -> ( |_ ` A ) e. CC )
23 ax-1cn 
 |-  1 e. CC
24 negdi2 
 |-  ( ( ( |_ ` A ) e. CC /\ 1 e. CC ) -> -u ( ( |_ ` A ) + 1 ) = ( -u ( |_ ` A ) - 1 ) )
25 24 oveq1d 
 |-  ( ( ( |_ ` A ) e. CC /\ 1 e. CC ) -> ( -u ( ( |_ ` A ) + 1 ) + 1 ) = ( ( -u ( |_ ` A ) - 1 ) + 1 ) )
26 negcl 
 |-  ( ( |_ ` A ) e. CC -> -u ( |_ ` A ) e. CC )
27 npcan 
 |-  ( ( -u ( |_ ` A ) e. CC /\ 1 e. CC ) -> ( ( -u ( |_ ` A ) - 1 ) + 1 ) = -u ( |_ ` A ) )
28 26 27 sylan 
 |-  ( ( ( |_ ` A ) e. CC /\ 1 e. CC ) -> ( ( -u ( |_ ` A ) - 1 ) + 1 ) = -u ( |_ ` A ) )
29 25 28 eqtr2d 
 |-  ( ( ( |_ ` A ) e. CC /\ 1 e. CC ) -> -u ( |_ ` A ) = ( -u ( ( |_ ` A ) + 1 ) + 1 ) )
30 22 23 29 sylancl 
 |-  ( A e. RR -> -u ( |_ ` A ) = ( -u ( ( |_ ` A ) + 1 ) + 1 ) )
31 30 breq2d 
 |-  ( A e. RR -> ( -u B < -u ( |_ ` A ) <-> -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) )
32 31 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -u B < -u ( |_ ` A ) <-> -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) )
33 21 32 bitrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B <-> -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) )
34 33 biimpd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B -> -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) )
35 19 34 anim12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B <_ A /\ ( |_ ` A ) < B ) -> ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) ) )
36 35 ancomsd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) < B /\ B <_ A ) -> ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) ) )
37 36 impl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) )
38 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
39 38 peano2zd 
 |-  ( A e. RR -> ( ( |_ ` A ) + 1 ) e. ZZ )
40 39 znegcld 
 |-  ( A e. RR -> -u ( ( |_ ` A ) + 1 ) e. ZZ )
41 rebtwnz 
 |-  ( -u B e. RR -> E! x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) )
42 3 41 syl 
 |-  ( B e. RR -> E! x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) )
43 breq1 
 |-  ( x = -u ( ( |_ ` A ) + 1 ) -> ( x <_ -u B <-> -u ( ( |_ ` A ) + 1 ) <_ -u B ) )
44 oveq1 
 |-  ( x = -u ( ( |_ ` A ) + 1 ) -> ( x + 1 ) = ( -u ( ( |_ ` A ) + 1 ) + 1 ) )
45 44 breq2d 
 |-  ( x = -u ( ( |_ ` A ) + 1 ) -> ( -u B < ( x + 1 ) <-> -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) )
46 43 45 anbi12d 
 |-  ( x = -u ( ( |_ ` A ) + 1 ) -> ( ( x <_ -u B /\ -u B < ( x + 1 ) ) <-> ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) ) )
47 46 riota2 
 |-  ( ( -u ( ( |_ ` A ) + 1 ) e. ZZ /\ E! x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) -> ( ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) = -u ( ( |_ ` A ) + 1 ) ) )
48 40 42 47 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) = -u ( ( |_ ` A ) + 1 ) ) )
49 48 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( ( -u ( ( |_ ` A ) + 1 ) <_ -u B /\ -u B < ( -u ( ( |_ ` A ) + 1 ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) = -u ( ( |_ ` A ) + 1 ) ) )
50 37 49 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( iota_ x e. ZZ ( x <_ -u B /\ -u B < ( x + 1 ) ) ) = -u ( ( |_ ` A ) + 1 ) )
51 6 50 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( |_ ` -u B ) = -u ( ( |_ ` A ) + 1 ) )
52 38 zcnd 
 |-  ( A e. RR -> ( |_ ` A ) e. CC )
53 peano2cn 
 |-  ( ( |_ ` A ) e. CC -> ( ( |_ ` A ) + 1 ) e. CC )
54 52 53 syl 
 |-  ( A e. RR -> ( ( |_ ` A ) + 1 ) e. CC )
55 3 flcld 
 |-  ( B e. RR -> ( |_ ` -u B ) e. ZZ )
56 55 zcnd 
 |-  ( B e. RR -> ( |_ ` -u B ) e. CC )
57 negcon2 
 |-  ( ( ( ( |_ ` A ) + 1 ) e. CC /\ ( |_ ` -u B ) e. CC ) -> ( ( ( |_ ` A ) + 1 ) = -u ( |_ ` -u B ) <-> ( |_ ` -u B ) = -u ( ( |_ ` A ) + 1 ) ) )
58 54 56 57 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) + 1 ) = -u ( |_ ` -u B ) <-> ( |_ ` -u B ) = -u ( ( |_ ` A ) + 1 ) ) )
59 58 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( ( ( |_ ` A ) + 1 ) = -u ( |_ ` -u B ) <-> ( |_ ` -u B ) = -u ( ( |_ ` A ) + 1 ) ) )
60 51 59 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> ( ( |_ ` A ) + 1 ) = -u ( |_ ` -u B ) )
61 2 60 breqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) /\ B <_ A ) -> A < -u ( |_ ` -u B ) )
62 61 ex 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) -> ( B <_ A -> A < -u ( |_ ` -u B ) ) )
63 ltnle 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -. B <_ A ) )
64 ceige 
 |-  ( B e. RR -> B <_ -u ( |_ ` -u B ) )
65 64 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> B <_ -u ( |_ ` -u B ) )
66 ceicl 
 |-  ( B e. RR -> -u ( |_ ` -u B ) e. ZZ )
67 66 zred 
 |-  ( B e. RR -> -u ( |_ ` -u B ) e. RR )
68 67 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> -u ( |_ ` -u B ) e. RR )
69 ltletr 
 |-  ( ( A e. RR /\ B e. RR /\ -u ( |_ ` -u B ) e. RR ) -> ( ( A < B /\ B <_ -u ( |_ ` -u B ) ) -> A < -u ( |_ ` -u B ) ) )
70 68 69 mpd3an3 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A < B /\ B <_ -u ( |_ ` -u B ) ) -> A < -u ( |_ ` -u B ) ) )
71 65 70 mpan2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> A < -u ( |_ ` -u B ) ) )
72 63 71 sylbird 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B <_ A -> A < -u ( |_ ` -u B ) ) )
73 72 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) -> ( -. B <_ A -> A < -u ( |_ ` -u B ) ) )
74 62 73 pm2.61d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( |_ ` A ) < B ) -> A < -u ( |_ ` -u B ) )
75 flval 
 |-  ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
76 75 ad3antrrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
77 ceim1l 
 |-  ( B e. RR -> ( -u ( |_ ` -u B ) - 1 ) < B )
78 77 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -u ( |_ ` -u B ) - 1 ) < B )
79 peano2rem 
 |-  ( -u ( |_ ` -u B ) e. RR -> ( -u ( |_ ` -u B ) - 1 ) e. RR )
80 67 79 syl 
 |-  ( B e. RR -> ( -u ( |_ ` -u B ) - 1 ) e. RR )
81 80 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -u ( |_ ` -u B ) - 1 ) e. RR )
82 ltleletr 
 |-  ( ( ( -u ( |_ ` -u B ) - 1 ) e. RR /\ B e. RR /\ A e. RR ) -> ( ( ( -u ( |_ ` -u B ) - 1 ) < B /\ B <_ A ) -> ( -u ( |_ ` -u B ) - 1 ) <_ A ) )
83 82 3com13 
 |-  ( ( A e. RR /\ B e. RR /\ ( -u ( |_ ` -u B ) - 1 ) e. RR ) -> ( ( ( -u ( |_ ` -u B ) - 1 ) < B /\ B <_ A ) -> ( -u ( |_ ` -u B ) - 1 ) <_ A ) )
84 81 83 mpd3an3 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( -u ( |_ ` -u B ) - 1 ) < B /\ B <_ A ) -> ( -u ( |_ ` -u B ) - 1 ) <_ A ) )
85 78 84 mpand 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B <_ A -> ( -u ( |_ ` -u B ) - 1 ) <_ A ) )
86 66 zcnd 
 |-  ( B e. RR -> -u ( |_ ` -u B ) e. CC )
87 npcan 
 |-  ( ( -u ( |_ ` -u B ) e. CC /\ 1 e. CC ) -> ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) = -u ( |_ ` -u B ) )
88 86 23 87 sylancl 
 |-  ( B e. RR -> ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) = -u ( |_ ` -u B ) )
89 88 breq2d 
 |-  ( B e. RR -> ( A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) <-> A < -u ( |_ ` -u B ) ) )
90 89 biimprd 
 |-  ( B e. RR -> ( A < -u ( |_ ` -u B ) -> A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) )
91 90 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < -u ( |_ ` -u B ) -> A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) )
92 85 91 anim12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B <_ A /\ A < -u ( |_ ` -u B ) ) -> ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) ) )
93 92 ancomsd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A < -u ( |_ ` -u B ) /\ B <_ A ) -> ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) ) )
94 93 impl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) )
95 peano2zm 
 |-  ( -u ( |_ ` -u B ) e. ZZ -> ( -u ( |_ ` -u B ) - 1 ) e. ZZ )
96 66 95 syl 
 |-  ( B e. RR -> ( -u ( |_ ` -u B ) - 1 ) e. ZZ )
97 rebtwnz 
 |-  ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
98 breq1 
 |-  ( x = ( -u ( |_ ` -u B ) - 1 ) -> ( x <_ A <-> ( -u ( |_ ` -u B ) - 1 ) <_ A ) )
99 oveq1 
 |-  ( x = ( -u ( |_ ` -u B ) - 1 ) -> ( x + 1 ) = ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) )
100 99 breq2d 
 |-  ( x = ( -u ( |_ ` -u B ) - 1 ) -> ( A < ( x + 1 ) <-> A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) )
101 98 100 anbi12d 
 |-  ( x = ( -u ( |_ ` -u B ) - 1 ) -> ( ( x <_ A /\ A < ( x + 1 ) ) <-> ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) ) )
102 101 riota2 
 |-  ( ( ( -u ( |_ ` -u B ) - 1 ) e. ZZ /\ E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) -> ( ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( -u ( |_ ` -u B ) - 1 ) ) )
103 96 97 102 syl2anr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( -u ( |_ ` -u B ) - 1 ) ) )
104 103 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( ( ( -u ( |_ ` -u B ) - 1 ) <_ A /\ A < ( ( -u ( |_ ` -u B ) - 1 ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( -u ( |_ ` -u B ) - 1 ) ) )
105 94 104 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( -u ( |_ ` -u B ) - 1 ) )
106 76 105 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( |_ ` A ) = ( -u ( |_ ` -u B ) - 1 ) )
107 77 ad3antlr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( -u ( |_ ` -u B ) - 1 ) < B )
108 106 107 eqbrtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) /\ B <_ A ) -> ( |_ ` A ) < B )
109 108 ex 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) -> ( B <_ A -> ( |_ ` A ) < B ) )
110 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
111 110 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( |_ ` A ) <_ A )
112 9 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( |_ ` A ) e. RR )
113 lelttr 
 |-  ( ( ( |_ ` A ) e. RR /\ A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) <_ A /\ A < B ) -> ( |_ ` A ) < B ) )
114 113 3coml 
 |-  ( ( A e. RR /\ B e. RR /\ ( |_ ` A ) e. RR ) -> ( ( ( |_ ` A ) <_ A /\ A < B ) -> ( |_ ` A ) < B ) )
115 112 114 mpd3an3 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( |_ ` A ) <_ A /\ A < B ) -> ( |_ ` A ) < B ) )
116 111 115 mpand 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> ( |_ ` A ) < B ) )
117 63 116 sylbird 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B <_ A -> ( |_ ` A ) < B ) )
118 117 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) -> ( -. B <_ A -> ( |_ ` A ) < B ) )
119 109 118 pm2.61d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A < -u ( |_ ` -u B ) ) -> ( |_ ` A ) < B )
120 74 119 impbida 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B <-> A < -u ( |_ ` -u B ) ) )