Step | Hyp | Ref
| Expression |
1 | | nmoleub2.n |
. 2
β’ π = (π normOp π) |
2 | | nmoleub2.v |
. 2
β’ π = (Baseβπ) |
3 | | nmoleub2.l |
. 2
β’ πΏ = (normβπ) |
4 | | nmoleub2.m |
. 2
β’ π = (normβπ) |
5 | | nmoleub2.g |
. 2
β’ πΊ = (Scalarβπ) |
6 | | nmoleub2.w |
. 2
β’ πΎ = (BaseβπΊ) |
7 | | nmoleub2.s |
. 2
β’ (π β π β (NrmMod β©
βMod)) |
8 | | nmoleub2.t |
. 2
β’ (π β π β (NrmMod β©
βMod)) |
9 | | nmoleub2.f |
. 2
β’ (π β πΉ β (π LMHom π)) |
10 | | nmoleub2.a |
. 2
β’ (π β π΄ β
β*) |
11 | | nmoleub2.r |
. 2
β’ (π β π
β
β+) |
12 | | nmoleub3.5 |
. . 3
β’ (π β 0 β€ π΄) |
13 | 12 | adantr 481 |
. 2
β’ ((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β 0 β€ π΄) |
14 | 9 | ad3antrrr 728 |
. . . . . . . . 9
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β πΉ β (π LMHom π)) |
15 | | nmoleub3.6 |
. . . . . . . . . . 11
β’ (π β β β πΎ) |
16 | 15 | ad3antrrr 728 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β β β πΎ) |
17 | 11 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π
β
β+) |
18 | 7 | elin1d 4197 |
. . . . . . . . . . . . . . 15
β’ (π β π β NrmMod) |
19 | 18 | ad3antrrr 728 |
. . . . . . . . . . . . . 14
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π β NrmMod) |
20 | | nlmngp 24185 |
. . . . . . . . . . . . . 14
β’ (π β NrmMod β π β NrmGrp) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π β NrmGrp) |
22 | | simprl 769 |
. . . . . . . . . . . . 13
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π¦ β π) |
23 | | simprr 771 |
. . . . . . . . . . . . 13
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π¦ β (0gβπ)) |
24 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(0gβπ) = (0gβπ) |
25 | 2, 3, 24 | nmrpcl 24120 |
. . . . . . . . . . . . 13
β’ ((π β NrmGrp β§ π¦ β π β§ π¦ β (0gβπ)) β (πΏβπ¦) β
β+) |
26 | 21, 22, 23, 25 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΏβπ¦) β
β+) |
27 | 17, 26 | rpdivcld 13029 |
. . . . . . . . . . 11
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (π
/ (πΏβπ¦)) β
β+) |
28 | 27 | rpred 13012 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (π
/ (πΏβπ¦)) β β) |
29 | 16, 28 | sseldd 3982 |
. . . . . . . . 9
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (π
/ (πΏβπ¦)) β πΎ) |
30 | | eqid 2732 |
. . . . . . . . . 10
β’ (
Β·π βπ) = ( Β·π
βπ) |
31 | | eqid 2732 |
. . . . . . . . . 10
β’ (
Β·π βπ) = ( Β·π
βπ) |
32 | 5, 6, 2, 30, 31 | lmhmlin 20638 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ (π
/ (πΏβπ¦)) β πΎ β§ π¦ β π) β (πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = ((π
/ (πΏβπ¦))( Β·π
βπ)(πΉβπ¦))) |
33 | 14, 29, 22, 32 | syl3anc 1371 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = ((π
/ (πΏβπ¦))( Β·π
βπ)(πΉβπ¦))) |
34 | 33 | fveq2d 6892 |
. . . . . . 7
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) = (πβ((π
/ (πΏβπ¦))( Β·π
βπ)(πΉβπ¦)))) |
35 | 8 | elin1d 4197 |
. . . . . . . . 9
β’ (π β π β NrmMod) |
36 | 35 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π β NrmMod) |
37 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Scalarβπ) =
(Scalarβπ) |
38 | 5, 37 | lmhmsca 20633 |
. . . . . . . . . . . 12
β’ (πΉ β (π LMHom π) β (Scalarβπ) = πΊ) |
39 | 14, 38 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (Scalarβπ) = πΊ) |
40 | 39 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (Baseβ(Scalarβπ)) = (BaseβπΊ)) |
41 | 40, 6 | eqtr4di 2790 |
. . . . . . . . 9
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (Baseβ(Scalarβπ)) = πΎ) |
42 | 29, 41 | eleqtrrd 2836 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (π
/ (πΏβπ¦)) β (Baseβ(Scalarβπ))) |
43 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
44 | 2, 43 | lmhmf 20637 |
. . . . . . . . . 10
β’ (πΉ β (π LMHom π) β πΉ:πβΆ(Baseβπ)) |
45 | 14, 44 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β πΉ:πβΆ(Baseβπ)) |
46 | 45, 22 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΉβπ¦) β (Baseβπ)) |
47 | | eqid 2732 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
48 | | eqid 2732 |
. . . . . . . . 9
β’
(normβ(Scalarβπ)) = (normβ(Scalarβπ)) |
49 | 43, 4, 31, 37, 47, 48 | nmvs 24184 |
. . . . . . . 8
β’ ((π β NrmMod β§ (π
/ (πΏβπ¦)) β (Baseβ(Scalarβπ)) β§ (πΉβπ¦) β (Baseβπ)) β (πβ((π
/ (πΏβπ¦))( Β·π
βπ)(πΉβπ¦))) = (((normβ(Scalarβπ))β(π
/ (πΏβπ¦))) Β· (πβ(πΉβπ¦)))) |
50 | 36, 42, 46, 49 | syl3anc 1371 |
. . . . . . 7
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ((π
/ (πΏβπ¦))( Β·π
βπ)(πΉβπ¦))) = (((normβ(Scalarβπ))β(π
/ (πΏβπ¦))) Β· (πβ(πΉβπ¦)))) |
51 | 39 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (normβ(Scalarβπ)) = (normβπΊ)) |
52 | 51 | fveq1d 6890 |
. . . . . . . . 9
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((normβ(Scalarβπ))β(π
/ (πΏβπ¦))) = ((normβπΊ)β(π
/ (πΏβπ¦)))) |
53 | 7 | elin2d 4198 |
. . . . . . . . . . . 12
β’ (π β π β βMod) |
54 | 53 | ad3antrrr 728 |
. . . . . . . . . . 11
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π β βMod) |
55 | 5, 6 | clmabs 24590 |
. . . . . . . . . . 11
β’ ((π β βMod β§ (π
/ (πΏβπ¦)) β πΎ) β (absβ(π
/ (πΏβπ¦))) = ((normβπΊ)β(π
/ (πΏβπ¦)))) |
56 | 54, 29, 55 | syl2anc 584 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (absβ(π
/ (πΏβπ¦))) = ((normβπΊ)β(π
/ (πΏβπ¦)))) |
57 | 27 | rpge0d 13016 |
. . . . . . . . . . 11
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β 0 β€ (π
/ (πΏβπ¦))) |
58 | 28, 57 | absidd 15365 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (absβ(π
/ (πΏβπ¦))) = (π
/ (πΏβπ¦))) |
59 | 56, 58 | eqtr3d 2774 |
. . . . . . . . 9
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((normβπΊ)β(π
/ (πΏβπ¦))) = (π
/ (πΏβπ¦))) |
60 | 52, 59 | eqtrd 2772 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((normβ(Scalarβπ))β(π
/ (πΏβπ¦))) = (π
/ (πΏβπ¦))) |
61 | 60 | oveq1d 7420 |
. . . . . . 7
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (((normβ(Scalarβπ))β(π
/ (πΏβπ¦))) Β· (πβ(πΉβπ¦))) = ((π
/ (πΏβπ¦)) Β· (πβ(πΉβπ¦)))) |
62 | 34, 50, 61 | 3eqtrd 2776 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) = ((π
/ (πΏβπ¦)) Β· (πβ(πΉβπ¦)))) |
63 | 62 | oveq1d 7420 |
. . . . 5
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
) = (((π
/ (πΏβπ¦)) Β· (πβ(πΉβπ¦))) / π
)) |
64 | 27 | rpcnd 13014 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (π
/ (πΏβπ¦)) β β) |
65 | | nlmngp 24185 |
. . . . . . . . 9
β’ (π β NrmMod β π β NrmGrp) |
66 | 36, 65 | syl 17 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π β NrmGrp) |
67 | 43, 4 | nmcl 24116 |
. . . . . . . 8
β’ ((π β NrmGrp β§ (πΉβπ¦) β (Baseβπ)) β (πβ(πΉβπ¦)) β β) |
68 | 66, 46, 67 | syl2anc 584 |
. . . . . . 7
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβπ¦)) β β) |
69 | 68 | recnd 11238 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβπ¦)) β β) |
70 | 17 | rpcnd 13014 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π
β β) |
71 | 17 | rpne0d 13017 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π
β 0) |
72 | 64, 69, 70, 71 | divassd 12021 |
. . . . 5
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (((π
/ (πΏβπ¦)) Β· (πβ(πΉβπ¦))) / π
) = ((π
/ (πΏβπ¦)) Β· ((πβ(πΉβπ¦)) / π
))) |
73 | 26 | rpcnd 13014 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΏβπ¦) β β) |
74 | 26 | rpne0d 13017 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΏβπ¦) β 0) |
75 | 69, 70, 73, 71, 74 | dmdcand 12015 |
. . . . 5
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((π
/ (πΏβπ¦)) Β· ((πβ(πΉβπ¦)) / π
)) = ((πβ(πΉβπ¦)) / (πΏβπ¦))) |
76 | 63, 72, 75 | 3eqtrd 2776 |
. . . 4
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
) = ((πβ(πΉβπ¦)) / (πΏβπ¦))) |
77 | | eqid 2732 |
. . . . . . . 8
β’
(normβπΊ) =
(normβπΊ) |
78 | 2, 3, 30, 5, 6, 77 | nmvs 24184 |
. . . . . . 7
β’ ((π β NrmMod β§ (π
/ (πΏβπ¦)) β πΎ β§ π¦ β π) β (πΏβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = (((normβπΊ)β(π
/ (πΏβπ¦))) Β· (πΏβπ¦))) |
79 | 19, 29, 22, 78 | syl3anc 1371 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΏβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = (((normβπΊ)β(π
/ (πΏβπ¦))) Β· (πΏβπ¦))) |
80 | 59 | oveq1d 7420 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (((normβπΊ)β(π
/ (πΏβπ¦))) Β· (πΏβπ¦)) = ((π
/ (πΏβπ¦)) Β· (πΏβπ¦))) |
81 | 70, 73, 74 | divcan1d 11987 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((π
/ (πΏβπ¦)) Β· (πΏβπ¦)) = π
) |
82 | 79, 80, 81 | 3eqtrd 2776 |
. . . . 5
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πΏβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = π
) |
83 | | fveqeq2 6897 |
. . . . . . 7
β’ (π₯ = ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β ((πΏβπ₯) = π
β (πΏβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = π
)) |
84 | | 2fveq3 6893 |
. . . . . . . . 9
β’ (π₯ = ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β (πβ(πΉβπ₯)) = (πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)))) |
85 | 84 | oveq1d 7420 |
. . . . . . . 8
β’ (π₯ = ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β ((πβ(πΉβπ₯)) / π
) = ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
)) |
86 | 85 | breq1d 5157 |
. . . . . . 7
β’ (π₯ = ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β (((πβ(πΉβπ₯)) / π
) β€ π΄ β ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
) β€ π΄)) |
87 | 83, 86 | imbi12d 344 |
. . . . . 6
β’ (π₯ = ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β (((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄) β ((πΏβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = π
β ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
) β€ π΄))) |
88 | | simpllr 774 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) |
89 | 2, 5, 30, 6 | clmvscl 24595 |
. . . . . . 7
β’ ((π β βMod β§ (π
/ (πΏβπ¦)) β πΎ β§ π¦ β π) β ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β π) |
90 | 54, 29, 22, 89 | syl3anc 1371 |
. . . . . 6
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((π
/ (πΏβπ¦))( Β·π
βπ)π¦) β π) |
91 | 87, 88, 90 | rspcdva 3613 |
. . . . 5
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((πΏβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦)) = π
β ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
) β€ π΄)) |
92 | 82, 91 | mpd 15 |
. . . 4
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((πβ(πΉβ((π
/ (πΏβπ¦))( Β·π
βπ)π¦))) / π
) β€ π΄) |
93 | 76, 92 | eqbrtrrd 5171 |
. . 3
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β ((πβ(πΉβπ¦)) / (πΏβπ¦)) β€ π΄) |
94 | | simplr 767 |
. . . 4
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β π΄ β β) |
95 | 68, 94, 26 | ledivmul2d 13066 |
. . 3
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (((πβ(πΉβπ¦)) / (πΏβπ¦)) β€ π΄ β (πβ(πΉβπ¦)) β€ (π΄ Β· (πΏβπ¦)))) |
96 | 93, 95 | mpbid 231 |
. 2
β’ ((((π β§ βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄)) β§ π΄ β β) β§ (π¦ β π β§ π¦ β (0gβπ))) β (πβ(πΉβπ¦)) β€ (π΄ Β· (πΏβπ¦))) |
97 | 11 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π) β π
β
β+) |
98 | 97 | rpred 13012 |
. . . 4
β’ ((π β§ π₯ β π) β π
β β) |
99 | 98 | leidd 11776 |
. . 3
β’ ((π β§ π₯ β π) β π
β€ π
) |
100 | | breq1 5150 |
. . 3
β’ ((πΏβπ₯) = π
β ((πΏβπ₯) β€ π
β π
β€ π
)) |
101 | 99, 100 | syl5ibrcom 246 |
. 2
β’ ((π β§ π₯ β π) β ((πΏβπ₯) = π
β (πΏβπ₯) β€ π
)) |
102 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 13, 96, 101 | nmoleub2lem 24621 |
1
β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π ((πΏβπ₯) = π
β ((πβ(πΉβπ₯)) / π
) β€ π΄))) |