Step | Hyp | Ref
| Expression |
1 | | abelth.3 |
. 2
β’ (π β π β β) |
2 | | abelth.4 |
. 2
β’ (π β 0 β€ π) |
3 | | 1cnd 11155 |
. . . 4
β’ ((π β β β§ 0 β€
π) β 1 β
β) |
4 | | 0le0 12259 |
. . . . 5
β’ 0 β€
0 |
5 | | simpl 484 |
. . . . . . 7
β’ ((π β β β§ 0 β€
π) β π β β) |
6 | 5 | recnd 11188 |
. . . . . 6
β’ ((π β β β§ 0 β€
π) β π β β) |
7 | 6 | mul01d 11359 |
. . . . 5
β’ ((π β β β§ 0 β€
π) β (π Β· 0) =
0) |
8 | 4, 7 | breqtrrid 5144 |
. . . 4
β’ ((π β β β§ 0 β€
π) β 0 β€ (π Β· 0)) |
9 | | oveq2 7366 |
. . . . . . . 8
β’ (π§ = 1 β (1 β π§) = (1 β
1)) |
10 | | 1m1e0 12230 |
. . . . . . . 8
β’ (1
β 1) = 0 |
11 | 9, 10 | eqtrdi 2789 |
. . . . . . 7
β’ (π§ = 1 β (1 β π§) = 0) |
12 | 11 | abs00bd 15182 |
. . . . . 6
β’ (π§ = 1 β (absβ(1
β π§)) =
0) |
13 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π§ = 1 β (absβπ§) =
(absβ1)) |
14 | | abs1 15188 |
. . . . . . . . . 10
β’
(absβ1) = 1 |
15 | 13, 14 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π§ = 1 β (absβπ§) = 1) |
16 | 15 | oveq2d 7374 |
. . . . . . . 8
β’ (π§ = 1 β (1 β
(absβπ§)) = (1 β
1)) |
17 | 16, 10 | eqtrdi 2789 |
. . . . . . 7
β’ (π§ = 1 β (1 β
(absβπ§)) =
0) |
18 | 17 | oveq2d 7374 |
. . . . . 6
β’ (π§ = 1 β (π Β· (1 β (absβπ§))) = (π Β· 0)) |
19 | 12, 18 | breq12d 5119 |
. . . . 5
β’ (π§ = 1 β ((absβ(1
β π§)) β€ (π Β· (1 β
(absβπ§))) β 0
β€ (π Β·
0))) |
20 | | abelth.5 |
. . . . 5
β’ π = {π§ β β β£ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))} |
21 | 19, 20 | elrab2 3649 |
. . . 4
β’ (1 β
π β (1 β β
β§ 0 β€ (π Β·
0))) |
22 | 3, 8, 21 | sylanbrc 584 |
. . 3
β’ ((π β β β§ 0 β€
π) β 1 β π) |
23 | | velsn 4603 |
. . . . . . . . . 10
β’ (π§ β {1} β π§ = 1) |
24 | 23 | necon3bbii 2988 |
. . . . . . . . 9
β’ (Β¬
π§ β {1} β π§ β 1) |
25 | | simprll 778 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β π§ β
β) |
26 | | 0cn 11152 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
27 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (abs
β β ) = (abs β β ) |
28 | 27 | cnmetdval 24150 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β β§ 0 β
β) β (π§(abs
β β )0) = (absβ(π§ β 0))) |
29 | 25, 26, 28 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π§(abs β β )0) =
(absβ(π§ β
0))) |
30 | 25 | subid1d 11506 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π§ β 0) = π§) |
31 | 30 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβ(π§ β 0)) =
(absβπ§)) |
32 | 29, 31 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π§(abs β β )0) =
(absβπ§)) |
33 | 25 | abscld 15327 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβπ§) β
β) |
34 | | 1red 11161 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 1 β
β) |
35 | | 1re 11160 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
β |
36 | | resubcl 11470 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((absβπ§)
β β β§ 1 β β) β ((absβπ§) β 1) β β) |
37 | 33, 35, 36 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
((absβπ§) β 1)
β β) |
38 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β |
39 | | subcl 11405 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((1
β β β§ π§
β β) β (1 β π§) β β) |
40 | 38, 25, 39 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (1
β π§) β
β) |
41 | 40 | abscld 15327 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβ(1 β π§))
β β) |
42 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β π β
β) |
43 | | resubcl 11470 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((1
β β β§ (absβπ§) β β) β (1 β
(absβπ§)) β
β) |
44 | 35, 33, 43 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (1
β (absβπ§))
β β) |
45 | 42, 44 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· (1 β
(absβπ§))) β
β) |
46 | 14 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((absβπ§)
β (absβ1)) = ((absβπ§) β 1) |
47 | | abs2dif 15223 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π§ β β β§ 1 β
β) β ((absβπ§) β (absβ1)) β€
(absβ(π§ β
1))) |
48 | 25, 38, 47 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
((absβπ§) β
(absβ1)) β€ (absβ(π§ β 1))) |
49 | 46, 48 | eqbrtrrid 5142 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
((absβπ§) β 1)
β€ (absβ(π§ β
1))) |
50 | | abssub 15217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ β β β§ 1 β
β) β (absβ(π§ β 1)) = (absβ(1 β π§))) |
51 | 25, 38, 50 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβ(π§ β 1)) =
(absβ(1 β π§))) |
52 | 49, 51 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
((absβπ§) β 1)
β€ (absβ(1 β π§))) |
53 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) |
54 | 37, 41, 45, 52, 53 | letrd 11317 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
((absβπ§) β 1)
β€ (π Β· (1 β
(absβπ§)))) |
55 | 33, 34, 45 | lesubaddd 11757 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(((absβπ§) β 1)
β€ (π Β· (1 β
(absβπ§))) β
(absβπ§) β€ ((π Β· (1 β
(absβπ§))) +
1))) |
56 | 54, 55 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβπ§) β€ ((π Β· (1 β
(absβπ§))) +
1)) |
57 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β π β
β) |
58 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 1 β
β) |
59 | 42, 33 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· (absβπ§)) β
β) |
60 | 59 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· (absβπ§)) β
β) |
61 | 57, 58, 60 | addsubd 11538 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π + 1) β (π Β· (absβπ§))) = ((π β (π Β· (absβπ§))) + 1)) |
62 | 33 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβπ§) β
β) |
63 | 57, 58, 62 | subdid 11616 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· (1 β
(absβπ§))) = ((π Β· 1) β (π Β· (absβπ§)))) |
64 | 57 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· 1) = π) |
65 | 64 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π Β· 1) β (π Β· (absβπ§))) = (π β (π Β· (absβπ§)))) |
66 | 63, 65 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· (1 β
(absβπ§))) = (π β (π Β· (absβπ§)))) |
67 | 66 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π Β· (1 β
(absβπ§))) + 1) =
((π β (π Β· (absβπ§))) + 1)) |
68 | 61, 67 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π + 1) β (π Β· (absβπ§))) = ((π Β· (1 β (absβπ§))) + 1)) |
69 | 56, 68 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβπ§) β€ ((π + 1) β (π Β· (absβπ§)))) |
70 | | peano2re 11333 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π + 1) β
β) |
71 | 42, 70 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π + 1) β
β) |
72 | 59, 33, 71 | leaddsub2d 11762 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (((π Β· (absβπ§)) + (absβπ§)) β€ (π + 1) β (absβπ§) β€ ((π + 1) β (π Β· (absβπ§))))) |
73 | 69, 72 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π Β· (absβπ§)) + (absβπ§)) β€ (π + 1)) |
74 | 57, 62 | adddirp1d 11186 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π + 1) Β· (absβπ§)) = ((π Β· (absβπ§)) + (absβπ§))) |
75 | 71 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π + 1) β
β) |
76 | 75 | mulid1d 11177 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π + 1) Β· 1) = (π + 1)) |
77 | 73, 74, 76 | 3brtr4d 5138 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((π + 1) Β· (absβπ§)) β€ ((π + 1) Β· 1)) |
78 | | 0red 11163 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 0 β
β) |
79 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 0 β€
π) |
80 | 42 | ltp1d 12090 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β π < (π + 1)) |
81 | 78, 42, 71, 79, 80 | lelttrd 11318 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 0 <
(π + 1)) |
82 | | lemul2 12013 |
. . . . . . . . . . . . . . . 16
β’
(((absβπ§)
β β β§ 1 β β β§ ((π + 1) β β β§ 0 < (π + 1))) β ((absβπ§) β€ 1 β ((π + 1) Β· (absβπ§)) β€ ((π + 1) Β· 1))) |
83 | 33, 34, 71, 81, 82 | syl112anc 1375 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
((absβπ§) β€ 1
β ((π + 1) Β·
(absβπ§)) β€ ((π + 1) Β·
1))) |
84 | 77, 83 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβπ§) β€
1) |
85 | 41, 45, 53 | lensymd 11311 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β Β¬
(π Β· (1 β
(absβπ§))) <
(absβ(1 β π§))) |
86 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· 0) =
0) |
87 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β π§ β 1) |
88 | 87 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 1 β
π§) |
89 | | subeq0 11432 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((1
β β β§ π§
β β) β ((1 β π§) = 0 β 1 = π§)) |
90 | 89 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((1
β β β§ π§
β β) β ((1 β π§) β 0 β 1 β π§)) |
91 | 38, 25, 90 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((1
β π§) β 0 β 1
β π§)) |
92 | 88, 91 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (1
β π§) β
0) |
93 | | absgt0 15215 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((1
β π§) β β
β ((1 β π§) β
0 β 0 < (absβ(1 β π§)))) |
94 | 40, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β ((1
β π§) β 0 β 0
< (absβ(1 β π§)))) |
95 | 92, 94 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 0 <
(absβ(1 β π§))) |
96 | 86, 95 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π Β· 0) < (absβ(1
β π§))) |
97 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 =
(absβπ§) β (1
β 1) = (1 β (absβπ§))) |
98 | 10, 97 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 =
(absβπ§) β 0 = (1
β (absβπ§))) |
99 | 98 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ (1 =
(absβπ§) β (π Β· 0) = (π Β· (1 β
(absβπ§)))) |
100 | 99 | breq1d 5116 |
. . . . . . . . . . . . . . . . 17
β’ (1 =
(absβπ§) β
((π Β· 0) <
(absβ(1 β π§))
β (π Β· (1
β (absβπ§)))
< (absβ(1 β π§)))) |
101 | 96, 100 | syl5ibcom 244 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (1 =
(absβπ§) β (π Β· (1 β
(absβπ§))) <
(absβ(1 β π§)))) |
102 | 101 | necon3bd 2954 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (Β¬
(π Β· (1 β
(absβπ§))) <
(absβ(1 β π§))
β 1 β (absβπ§))) |
103 | 85, 102 | mpd 15 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β 1 β
(absβπ§)) |
104 | 33, 34, 84, 103 | leneltd 11314 |
. . . . . . . . . . . . 13
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β
(absβπ§) <
1) |
105 | 32, 104 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π§(abs β β )0) <
1) |
106 | | cnxmet 24152 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) β (βMetββ) |
107 | | 1xr 11219 |
. . . . . . . . . . . . . 14
β’ 1 β
β* |
108 | | elbl3 23761 |
. . . . . . . . . . . . . 14
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (0 β β β§ π§ β β)) β (π§ β (0(ballβ(abs β β
))1) β (π§(abs β
β )0) < 1)) |
109 | 106, 107,
108 | mpanl12 701 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ π§
β β) β (π§
β (0(ballβ(abs β β ))1) β (π§(abs β β )0) <
1)) |
110 | 26, 25, 109 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β (π§ β (0(ballβ(abs
β β ))1) β (π§(abs β β )0) <
1)) |
111 | 105, 110 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β β β§ 0 β€
π) β§ ((π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))) β§
π§ β 1)) β π§ β (0(ballβ(abs
β β ))1)) |
112 | 111 | expr 458 |
. . . . . . . . . 10
β’ (((π β β β§ 0 β€
π) β§ (π§ β β β§
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§))))) β
(π§ β 1 β π§ β (0(ballβ(abs
β β ))1))) |
113 | 112 | 3impb 1116 |
. . . . . . . . 9
β’ (((π β β β§ 0 β€
π) β§ π§ β β β§ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))) β (π§ β 1 β π§ β (0(ballβ(abs β β
))1))) |
114 | 24, 113 | biimtrid 241 |
. . . . . . . 8
β’ (((π β β β§ 0 β€
π) β§ π§ β β β§ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))) β (Β¬ π§ β {1} β π§ β (0(ballβ(abs
β β ))1))) |
115 | 114 | orrd 862 |
. . . . . . 7
β’ (((π β β β§ 0 β€
π) β§ π§ β β β§ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))) β (π§ β {1} β¨ π§ β (0(ballβ(abs β β
))1))) |
116 | | elun 4109 |
. . . . . . 7
β’ (π§ β ({1} βͺ
(0(ballβ(abs β β ))1)) β (π§ β {1} β¨ π§ β (0(ballβ(abs β β
))1))) |
117 | 115, 116 | sylibr 233 |
. . . . . 6
β’ (((π β β β§ 0 β€
π) β§ π§ β β β§ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))) β π§ β ({1} βͺ (0(ballβ(abs β
β ))1))) |
118 | 117 | rabssdv 4033 |
. . . . 5
β’ ((π β β β§ 0 β€
π) β {π§ β β β£
(absβ(1 β π§))
β€ (π Β· (1 β
(absβπ§)))} β
({1} βͺ (0(ballβ(abs β β ))1))) |
119 | 20, 118 | eqsstrid 3993 |
. . . 4
β’ ((π β β β§ 0 β€
π) β π β ({1} βͺ (0(ballβ(abs
β β ))1))) |
120 | | ssundif 4446 |
. . . 4
β’ (π β ({1} βͺ
(0(ballβ(abs β β ))1)) β (π β {1}) β (0(ballβ(abs
β β ))1)) |
121 | 119, 120 | sylib 217 |
. . 3
β’ ((π β β β§ 0 β€
π) β (π β {1}) β
(0(ballβ(abs β β ))1)) |
122 | 22, 121 | jca 513 |
. 2
β’ ((π β β β§ 0 β€
π) β (1 β π β§ (π β {1}) β (0(ballβ(abs
β β ))1))) |
123 | 1, 2, 122 | syl2anc 585 |
1
β’ (π β (1 β π β§ (π β {1}) β (0(ballβ(abs
β β ))1))) |