Step | Hyp | Ref
| Expression |
1 | | divalglem0.2 |
. . . . . 6
โข ๐ท โ โค |
2 | | divalglem0.1 |
. . . . . . 7
โข ๐ โ โค |
3 | | nn0z 12529 |
. . . . . . 7
โข (๐ง โ โ0
โ ๐ง โ
โค) |
4 | | zsubcl 12550 |
. . . . . . 7
โข ((๐ โ โค โง ๐ง โ โค) โ (๐ โ ๐ง) โ โค) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . 6
โข (๐ง โ โ0
โ (๐ โ ๐ง) โ
โค) |
6 | | divides 16143 |
. . . . . 6
โข ((๐ท โ โค โง (๐ โ ๐ง) โ โค) โ (๐ท โฅ (๐ โ ๐ง) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐ง))) |
7 | 1, 5, 6 | sylancr 588 |
. . . . 5
โข (๐ง โ โ0
โ (๐ท โฅ (๐ โ ๐ง) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐ง))) |
8 | | nn0cn 12428 |
. . . . . . . 8
โข (๐ง โ โ0
โ ๐ง โ
โ) |
9 | | zmulcl 12557 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ท โ โค) โ (๐ ยท ๐ท) โ โค) |
10 | 1, 9 | mpan2 690 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ ยท ๐ท) โ โค) |
11 | 10 | zcnd 12613 |
. . . . . . . 8
โข (๐ โ โค โ (๐ ยท ๐ท) โ โ) |
12 | | zcn 12509 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
13 | 2, 12 | ax-mp 5 |
. . . . . . . . . 10
โข ๐ โ โ |
14 | | subadd 11409 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ (๐ง + (๐ ยท ๐ท)) = ๐)) |
15 | 13, 14 | mp3an1 1449 |
. . . . . . . . 9
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ (๐ง + (๐ ยท ๐ท)) = ๐)) |
16 | | addcom 11346 |
. . . . . . . . . 10
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ (๐ง + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ๐ง)) |
17 | 16 | eqeq1d 2735 |
. . . . . . . . 9
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ง + (๐ ยท ๐ท)) = ๐ โ ((๐ ยท ๐ท) + ๐ง) = ๐)) |
18 | 15, 17 | bitrd 279 |
. . . . . . . 8
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ ((๐ ยท ๐ท) + ๐ง) = ๐)) |
19 | 8, 11, 18 | syl2an 597 |
. . . . . . 7
โข ((๐ง โ โ0
โง ๐ โ โค)
โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ ((๐ ยท ๐ท) + ๐ง) = ๐)) |
20 | | eqcom 2740 |
. . . . . . 7
โข ((๐ โ ๐ง) = (๐ ยท ๐ท) โ (๐ ยท ๐ท) = (๐ โ ๐ง)) |
21 | | eqcom 2740 |
. . . . . . 7
โข (((๐ ยท ๐ท) + ๐ง) = ๐ โ ๐ = ((๐ ยท ๐ท) + ๐ง)) |
22 | 19, 20, 21 | 3bitr3g 313 |
. . . . . 6
โข ((๐ง โ โ0
โง ๐ โ โค)
โ ((๐ ยท ๐ท) = (๐ โ ๐ง) โ ๐ = ((๐ ยท ๐ท) + ๐ง))) |
23 | 22 | rexbidva 3170 |
. . . . 5
โข (๐ง โ โ0
โ (โ๐ โ
โค (๐ ยท ๐ท) = (๐ โ ๐ง) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ง))) |
24 | 7, 23 | bitrd 279 |
. . . 4
โข (๐ง โ โ0
โ (๐ท โฅ (๐ โ ๐ง) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ง))) |
25 | 24 | pm5.32i 576 |
. . 3
โข ((๐ง โ โ0
โง ๐ท โฅ (๐ โ ๐ง)) โ (๐ง โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ง))) |
26 | | oveq2 7366 |
. . . . 5
โข (๐ = ๐ง โ (๐ โ ๐) = (๐ โ ๐ง)) |
27 | 26 | breq2d 5118 |
. . . 4
โข (๐ = ๐ง โ (๐ท โฅ (๐ โ ๐) โ ๐ท โฅ (๐ โ ๐ง))) |
28 | | divalglem2.4 |
. . . 4
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
29 | 27, 28 | elrab2 3649 |
. . 3
โข (๐ง โ ๐ โ (๐ง โ โ0 โง ๐ท โฅ (๐ โ ๐ง))) |
30 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐ง โ ((๐ ยท ๐ท) + ๐) = ((๐ ยท ๐ท) + ๐ง)) |
31 | 30 | eqeq2d 2744 |
. . . . 5
โข (๐ = ๐ง โ (๐ = ((๐ ยท ๐ท) + ๐) โ ๐ = ((๐ ยท ๐ท) + ๐ง))) |
32 | 31 | rexbidv 3172 |
. . . 4
โข (๐ = ๐ง โ (โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ง))) |
33 | 32 | elrab 3646 |
. . 3
โข (๐ง โ {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)} โ (๐ง โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ง))) |
34 | 25, 29, 33 | 3bitr4i 303 |
. 2
โข (๐ง โ ๐ โ ๐ง โ {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)}) |
35 | 34 | eqriv 2730 |
1
โข ๐ = {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)} |