Step | Hyp | Ref
| Expression |
1 | | divalglem5.5 |
. . . . . 6
โข ๐
= inf(๐, โ, < ) |
2 | | divalglem0.1 |
. . . . . . 7
โข ๐ โ โค |
3 | | divalglem0.2 |
. . . . . . 7
โข ๐ท โ โค |
4 | | divalglem1.3 |
. . . . . . 7
โข ๐ท โ 0 |
5 | | divalglem2.4 |
. . . . . . 7
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
6 | 2, 3, 4, 5 | divalglem2 16284 |
. . . . . 6
โข inf(๐, โ, < ) โ ๐ |
7 | 1, 6 | eqeltri 2834 |
. . . . 5
โข ๐
โ ๐ |
8 | | oveq2 7370 |
. . . . . . 7
โข (๐ฅ = ๐
โ (๐ โ ๐ฅ) = (๐ โ ๐
)) |
9 | 8 | breq2d 5122 |
. . . . . 6
โข (๐ฅ = ๐
โ (๐ท โฅ (๐ โ ๐ฅ) โ ๐ท โฅ (๐ โ ๐
))) |
10 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (๐ โ ๐) = (๐ โ ๐ฅ)) |
11 | 10 | breq2d 5122 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (๐ท โฅ (๐ โ ๐) โ ๐ท โฅ (๐ โ ๐ฅ))) |
12 | 11 | cbvrabv 3420 |
. . . . . . 7
โข {๐ โ โ0
โฃ ๐ท โฅ (๐ โ ๐)} = {๐ฅ โ โ0 โฃ ๐ท โฅ (๐ โ ๐ฅ)} |
13 | 5, 12 | eqtri 2765 |
. . . . . 6
โข ๐ = {๐ฅ โ โ0 โฃ ๐ท โฅ (๐ โ ๐ฅ)} |
14 | 9, 13 | elrab2 3653 |
. . . . 5
โข (๐
โ ๐ โ (๐
โ โ0 โง ๐ท โฅ (๐ โ ๐
))) |
15 | 7, 14 | mpbi 229 |
. . . 4
โข (๐
โ โ0
โง ๐ท โฅ (๐ โ ๐
)) |
16 | 15 | simpli 485 |
. . 3
โข ๐
โ
โ0 |
17 | 16 | nn0ge0i 12447 |
. 2
โข 0 โค
๐
|
18 | | nnabscl 15217 |
. . . . . . 7
โข ((๐ท โ โค โง ๐ท โ 0) โ (absโ๐ท) โ
โ) |
19 | 3, 4, 18 | mp2an 691 |
. . . . . 6
โข
(absโ๐ท) โ
โ |
20 | 19 | nngt0i 12199 |
. . . . 5
โข 0 <
(absโ๐ท) |
21 | | 0re 11164 |
. . . . . 6
โข 0 โ
โ |
22 | | zcn 12511 |
. . . . . . . 8
โข (๐ท โ โค โ ๐ท โ
โ) |
23 | 3, 22 | ax-mp 5 |
. . . . . . 7
โข ๐ท โ โ |
24 | 23 | abscli 15287 |
. . . . . 6
โข
(absโ๐ท) โ
โ |
25 | 21, 24 | ltnlei 11283 |
. . . . 5
โข (0 <
(absโ๐ท) โ ยฌ
(absโ๐ท) โค
0) |
26 | 20, 25 | mpbi 229 |
. . . 4
โข ยฌ
(absโ๐ท) โค
0 |
27 | 5 | ssrab3 4045 |
. . . . . . . 8
โข ๐ โ
โ0 |
28 | | nn0uz 12812 |
. . . . . . . 8
โข
โ0 = (โคโฅโ0) |
29 | 27, 28 | sseqtri 3985 |
. . . . . . 7
โข ๐ โ
(โคโฅโ0) |
30 | | nn0abscl 15204 |
. . . . . . . . . 10
โข (๐ท โ โค โ
(absโ๐ท) โ
โ0) |
31 | 3, 30 | ax-mp 5 |
. . . . . . . . 9
โข
(absโ๐ท) โ
โ0 |
32 | | nn0sub2 12571 |
. . . . . . . . 9
โข
(((absโ๐ท)
โ โ0 โง ๐
โ โ0 โง
(absโ๐ท) โค ๐
) โ (๐
โ (absโ๐ท)) โ
โ0) |
33 | 31, 16, 32 | mp3an12 1452 |
. . . . . . . 8
โข
((absโ๐ท) โค
๐
โ (๐
โ (absโ๐ท)) โ
โ0) |
34 | 15 | a1i 11 |
. . . . . . . . 9
โข
((absโ๐ท) โค
๐
โ (๐
โ โ0 โง ๐ท โฅ (๐ โ ๐
))) |
35 | | nn0z 12531 |
. . . . . . . . . . 11
โข (๐
โ โ0
โ ๐
โ
โค) |
36 | | 1z 12540 |
. . . . . . . . . . . . 13
โข 1 โ
โค |
37 | 2, 3 | divalglem0 16282 |
. . . . . . . . . . . . 13
โข ((๐
โ โค โง 1 โ
โค) โ (๐ท โฅ
(๐ โ ๐
) โ ๐ท โฅ (๐ โ (๐
โ (1 ยท (absโ๐ท)))))) |
38 | 36, 37 | mpan2 690 |
. . . . . . . . . . . 12
โข (๐
โ โค โ (๐ท โฅ (๐ โ ๐
) โ ๐ท โฅ (๐ โ (๐
โ (1 ยท (absโ๐ท)))))) |
39 | 24 | recni 11176 |
. . . . . . . . . . . . . . . 16
โข
(absโ๐ท) โ
โ |
40 | 39 | mulid2i 11167 |
. . . . . . . . . . . . . . 15
โข (1
ยท (absโ๐ท)) =
(absโ๐ท) |
41 | 40 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข (๐
โ (1 ยท
(absโ๐ท))) = (๐
โ (absโ๐ท)) |
42 | 41 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข (๐ โ (๐
โ (1 ยท (absโ๐ท)))) = (๐ โ (๐
โ (absโ๐ท))) |
43 | 42 | breq2i 5118 |
. . . . . . . . . . . 12
โข (๐ท โฅ (๐ โ (๐
โ (1 ยท (absโ๐ท)))) โ ๐ท โฅ (๐ โ (๐
โ (absโ๐ท)))) |
44 | 38, 43 | syl6ib 251 |
. . . . . . . . . . 11
โข (๐
โ โค โ (๐ท โฅ (๐ โ ๐
) โ ๐ท โฅ (๐ โ (๐
โ (absโ๐ท))))) |
45 | 35, 44 | syl 17 |
. . . . . . . . . 10
โข (๐
โ โ0
โ (๐ท โฅ (๐ โ ๐
) โ ๐ท โฅ (๐ โ (๐
โ (absโ๐ท))))) |
46 | 45 | imp 408 |
. . . . . . . . 9
โข ((๐
โ โ0
โง ๐ท โฅ (๐ โ ๐
)) โ ๐ท โฅ (๐ โ (๐
โ (absโ๐ท)))) |
47 | 34, 46 | syl 17 |
. . . . . . . 8
โข
((absโ๐ท) โค
๐
โ ๐ท โฅ (๐ โ (๐
โ (absโ๐ท)))) |
48 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ฅ = (๐
โ (absโ๐ท)) โ (๐ โ ๐ฅ) = (๐ โ (๐
โ (absโ๐ท)))) |
49 | 48 | breq2d 5122 |
. . . . . . . . 9
โข (๐ฅ = (๐
โ (absโ๐ท)) โ (๐ท โฅ (๐ โ ๐ฅ) โ ๐ท โฅ (๐ โ (๐
โ (absโ๐ท))))) |
50 | 49, 13 | elrab2 3653 |
. . . . . . . 8
โข ((๐
โ (absโ๐ท)) โ ๐ โ ((๐
โ (absโ๐ท)) โ โ0 โง ๐ท โฅ (๐ โ (๐
โ (absโ๐ท))))) |
51 | 33, 47, 50 | sylanbrc 584 |
. . . . . . 7
โข
((absโ๐ท) โค
๐
โ (๐
โ (absโ๐ท)) โ ๐) |
52 | | infssuzle 12863 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ0) โง (๐
โ (absโ๐ท)) โ ๐) โ inf(๐, โ, < ) โค (๐
โ (absโ๐ท))) |
53 | 29, 51, 52 | sylancr 588 |
. . . . . 6
โข
((absโ๐ท) โค
๐
โ inf(๐, โ, < ) โค (๐
โ (absโ๐ท))) |
54 | 1, 53 | eqbrtrid 5145 |
. . . . 5
โข
((absโ๐ท) โค
๐
โ ๐
โค (๐
โ (absโ๐ท))) |
55 | 34 | simpld 496 |
. . . . . . . 8
โข
((absโ๐ท) โค
๐
โ ๐
โ
โ0) |
56 | 55 | nn0red 12481 |
. . . . . . 7
โข
((absโ๐ท) โค
๐
โ ๐
โ โ) |
57 | | lesub 11641 |
. . . . . . . 8
โข ((๐
โ โ โง ๐
โ โ โง
(absโ๐ท) โ
โ) โ (๐
โค
(๐
โ (absโ๐ท)) โ (absโ๐ท) โค (๐
โ ๐
))) |
58 | 24, 57 | mp3an3 1451 |
. . . . . . 7
โข ((๐
โ โ โง ๐
โ โ) โ (๐
โค (๐
โ (absโ๐ท)) โ (absโ๐ท) โค (๐
โ ๐
))) |
59 | 56, 56, 58 | syl2anc 585 |
. . . . . 6
โข
((absโ๐ท) โค
๐
โ (๐
โค (๐
โ (absโ๐ท)) โ (absโ๐ท) โค (๐
โ ๐
))) |
60 | 56 | recnd 11190 |
. . . . . . . 8
โข
((absโ๐ท) โค
๐
โ ๐
โ โ) |
61 | 60 | subidd 11507 |
. . . . . . 7
โข
((absโ๐ท) โค
๐
โ (๐
โ ๐
) = 0) |
62 | 61 | breq2d 5122 |
. . . . . 6
โข
((absโ๐ท) โค
๐
โ ((absโ๐ท) โค (๐
โ ๐
) โ (absโ๐ท) โค 0)) |
63 | 59, 62 | bitrd 279 |
. . . . 5
โข
((absโ๐ท) โค
๐
โ (๐
โค (๐
โ (absโ๐ท)) โ (absโ๐ท) โค 0)) |
64 | 54, 63 | mpbid 231 |
. . . 4
โข
((absโ๐ท) โค
๐
โ (absโ๐ท) โค 0) |
65 | 26, 64 | mto 196 |
. . 3
โข ยฌ
(absโ๐ท) โค ๐
|
66 | 16 | nn0rei 12431 |
. . . 4
โข ๐
โ โ |
67 | 66, 24 | ltnlei 11283 |
. . 3
โข (๐
< (absโ๐ท) โ ยฌ (absโ๐ท) โค ๐
) |
68 | 65, 67 | mpbir 230 |
. 2
โข ๐
< (absโ๐ท) |
69 | 17, 68 | pm3.2i 472 |
1
โข (0 โค
๐
โง ๐
< (absโ๐ท)) |