Step | Hyp | Ref
| Expression |
1 | | gcdcl 16391 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ
โ0) |
2 | 1 | nn0cnd 12480 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ โ) |
3 | 2 | mul02d 11358 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ (0
ยท (๐ gcd ๐)) = 0) |
4 | | 0z 12515 |
. . . . . . . . . 10
โข 0 โ
โค |
5 | | lcmcom 16474 |
. . . . . . . . . 10
โข ((๐ โ โค โง 0 โ
โค) โ (๐ lcm 0) =
(0 lcm ๐)) |
6 | 4, 5 | mpan2 690 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ lcm 0) = (0 lcm ๐)) |
7 | | lcm0val 16475 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ lcm 0) = 0) |
8 | 6, 7 | eqtr3d 2775 |
. . . . . . . 8
โข (๐ โ โค โ (0 lcm
๐) = 0) |
9 | 8 | adantl 483 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (0 lcm
๐) = 0) |
10 | 9 | oveq1d 7373 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ ((0 lcm
๐) ยท (๐ gcd ๐)) = (0 ยท (๐ gcd ๐))) |
11 | | zcn 12509 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
12 | 11 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
13 | 12 | mul02d 11358 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (0
ยท ๐) =
0) |
14 | 13 | abs00bd 15182 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ(0 ยท ๐))
= 0) |
15 | 3, 10, 14 | 3eqtr4d 2783 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ ((0 lcm
๐) ยท (๐ gcd ๐)) = (absโ(0 ยท ๐))) |
16 | 15 | adantr 482 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((0 lcm ๐) ยท (๐ gcd ๐)) = (absโ(0 ยท ๐))) |
17 | | simpr 486 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ๐ = 0) |
18 | 17 | oveq1d 7373 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ lcm ๐) = (0 lcm ๐)) |
19 | 18 | oveq1d 7373 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = ((0 lcm ๐) ยท (๐ gcd ๐))) |
20 | 17 | oveq1d 7373 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ ยท ๐) = (0 ยท ๐)) |
21 | 20 | fveq2d 6847 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (absโ(๐ ยท ๐)) = (absโ(0 ยท ๐))) |
22 | 16, 19, 21 | 3eqtr4d 2783 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
23 | | lcm0val 16475 |
. . . . . . . 8
โข (๐ โ โค โ (๐ lcm 0) = 0) |
24 | 23 | adantr 482 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm 0) = 0) |
25 | 24 | oveq1d 7373 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ lcm 0) ยท (๐ gcd ๐)) = (0 ยท (๐ gcd ๐))) |
26 | | zcn 12509 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
27 | 26 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
28 | 27 | mul01d 11359 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท 0) =
0) |
29 | 28 | abs00bd 15182 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ(๐ ยท 0))
= 0) |
30 | 3, 25, 29 | 3eqtr4d 2783 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ lcm 0) ยท (๐ gcd ๐)) = (absโ(๐ ยท 0))) |
31 | 30 | adantr 482 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ lcm 0) ยท (๐ gcd ๐)) = (absโ(๐ ยท 0))) |
32 | | simpr 486 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ๐ = 0) |
33 | 32 | oveq2d 7374 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ lcm ๐) = (๐ lcm 0)) |
34 | 33 | oveq1d 7373 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = ((๐ lcm 0) ยท (๐ gcd ๐))) |
35 | 32 | oveq2d 7374 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ ยท ๐) = (๐ ยท 0)) |
36 | 35 | fveq2d 6847 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (absโ(๐ ยท ๐)) = (absโ(๐ ยท 0))) |
37 | 31, 34, 36 | 3eqtr4d 2783 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
38 | 22, 37 | jaodan 957 |
. 2
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โจ ๐ = 0)) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
39 | | neanior 3034 |
. . . . 5
โข ((๐ โ 0 โง ๐ โ 0) โ ยฌ (๐ = 0 โจ ๐ = 0)) |
40 | | nnabscl 15216 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
41 | | nnabscl 15216 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
42 | 40, 41 | anim12i 614 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ
((absโ๐) โ
โ โง (absโ๐)
โ โ)) |
43 | 42 | an4s 659 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ 0 โง ๐ โ 0)) โ ((absโ๐) โ โ โง
(absโ๐) โ
โ)) |
44 | 39, 43 | sylan2br 596 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ((absโ๐) โ โ โง
(absโ๐) โ
โ)) |
45 | | lcmgcdlem 16487 |
. . . . 5
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ ((((absโ๐) lcm (absโ๐)) ยท ((absโ๐) gcd (absโ๐))) =
(absโ((absโ๐)
ยท (absโ๐)))
โง ((0 โ โ โง ((absโ๐) โฅ 0 โง (absโ๐) โฅ 0)) โ
((absโ๐) lcm
(absโ๐)) โฅ
0))) |
46 | 45 | simpld 496 |
. . . 4
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ (((absโ๐) lcm (absโ๐)) ยท ((absโ๐) gcd (absโ๐))) =
(absโ((absโ๐)
ยท (absโ๐)))) |
47 | 44, 46 | syl 17 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (((absโ๐) lcm (absโ๐)) ยท ((absโ๐) gcd (absโ๐))) =
(absโ((absโ๐)
ยท (absโ๐)))) |
48 | | lcmabs 16486 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ๐) lcm
(absโ๐)) = (๐ lcm ๐)) |
49 | | gcdabs 16416 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ๐) gcd
(absโ๐)) = (๐ gcd ๐)) |
50 | 48, 49 | oveq12d 7376 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ
(((absโ๐) lcm
(absโ๐)) ยท
((absโ๐) gcd
(absโ๐))) = ((๐ lcm ๐) ยท (๐ gcd ๐))) |
51 | 50 | adantr 482 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (((absโ๐) lcm (absโ๐)) ยท ((absโ๐) gcd (absโ๐))) = ((๐ lcm ๐) ยท (๐ gcd ๐))) |
52 | | absidm 15214 |
. . . . . . 7
โข (๐ โ โ โ
(absโ(absโ๐)) =
(absโ๐)) |
53 | | absidm 15214 |
. . . . . . 7
โข (๐ โ โ โ
(absโ(absโ๐)) =
(absโ๐)) |
54 | 52, 53 | oveqan12d 7377 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ
((absโ(absโ๐))
ยท (absโ(absโ๐))) = ((absโ๐) ยท (absโ๐))) |
55 | 26, 11, 54 | syl2an 597 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(absโ๐))
ยท (absโ(absโ๐))) = ((absโ๐) ยท (absโ๐))) |
56 | | nn0abscl 15203 |
. . . . . . . 8
โข (๐ โ โค โ
(absโ๐) โ
โ0) |
57 | 56 | nn0cnd 12480 |
. . . . . . 7
โข (๐ โ โค โ
(absโ๐) โ
โ) |
58 | 57 | adantr 482 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ๐) โ
โ) |
59 | | nn0abscl 15203 |
. . . . . . . 8
โข (๐ โ โค โ
(absโ๐) โ
โ0) |
60 | 59 | nn0cnd 12480 |
. . . . . . 7
โข (๐ โ โค โ
(absโ๐) โ
โ) |
61 | 60 | adantl 483 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ๐) โ
โ) |
62 | 58, 61 | absmuld 15345 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ((absโ๐)
ยท (absโ๐))) =
((absโ(absโ๐))
ยท (absโ(absโ๐)))) |
63 | 27, 12 | absmuld 15345 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ(๐ ยท
๐)) = ((absโ๐) ยท (absโ๐))) |
64 | 55, 62, 63 | 3eqtr4d 2783 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ((absโ๐)
ยท (absโ๐))) =
(absโ(๐ ยท
๐))) |
65 | 64 | adantr 482 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ
(absโ((absโ๐)
ยท (absโ๐))) =
(absโ(๐ ยท
๐))) |
66 | 47, 51, 65 | 3eqtr3d 2781 |
. 2
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |
67 | 38, 66 | pm2.61dan 812 |
1
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) |