Step | Hyp | Ref
| Expression |
1 | | divalglem0.2 |
. . . . . 6
โข ๐ท โ โค |
2 | | divalglem0.1 |
. . . . . . 7
โข ๐ โ โค |
3 | | nn0z 12582 |
. . . . . . 7
โข (๐ง โ โ0
โ ๐ง โ
โค) |
4 | | zsubcl 12603 |
. . . . . . 7
โข ((๐ โ โค โง ๐ง โ โค) โ (๐ โ ๐ง) โ โค) |
5 | 2, 3, 4 | sylancr 587 |
. . . . . 6
โข (๐ง โ โ0
โ (๐ โ ๐ง) โ
โค) |
6 | | divides 16198 |
. . . . . 6
โข ((๐ท โ โค โง (๐ โ ๐ง) โ โค) โ (๐ท โฅ (๐ โ ๐ง) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐ง))) |
7 | 1, 5, 6 | sylancr 587 |
. . . . 5
โข (๐ง โ โ0
โ (๐ท โฅ (๐ โ ๐ง) โ โ๐ โ โค (๐ ยท ๐ท) = (๐ โ ๐ง))) |
8 | | nn0cn 12481 |
. . . . . . . 8
โข (๐ง โ โ0
โ ๐ง โ
โ) |
9 | | zmulcl 12610 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ท โ โค) โ (๐ ยท ๐ท) โ โค) |
10 | 1, 9 | mpan2 689 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ ยท ๐ท) โ โค) |
11 | 10 | zcnd 12666 |
. . . . . . . 8
โข (๐ โ โค โ (๐ ยท ๐ท) โ โ) |
12 | | zcn 12562 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
13 | 2, 12 | ax-mp 5 |
. . . . . . . . . 10
โข ๐ โ โ |
14 | | subadd 11462 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ (๐ง + (๐ ยท ๐ท)) = ๐)) |
15 | 13, 14 | mp3an1 1448 |
. . . . . . . . 9
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ (๐ง + (๐ ยท ๐ท)) = ๐)) |
16 | | addcom 11399 |
. . . . . . . . . 10
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ (๐ง + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ๐ง)) |
17 | 16 | eqeq1d 2734 |
. . . . . . . . 9
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ง + (๐ ยท ๐ท)) = ๐ โ ((๐ ยท ๐ท) + ๐ง) = ๐)) |
18 | 15, 17 | bitrd 278 |
. . . . . . . 8
โข ((๐ง โ โ โง (๐ ยท ๐ท) โ โ) โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ ((๐ ยท ๐ท) + ๐ง) = ๐)) |
19 | 8, 11, 18 | syl2an 596 |
. . . . . . 7
โข ((๐ง โ โ0
โง ๐ โ โค)
โ ((๐ โ ๐ง) = (๐ ยท ๐ท) โ ((๐ ยท ๐ท) + ๐ง) = ๐)) |
20 | | eqcom 2739 |
. . . . . . 7
โข ((๐ โ ๐ง) = (๐ ยท ๐ท) โ (๐ ยท ๐ท) = (๐ โ ๐ง)) |
21 | | eqcom 2739 |
. . . . . . 7
โข (((๐ ยท ๐ท) + ๐ง) = ๐ โ ๐ = ((๐ ยท ๐ท) + ๐ง)) |
22 | 19, 20, 21 | 3bitr3g 312 |
. . . . . 6
โข ((๐ง โ โ0
โง ๐ โ โค)
โ ((๐ ยท ๐ท) = (๐ โ ๐ง) โ ๐ = ((๐ ยท ๐ท) + ๐ง))) |
23 | 22 | rexbidva 3176 |
. . . . 5
โข (๐ง โ โ0
โ (โ๐ โ
โค (๐ ยท ๐ท) = (๐ โ ๐ง) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ง))) |
24 | 7, 23 | bitrd 278 |
. . . 4
โข (๐ง โ โ0
โ (๐ท โฅ (๐ โ ๐ง) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ง))) |
25 | 24 | pm5.32i 575 |
. . 3
โข ((๐ง โ โ0
โง ๐ท โฅ (๐ โ ๐ง)) โ (๐ง โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ง))) |
26 | | oveq2 7416 |
. . . . 5
โข (๐ = ๐ง โ (๐ โ ๐) = (๐ โ ๐ง)) |
27 | 26 | breq2d 5160 |
. . . 4
โข (๐ = ๐ง โ (๐ท โฅ (๐ โ ๐) โ ๐ท โฅ (๐ โ ๐ง))) |
28 | | divalglem2.4 |
. . . 4
โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} |
29 | 27, 28 | elrab2 3686 |
. . 3
โข (๐ง โ ๐ โ (๐ง โ โ0 โง ๐ท โฅ (๐ โ ๐ง))) |
30 | | oveq2 7416 |
. . . . . 6
โข (๐ = ๐ง โ ((๐ ยท ๐ท) + ๐) = ((๐ ยท ๐ท) + ๐ง)) |
31 | 30 | eqeq2d 2743 |
. . . . 5
โข (๐ = ๐ง โ (๐ = ((๐ ยท ๐ท) + ๐) โ ๐ = ((๐ ยท ๐ท) + ๐ง))) |
32 | 31 | rexbidv 3178 |
. . . 4
โข (๐ = ๐ง โ (โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐) โ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐ง))) |
33 | 32 | elrab 3683 |
. . 3
โข (๐ง โ {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)} โ (๐ง โ โ0 โง
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐ง))) |
34 | 25, 29, 33 | 3bitr4i 302 |
. 2
โข (๐ง โ ๐ โ ๐ง โ {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)}) |
35 | 34 | eqriv 2729 |
1
โข ๐ = {๐ โ โ0 โฃ
โ๐ โ โค
๐ = ((๐ ยท ๐ท) + ๐)} |