Proof of Theorem nmoleub2lem3
Step | Hyp | Ref
| Expression |
1 | | simprl 768 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟) |
2 | | qre 12693 |
. . . . . 6
⊢ (𝑟 ∈ ℚ → 𝑟 ∈
ℝ) |
3 | 2 | ad2antlr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑟 ∈ ℝ) |
4 | | nmoleub2lem3.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
5 | | nmoleub2.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
6 | 5 | rpred 12772 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℝ) |
7 | 4, 6 | remulcld 11005 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝑅) ∈ ℝ) |
8 | | nmoleub2.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩
ℂMod)) |
9 | 8 | elin1d 4132 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ NrmMod) |
10 | | nlmngp 23841 |
. . . . . . . . . 10
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ NrmGrp) |
12 | | nmoleub2.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
13 | | nmoleub2.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Base‘𝑆) |
14 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑇) =
(Base‘𝑇) |
15 | 13, 14 | lmhmf 20296 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
16 | 12, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑉⟶(Base‘𝑇)) |
17 | | nmoleub2lem3.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
18 | 16, 17 | ffvelrnd 6962 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐵) ∈ (Base‘𝑇)) |
19 | | nmoleub2.m |
. . . . . . . . . 10
⊢ 𝑀 = (norm‘𝑇) |
20 | 14, 19 | nmcl 23772 |
. . . . . . . . 9
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝐵) ∈ (Base‘𝑇)) → (𝑀‘(𝐹‘𝐵)) ∈ ℝ) |
21 | 11, 18, 20 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝐹‘𝐵)) ∈ ℝ) |
22 | | 0red 10978 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
23 | | nmoleub2.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩
ℂMod)) |
24 | 23 | elin1d 4132 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ NrmMod) |
25 | | nlmngp 23841 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ NrmGrp) |
27 | | nmoleub2.l |
. . . . . . . . . . . 12
⊢ 𝐿 = (norm‘𝑆) |
28 | 13, 27 | nmcl 23772 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉) → (𝐿‘𝐵) ∈ ℝ) |
29 | 26, 17, 28 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿‘𝐵) ∈ ℝ) |
30 | 4, 29 | remulcld 11005 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · (𝐿‘𝐵)) ∈ ℝ) |
31 | | nmoleub2lem3.2 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐴) |
32 | 13, 27 | nmge0 23773 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉) → 0 ≤ (𝐿‘𝐵)) |
33 | 26, 17, 32 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝐿‘𝐵)) |
34 | 4, 29, 31, 33 | mulge0d 11552 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝐴 · (𝐿‘𝐵))) |
35 | | nmoleub2lem3.6 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝑀‘(𝐹‘𝐵)) ≤ (𝐴 · (𝐿‘𝐵))) |
36 | 30, 21 | ltnled 11122 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 · (𝐿‘𝐵)) < (𝑀‘(𝐹‘𝐵)) ↔ ¬ (𝑀‘(𝐹‘𝐵)) ≤ (𝐴 · (𝐿‘𝐵)))) |
37 | 35, 36 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · (𝐿‘𝐵)) < (𝑀‘(𝐹‘𝐵))) |
38 | 22, 30, 21, 34, 37 | lelttrd 11133 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝑀‘(𝐹‘𝐵))) |
39 | 21, 38 | elrpd 12769 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘(𝐹‘𝐵)) ∈
ℝ+) |
40 | 7, 39 | rerpdivcld 12803 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) ∈ ℝ) |
41 | 40 | ad2antrr 723 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) ∈ ℝ) |
42 | 12 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
43 | | nmoleub2a.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℚ ⊆ 𝐾) |
44 | 43 | sselda 3921 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℚ) → 𝑟 ∈ 𝐾) |
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑟 ∈ 𝐾) |
46 | 17 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝐵 ∈ 𝑉) |
47 | | nmoleub2.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (Scalar‘𝑆) |
48 | | nmoleub2.w |
. . . . . . . . . . . . 13
⊢ 𝐾 = (Base‘𝐺) |
49 | | nmoleub2lem3.p |
. . . . . . . . . . . . 13
⊢ · = (
·𝑠 ‘𝑆) |
50 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
51 | 47, 48, 13, 49, 50 | lmhmlin 20297 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑟 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → (𝐹‘(𝑟 · 𝐵)) = (𝑟( ·𝑠
‘𝑇)(𝐹‘𝐵))) |
52 | 42, 45, 46, 51 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝐹‘(𝑟 · 𝐵)) = (𝑟( ·𝑠
‘𝑇)(𝐹‘𝐵))) |
53 | 52 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑀‘(𝐹‘(𝑟 · 𝐵))) = (𝑀‘(𝑟( ·𝑠
‘𝑇)(𝐹‘𝐵)))) |
54 | 9 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑇 ∈ NrmMod) |
55 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
56 | 47, 55 | lmhmsca 20292 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = 𝐺) |
57 | 42, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (Scalar‘𝑇) = 𝐺) |
58 | 57 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (Base‘(Scalar‘𝑇)) = (Base‘𝐺)) |
59 | 58, 48 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (Base‘(Scalar‘𝑇)) = 𝐾) |
60 | 45, 59 | eleqtrrd 2842 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑟 ∈ (Base‘(Scalar‘𝑇))) |
61 | 18 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝐹‘𝐵) ∈ (Base‘𝑇)) |
62 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) |
63 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(norm‘(Scalar‘𝑇)) = (norm‘(Scalar‘𝑇)) |
64 | 14, 19, 50, 55, 62, 63 | nmvs 23840 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ NrmMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑇)) ∧ (𝐹‘𝐵) ∈ (Base‘𝑇)) → (𝑀‘(𝑟( ·𝑠
‘𝑇)(𝐹‘𝐵))) = (((norm‘(Scalar‘𝑇))‘𝑟) · (𝑀‘(𝐹‘𝐵)))) |
65 | 54, 60, 61, 64 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑀‘(𝑟( ·𝑠
‘𝑇)(𝐹‘𝐵))) = (((norm‘(Scalar‘𝑇))‘𝑟) · (𝑀‘(𝐹‘𝐵)))) |
66 | 57 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (norm‘(Scalar‘𝑇)) = (norm‘𝐺)) |
67 | 66 | fveq1d 6776 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((norm‘(Scalar‘𝑇))‘𝑟) = ((norm‘𝐺)‘𝑟)) |
68 | 23 | elin2d 4133 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ ℂMod) |
69 | 68 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑆 ∈ ℂMod) |
70 | 47, 48 | clmabs 24246 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℂMod ∧ 𝑟 ∈ 𝐾) → (abs‘𝑟) = ((norm‘𝐺)‘𝑟)) |
71 | 69, 45, 70 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (abs‘𝑟) = ((norm‘𝐺)‘𝑟)) |
72 | | 0red 10978 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 0 ∈
ℝ) |
73 | 5 | rpge0d 12776 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 𝑅) |
74 | 4, 6, 31, 73 | mulge0d 11552 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (𝐴 · 𝑅)) |
75 | | divge0 11844 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 · 𝑅) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝑅)) ∧ ((𝑀‘(𝐹‘𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹‘𝐵)))) → 0 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵)))) |
76 | 7, 74, 21, 38, 75 | syl22anc 836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵)))) |
77 | 76 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 0 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵)))) |
78 | 72, 41, 3, 77, 1 | lelttrd 11133 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 0 < 𝑟) |
79 | 72, 3, 78 | ltled 11123 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 0 ≤ 𝑟) |
80 | 3, 79 | absidd 15134 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (abs‘𝑟) = 𝑟) |
81 | 71, 80 | eqtr3d 2780 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((norm‘𝐺)‘𝑟) = 𝑟) |
82 | 67, 81 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((norm‘(Scalar‘𝑇))‘𝑟) = 𝑟) |
83 | 82 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) →
(((norm‘(Scalar‘𝑇))‘𝑟) · (𝑀‘(𝐹‘𝐵))) = (𝑟 · (𝑀‘(𝐹‘𝐵)))) |
84 | 53, 65, 83 | 3eqtrd 2782 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑀‘(𝐹‘(𝑟 · 𝐵))) = (𝑟 · (𝑀‘(𝐹‘𝐵)))) |
85 | 84 | oveq1d 7290 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) = ((𝑟 · (𝑀‘(𝐹‘𝐵))) / 𝑅)) |
86 | 13, 47, 49, 48 | clmvscl 24251 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℂMod ∧ 𝑟 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → (𝑟 · 𝐵) ∈ 𝑉) |
87 | 69, 45, 46, 86 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑟 · 𝐵) ∈ 𝑉) |
88 | 24 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑆 ∈ NrmMod) |
89 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(norm‘𝐺) =
(norm‘𝐺) |
90 | 13, 27, 49, 47, 48, 89 | nmvs 23840 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ NrmMod ∧ 𝑟 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉) → (𝐿‘(𝑟 · 𝐵)) = (((norm‘𝐺)‘𝑟) · (𝐿‘𝐵))) |
91 | 88, 45, 46, 90 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝐿‘(𝑟 · 𝐵)) = (((norm‘𝐺)‘𝑟) · (𝐿‘𝐵))) |
92 | 81 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (((norm‘𝐺)‘𝑟) · (𝐿‘𝐵)) = (𝑟 · (𝐿‘𝐵))) |
93 | 91, 92 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝐿‘(𝑟 · 𝐵)) = (𝑟 · (𝐿‘𝐵))) |
94 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑟 < (𝑅 / (𝐿‘𝐵))) |
95 | 6 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑅 ∈ ℝ) |
96 | | nmoleub2lem3.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ (0g‘𝑆)) |
97 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑆) = (0g‘𝑆) |
98 | 13, 27, 97 | nmrpcl 23776 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ∧ 𝐵 ≠ (0g‘𝑆)) → (𝐿‘𝐵) ∈
ℝ+) |
99 | 26, 17, 96, 98 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿‘𝐵) ∈
ℝ+) |
100 | 99 | rpregt0d 12778 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿‘𝐵) ∈ ℝ ∧ 0 < (𝐿‘𝐵))) |
101 | 100 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝐿‘𝐵) ∈ ℝ ∧ 0 < (𝐿‘𝐵))) |
102 | | ltmuldiv 11848 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((𝐿‘𝐵) ∈ ℝ ∧ 0 < (𝐿‘𝐵))) → ((𝑟 · (𝐿‘𝐵)) < 𝑅 ↔ 𝑟 < (𝑅 / (𝐿‘𝐵)))) |
103 | 3, 95, 101, 102 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑟 · (𝐿‘𝐵)) < 𝑅 ↔ 𝑟 < (𝑅 / (𝐿‘𝐵)))) |
104 | 94, 103 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑟 · (𝐿‘𝐵)) < 𝑅) |
105 | 93, 104 | eqbrtrd 5096 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝐿‘(𝑟 · 𝐵)) < 𝑅) |
106 | | nmoleub2lem3.5 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑟 · 𝐵) ∈ 𝑉 → ((𝐿‘(𝑟 · 𝐵)) < 𝑅 → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴))) |
107 | 106 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑟 · 𝐵) ∈ 𝑉 → ((𝐿‘(𝑟 · 𝐵)) < 𝑅 → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴))) |
108 | 87, 105, 107 | mp2d 49 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑀‘(𝐹‘(𝑟 · 𝐵))) / 𝑅) ≤ 𝐴) |
109 | 85, 108 | eqbrtrrd 5098 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑟 · (𝑀‘(𝐹‘𝐵))) / 𝑅) ≤ 𝐴) |
110 | 21 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑀‘(𝐹‘𝐵)) ∈ ℝ) |
111 | 3, 110 | remulcld 11005 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑟 · (𝑀‘(𝐹‘𝐵))) ∈ ℝ) |
112 | 4 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝐴 ∈ ℝ) |
113 | 5 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑅 ∈
ℝ+) |
114 | 111, 112,
113 | ledivmul2d 12826 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (((𝑟 · (𝑀‘(𝐹‘𝐵))) / 𝑅) ≤ 𝐴 ↔ (𝑟 · (𝑀‘(𝐹‘𝐵))) ≤ (𝐴 · 𝑅))) |
115 | 109, 114 | mpbid 231 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑟 · (𝑀‘(𝐹‘𝐵))) ≤ (𝐴 · 𝑅)) |
116 | 112, 95 | remulcld 11005 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝐴 · 𝑅) ∈ ℝ) |
117 | 21, 38 | jca 512 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀‘(𝐹‘𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹‘𝐵)))) |
118 | 117 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑀‘(𝐹‘𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹‘𝐵)))) |
119 | | lemuldiv 11855 |
. . . . . . 7
⊢ ((𝑟 ∈ ℝ ∧ (𝐴 · 𝑅) ∈ ℝ ∧ ((𝑀‘(𝐹‘𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹‘𝐵)))) → ((𝑟 · (𝑀‘(𝐹‘𝐵))) ≤ (𝐴 · 𝑅) ↔ 𝑟 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))))) |
120 | 3, 116, 118, 119 | syl3anc 1370 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ((𝑟 · (𝑀‘(𝐹‘𝐵))) ≤ (𝐴 · 𝑅) ↔ 𝑟 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))))) |
121 | 115, 120 | mpbid 231 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → 𝑟 ≤ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵)))) |
122 | 3, 41, 121 | lensymd 11126 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → ¬ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟) |
123 | 1, 122 | pm2.21dd 194 |
. . 3
⊢ (((𝜑 ∧ 𝑟 ∈ ℚ) ∧ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) → (𝑀‘(𝐹‘𝐵)) ≤ (𝐴 · (𝐿‘𝐵))) |
124 | 6, 99 | rerpdivcld 12803 |
. . . 4
⊢ (𝜑 → (𝑅 / (𝐿‘𝐵)) ∈ ℝ) |
125 | 4 | recnd 11003 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
126 | 6 | recnd 11003 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℂ) |
127 | 29 | recnd 11003 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘𝐵) ∈ ℂ) |
128 | | mulass 10959 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (𝐿‘𝐵) ∈ ℂ) → ((𝐴 · 𝑅) · (𝐿‘𝐵)) = (𝐴 · (𝑅 · (𝐿‘𝐵)))) |
129 | | mul12 11140 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (𝐿‘𝐵) ∈ ℂ) → (𝐴 · (𝑅 · (𝐿‘𝐵))) = (𝑅 · (𝐴 · (𝐿‘𝐵)))) |
130 | 128, 129 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (𝐿‘𝐵) ∈ ℂ) → ((𝐴 · 𝑅) · (𝐿‘𝐵)) = (𝑅 · (𝐴 · (𝐿‘𝐵)))) |
131 | 125, 126,
127, 130 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · 𝑅) · (𝐿‘𝐵)) = (𝑅 · (𝐴 · (𝐿‘𝐵)))) |
132 | 30, 21, 5, 37 | ltmul2dd 12828 |
. . . . . 6
⊢ (𝜑 → (𝑅 · (𝐴 · (𝐿‘𝐵))) < (𝑅 · (𝑀‘(𝐹‘𝐵)))) |
133 | 131, 132 | eqbrtrd 5096 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝑅) · (𝐿‘𝐵)) < (𝑅 · (𝑀‘(𝐹‘𝐵)))) |
134 | | lt2mul2div 11853 |
. . . . . 6
⊢ ((((𝐴 · 𝑅) ∈ ℝ ∧ ((𝐿‘𝐵) ∈ ℝ ∧ 0 < (𝐿‘𝐵))) ∧ (𝑅 ∈ ℝ ∧ ((𝑀‘(𝐹‘𝐵)) ∈ ℝ ∧ 0 < (𝑀‘(𝐹‘𝐵))))) → (((𝐴 · 𝑅) · (𝐿‘𝐵)) < (𝑅 · (𝑀‘(𝐹‘𝐵))) ↔ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < (𝑅 / (𝐿‘𝐵)))) |
135 | 7, 100, 6, 117, 134 | syl22anc 836 |
. . . . 5
⊢ (𝜑 → (((𝐴 · 𝑅) · (𝐿‘𝐵)) < (𝑅 · (𝑀‘(𝐹‘𝐵))) ↔ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < (𝑅 / (𝐿‘𝐵)))) |
136 | 133, 135 | mpbid 231 |
. . . 4
⊢ (𝜑 → ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < (𝑅 / (𝐿‘𝐵))) |
137 | | qbtwnre 12933 |
. . . 4
⊢ ((((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) ∈ ℝ ∧ (𝑅 / (𝐿‘𝐵)) ∈ ℝ ∧ ((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < (𝑅 / (𝐿‘𝐵))) → ∃𝑟 ∈ ℚ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) |
138 | 40, 124, 136, 137 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ ℚ (((𝐴 · 𝑅) / (𝑀‘(𝐹‘𝐵))) < 𝑟 ∧ 𝑟 < (𝑅 / (𝐿‘𝐵)))) |
139 | 123, 138 | r19.29a 3218 |
. 2
⊢ (𝜑 → (𝑀‘(𝐹‘𝐵)) ≤ (𝐴 · (𝐿‘𝐵))) |
140 | 139, 35 | pm2.65i 193 |
1
⊢ ¬
𝜑 |