Step | Hyp | Ref
| Expression |
1 | | nrginvrcn.t |
. . 3
β’ π = (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) |
2 | | 1rp 12927 |
. . . . 5
β’ 1 β
β+ |
3 | | nrginvrcn.r |
. . . . . . . 8
β’ (π β π
β NrmRing) |
4 | | nrgngp 24049 |
. . . . . . . 8
β’ (π
β NrmRing β π
β NrmGrp) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π β π
β NrmGrp) |
6 | | nrginvrcn.x |
. . . . . . . . 9
β’ π = (Baseβπ
) |
7 | | nrginvrcn.u |
. . . . . . . . 9
β’ π = (Unitβπ
) |
8 | 6, 7 | unitss 20097 |
. . . . . . . 8
β’ π β π |
9 | | nrginvrcn.a |
. . . . . . . 8
β’ (π β π΄ β π) |
10 | 8, 9 | sselid 3946 |
. . . . . . 7
β’ (π β π΄ β π) |
11 | | nrginvrcn.z |
. . . . . . . 8
β’ (π β π
β NzRing) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
13 | 7, 12 | nzrunit 20205 |
. . . . . . . 8
β’ ((π
β NzRing β§ π΄ β π) β π΄ β (0gβπ
)) |
14 | 11, 9, 13 | syl2anc 585 |
. . . . . . 7
β’ (π β π΄ β (0gβπ
)) |
15 | | nrginvrcn.n |
. . . . . . . 8
β’ π = (normβπ
) |
16 | 6, 15, 12 | nmrpcl 23999 |
. . . . . . 7
β’ ((π
β NrmGrp β§ π΄ β π β§ π΄ β (0gβπ
)) β (πβπ΄) β
β+) |
17 | 5, 10, 14, 16 | syl3anc 1372 |
. . . . . 6
β’ (π β (πβπ΄) β
β+) |
18 | | nrginvrcn.b |
. . . . . 6
β’ (π β π΅ β
β+) |
19 | 17, 18 | rpmulcld 12981 |
. . . . 5
β’ (π β ((πβπ΄) Β· π΅) β
β+) |
20 | | ifcl 4535 |
. . . . 5
β’ ((1
β β+ β§ ((πβπ΄) Β· π΅) β β+) β if(1
β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β
β+) |
21 | 2, 19, 20 | sylancr 588 |
. . . 4
β’ (π β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β
β+) |
22 | 17 | rphalfcld 12977 |
. . . 4
β’ (π β ((πβπ΄) / 2) β
β+) |
23 | 21, 22 | rpmulcld 12981 |
. . 3
β’ (π β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β
β+) |
24 | 1, 23 | eqeltrid 2838 |
. 2
β’ (π β π β
β+) |
25 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π
β NrmGrp) |
26 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π΄ β π) |
27 | 6, 7 | unitcl 20096 |
. . . . . . . . . . . 12
β’ (π΄ β π β π΄ β π) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π΄ β π) |
29 | 6, 15 | nmcl 23995 |
. . . . . . . . . . 11
β’ ((π
β NrmGrp β§ π΄ β π) β (πβπ΄) β β) |
30 | 25, 28, 29 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ΄) β β) |
31 | 30 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ΄) β β) |
32 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π¦ β π) |
33 | 8, 32 | sselid 3946 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π¦ β π) |
34 | 6, 15 | nmcl 23995 |
. . . . . . . . . . 11
β’ ((π
β NrmGrp β§ π¦ β π) β (πβπ¦) β β) |
35 | 25, 33, 34 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ¦) β β) |
36 | 35 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ¦) β β) |
37 | | ngpgrp 23978 |
. . . . . . . . . . . . 13
β’ (π
β NrmGrp β π
β Grp) |
38 | 25, 37 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π
β Grp) |
39 | | nrgring 24050 |
. . . . . . . . . . . . . . 15
β’ (π
β NrmRing β π
β Ring) |
40 | 3, 39 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π
β Ring) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π
β Ring) |
42 | | nrginvrcn.i |
. . . . . . . . . . . . . 14
β’ πΌ = (invrβπ
) |
43 | 7, 42, 6 | ringinvcl 20113 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π΄ β π) β (πΌβπ΄) β π) |
44 | 41, 26, 43 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πΌβπ΄) β π) |
45 | 7, 42, 6 | ringinvcl 20113 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β π) β (πΌβπ¦) β π) |
46 | 41, 32, 45 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πΌβπ¦) β π) |
47 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(-gβπ
) = (-gβπ
) |
48 | 6, 47 | grpsubcl 18835 |
. . . . . . . . . . . 12
β’ ((π
β Grp β§ (πΌβπ΄) β π β§ (πΌβπ¦) β π) β ((πΌβπ΄)(-gβπ
)(πΌβπ¦)) β π) |
49 | 38, 44, 46, 48 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πΌβπ΄)(-gβπ
)(πΌβπ¦)) β π) |
50 | 6, 15 | nmcl 23995 |
. . . . . . . . . . 11
β’ ((π
β NrmGrp β§ ((πΌβπ΄)(-gβπ
)(πΌβπ¦)) β π) β (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦))) β β) |
51 | 25, 49, 50 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦))) β β) |
52 | 51 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦))) β β) |
53 | 31, 36, 52 | mul32d 11373 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· (πβπ¦)) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = (((πβπ΄) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) Β· (πβπ¦))) |
54 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π
β NrmRing) |
55 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(.rβπ
) = (.rβπ
) |
56 | 6, 15, 55 | nmmul 24051 |
. . . . . . . . . . 11
β’ ((π
β NrmRing β§ π΄ β π β§ ((πΌβπ΄)(-gβπ
)(πΌβπ¦)) β π) β (πβ(π΄(.rβπ
)((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = ((πβπ΄) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦))))) |
57 | 54, 28, 49, 56 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ(π΄(.rβπ
)((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = ((πβπ΄) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦))))) |
58 | 6, 55, 47, 41, 28, 44, 46 | ringsubdi 20031 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄(.rβπ
)((πΌβπ΄)(-gβπ
)(πΌβπ¦))) = ((π΄(.rβπ
)(πΌβπ΄))(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) |
59 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(1rβπ
) = (1rβπ
) |
60 | 7, 42, 55, 59 | unitrinv 20115 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π΄ β π) β (π΄(.rβπ
)(πΌβπ΄)) = (1rβπ
)) |
61 | 41, 26, 60 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄(.rβπ
)(πΌβπ΄)) = (1rβπ
)) |
62 | 61 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((π΄(.rβπ
)(πΌβπ΄))(-gβπ
)(π΄(.rβπ
)(πΌβπ¦))) = ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) |
63 | 58, 62 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄(.rβπ
)((πΌβπ΄)(-gβπ
)(πΌβπ¦))) = ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) |
64 | 63 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ(π΄(.rβπ
)((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = (πβ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦))))) |
65 | 57, 64 | eqtr3d 2775 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = (πβ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦))))) |
66 | 65 | oveq1d 7376 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) Β· (πβπ¦)) = ((πβ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) Β· (πβπ¦))) |
67 | 6, 59 | ringidcl 19997 |
. . . . . . . . . . . 12
β’ (π
β Ring β
(1rβπ
)
β π) |
68 | 41, 67 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (1rβπ
) β π) |
69 | 6, 55 | ringcl 19989 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π΄ β π β§ (πΌβπ¦) β π) β (π΄(.rβπ
)(πΌβπ¦)) β π) |
70 | 41, 28, 46, 69 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄(.rβπ
)(πΌβπ¦)) β π) |
71 | 6, 47 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((π
β Grp β§
(1rβπ
)
β π β§ (π΄(.rβπ
)(πΌβπ¦)) β π) β ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦))) β π) |
72 | 38, 68, 70, 71 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦))) β π) |
73 | 6, 15, 55 | nmmul 24051 |
. . . . . . . . . 10
β’ ((π
β NrmRing β§
((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦))) β π β§ π¦ β π) β (πβ(((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))(.rβπ
)π¦)) = ((πβ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) Β· (πβπ¦))) |
74 | 54, 72, 33, 73 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ(((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))(.rβπ
)π¦)) = ((πβ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) Β· (πβπ¦))) |
75 | 6, 55, 47, 41, 68, 70, 33 | ringsubdir 20032 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))(.rβπ
)π¦) = (((1rβπ
)(.rβπ
)π¦)(-gβπ
)((π΄(.rβπ
)(πΌβπ¦))(.rβπ
)π¦))) |
76 | 6, 55, 59 | ringlidm 20000 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π¦ β π) β ((1rβπ
)(.rβπ
)π¦) = π¦) |
77 | 41, 33, 76 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((1rβπ
)(.rβπ
)π¦) = π¦) |
78 | 6, 55 | ringass 19992 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ (π΄ β π β§ (πΌβπ¦) β π β§ π¦ β π)) β ((π΄(.rβπ
)(πΌβπ¦))(.rβπ
)π¦) = (π΄(.rβπ
)((πΌβπ¦)(.rβπ
)π¦))) |
79 | 41, 28, 46, 33, 78 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((π΄(.rβπ
)(πΌβπ¦))(.rβπ
)π¦) = (π΄(.rβπ
)((πΌβπ¦)(.rβπ
)π¦))) |
80 | 7, 42, 55, 59 | unitlinv 20114 |
. . . . . . . . . . . . . . 15
β’ ((π
β Ring β§ π¦ β π) β ((πΌβπ¦)(.rβπ
)π¦) = (1rβπ
)) |
81 | 41, 32, 80 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πΌβπ¦)(.rβπ
)π¦) = (1rβπ
)) |
82 | 81 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄(.rβπ
)((πΌβπ¦)(.rβπ
)π¦)) = (π΄(.rβπ
)(1rβπ
))) |
83 | 6, 55, 59 | ringridm 20001 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π΄ β π) β (π΄(.rβπ
)(1rβπ
)) = π΄) |
84 | 41, 28, 83 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄(.rβπ
)(1rβπ
)) = π΄) |
85 | 79, 82, 84 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((π΄(.rβπ
)(πΌβπ¦))(.rβπ
)π¦) = π΄) |
86 | 77, 85 | oveq12d 7379 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((1rβπ
)(.rβπ
)π¦)(-gβπ
)((π΄(.rβπ
)(πΌβπ¦))(.rβπ
)π¦)) = (π¦(-gβπ
)π΄)) |
87 | 75, 86 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))(.rβπ
)π¦) = (π¦(-gβπ
)π΄)) |
88 | 87 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ(((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))(.rβπ
)π¦)) = (πβ(π¦(-gβπ
)π΄))) |
89 | 74, 88 | eqtr3d 2775 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβ((1rβπ
)(-gβπ
)(π΄(.rβπ
)(πΌβπ¦)))) Β· (πβπ¦)) = (πβ(π¦(-gβπ
)π΄))) |
90 | 53, 66, 89 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· (πβπ¦)) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = (πβ(π¦(-gβπ
)π΄))) |
91 | 6, 47 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((π
β Grp β§ π¦ β π β§ π΄ β π) β (π¦(-gβπ
)π΄) β π) |
92 | 38, 33, 28, 91 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π¦(-gβπ
)π΄) β π) |
93 | 6, 15 | nmcl 23995 |
. . . . . . . . . 10
β’ ((π
β NrmGrp β§ (π¦(-gβπ
)π΄) β π) β (πβ(π¦(-gβπ
)π΄)) β β) |
94 | 25, 92, 93 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ(π¦(-gβπ
)π΄)) β β) |
95 | 94 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβ(π¦(-gβπ
)π΄)) β β) |
96 | 17 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ΄) β
β+) |
97 | 11 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π
β NzRing) |
98 | 7, 12 | nzrunit 20205 |
. . . . . . . . . . . . 13
β’ ((π
β NzRing β§ π¦ β π) β π¦ β (0gβπ
)) |
99 | 97, 32, 98 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π¦ β (0gβπ
)) |
100 | 6, 15, 12 | nmrpcl 23999 |
. . . . . . . . . . . 12
β’ ((π
β NrmGrp β§ π¦ β π β§ π¦ β (0gβπ
)) β (πβπ¦) β
β+) |
101 | 25, 33, 99, 100 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ¦) β
β+) |
102 | 96, 101 | rpmulcld 12981 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· (πβπ¦)) β
β+) |
103 | 102 | rpred 12965 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· (πβπ¦)) β β) |
104 | 103 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· (πβπ¦)) β β) |
105 | 102 | rpne0d 12970 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· (πβπ¦)) β 0) |
106 | 95, 104, 52, 105 | divmuld 11961 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβ(π¦(-gβπ
)π΄)) / ((πβπ΄) Β· (πβπ¦))) = (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦))) β (((πβπ΄) Β· (πβπ¦)) Β· (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) = (πβ(π¦(-gβπ
)π΄)))) |
107 | 90, 106 | mpbird 257 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβ(π¦(-gβπ
)π΄)) / ((πβπ΄) Β· (πβπ¦))) = (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) |
108 | | nrginvrcn.d |
. . . . . . . . 9
β’ π· = (distβπ
) |
109 | 15, 6, 47, 108 | ngpdsr 23984 |
. . . . . . . 8
β’ ((π
β NrmGrp β§ π΄ β π β§ π¦ β π) β (π΄π·π¦) = (πβ(π¦(-gβπ
)π΄))) |
110 | 25, 28, 33, 109 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄π·π¦) = (πβ(π¦(-gβπ
)π΄))) |
111 | 110 | oveq1d 7376 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((π΄π·π¦) / ((πβπ΄) Β· (πβπ¦))) = ((πβ(π¦(-gβπ
)π΄)) / ((πβπ΄) Β· (πβπ¦)))) |
112 | 15, 6, 47, 108 | ngpds 23983 |
. . . . . . 7
β’ ((π
β NrmGrp β§ (πΌβπ΄) β π β§ (πΌβπ¦) β π) β ((πΌβπ΄)π·(πΌβπ¦)) = (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) |
113 | 25, 44, 46, 112 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πΌβπ΄)π·(πΌβπ¦)) = (πβ((πΌβπ΄)(-gβπ
)(πΌβπ¦)))) |
114 | 107, 111,
113 | 3eqtr4rd 2784 |
. . . . 5
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πΌβπ΄)π·(πΌβπ¦)) = ((π΄π·π¦) / ((πβπ΄) Β· (πβπ¦)))) |
115 | 110, 94 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄π·π¦) β β) |
116 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π β
β+) |
117 | 116 | rpred 12965 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π β β) |
118 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π΅ β
β+) |
119 | 118 | rpred 12965 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π΅ β β) |
120 | 103, 119 | remulcld 11193 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· (πβπ¦)) Β· π΅) β β) |
121 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄π·π¦) < π) |
122 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· π΅) β
β+) |
123 | 96 | rphalfcld 12977 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) / 2) β
β+) |
124 | 122, 123 | rpmulcld 12981 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2)) β
β+) |
125 | 124 | rpred 12965 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2)) β β) |
126 | | 1re 11163 |
. . . . . . . . . . 11
β’ 1 β
β |
127 | 122 | rpred 12965 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) Β· π΅) β β) |
128 | | min2 13118 |
. . . . . . . . . . 11
β’ ((1
β β β§ ((πβπ΄) Β· π΅) β β) β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β€ ((πβπ΄) Β· π΅)) |
129 | 126, 127,
128 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β€ ((πβπ΄) Β· π΅)) |
130 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β
β+) |
131 | 130 | rpred 12965 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β β) |
132 | 131, 127,
123 | lemul1d 13008 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β€ ((πβπ΄) Β· π΅) β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β€ (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2)))) |
133 | 129, 132 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β€ (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2))) |
134 | 1, 133 | eqbrtrid 5144 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π β€ (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2))) |
135 | 123 | rpred 12965 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) / 2) β β) |
136 | 31 | 2halvesd 12407 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) / 2) + ((πβπ΄) / 2)) = (πβπ΄)) |
137 | 30, 35 | resubcld 11591 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) β (πβπ¦)) β β) |
138 | 6, 15, 47 | nm2dif 24004 |
. . . . . . . . . . . . . . . 16
β’ ((π
β NrmGrp β§ π΄ β π β§ π¦ β π) β ((πβπ΄) β (πβπ¦)) β€ (πβ(π΄(-gβπ
)π¦))) |
139 | 25, 28, 33, 138 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) β (πβπ¦)) β€ (πβ(π΄(-gβπ
)π¦))) |
140 | 15, 6, 47, 108 | ngpds 23983 |
. . . . . . . . . . . . . . . 16
β’ ((π
β NrmGrp β§ π΄ β π β§ π¦ β π) β (π΄π·π¦) = (πβ(π΄(-gβπ
)π¦))) |
141 | 25, 28, 33, 140 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄π·π¦) = (πβ(π΄(-gβπ
)π¦))) |
142 | 139, 141 | breqtrrd 5137 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) β (πβπ¦)) β€ (π΄π·π¦)) |
143 | | min1 13117 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1
β β β§ ((πβπ΄) Β· π΅) β β) β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β€ 1) |
144 | 126, 127,
143 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β€ 1) |
145 | | 1red 11164 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β 1 β β) |
146 | 131, 145,
123 | lemul1d 13008 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) β€ 1 β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β€ (1 Β· ((πβπ΄) / 2)))) |
147 | 144, 146 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β€ (1 Β· ((πβπ΄) / 2))) |
148 | 1, 147 | eqbrtrid 5144 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π β€ (1 Β· ((πβπ΄) / 2))) |
149 | 135 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) / 2) β β) |
150 | 149 | mulid2d 11181 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (1 Β· ((πβπ΄) / 2)) = ((πβπ΄) / 2)) |
151 | 148, 150 | breqtrd 5135 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π β€ ((πβπ΄) / 2)) |
152 | 115, 117,
135, 121, 151 | ltletrd 11323 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄π·π¦) < ((πβπ΄) / 2)) |
153 | 137, 115,
135, 142, 152 | lelttrd 11321 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) β (πβπ¦)) < ((πβπ΄) / 2)) |
154 | 30, 35, 135 | ltsubadd2d 11761 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) β (πβπ¦)) < ((πβπ΄) / 2) β (πβπ΄) < ((πβπ¦) + ((πβπ΄) / 2)))) |
155 | 153, 154 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (πβπ΄) < ((πβπ¦) + ((πβπ΄) / 2))) |
156 | 136, 155 | eqbrtrd 5131 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) / 2) + ((πβπ΄) / 2)) < ((πβπ¦) + ((πβπ΄) / 2))) |
157 | 135, 35, 135 | ltadd1d 11756 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) / 2) < (πβπ¦) β (((πβπ΄) / 2) + ((πβπ΄) / 2)) < ((πβπ¦) + ((πβπ΄) / 2)))) |
158 | 156, 157 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πβπ΄) / 2) < (πβπ¦)) |
159 | 135, 35, 122, 158 | ltmul2dd 13021 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2)) < (((πβπ΄) Β· π΅) Β· (πβπ¦))) |
160 | 119 | recnd 11191 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π΅ β β) |
161 | 31, 36, 160 | mul32d 11373 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· (πβπ¦)) Β· π΅) = (((πβπ΄) Β· π΅) Β· (πβπ¦))) |
162 | 159, 161 | breqtrrd 5137 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((πβπ΄) Β· π΅) Β· ((πβπ΄) / 2)) < (((πβπ΄) Β· (πβπ¦)) Β· π΅)) |
163 | 117, 125,
120, 134, 162 | lelttrd 11321 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β π < (((πβπ΄) Β· (πβπ¦)) Β· π΅)) |
164 | 115, 117,
120, 121, 163 | lttrd 11324 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (π΄π·π¦) < (((πβπ΄) Β· (πβπ¦)) Β· π΅)) |
165 | 115, 119,
102 | ltdivmuld 13016 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β (((π΄π·π¦) / ((πβπ΄) Β· (πβπ¦))) < π΅ β (π΄π·π¦) < (((πβπ΄) Β· (πβπ¦)) Β· π΅))) |
166 | 164, 165 | mpbird 257 |
. . . . 5
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((π΄π·π¦) / ((πβπ΄) Β· (πβπ¦))) < π΅) |
167 | 114, 166 | eqbrtrd 5131 |
. . . 4
β’ ((π β§ (π¦ β π β§ (π΄π·π¦) < π)) β ((πΌβπ΄)π·(πΌβπ¦)) < π΅) |
168 | 167 | expr 458 |
. . 3
β’ ((π β§ π¦ β π) β ((π΄π·π¦) < π β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) |
169 | 168 | ralrimiva 3140 |
. 2
β’ (π β βπ¦ β π ((π΄π·π¦) < π β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) |
170 | | breq2 5113 |
. . 3
β’ (π₯ = π β ((π΄π·π¦) < π₯ β (π΄π·π¦) < π)) |
171 | 170 | rspceaimv 3587 |
. 2
β’ ((π β β+
β§ βπ¦ β
π ((π΄π·π¦) < π β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) β βπ₯ β β+ βπ¦ β π ((π΄π·π¦) < π₯ β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) |
172 | 24, 169, 171 | syl2anc 585 |
1
β’ (π β βπ₯ β β+ βπ¦ β π ((π΄π·π¦) < π₯ β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) |