Step | Hyp | Ref
| Expression |
1 | | neg1z 12600 |
. . 3
β’ -1 β
β€ |
2 | | archirng.1 |
. . . . . . . . . 10
β’ (π β π β oGrp) |
3 | | ogrpgrp 32262 |
. . . . . . . . . 10
β’ (π β oGrp β π β Grp) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
β’ (π β π β Grp) |
5 | | 1zzd 12595 |
. . . . . . . . 9
β’ (π β 1 β
β€) |
6 | | archirng.3 |
. . . . . . . . 9
β’ (π β π β π΅) |
7 | | archirng.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
8 | | archirng.x |
. . . . . . . . . 10
β’ Β· =
(.gβπ) |
9 | | eqid 2732 |
. . . . . . . . . 10
β’
(invgβπ) = (invgβπ) |
10 | 7, 8, 9 | mulgneg 18974 |
. . . . . . . . 9
β’ ((π β Grp β§ 1 β
β€ β§ π β
π΅) β (-1 Β· π) =
((invgβπ)β(1 Β· π))) |
11 | 4, 5, 6, 10 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (-1 Β· π) = ((invgβπ)β(1 Β· π))) |
12 | 7, 8 | mulg1 18963 |
. . . . . . . . . 10
β’ (π β π΅ β (1 Β· π) = π) |
13 | 6, 12 | syl 17 |
. . . . . . . . 9
β’ (π β (1 Β· π) = π) |
14 | 13 | fveq2d 6895 |
. . . . . . . 8
β’ (π β
((invgβπ)β(1 Β· π)) = ((invgβπ)βπ)) |
15 | 11, 14 | eqtrd 2772 |
. . . . . . 7
β’ (π β (-1 Β· π) = ((invgβπ)βπ)) |
16 | | archirng.5 |
. . . . . . . 8
β’ (π β 0 < π) |
17 | | archirng.i |
. . . . . . . . . 10
β’ < =
(ltβπ) |
18 | | archirng.0 |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
19 | 7, 17, 9, 18 | ogrpinv0lt 32281 |
. . . . . . . . 9
β’ ((π β oGrp β§ π β π΅) β ( 0 < π β ((invgβπ)βπ) < 0 )) |
20 | 19 | biimpa 477 |
. . . . . . . 8
β’ (((π β oGrp β§ π β π΅) β§ 0 < π) β ((invgβπ)βπ) < 0 ) |
21 | 2, 6, 16, 20 | syl21anc 836 |
. . . . . . 7
β’ (π β
((invgβπ)βπ) < 0 ) |
22 | 15, 21 | eqbrtrd 5170 |
. . . . . 6
β’ (π β (-1 Β· π) < 0 ) |
23 | 22 | adantr 481 |
. . . . 5
β’ ((π β§ π = 0 ) β (-1 Β· π) < 0 ) |
24 | | simpr 485 |
. . . . 5
β’ ((π β§ π = 0 ) β π = 0 ) |
25 | 23, 24 | breqtrrd 5176 |
. . . 4
β’ ((π β§ π = 0 ) β (-1 Β· π) < π) |
26 | | isogrp 32261 |
. . . . . . . . . 10
β’ (π β oGrp β (π β Grp β§ π β oMnd)) |
27 | 26 | simprbi 497 |
. . . . . . . . 9
β’ (π β oGrp β π β oMnd) |
28 | | omndtos 32264 |
. . . . . . . . 9
β’ (π β oMnd β π β Toset) |
29 | 2, 27, 28 | 3syl 18 |
. . . . . . . 8
β’ (π β π β Toset) |
30 | | tospos 18375 |
. . . . . . . 8
β’ (π β Toset β π β Poset) |
31 | 29, 30 | syl 17 |
. . . . . . 7
β’ (π β π β Poset) |
32 | 7, 18 | grpidcl 18852 |
. . . . . . . 8
β’ (π β Grp β 0 β π΅) |
33 | 2, 3, 32 | 3syl 18 |
. . . . . . 7
β’ (π β 0 β π΅) |
34 | | archirng.l |
. . . . . . . 8
β’ β€ =
(leβπ) |
35 | 7, 34 | posref 18273 |
. . . . . . 7
β’ ((π β Poset β§ 0 β π΅) β 0 β€ 0 ) |
36 | 31, 33, 35 | syl2anc 584 |
. . . . . 6
β’ (π β 0 β€ 0 ) |
37 | 36 | adantr 481 |
. . . . 5
β’ ((π β§ π = 0 ) β 0 β€ 0
) |
38 | | 1m1e0 12286 |
. . . . . . . . . 10
β’ (1
β 1) = 0 |
39 | 38 | negeqi 11455 |
. . . . . . . . 9
β’ -(1
β 1) = -0 |
40 | | ax-1cn 11170 |
. . . . . . . . . 10
β’ 1 β
β |
41 | 40, 40 | negsubdii 11547 |
. . . . . . . . 9
β’ -(1
β 1) = (-1 + 1) |
42 | | neg0 11508 |
. . . . . . . . 9
β’ -0 =
0 |
43 | 39, 41, 42 | 3eqtr3i 2768 |
. . . . . . . 8
β’ (-1 + 1)
= 0 |
44 | 43 | oveq1i 7421 |
. . . . . . 7
β’ ((-1 + 1)
Β·
π) = (0 Β· π) |
45 | 7, 18, 8 | mulg0 18959 |
. . . . . . . 8
β’ (π β π΅ β (0 Β· π) = 0 ) |
46 | 6, 45 | syl 17 |
. . . . . . 7
β’ (π β (0 Β· π) = 0 ) |
47 | 44, 46 | eqtrid 2784 |
. . . . . 6
β’ (π β ((-1 + 1) Β· π) = 0 ) |
48 | 47 | adantr 481 |
. . . . 5
β’ ((π β§ π = 0 ) β ((-1 + 1) Β· π) = 0 ) |
49 | 37, 24, 48 | 3brtr4d 5180 |
. . . 4
β’ ((π β§ π = 0 ) β π β€ ((-1 + 1) Β· π)) |
50 | 25, 49 | jca 512 |
. . 3
β’ ((π β§ π = 0 ) β ((-1 Β· π) < π β§ π β€ ((-1 + 1) Β· π))) |
51 | | oveq1 7418 |
. . . . . 6
β’ (π = -1 β (π Β· π) = (-1 Β· π)) |
52 | 51 | breq1d 5158 |
. . . . 5
β’ (π = -1 β ((π Β· π) < π β (-1 Β· π) < π)) |
53 | | oveq1 7418 |
. . . . . . 7
β’ (π = -1 β (π + 1) = (-1 + 1)) |
54 | 53 | oveq1d 7426 |
. . . . . 6
β’ (π = -1 β ((π + 1) Β· π) = ((-1 + 1) Β· π)) |
55 | 54 | breq2d 5160 |
. . . . 5
β’ (π = -1 β (π β€ ((π + 1) Β· π) β π β€ ((-1 + 1) Β· π))) |
56 | 52, 55 | anbi12d 631 |
. . . 4
β’ (π = -1 β (((π Β· π) < π β§ π β€ ((π + 1) Β· π)) β ((-1 Β· π) < π β§ π β€ ((-1 + 1) Β· π)))) |
57 | 56 | rspcev 3612 |
. . 3
β’ ((-1
β β€ β§ ((-1 Β· π) < π β§ π β€ ((-1 + 1) Β· π))) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
58 | 1, 50, 57 | sylancr 587 |
. 2
β’ ((π β§ π = 0 ) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
59 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β π β
β0) |
60 | 59 | nn0zd 12586 |
. . . . . . . 8
β’ (((π β§ π < 0 ) β§ π β β0) β π β
β€) |
61 | 60 | ad2antrr 724 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β π β β€) |
62 | 61 | znegcld 12670 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β -π β β€) |
63 | | 2z 12596 |
. . . . . . 7
β’ 2 β
β€ |
64 | 63 | a1i 11 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β 2 β β€) |
65 | 62, 64 | zsubcld 12673 |
. . . . 5
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β (-π β 2) β β€) |
66 | | nn0cn 12484 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β) |
67 | 66 | adantl 482 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β π β
β) |
68 | | 2cnd 12292 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β 2 β
β) |
69 | 67, 68 | negdi2d 11587 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β -(π + 2) = (-π β 2)) |
70 | 69 | oveq1d 7426 |
. . . . . . . 8
β’ (((π β§ π < 0 ) β§ π β β0) β (-(π + 2) Β· π) = ((-π β 2) Β· π)) |
71 | 2 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β π β oGrp) |
72 | | archirngz.1 |
. . . . . . . . . . . 12
β’ (π β
(oppgβπ) β oGrp) |
73 | 72 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β
(oppgβπ) β oGrp) |
74 | 71, 73 | jca 512 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β (π β oGrp β§
(oppgβπ) β oGrp)) |
75 | 4 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β π β Grp) |
76 | 60 | peano2zd 12671 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (π + 1) β
β€) |
77 | 6 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β π β π΅) |
78 | 7, 8 | mulgcl 18973 |
. . . . . . . . . . 11
β’ ((π β Grp β§ (π + 1) β β€ β§ π β π΅) β ((π + 1) Β· π) β π΅) |
79 | 75, 76, 77, 78 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β ((π + 1) Β· π) β π΅) |
80 | 63 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β 2 β
β€) |
81 | 60, 80 | zaddcld 12672 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (π + 2) β
β€) |
82 | 7, 8 | mulgcl 18973 |
. . . . . . . . . . 11
β’ ((π β Grp β§ (π + 2) β β€ β§ π β π΅) β ((π + 2) Β· π) β π΅) |
83 | 75, 81, 77, 82 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β ((π + 2) Β· π) β π΅) |
84 | 75, 32 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β 0 β π΅) |
85 | 16 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β 0 < π) |
86 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(+gβπ) = (+gβπ) |
87 | 7, 17, 86 | ogrpaddlt 32276 |
. . . . . . . . . . . 12
β’ ((π β oGrp β§ ( 0 β π΅ β§ π β π΅ β§ ((π + 1) Β· π) β π΅) β§ 0 < π) β ( 0 (+gβπ)((π + 1) Β· π)) < (π(+gβπ)((π + 1) Β· π))) |
88 | 71, 84, 77, 79, 85, 87 | syl131anc 1383 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β ( 0
(+gβπ)((π + 1) Β· π)) < (π(+gβπ)((π + 1) Β· π))) |
89 | 7, 86, 18 | grplid 18854 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ ((π + 1) Β· π) β π΅) β ( 0 (+gβπ)((π + 1) Β· π)) = ((π + 1) Β· π)) |
90 | 75, 79, 89 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β ( 0
(+gβπ)((π + 1) Β· π)) = ((π + 1) Β· π)) |
91 | | 1cnd 11211 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β 1 β β) |
92 | 66, 91, 91 | addassd 11238 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β ((π + 1) + 1) =
(π + (1 +
1))) |
93 | | 1p1e2 12339 |
. . . . . . . . . . . . . . . . 17
β’ (1 + 1) =
2 |
94 | 93 | oveq2i 7422 |
. . . . . . . . . . . . . . . 16
β’ (π + (1 + 1)) = (π + 2) |
95 | 92, 94 | eqtrdi 2788 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ((π + 1) + 1) =
(π + 2)) |
96 | 66, 91 | addcld 11235 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β) |
97 | 96, 91 | addcomd 11418 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ((π + 1) + 1) = (1 +
(π + 1))) |
98 | 95, 97 | eqtr3d 2774 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 2) = (1 +
(π + 1))) |
99 | 98 | oveq1d 7426 |
. . . . . . . . . . . . 13
β’ (π β β0
β ((π + 2) Β· π) = ((1 + (π + 1)) Β· π)) |
100 | 99 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β ((π + 2) Β· π) = ((1 + (π + 1)) Β· π)) |
101 | | 1zzd 12595 |
. . . . . . . . . . . . 13
β’ (((π β§ π < 0 ) β§ π β β0) β 1 β
β€) |
102 | 7, 8, 86 | mulgdir 18988 |
. . . . . . . . . . . . 13
β’ ((π β Grp β§ (1 β
β€ β§ (π + 1)
β β€ β§ π
β π΅)) β ((1 +
(π + 1)) Β· π) = ((1 Β· π)(+gβπ)((π + 1) Β· π))) |
103 | 75, 101, 76, 77, 102 | syl13anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β ((1 +
(π + 1)) Β· π) = ((1 Β· π)(+gβπ)((π + 1) Β· π))) |
104 | 77, 12 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π < 0 ) β§ π β β0) β (1 Β· π) = π) |
105 | 104 | oveq1d 7426 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β ((1 Β· π)(+gβπ)((π + 1) Β· π)) = (π(+gβπ)((π + 1) Β· π))) |
106 | 100, 103,
105 | 3eqtrrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (π(+gβπ)((π + 1) Β· π)) = ((π + 2) Β· π)) |
107 | 88, 90, 106 | 3brtr3d 5179 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β ((π + 1) Β· π) < ((π + 2) Β· π)) |
108 | 7, 17, 9 | ogrpinvlt 32282 |
. . . . . . . . . . 11
β’ (((π β oGrp β§
(oppgβπ) β oGrp) β§ ((π + 1) Β· π) β π΅ β§ ((π + 2) Β· π) β π΅) β (((π + 1) Β· π) < ((π + 2) Β· π) β ((invgβπ)β((π + 2) Β· π)) <
((invgβπ)β((π + 1) Β· π)))) |
109 | 108 | biimpa 477 |
. . . . . . . . . 10
β’ ((((π β oGrp β§
(oppgβπ) β oGrp) β§ ((π + 1) Β· π) β π΅ β§ ((π + 2) Β· π) β π΅) β§ ((π + 1) Β· π) < ((π + 2) Β· π)) β ((invgβπ)β((π + 2) Β· π)) <
((invgβπ)β((π + 1) Β· π))) |
110 | 74, 79, 83, 107, 109 | syl31anc 1373 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β
((invgβπ)β((π + 2) Β· π)) <
((invgβπ)β((π + 1) Β· π))) |
111 | 7, 8, 9 | mulgneg 18974 |
. . . . . . . . . 10
β’ ((π β Grp β§ (π + 2) β β€ β§ π β π΅) β (-(π + 2) Β· π) = ((invgβπ)β((π + 2) Β· π))) |
112 | 75, 81, 77, 111 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β (-(π + 2) Β· π) = ((invgβπ)β((π + 2) Β· π))) |
113 | 7, 8, 9 | mulgneg 18974 |
. . . . . . . . . 10
β’ ((π β Grp β§ (π + 1) β β€ β§ π β π΅) β (-(π + 1) Β· π) = ((invgβπ)β((π + 1) Β· π))) |
114 | 75, 76, 77, 113 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β (-(π + 1) Β· π) = ((invgβπ)β((π + 1) Β· π))) |
115 | 110, 112,
114 | 3brtr4d 5180 |
. . . . . . . 8
β’ (((π β§ π < 0 ) β§ π β β0) β (-(π + 2) Β· π) < (-(π + 1) Β· π)) |
116 | 70, 115 | eqbrtrrd 5172 |
. . . . . . 7
β’ (((π β§ π < 0 ) β§ π β β0) β ((-π β 2) Β· π) < (-(π + 1) Β· π)) |
117 | 116 | ad2antrr 724 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((-π β 2) Β· π) < (-(π + 1) Β· π)) |
118 | 114 | ad2antrr 724 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β (-(π + 1) Β· π) = ((invgβπ)β((π + 1) Β· π))) |
119 | 31 | ad4antr 730 |
. . . . . . . . 9
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β π β Poset) |
120 | | archirng.4 |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
121 | 7, 9 | grpinvcl 18874 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π β π΅) β ((invgβπ)βπ) β π΅) |
122 | 4, 120, 121 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β
((invgβπ)βπ) β π΅) |
123 | 122 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β
((invgβπ)βπ) β π΅) |
124 | 123 | ad2antrr 724 |
. . . . . . . . 9
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((invgβπ)βπ) β π΅) |
125 | 79 | ad2antrr 724 |
. . . . . . . . 9
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((π + 1) Β· π) β π΅) |
126 | | simplrr 776 |
. . . . . . . . 9
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((invgβπ)βπ) β€ ((π + 1) Β· π)) |
127 | | simpr 485 |
. . . . . . . . 9
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((π + 1) Β· π) β€
((invgβπ)βπ)) |
128 | 7, 34 | posasymb 18274 |
. . . . . . . . . 10
β’ ((π β Poset β§
((invgβπ)βπ) β π΅ β§ ((π + 1) Β· π) β π΅) β ((((invgβπ)βπ) β€ ((π + 1) Β· π) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((invgβπ)βπ) = ((π + 1) Β· π))) |
129 | 128 | biimpa 477 |
. . . . . . . . 9
β’ (((π β Poset β§
((invgβπ)βπ) β π΅ β§ ((π + 1) Β· π) β π΅) β§ (((invgβπ)βπ) β€ ((π + 1) Β· π) β§ ((π + 1) Β· π) β€
((invgβπ)βπ))) β ((invgβπ)βπ) = ((π + 1) Β· π)) |
130 | 119, 124,
125, 126, 127, 129 | syl32anc 1378 |
. . . . . . . 8
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((invgβπ)βπ) = ((π + 1) Β· π)) |
131 | 130 | fveq2d 6895 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((invgβπ)β((invgβπ)βπ)) = ((invgβπ)β((π + 1) Β· π))) |
132 | 7, 9 | grpinvinv 18892 |
. . . . . . . . 9
β’ ((π β Grp β§ π β π΅) β ((invgβπ)β((invgβπ)βπ)) = π) |
133 | 4, 120, 132 | syl2anc 584 |
. . . . . . . 8
β’ (π β
((invgβπ)β((invgβπ)βπ)) = π) |
134 | 133 | ad4antr 730 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((invgβπ)β((invgβπ)βπ)) = π) |
135 | 118, 131,
134 | 3eqtr2rd 2779 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β π = (-(π + 1) Β· π)) |
136 | 117, 135 | breqtrrd 5176 |
. . . . 5
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β ((-π β 2) Β· π) < π) |
137 | | 1cnd 11211 |
. . . . . . . . . . . . 13
β’ (((π β§ π < 0 ) β§ π β β0) β 1 β
β) |
138 | 67, 68, 137 | addsubassd 11593 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β ((π + 2) β 1) = (π + (2 β
1))) |
139 | | 2m1e1 12340 |
. . . . . . . . . . . . 13
β’ (2
β 1) = 1 |
140 | 139 | oveq2i 7422 |
. . . . . . . . . . . 12
β’ (π + (2 β 1)) = (π + 1) |
141 | 138, 140 | eqtr2di 2789 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (π + 1) = ((π + 2) β 1)) |
142 | 141 | negeqd 11456 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β -(π + 1) = -((π + 2) β 1)) |
143 | 67, 68 | addcld 11235 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (π + 2) β
β) |
144 | 143, 137 | negsubdid 11588 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β -((π + 2) β 1) = (-(π + 2) + 1)) |
145 | 69 | oveq1d 7426 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β (-(π + 2) + 1) = ((-π β 2) +
1)) |
146 | 142, 144,
145 | 3eqtrrd 2777 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β ((-π β 2) + 1) = -(π + 1)) |
147 | 146 | oveq1d 7426 |
. . . . . . . 8
β’ (((π β§ π < 0 ) β§ π β β0) β (((-π β 2) + 1) Β· π) = (-(π + 1) Β· π)) |
148 | 29 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β π β Toset) |
149 | 148, 30 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β π β Poset) |
150 | 60 | znegcld 12670 |
. . . . . . . . . . . 12
β’ (((π β§ π < 0 ) β§ π β β0) β -π β
β€) |
151 | 150, 80 | zsubcld 12673 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (-π β 2) β
β€) |
152 | 151 | peano2zd 12671 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β ((-π β 2) + 1) β
β€) |
153 | 7, 8 | mulgcl 18973 |
. . . . . . . . . 10
β’ ((π β Grp β§ ((-π β 2) + 1) β β€
β§ π β π΅) β (((-π β 2) + 1) Β· π) β π΅) |
154 | 75, 152, 77, 153 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β (((-π β 2) + 1) Β· π) β π΅) |
155 | 7, 34 | posref 18273 |
. . . . . . . . 9
β’ ((π β Poset β§ (((-π β 2) + 1) Β· π) β π΅) β (((-π β 2) + 1) Β· π) β€ (((-π β 2) + 1) Β· π)) |
156 | 149, 154,
155 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ π < 0 ) β§ π β β0) β (((-π β 2) + 1) Β· π) β€ (((-π β 2) + 1) Β· π)) |
157 | 147, 156 | eqbrtrrd 5172 |
. . . . . . 7
β’ (((π β§ π < 0 ) β§ π β β0) β (-(π + 1) Β· π) β€ (((-π β 2) + 1) Β· π)) |
158 | 157 | ad2antrr 724 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β (-(π + 1) Β· π) β€ (((-π β 2) + 1) Β· π)) |
159 | 135, 158 | eqbrtrd 5170 |
. . . . 5
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β π β€ (((-π β 2) + 1) Β· π)) |
160 | | oveq1 7418 |
. . . . . . . 8
β’ (π = (-π β 2) β (π Β· π) = ((-π β 2) Β· π)) |
161 | 160 | breq1d 5158 |
. . . . . . 7
β’ (π = (-π β 2) β ((π Β· π) < π β ((-π β 2) Β· π) < π)) |
162 | | oveq1 7418 |
. . . . . . . . 9
β’ (π = (-π β 2) β (π + 1) = ((-π β 2) + 1)) |
163 | 162 | oveq1d 7426 |
. . . . . . . 8
β’ (π = (-π β 2) β ((π + 1) Β· π) = (((-π β 2) + 1) Β· π)) |
164 | 163 | breq2d 5160 |
. . . . . . 7
β’ (π = (-π β 2) β (π β€ ((π + 1) Β· π) β π β€ (((-π β 2) + 1) Β· π))) |
165 | 161, 164 | anbi12d 631 |
. . . . . 6
β’ (π = (-π β 2) β (((π Β· π) < π β§ π β€ ((π + 1) Β· π)) β (((-π β 2) Β· π) < π β§ π β€ (((-π β 2) + 1) Β· π)))) |
166 | 165 | rspcev 3612 |
. . . . 5
β’ (((-π β 2) β β€ β§
(((-π β 2) Β· π) < π β§ π β€ (((-π β 2) + 1) Β· π))) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
167 | 65, 136, 159, 166 | syl12anc 835 |
. . . 4
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((π + 1) Β· π) β€
((invgβπ)βπ)) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
168 | 76 | ad2antrr 724 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β (π + 1) β β€) |
169 | 168 | znegcld 12670 |
. . . . 5
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β -(π + 1) β β€) |
170 | 2 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ (π β β0
β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π)) β§ ((invgβπ)βπ) < ((π + 1) Β· π))) β π β oGrp) |
171 | 72 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ (π β β0
β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π)) β§ ((invgβπ)βπ) < ((π + 1) Β· π))) β
(oppgβπ) β oGrp) |
172 | 170, 171 | jca 512 |
. . . . . . . 8
β’ (((π β§ π < 0 ) β§ (π β β0
β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π)) β§ ((invgβπ)βπ) < ((π + 1) Β· π))) β (π β oGrp β§
(oppgβπ) β oGrp)) |
173 | 172 | 3anassrs 1360 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β (π β oGrp β§
(oppgβπ) β oGrp)) |
174 | 123 | ad2antrr 724 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)βπ) β π΅) |
175 | 79 | ad2antrr 724 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((π + 1) Β· π) β π΅) |
176 | | simpr 485 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)βπ) < ((π + 1) Β· π)) |
177 | 7, 17, 9 | ogrpinvlt 32282 |
. . . . . . . 8
β’ (((π β oGrp β§
(oppgβπ) β oGrp) β§
((invgβπ)βπ) β π΅ β§ ((π + 1) Β· π) β π΅) β (((invgβπ)βπ) < ((π + 1) Β· π) β ((invgβπ)β((π + 1) Β· π)) <
((invgβπ)β((invgβπ)βπ)))) |
178 | 177 | biimpa 477 |
. . . . . . 7
β’ ((((π β oGrp β§
(oppgβπ) β oGrp) β§
((invgβπ)βπ) β π΅ β§ ((π + 1) Β· π) β π΅) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)β((π + 1) Β· π)) <
((invgβπ)β((invgβπ)βπ))) |
179 | 173, 174,
175, 176, 178 | syl31anc 1373 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)β((π + 1) Β· π)) <
((invgβπ)β((invgβπ)βπ))) |
180 | 114 | ad2antrr 724 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β (-(π + 1) Β· π) = ((invgβπ)β((π + 1) Β· π))) |
181 | 180 | eqcomd 2738 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)β((π + 1) Β· π)) = (-(π + 1) Β· π)) |
182 | 133 | ad4antr 730 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)β((invgβπ)βπ)) = π) |
183 | 179, 181,
182 | 3brtr3d 5179 |
. . . . 5
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β (-(π + 1) Β· π) < π) |
184 | | simp-4l 781 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β π) |
185 | 7, 8 | mulgcl 18973 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π β β€ β§ π β π΅) β (π Β· π) β π΅) |
186 | 75, 60, 77, 185 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (((π β§ π < 0 ) β§ π β β0) β (π Β· π) β π΅) |
187 | 7, 17, 9 | ogrpinvlt 32282 |
. . . . . . . . . . 11
β’ (((π β oGrp β§
(oppgβπ) β oGrp) β§ (π Β· π) β π΅ β§ ((invgβπ)βπ) β π΅) β ((π Β· π) <
((invgβπ)βπ) β ((invgβπ)β((invgβπ)βπ)) <
((invgβπ)β(π Β· π)))) |
188 | 74, 186, 123, 187 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β ((π Β· π) <
((invgβπ)βπ) β ((invgβπ)β((invgβπ)βπ)) <
((invgβπ)β(π Β· π)))) |
189 | 188 | biimpa 477 |
. . . . . . . . 9
β’ ((((π β§ π < 0 ) β§ π β β0) β§ (π Β· π) <
((invgβπ)βπ)) β ((invgβπ)β((invgβπ)βπ)) <
((invgβπ)β(π Β· π))) |
190 | 189 | adantrr 715 |
. . . . . . . 8
β’ ((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β ((invgβπ)β((invgβπ)βπ)) <
((invgβπ)β(π Β· π))) |
191 | 190 | adantr 481 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)β((invgβπ)βπ)) <
((invgβπ)β(π Β· π))) |
192 | | negdi 11519 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 1 β
β) β -(π + 1) =
(-π + -1)) |
193 | 66, 40, 192 | sylancl 586 |
. . . . . . . . . . . . . 14
β’ (π β β0
β -(π + 1) = (-π + -1)) |
194 | 193 | oveq1d 7426 |
. . . . . . . . . . . . 13
β’ (π β β0
β (-(π + 1) + 1) =
((-π + -1) +
1)) |
195 | 66 | negcld 11560 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β -π β
β) |
196 | 91 | negcld 11560 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β -1 β β) |
197 | 195, 196,
91 | addassd 11238 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ((-π + -1) + 1) =
(-π + (-1 +
1))) |
198 | 43 | oveq2i 7422 |
. . . . . . . . . . . . . . 15
β’ (-π + (-1 + 1)) = (-π + 0) |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (-π + (-1 + 1)) =
(-π + 0)) |
200 | 195 | addridd 11416 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (-π + 0) = -π) |
201 | 197, 199,
200 | 3eqtrd 2776 |
. . . . . . . . . . . . 13
β’ (π β β0
β ((-π + -1) + 1) =
-π) |
202 | 194, 201 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ (π β β0
β (-(π + 1) + 1) =
-π) |
203 | 202 | oveq1d 7426 |
. . . . . . . . . . 11
β’ (π β β0
β ((-(π + 1) + 1)
Β·
π) = (-π Β· π)) |
204 | 203 | adantl 482 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β ((-(π + 1) + 1) Β· π) = (-π Β· π)) |
205 | 7, 8, 9 | mulgneg 18974 |
. . . . . . . . . . 11
β’ ((π β Grp β§ π β β€ β§ π β π΅) β (-π Β· π) = ((invgβπ)β(π Β· π))) |
206 | 75, 60, 77, 205 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ π < 0 ) β§ π β β0) β (-π Β· π) = ((invgβπ)β(π Β· π))) |
207 | 204, 206 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π β§ π < 0 ) β§ π β β0) β ((-(π + 1) + 1) Β· π) = ((invgβπ)β(π Β· π))) |
208 | 207 | ad2antrr 724 |
. . . . . . . 8
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((-(π + 1) + 1) Β· π) = ((invgβπ)β(π Β· π))) |
209 | 208 | eqcomd 2738 |
. . . . . . 7
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β ((invgβπ)β(π Β· π)) = ((-(π + 1) + 1) Β· π)) |
210 | 191, 182,
209 | 3brtr3d 5179 |
. . . . . 6
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β π < ((-(π + 1) + 1) Β· π)) |
211 | | ovexd 7446 |
. . . . . . 7
β’ (π β ((-(π + 1) + 1) Β· π) β V) |
212 | 34, 17 | pltle 18288 |
. . . . . . 7
β’ ((π β oGrp β§ π β π΅ β§ ((-(π + 1) + 1) Β· π) β V) β (π < ((-(π + 1) + 1) Β· π) β π β€ ((-(π + 1) + 1) Β· π))) |
213 | 2, 120, 211, 212 | syl3anc 1371 |
. . . . . 6
β’ (π β (π < ((-(π + 1) + 1) Β· π) β π β€ ((-(π + 1) + 1) Β· π))) |
214 | 184, 210,
213 | sylc 65 |
. . . . 5
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β π β€ ((-(π + 1) + 1) Β· π)) |
215 | | oveq1 7418 |
. . . . . . . 8
β’ (π = -(π + 1) β (π Β· π) = (-(π + 1) Β· π)) |
216 | 215 | breq1d 5158 |
. . . . . . 7
β’ (π = -(π + 1) β ((π Β· π) < π β (-(π + 1) Β· π) < π)) |
217 | | oveq1 7418 |
. . . . . . . . 9
β’ (π = -(π + 1) β (π + 1) = (-(π + 1) + 1)) |
218 | 217 | oveq1d 7426 |
. . . . . . . 8
β’ (π = -(π + 1) β ((π + 1) Β· π) = ((-(π + 1) + 1) Β· π)) |
219 | 218 | breq2d 5160 |
. . . . . . 7
β’ (π = -(π + 1) β (π β€ ((π + 1) Β· π) β π β€ ((-(π + 1) + 1) Β· π))) |
220 | 216, 219 | anbi12d 631 |
. . . . . 6
β’ (π = -(π + 1) β (((π Β· π) < π β§ π β€ ((π + 1) Β· π)) β ((-(π + 1) Β· π) < π β§ π β€ ((-(π + 1) + 1) Β· π)))) |
221 | 220 | rspcev 3612 |
. . . . 5
β’ ((-(π + 1) β β€ β§
((-(π + 1) Β· π) < π β§ π β€ ((-(π + 1) + 1) Β· π))) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
222 | 169, 183,
214, 221 | syl12anc 835 |
. . . 4
β’
(((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β§ ((invgβπ)βπ) < ((π + 1) Β· π)) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
223 | 7, 34, 17 | tlt2 32177 |
. . . . . 6
β’ ((π β Toset β§ ((π + 1) Β· π) β π΅ β§ ((invgβπ)βπ) β π΅) β (((π + 1) Β· π) β€
((invgβπ)βπ) β¨ ((invgβπ)βπ) < ((π + 1) Β· π))) |
224 | 148, 79, 123, 223 | syl3anc 1371 |
. . . . 5
β’ (((π β§ π < 0 ) β§ π β β0) β (((π + 1) Β· π) β€
((invgβπ)βπ) β¨ ((invgβπ)βπ) < ((π + 1) Β· π))) |
225 | 224 | adantr 481 |
. . . 4
β’ ((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β (((π + 1) Β· π) β€
((invgβπ)βπ) β¨ ((invgβπ)βπ) < ((π + 1) Β· π))) |
226 | 167, 222,
225 | mpjaodan 957 |
. . 3
β’ ((((π β§ π < 0 ) β§ π β β0) β§ ((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
227 | 2 | adantr 481 |
. . . 4
β’ ((π β§ π < 0 ) β π β oGrp) |
228 | | archirng.2 |
. . . . 5
β’ (π β π β Archi) |
229 | 228 | adantr 481 |
. . . 4
β’ ((π β§ π < 0 ) β π β Archi) |
230 | 6 | adantr 481 |
. . . 4
β’ ((π β§ π < 0 ) β π β π΅) |
231 | 122 | adantr 481 |
. . . 4
β’ ((π β§ π < 0 ) β
((invgβπ)βπ) β π΅) |
232 | 16 | adantr 481 |
. . . 4
β’ ((π β§ π < 0 ) β 0 < π) |
233 | 133 | breq1d 5158 |
. . . . . 6
β’ (π β
(((invgβπ)β((invgβπ)βπ)) < 0 β π < 0 )) |
234 | 233 | biimpar 478 |
. . . . 5
β’ ((π β§ π < 0 ) β
((invgβπ)β((invgβπ)βπ)) < 0 ) |
235 | 7, 17, 9, 18 | ogrpinv0lt 32281 |
. . . . . . 7
β’ ((π β oGrp β§
((invgβπ)βπ) β π΅) β ( 0 <
((invgβπ)βπ) β ((invgβπ)β((invgβπ)βπ)) < 0 )) |
236 | 2, 122, 235 | syl2anc 584 |
. . . . . 6
β’ (π β ( 0 <
((invgβπ)βπ) β ((invgβπ)β((invgβπ)βπ)) < 0 )) |
237 | 236 | biimpar 478 |
. . . . 5
β’ ((π β§
((invgβπ)β((invgβπ)βπ)) < 0 ) β 0 <
((invgβπ)βπ)) |
238 | 234, 237 | syldan 591 |
. . . 4
β’ ((π β§ π < 0 ) β 0 <
((invgβπ)βπ)) |
239 | 7, 18, 17, 34, 8, 227, 229, 230, 231, 232, 238 | archirng 32375 |
. . 3
β’ ((π β§ π < 0 ) β βπ β β0
((π Β· π) <
((invgβπ)βπ) β§ ((invgβπ)βπ) β€ ((π + 1) Β· π))) |
240 | 226, 239 | r19.29a 3162 |
. 2
β’ ((π β§ π < 0 ) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
241 | | nn0ssz 12583 |
. . 3
β’
β0 β β€ |
242 | 2 | adantr 481 |
. . . 4
β’ ((π β§ 0 < π) β π β oGrp) |
243 | 228 | adantr 481 |
. . . 4
β’ ((π β§ 0 < π) β π β Archi) |
244 | 6 | adantr 481 |
. . . 4
β’ ((π β§ 0 < π) β π β π΅) |
245 | 120 | adantr 481 |
. . . 4
β’ ((π β§ 0 < π) β π β π΅) |
246 | 16 | adantr 481 |
. . . 4
β’ ((π β§ 0 < π) β 0 < π) |
247 | | simpr 485 |
. . . 4
β’ ((π β§ 0 < π) β 0 < π) |
248 | 7, 18, 17, 34, 8, 242, 243, 244, 245, 246, 247 | archirng 32375 |
. . 3
β’ ((π β§ 0 < π) β βπ β β0 ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
249 | | ssrexv 4051 |
. . 3
β’
(β0 β β€ β (βπ β β0 ((π Β· π) < π β§ π β€ ((π + 1) Β· π)) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π)))) |
250 | 241, 248,
249 | mpsyl 68 |
. 2
β’ ((π β§ 0 < π) β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |
251 | 7, 17 | tlt3 32178 |
. . 3
β’ ((π β Toset β§ π β π΅ β§ 0 β π΅) β (π = 0 β¨ π < 0 β¨ 0 < π)) |
252 | 29, 120, 33, 251 | syl3anc 1371 |
. 2
β’ (π β (π = 0 β¨ π < 0 β¨ 0 < π)) |
253 | 58, 240, 250, 252 | mpjao3dan 1431 |
1
β’ (π β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) |