Metamath Proof Explorer

Theorem nmoleub2lem3

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015) (Proof shortened by AV, 29-Sep-2021)

Ref Expression
Hypotheses nmoleub2.n 
|- N = ( S normOp T )
nmoleub2.v 
|- V = ( Base ` S )
nmoleub2.l 
|- L = ( norm ` S )
nmoleub2.m 
|- M = ( norm ` T )
nmoleub2.g 
|- G = ( Scalar ` S )
nmoleub2.w 
|- K = ( Base ` G )
nmoleub2.s 
|- ( ph -> S e. ( NrmMod i^i CMod ) )
nmoleub2.t 
|- ( ph -> T e. ( NrmMod i^i CMod ) )
nmoleub2.f 
|- ( ph -> F e. ( S LMHom T ) )
nmoleub2.a 
|- ( ph -> A e. RR* )
nmoleub2.r 
|- ( ph -> R e. RR+ )
nmoleub2a.5 
|- ( ph -> QQ C_ K )
nmoleub2lem3.p 
|- .x. = ( .s ` S )
nmoleub2lem3.1 
|- ( ph -> A e. RR )
nmoleub2lem3.2 
|- ( ph -> 0 <_ A )
nmoleub2lem3.3 
|- ( ph -> B e. V )
nmoleub2lem3.4 
|- ( ph -> B =/= ( 0g ` S ) )
nmoleub2lem3.5 
|- ( ph -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )
nmoleub2lem3.6 
|- ( ph -> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
Assertion nmoleub2lem3 
|- -. ph

Proof

Step Hyp Ref Expression
1 nmoleub2.n 
 |-  N = ( S normOp T )
2 nmoleub2.v 
 |-  V = ( Base ` S )
3 nmoleub2.l 
 |-  L = ( norm ` S )
4 nmoleub2.m 
 |-  M = ( norm ` T )
5 nmoleub2.g 
 |-  G = ( Scalar ` S )
6 nmoleub2.w 
 |-  K = ( Base ` G )
7 nmoleub2.s 
 |-  ( ph -> S e. ( NrmMod i^i CMod ) )
8 nmoleub2.t 
 |-  ( ph -> T e. ( NrmMod i^i CMod ) )
9 nmoleub2.f 
 |-  ( ph -> F e. ( S LMHom T ) )
10 nmoleub2.a 
 |-  ( ph -> A e. RR* )
11 nmoleub2.r 
 |-  ( ph -> R e. RR+ )
12 nmoleub2a.5 
 |-  ( ph -> QQ C_ K )
13 nmoleub2lem3.p 
 |-  .x. = ( .s ` S )
14 nmoleub2lem3.1 
 |-  ( ph -> A e. RR )
15 nmoleub2lem3.2 
 |-  ( ph -> 0 <_ A )
16 nmoleub2lem3.3 
 |-  ( ph -> B e. V )
17 nmoleub2lem3.4 
 |-  ( ph -> B =/= ( 0g ` S ) )
18 nmoleub2lem3.5 
 |-  ( ph -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )
19 nmoleub2lem3.6 
 |-  ( ph -> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
20 simprl 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r )
21 qre 
 |-  ( r e. QQ -> r e. RR )
22 21 ad2antlr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. RR )
23 11 rpred 
 |-  ( ph -> R e. RR )
24 14 23 remulcld 
 |-  ( ph -> ( A x. R ) e. RR )
25 8 elin1d 
 |-  ( ph -> T e. NrmMod )
26 nlmngp 
 |-  ( T e. NrmMod -> T e. NrmGrp )
27 25 26 syl 
 |-  ( ph -> T e. NrmGrp )
28 eqid 
 |-  ( Base ` T ) = ( Base ` T )
29 2 28 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : V --> ( Base ` T ) )
30 9 29 syl 
 |-  ( ph -> F : V --> ( Base ` T ) )
31 30 16 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. ( Base ` T ) )
32 28 4 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` B ) e. ( Base ` T ) ) -> ( M ` ( F ` B ) ) e. RR )
33 27 31 32 syl2anc 
 |-  ( ph -> ( M ` ( F ` B ) ) e. RR )
34 0red 
 |-  ( ph -> 0 e. RR )
35 7 elin1d 
 |-  ( ph -> S e. NrmMod )
36 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
37 35 36 syl 
 |-  ( ph -> S e. NrmGrp )
38 2 3 nmcl 
 |-  ( ( S e. NrmGrp /\ B e. V ) -> ( L ` B ) e. RR )
39 37 16 38 syl2anc 
 |-  ( ph -> ( L ` B ) e. RR )
40 14 39 remulcld 
 |-  ( ph -> ( A x. ( L ` B ) ) e. RR )
41 2 3 nmge0 
 |-  ( ( S e. NrmGrp /\ B e. V ) -> 0 <_ ( L ` B ) )
42 37 16 41 syl2anc 
 |-  ( ph -> 0 <_ ( L ` B ) )
43 14 39 15 42 mulge0d 
 |-  ( ph -> 0 <_ ( A x. ( L ` B ) ) )
44 40 33 ltnled 
 |-  ( ph -> ( ( A x. ( L ` B ) ) < ( M ` ( F ` B ) ) <-> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) ) )
45 19 44 mpbird 
 |-  ( ph -> ( A x. ( L ` B ) ) < ( M ` ( F ` B ) ) )
46 34 40 33 43 45 lelttrd 
 |-  ( ph -> 0 < ( M ` ( F ` B ) ) )
47 33 46 elrpd 
 |-  ( ph -> ( M ` ( F ` B ) ) e. RR+ )
48 24 47 rerpdivcld 
 |-  ( ph -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR )
49 48 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR )
50 9 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> F e. ( S LMHom T ) )
51 12 sselda 
 |-  ( ( ph /\ r e. QQ ) -> r e. K )
52 51 adantr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. K )
53 16 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> B e. V )
54 eqid 
 |-  ( .s ` T ) = ( .s ` T )
55 5 6 2 13 54 lmhmlin 
 |-  ( ( F e. ( S LMHom T ) /\ r e. K /\ B e. V ) -> ( F ` ( r .x. B ) ) = ( r ( .s ` T ) ( F ` B ) ) )
56 50 52 53 55 syl3anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( F ` ( r .x. B ) ) = ( r ( .s ` T ) ( F ` B ) ) )
57 56 fveq2d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` ( r .x. B ) ) ) = ( M ` ( r ( .s ` T ) ( F ` B ) ) ) )
58 25 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> T e. NrmMod )
59 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
60 5 59 lmhmsca 
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = G )
61 50 60 syl 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( Scalar ` T ) = G )
62 61 fveq2d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( Base ` ( Scalar ` T ) ) = ( Base ` G ) )
63 62 6 eqtr4di 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( Base ` ( Scalar ` T ) ) = K )
64 52 63 eleqtrrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. ( Base ` ( Scalar ` T ) ) )
65 31 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( F ` B ) e. ( Base ` T ) )
66 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
67 eqid 
 |-  ( norm ` ( Scalar ` T ) ) = ( norm ` ( Scalar ` T ) )
68 28 4 54 59 66 67 nmvs 
 |-  ( ( T e. NrmMod /\ r e. ( Base ` ( Scalar ` T ) ) /\ ( F ` B ) e. ( Base ` T ) ) -> ( M ` ( r ( .s ` T ) ( F ` B ) ) ) = ( ( ( norm ` ( Scalar ` T ) ) ` r ) x. ( M ` ( F ` B ) ) ) )
69 58 64 65 68 syl3anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( r ( .s ` T ) ( F ` B ) ) ) = ( ( ( norm ` ( Scalar ` T ) ) ` r ) x. ( M ` ( F ` B ) ) ) )
70 61 fveq2d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( norm ` ( Scalar ` T ) ) = ( norm ` G ) )
71 70 fveq1d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( norm ` ( Scalar ` T ) ) ` r ) = ( ( norm ` G ) ` r ) )
72 7 elin2d 
 |-  ( ph -> S e. CMod )
73 72 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> S e. CMod )
74 5 6 clmabs 
 |-  ( ( S e. CMod /\ r e. K ) -> ( abs ` r ) = ( ( norm ` G ) ` r ) )
75 73 52 74 syl2anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( abs ` r ) = ( ( norm ` G ) ` r ) )
76 0red 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 e. RR )
77 11 rpge0d 
 |-  ( ph -> 0 <_ R )
78 14 23 15 77 mulge0d 
 |-  ( ph -> 0 <_ ( A x. R ) )
79 divge0 
 |-  ( ( ( ( A x. R ) e. RR /\ 0 <_ ( A x. R ) ) /\ ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) ) -> 0 <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
80 24 78 33 46 79 syl22anc 
 |-  ( ph -> 0 <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
81 80 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
82 76 49 22 81 20 lelttrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 < r )
83 76 22 82 ltled 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 <_ r )
84 22 83 absidd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( abs ` r ) = r )
85 75 84 eqtr3d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( norm ` G ) ` r ) = r )
86 71 85 eqtrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( norm ` ( Scalar ` T ) ) ` r ) = r )
87 86 oveq1d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( ( norm ` ( Scalar ` T ) ) ` r ) x. ( M ` ( F ` B ) ) ) = ( r x. ( M ` ( F ` B ) ) ) )
88 57 69 87 3eqtrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` ( r .x. B ) ) ) = ( r x. ( M ` ( F ` B ) ) ) )
89 88 oveq1d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) = ( ( r x. ( M ` ( F ` B ) ) ) / R ) )
90 2 5 13 6 clmvscl 
 |-  ( ( S e. CMod /\ r e. K /\ B e. V ) -> ( r .x. B ) e. V )
91 73 52 53 90 syl3anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r .x. B ) e. V )
92 35 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> S e. NrmMod )
93 eqid 
 |-  ( norm ` G ) = ( norm ` G )
94 2 3 13 5 6 93 nmvs 
 |-  ( ( S e. NrmMod /\ r e. K /\ B e. V ) -> ( L ` ( r .x. B ) ) = ( ( ( norm ` G ) ` r ) x. ( L ` B ) ) )
95 92 52 53 94 syl3anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( L ` ( r .x. B ) ) = ( ( ( norm ` G ) ` r ) x. ( L ` B ) ) )
96 85 oveq1d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( ( norm ` G ) ` r ) x. ( L ` B ) ) = ( r x. ( L ` B ) ) )
97 95 96 eqtrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( L ` ( r .x. B ) ) = ( r x. ( L ` B ) ) )
98 simprr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r < ( R / ( L ` B ) ) )
99 23 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> R e. RR )
100 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
101 2 3 100 nmrpcl 
 |-  ( ( S e. NrmGrp /\ B e. V /\ B =/= ( 0g ` S ) ) -> ( L ` B ) e. RR+ )
102 37 16 17 101 syl3anc 
 |-  ( ph -> ( L ` B ) e. RR+ )
103 102 rpregt0d 
 |-  ( ph -> ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) )
104 103 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) )
105 ltmuldiv 
 |-  ( ( r e. RR /\ R e. RR /\ ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) ) -> ( ( r x. ( L ` B ) ) < R <-> r < ( R / ( L ` B ) ) ) )
106 22 99 104 105 syl3anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r x. ( L ` B ) ) < R <-> r < ( R / ( L ` B ) ) ) )
107 98 106 mpbird 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r x. ( L ` B ) ) < R )
108 97 107 eqbrtrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( L ` ( r .x. B ) ) < R )
109 18 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )
110 91 108 109 mp2d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A )
111 89 110 eqbrtrrd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r x. ( M ` ( F ` B ) ) ) / R ) <_ A )
112 33 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` B ) ) e. RR )
113 22 112 remulcld 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r x. ( M ` ( F ` B ) ) ) e. RR )
114 14 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> A e. RR )
115 11 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> R e. RR+ )
116 113 114 115 ledivmul2d 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( ( r x. ( M ` ( F ` B ) ) ) / R ) <_ A <-> ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) ) )
117 111 116 mpbid 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) )
118 114 99 remulcld 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( A x. R ) e. RR )
119 33 46 jca 
 |-  ( ph -> ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) )
120 119 ad2antrr 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) )
121 lemuldiv 
 |-  ( ( r e. RR /\ ( A x. R ) e. RR /\ ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) ) -> ( ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) <-> r <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) ) )
122 22 118 120 121 syl3anc 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) <-> r <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) ) )
123 117 122 mpbid 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
124 22 49 123 lensymd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> -. ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r )
125 20 124 pm2.21dd 
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
126 23 102 rerpdivcld 
 |-  ( ph -> ( R / ( L ` B ) ) e. RR )
127 14 recnd 
 |-  ( ph -> A e. CC )
128 23 recnd 
 |-  ( ph -> R e. CC )
129 39 recnd 
 |-  ( ph -> ( L ` B ) e. CC )
130 mulass 
 |-  ( ( A e. CC /\ R e. CC /\ ( L ` B ) e. CC ) -> ( ( A x. R ) x. ( L ` B ) ) = ( A x. ( R x. ( L ` B ) ) ) )
131 mul12 
 |-  ( ( A e. CC /\ R e. CC /\ ( L ` B ) e. CC ) -> ( A x. ( R x. ( L ` B ) ) ) = ( R x. ( A x. ( L ` B ) ) ) )
132 130 131 eqtrd 
 |-  ( ( A e. CC /\ R e. CC /\ ( L ` B ) e. CC ) -> ( ( A x. R ) x. ( L ` B ) ) = ( R x. ( A x. ( L ` B ) ) ) )
133 127 128 129 132 syl3anc 
 |-  ( ph -> ( ( A x. R ) x. ( L ` B ) ) = ( R x. ( A x. ( L ` B ) ) ) )
134 40 33 11 45 ltmul2dd 
 |-  ( ph -> ( R x. ( A x. ( L ` B ) ) ) < ( R x. ( M ` ( F ` B ) ) ) )
135 133 134 eqbrtrd 
 |-  ( ph -> ( ( A x. R ) x. ( L ` B ) ) < ( R x. ( M ` ( F ` B ) ) ) )
136 lt2mul2div 
 |-  ( ( ( ( A x. R ) e. RR /\ ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) ) /\ ( R e. RR /\ ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) ) ) -> ( ( ( A x. R ) x. ( L ` B ) ) < ( R x. ( M ` ( F ` B ) ) ) <-> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) ) )
137 24 103 23 119 136 syl22anc 
 |-  ( ph -> ( ( ( A x. R ) x. ( L ` B ) ) < ( R x. ( M ` ( F ` B ) ) ) <-> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) ) )
138 135 137 mpbid 
 |-  ( ph -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) )
139 qbtwnre 
 |-  ( ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR /\ ( R / ( L ` B ) ) e. RR /\ ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) ) -> E. r e. QQ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) )
140 48 126 138 139 syl3anc 
 |-  ( ph -> E. r e. QQ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) )
141 125 140 r19.29a 
 |-  ( ph -> ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
142 141 19 pm2.65i 
 |-  -. ph