Step | Hyp | Ref
| Expression |
1 | | difin 4225 |
. . 3
โข ((
โฅ โ {๐})
โ (( โฅ โ {๐}) โฉ ( โฅ โ {๐}))) = (( โฅ โ {๐}) โ ( โฅ โ
{๐})) |
2 | | nzprmdif.m |
. . . . . 6
โข (๐ โ ๐ โ โ) |
3 | | prmz 16559 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
4 | 2, 3 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โค) |
5 | | nzprmdif.n |
. . . . . 6
โข (๐ โ ๐ โ โ) |
6 | | prmz 16559 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
7 | 5, 6 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โค) |
8 | 4, 7 | nzin 42690 |
. . . 4
โข (๐ โ (( โฅ โ {๐}) โฉ ( โฅ โ
{๐})) = ( โฅ โ
{(๐ lcm ๐)})) |
9 | 8 | difeq2d 4086 |
. . 3
โข (๐ โ (( โฅ โ {๐}) โ (( โฅ โ
{๐}) โฉ ( โฅ
โ {๐}))) = (( โฅ
โ {๐}) โ (
โฅ โ {(๐ lcm
๐)}))) |
10 | 1, 9 | eqtr3id 2787 |
. 2
โข (๐ โ (( โฅ โ {๐}) โ ( โฅ โ
{๐})) = (( โฅ โ
{๐}) โ ( โฅ
โ {(๐ lcm ๐)}))) |
11 | | lcmgcd 16491 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
12 | 4, 7, 11 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
13 | | nzprmdif.ne |
. . . . . . . . 9
โข (๐ โ ๐ โ ๐) |
14 | | prmrp 16596 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
15 | 2, 5, 14 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
16 | 13, 15 | mpbird 257 |
. . . . . . . 8
โข (๐ โ (๐ gcd ๐) = 1) |
17 | 16 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = ((๐ lcm ๐) ยท 1)) |
18 | | lcmcl 16485 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โ
โ0) |
19 | 4, 7, 18 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ lcm ๐) โ
โ0) |
20 | 19 | nn0cnd 12483 |
. . . . . . . 8
โข (๐ โ (๐ lcm ๐) โ โ) |
21 | 20 | mulridd 11180 |
. . . . . . 7
โข (๐ โ ((๐ lcm ๐) ยท 1) = (๐ lcm ๐)) |
22 | 17, 21 | eqtrd 2773 |
. . . . . 6
โข (๐ โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (๐ lcm ๐)) |
23 | 4 | zred 12615 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
24 | 7 | zred 12615 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
25 | 23, 24 | remulcld 11193 |
. . . . . . 7
โข (๐ โ (๐ ยท ๐) โ โ) |
26 | | prmnn 16558 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
27 | 2, 26 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
28 | 27 | nnnn0d 12481 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
29 | 28 | nn0ge0d 12484 |
. . . . . . . 8
โข (๐ โ 0 โค ๐) |
30 | | prmnn 16558 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
31 | 5, 30 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
32 | 31 | nnnn0d 12481 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
33 | 32 | nn0ge0d 12484 |
. . . . . . . 8
โข (๐ โ 0 โค ๐) |
34 | 23, 24, 29, 33 | mulge0d 11740 |
. . . . . . 7
โข (๐ โ 0 โค (๐ ยท ๐)) |
35 | 25, 34 | absidd 15316 |
. . . . . 6
โข (๐ โ (absโ(๐ ยท ๐)) = (๐ ยท ๐)) |
36 | 12, 22, 35 | 3eqtr3d 2781 |
. . . . 5
โข (๐ โ (๐ lcm ๐) = (๐ ยท ๐)) |
37 | 36 | sneqd 4602 |
. . . 4
โข (๐ โ {(๐ lcm ๐)} = {(๐ ยท ๐)}) |
38 | 37 | imaeq2d 6017 |
. . 3
โข (๐ โ ( โฅ โ {(๐ lcm ๐)}) = ( โฅ โ {(๐ ยท ๐)})) |
39 | 38 | difeq2d 4086 |
. 2
โข (๐ โ (( โฅ โ {๐}) โ ( โฅ โ
{(๐ lcm ๐)})) = (( โฅ โ {๐}) โ ( โฅ โ {(๐ ยท ๐)}))) |
40 | 10, 39 | eqtrd 2773 |
1
โข (๐ โ (( โฅ โ {๐}) โ ( โฅ โ
{๐})) = (( โฅ โ
{๐}) โ ( โฅ
โ {(๐ ยท ๐)}))) |