Step | Hyp | Ref
| Expression |
1 | | divalglem8.1 |
. . . 4
โข ๐ โ โค |
2 | | divalglem8.2 |
. . . 4
โข ๐ท โ โค |
3 | | divalglem8.3 |
. . . 4
โข ๐ท โ 0 |
4 | | divalglem8.4 |
. . . 4
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
5 | | eqid 2733 |
. . . 4
โข inf(๐, โ, < ) = inf(๐, โ, <
) |
6 | 1, 2, 3, 4, 5 | divalglem9 16288 |
. . 3
โข
โ!๐ฅ โ
๐ ๐ฅ < (absโ๐ท) |
7 | | elnn0z 12517 |
. . . . . . . . . 10
โข (๐ฅ โ โ0
โ (๐ฅ โ โค
โง 0 โค ๐ฅ)) |
8 | 7 | anbi2i 624 |
. . . . . . . . 9
โข ((๐ฅ < (absโ๐ท) โง ๐ฅ โ โ0) โ (๐ฅ < (absโ๐ท) โง (๐ฅ โ โค โง 0 โค ๐ฅ))) |
9 | | an12 644 |
. . . . . . . . . 10
โข ((๐ฅ < (absโ๐ท) โง (๐ฅ โ โค โง 0 โค ๐ฅ)) โ (๐ฅ โ โค โง (๐ฅ < (absโ๐ท) โง 0 โค ๐ฅ))) |
10 | | ancom 462 |
. . . . . . . . . . 11
โข ((๐ฅ < (absโ๐ท) โง 0 โค ๐ฅ) โ (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท))) |
11 | 10 | anbi2i 624 |
. . . . . . . . . 10
โข ((๐ฅ โ โค โง (๐ฅ < (absโ๐ท) โง 0 โค ๐ฅ)) โ (๐ฅ โ โค โง (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)))) |
12 | 9, 11 | bitri 275 |
. . . . . . . . 9
โข ((๐ฅ < (absโ๐ท) โง (๐ฅ โ โค โง 0 โค ๐ฅ)) โ (๐ฅ โ โค โง (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)))) |
13 | 8, 12 | bitri 275 |
. . . . . . . 8
โข ((๐ฅ < (absโ๐ท) โง ๐ฅ โ โ0) โ (๐ฅ โ โค โง (0 โค
๐ฅ โง ๐ฅ < (absโ๐ท)))) |
14 | 13 | anbi1i 625 |
. . . . . . 7
โข (((๐ฅ < (absโ๐ท) โง ๐ฅ โ โ0) โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ ((๐ฅ โ โค โง (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท))) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
15 | | anass 470 |
. . . . . . 7
โข (((๐ฅ โ โค โง (0 โค
๐ฅ โง ๐ฅ < (absโ๐ท))) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ (๐ฅ โ โค โง ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
16 | 14, 15 | bitri 275 |
. . . . . 6
โข (((๐ฅ < (absโ๐ท) โง ๐ฅ โ โ0) โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ (๐ฅ โ โค โง ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
17 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ ((๐ ยท ๐ท) + ๐) = ((๐ ยท ๐ท) + ๐ฅ)) |
18 | 17 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ = ((๐ ยท ๐ท) + ๐) โ ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
19 | 18 | rexbidv 3172 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
20 | 1, 2, 3, 4 | divalglem4 16283 |
. . . . . . . . 9
โข ๐ = {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)} |
21 | 19, 20 | elrab2 3649 |
. . . . . . . 8
โข (๐ฅ โ ๐ โ (๐ฅ โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
22 | 21 | anbi2i 624 |
. . . . . . 7
โข ((๐ฅ < (absโ๐ท) โง ๐ฅ โ ๐) โ (๐ฅ < (absโ๐ท) โง (๐ฅ โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
23 | | ancom 462 |
. . . . . . 7
โข ((๐ฅ โ ๐ โง ๐ฅ < (absโ๐ท)) โ (๐ฅ < (absโ๐ท) โง ๐ฅ โ ๐)) |
24 | | anass 470 |
. . . . . . 7
โข (((๐ฅ < (absโ๐ท) โง ๐ฅ โ โ0) โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ (๐ฅ < (absโ๐ท) โง (๐ฅ โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
25 | 22, 23, 24 | 3bitr4i 303 |
. . . . . 6
โข ((๐ฅ โ ๐ โง ๐ฅ < (absโ๐ท)) โ ((๐ฅ < (absโ๐ท) โง ๐ฅ โ โ0) โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
26 | | df-3an 1090 |
. . . . . . . . 9
โข ((0 โค
๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
27 | 26 | rexbii 3094 |
. . . . . . . 8
โข
(โ๐ โ
โค (0 โค ๐ฅ โง
๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ โ๐ โ โค ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
28 | | r19.42v 3184 |
. . . . . . . 8
โข
(โ๐ โ
โค ((0 โค ๐ฅ โง
๐ฅ < (absโ๐ท)) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
29 | 27, 28 | bitri 275 |
. . . . . . 7
โข
(โ๐ โ
โค (0 โค ๐ฅ โง
๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
30 | 29 | anbi2i 624 |
. . . . . 6
โข ((๐ฅ โ โค โง
โ๐ โ โค (0
โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ))) โ (๐ฅ โ โค โง ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท)) โง โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
31 | 16, 25, 30 | 3bitr4i 303 |
. . . . 5
โข ((๐ฅ โ ๐ โง ๐ฅ < (absโ๐ท)) โ (๐ฅ โ โค โง โ๐ โ โค (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
32 | 31 | eubii 2580 |
. . . 4
โข
(โ!๐ฅ(๐ฅ โ ๐ โง ๐ฅ < (absโ๐ท)) โ โ!๐ฅ(๐ฅ โ โค โง โ๐ โ โค (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
33 | | df-reu 3353 |
. . . 4
โข
(โ!๐ฅ โ
๐ ๐ฅ < (absโ๐ท) โ โ!๐ฅ(๐ฅ โ ๐ โง ๐ฅ < (absโ๐ท))) |
34 | | df-reu 3353 |
. . . 4
โข
(โ!๐ฅ โ
โค โ๐ โ
โค (0 โค ๐ฅ โง
๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ โ!๐ฅ(๐ฅ โ โค โง โ๐ โ โค (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)))) |
35 | 32, 33, 34 | 3bitr4i 303 |
. . 3
โข
(โ!๐ฅ โ
๐ ๐ฅ < (absโ๐ท) โ โ!๐ฅ โ โค โ๐ โ โค (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ))) |
36 | 6, 35 | mpbi 229 |
. 2
โข
โ!๐ฅ โ
โค โ๐ โ
โค (0 โค ๐ฅ โง
๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) |
37 | | breq2 5110 |
. . . . 5
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
38 | | breq1 5109 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ฅ < (absโ๐ท) โ ๐ < (absโ๐ท))) |
39 | | oveq2 7366 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ ยท ๐ท) + ๐ฅ) = ((๐ ยท ๐ท) + ๐)) |
40 | 39 | eqeq2d 2744 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ = ((๐ ยท ๐ท) + ๐ฅ) โ ๐ = ((๐ ยท ๐ท) + ๐))) |
41 | 37, 38, 40 | 3anbi123d 1437 |
. . . 4
โข (๐ฅ = ๐ โ ((0 โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)))) |
42 | 41 | rexbidv 3172 |
. . 3
โข (๐ฅ = ๐ โ (โ๐ โ โค (0 โค ๐ฅ โง ๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)))) |
43 | 42 | cbvreuvw 3376 |
. 2
โข
(โ!๐ฅ โ
โค โ๐ โ
โค (0 โค ๐ฅ โง
๐ฅ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐ฅ)) โ โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐))) |
44 | 36, 43 | mpbi 229 |
1
โข
โ!๐ โ
โค โ๐ โ
โค (0 โค ๐ โง
๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) |