Step | Hyp | Ref
| Expression |
1 | | divalglem9.5 |
. . . 4
โข ๐
= inf(๐, โ, < ) |
2 | | divalglem8.1 |
. . . . 5
โข ๐ โ โค |
3 | | divalglem8.2 |
. . . . 5
โข ๐ท โ โค |
4 | | divalglem8.3 |
. . . . 5
โข ๐ท โ 0 |
5 | | divalglem8.4 |
. . . . 5
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
6 | 2, 3, 4, 5 | divalglem2 16282 |
. . . 4
โข inf(๐, โ, < ) โ ๐ |
7 | 1, 6 | eqeltri 2830 |
. . 3
โข ๐
โ ๐ |
8 | 2, 3, 4, 5, 1 | divalglem5 16284 |
. . . 4
โข (0 โค
๐
โง ๐
< (absโ๐ท)) |
9 | 8 | simpri 487 |
. . 3
โข ๐
< (absโ๐ท) |
10 | | breq1 5109 |
. . . 4
โข (๐ฅ = ๐
โ (๐ฅ < (absโ๐ท) โ ๐
< (absโ๐ท))) |
11 | 10 | rspcev 3580 |
. . 3
โข ((๐
โ ๐ โง ๐
< (absโ๐ท)) โ โ๐ฅ โ ๐ ๐ฅ < (absโ๐ท)) |
12 | 7, 9, 11 | mp2an 691 |
. 2
โข
โ๐ฅ โ
๐ ๐ฅ < (absโ๐ท) |
13 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (๐ โ ๐) = (๐ โ ๐ฅ)) |
14 | 13 | breq2d 5118 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ (๐ท โฅ (๐ โ ๐) โ ๐ท โฅ (๐ โ ๐ฅ))) |
15 | 14, 5 | elrab2 3649 |
. . . . . . . . . . . . 13
โข (๐ฅ โ ๐ โ (๐ฅ โ โ0 โง ๐ท โฅ (๐ โ ๐ฅ))) |
16 | 15 | simplbi 499 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ โ ๐ฅ โ โ0) |
17 | 16 | nn0zd 12530 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ โ ๐ฅ โ โค) |
18 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฆ โ (๐ โ ๐) = (๐ โ ๐ฆ)) |
19 | 18 | breq2d 5118 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ (๐ท โฅ (๐ โ ๐) โ ๐ท โฅ (๐ โ ๐ฆ))) |
20 | 19, 5 | elrab2 3649 |
. . . . . . . . . . . . 13
โข (๐ฆ โ ๐ โ (๐ฆ โ โ0 โง ๐ท โฅ (๐ โ ๐ฆ))) |
21 | 20 | simplbi 499 |
. . . . . . . . . . . 12
โข (๐ฆ โ ๐ โ ๐ฆ โ โ0) |
22 | 21 | nn0zd 12530 |
. . . . . . . . . . 11
โข (๐ฆ โ ๐ โ ๐ฆ โ โค) |
23 | | zsubcl 12550 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ฅ โ โค) โ (๐ โ ๐ฅ) โ โค) |
24 | 2, 23 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ฅ โ โค โ (๐ โ ๐ฅ) โ โค) |
25 | | zsubcl 12550 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ฆ โ โค) โ (๐ โ ๐ฆ) โ โค) |
26 | 2, 25 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ฆ โ โค โ (๐ โ ๐ฆ) โ โค) |
27 | 24, 26 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ โ ๐ฅ) โ โค โง (๐ โ ๐ฆ) โ โค)) |
28 | 17, 22, 27 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ((๐ โ ๐ฅ) โ โค โง (๐ โ ๐ฆ) โ โค)) |
29 | 15 | simprbi 498 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ โ ๐ท โฅ (๐ โ ๐ฅ)) |
30 | 20 | simprbi 498 |
. . . . . . . . . . 11
โข (๐ฆ โ ๐ โ ๐ท โฅ (๐ โ ๐ฆ)) |
31 | 29, 30 | anim12i 614 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ท โฅ (๐ โ ๐ฅ) โง ๐ท โฅ (๐ โ ๐ฆ))) |
32 | | dvds2sub 16178 |
. . . . . . . . . . 11
โข ((๐ท โ โค โง (๐ โ ๐ฅ) โ โค โง (๐ โ ๐ฆ) โ โค) โ ((๐ท โฅ (๐ โ ๐ฅ) โง ๐ท โฅ (๐ โ ๐ฆ)) โ ๐ท โฅ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ)))) |
33 | 3, 32 | mp3an1 1449 |
. . . . . . . . . 10
โข (((๐ โ ๐ฅ) โ โค โง (๐ โ ๐ฆ) โ โค) โ ((๐ท โฅ (๐ โ ๐ฅ) โง ๐ท โฅ (๐ โ ๐ฆ)) โ ๐ท โฅ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ)))) |
34 | 28, 31, 33 | sylc 65 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ท โฅ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ))) |
35 | | zcn 12509 |
. . . . . . . . . . . 12
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
36 | | zcn 12509 |
. . . . . . . . . . . 12
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
37 | 2 | zrei 12510 |
. . . . . . . . . . . . . . . . 17
โข ๐ โ โ |
38 | 37 | recni 11174 |
. . . . . . . . . . . . . . . 16
โข ๐ โ โ |
39 | 38 | subidi 11477 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐) = 0 |
40 | 39 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐) โ (๐ฅ โ ๐ฆ)) = (0 โ (๐ฅ โ ๐ฆ)) |
41 | | 0cn 11152 |
. . . . . . . . . . . . . . 15
โข 0 โ
โ |
42 | | subsub2 11434 |
. . . . . . . . . . . . . . 15
โข ((0
โ โ โง ๐ฅ
โ โ โง ๐ฆ
โ โ) โ (0 โ (๐ฅ โ ๐ฆ)) = (0 + (๐ฆ โ ๐ฅ))) |
43 | 41, 42 | mp3an1 1449 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0
โ (๐ฅ โ ๐ฆ)) = (0 + (๐ฆ โ ๐ฅ))) |
44 | 40, 43 | eqtrid 2785 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ โ ๐) โ (๐ฅ โ ๐ฆ)) = (0 + (๐ฆ โ ๐ฅ))) |
45 | | sub4 11451 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ โ ๐) โ (๐ฅ โ ๐ฆ)) = ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ))) |
46 | 38, 38, 45 | mpanl12 701 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ โ ๐) โ (๐ฅ โ ๐ฆ)) = ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ))) |
47 | | subcl 11405 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง ๐ฅ โ โ) โ (๐ฆ โ ๐ฅ) โ โ) |
48 | 47 | ancoms 460 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฆ โ ๐ฅ) โ โ) |
49 | 48 | addid2d 11361 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (0 +
(๐ฆ โ ๐ฅ)) = (๐ฆ โ ๐ฅ)) |
50 | 44, 46, 49 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ)) = (๐ฆ โ ๐ฅ)) |
51 | 35, 36, 50 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ)) = (๐ฆ โ ๐ฅ)) |
52 | 17, 22, 51 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ)) = (๐ฆ โ ๐ฅ)) |
53 | 52 | breq2d 5118 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ท โฅ ((๐ โ ๐ฅ) โ (๐ โ ๐ฆ)) โ ๐ท โฅ (๐ฆ โ ๐ฅ))) |
54 | 34, 53 | mpbid 231 |
. . . . . . . 8
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ๐ท โฅ (๐ฆ โ ๐ฅ)) |
55 | | zsubcl 12550 |
. . . . . . . . . . 11
โข ((๐ฆ โ โค โง ๐ฅ โ โค) โ (๐ฆ โ ๐ฅ) โ โค) |
56 | 55 | ancoms 460 |
. . . . . . . . . 10
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฆ โ ๐ฅ) โ โค) |
57 | | absdvdsb 16162 |
. . . . . . . . . 10
โข ((๐ท โ โค โง (๐ฆ โ ๐ฅ) โ โค) โ (๐ท โฅ (๐ฆ โ ๐ฅ) โ (absโ๐ท) โฅ (๐ฆ โ ๐ฅ))) |
58 | 3, 56, 57 | sylancr 588 |
. . . . . . . . 9
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ท โฅ (๐ฆ โ ๐ฅ) โ (absโ๐ท) โฅ (๐ฆ โ ๐ฅ))) |
59 | 17, 22, 58 | syl2an 597 |
. . . . . . . 8
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ท โฅ (๐ฆ โ ๐ฅ) โ (absโ๐ท) โฅ (๐ฆ โ ๐ฅ))) |
60 | 54, 59 | mpbid 231 |
. . . . . . 7
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (absโ๐ท) โฅ (๐ฆ โ ๐ฅ)) |
61 | | nnabscl 15216 |
. . . . . . . . . . 11
โข ((๐ท โ โค โง ๐ท โ 0) โ (absโ๐ท) โ
โ) |
62 | 3, 4, 61 | mp2an 691 |
. . . . . . . . . 10
โข
(absโ๐ท) โ
โ |
63 | 62 | nnzi 12532 |
. . . . . . . . 9
โข
(absโ๐ท) โ
โค |
64 | | divides 16143 |
. . . . . . . . 9
โข
(((absโ๐ท)
โ โค โง (๐ฆ
โ ๐ฅ) โ โค)
โ ((absโ๐ท)
โฅ (๐ฆ โ ๐ฅ) โ โ๐ โ โค (๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ))) |
65 | 63, 56, 64 | sylancr 588 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
((absโ๐ท) โฅ
(๐ฆ โ ๐ฅ) โ โ๐ โ โค (๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ))) |
66 | 17, 22, 65 | syl2an 597 |
. . . . . . 7
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ((absโ๐ท) โฅ (๐ฆ โ ๐ฅ) โ โ๐ โ โค (๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ))) |
67 | 60, 66 | mpbid 231 |
. . . . . 6
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ โ๐ โ โค (๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ)) |
68 | 67 | adantr 482 |
. . . . 5
โข (((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง (๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท))) โ โ๐ โ โค (๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ)) |
69 | 2, 3, 4, 5 | divalglem8 16287 |
. . . . . 6
โข (((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง (๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท))) โ (๐ โ โค โ ((๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ) โ ๐ฅ = ๐ฆ))) |
70 | 69 | rexlimdv 3147 |
. . . . 5
โข (((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง (๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท))) โ (โ๐ โ โค (๐ ยท (absโ๐ท)) = (๐ฆ โ ๐ฅ) โ ๐ฅ = ๐ฆ)) |
71 | 68, 70 | mpd 15 |
. . . 4
โข (((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง (๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท))) โ ๐ฅ = ๐ฆ) |
72 | 71 | ex 414 |
. . 3
โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ ((๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท)) โ ๐ฅ = ๐ฆ)) |
73 | 72 | rgen2 3191 |
. 2
โข
โ๐ฅ โ
๐ โ๐ฆ โ ๐ ((๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท)) โ ๐ฅ = ๐ฆ) |
74 | | breq1 5109 |
. . 3
โข (๐ฅ = ๐ฆ โ (๐ฅ < (absโ๐ท) โ ๐ฆ < (absโ๐ท))) |
75 | 74 | reu4 3690 |
. 2
โข
(โ!๐ฅ โ
๐ ๐ฅ < (absโ๐ท) โ (โ๐ฅ โ ๐ ๐ฅ < (absโ๐ท) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ < (absโ๐ท) โง ๐ฆ < (absโ๐ท)) โ ๐ฅ = ๐ฆ))) |
76 | 12, 73, 75 | mpbir2an 710 |
1
โข
โ!๐ฅ โ
๐ ๐ฅ < (absโ๐ท) |