# 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}\mathrm{normOp}{T}$
nmoleub2.v ${⊢}{V}={\mathrm{Base}}_{{S}}$
nmoleub2.l ${⊢}{L}=\mathrm{norm}\left({S}\right)$
nmoleub2.m ${⊢}{M}=\mathrm{norm}\left({T}\right)$
nmoleub2.g ${⊢}{G}=\mathrm{Scalar}\left({S}\right)$
nmoleub2.w ${⊢}{K}={\mathrm{Base}}_{{G}}$
nmoleub2.s ${⊢}{\phi }\to {S}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
nmoleub2.t ${⊢}{\phi }\to {T}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
nmoleub2.f ${⊢}{\phi }\to {F}\in \left({S}\mathrm{LMHom}{T}\right)$
nmoleub2.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
nmoleub2.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
nmoleub2a.5 ${⊢}{\phi }\to ℚ\subseteq {K}$
nmoleub2lem3.p
nmoleub2lem3.1 ${⊢}{\phi }\to {A}\in ℝ$
nmoleub2lem3.2 ${⊢}{\phi }\to 0\le {A}$
nmoleub2lem3.3 ${⊢}{\phi }\to {B}\in {V}$
nmoleub2lem3.4 ${⊢}{\phi }\to {B}\ne {0}_{{S}}$
nmoleub2lem3.5
nmoleub2lem3.6 ${⊢}{\phi }\to ¬{M}\left({F}\left({B}\right)\right)\le {A}{L}\left({B}\right)$
Assertion nmoleub2lem3 ${⊢}¬{\phi }$

### Proof

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