Step | Hyp | Ref
| Expression |
1 | | df-lcm 12060 |
. . 3
โข lcm =
(๐ฅ โ โค, ๐ฆ โ โค โฆ
if((๐ฅ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < ))) |
2 | 1 | a1i 9 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ lcm =
(๐ฅ โ โค, ๐ฆ โ โค โฆ
if((๐ฅ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < )))) |
3 | | eqeq1 2184 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ = 0 โ ๐ = 0)) |
4 | 3 | orbi1d 791 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ฅ = 0 โจ ๐ฆ = 0) โ (๐ = 0 โจ ๐ฆ = 0))) |
5 | | breq1 4006 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฅ โฅ ๐ โ ๐ โฅ ๐)) |
6 | 5 | anbi1d 465 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐) โ (๐ โฅ ๐ โง ๐ฆ โฅ ๐))) |
7 | 6 | rabbidv 2726 |
. . . . . 6
โข (๐ฅ = ๐ โ {๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)} = {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ฆ โฅ ๐)}) |
8 | 7 | infeq1d 7010 |
. . . . 5
โข (๐ฅ = ๐ โ inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < ) = inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < )) |
9 | 4, 8 | ifbieq2d 3558 |
. . . 4
โข (๐ฅ = ๐ โ if((๐ฅ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < )) = if((๐ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < ))) |
10 | | eqeq1 2184 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ฆ = 0 โ ๐ = 0)) |
11 | 10 | orbi2d 790 |
. . . . 5
โข (๐ฆ = ๐ โ ((๐ = 0 โจ ๐ฆ = 0) โ (๐ = 0 โจ ๐ = 0))) |
12 | | breq1 4006 |
. . . . . . . 8
โข (๐ฆ = ๐ โ (๐ฆ โฅ ๐ โ ๐ โฅ ๐)) |
13 | 12 | anbi2d 464 |
. . . . . . 7
โข (๐ฆ = ๐ โ ((๐ โฅ ๐ โง ๐ฆ โฅ ๐) โ (๐ โฅ ๐ โง ๐ โฅ ๐))) |
14 | 13 | rabbidv 2726 |
. . . . . 6
โข (๐ฆ = ๐ โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ฆ โฅ ๐)} = {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}) |
15 | 14 | infeq1d 7010 |
. . . . 5
โข (๐ฆ = ๐ โ inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < ) = inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < )) |
16 | 11, 15 | ifbieq2d 3558 |
. . . 4
โข (๐ฆ = ๐ โ if((๐ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < )) = if((๐ = 0 โจ ๐ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ))) |
17 | 9, 16 | sylan9eq 2230 |
. . 3
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ if((๐ฅ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < )) = if((๐ = 0 โจ ๐ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ))) |
18 | 17 | adantl 277 |
. 2
โข (((๐ โ โค โง ๐ โ โค) โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ if((๐ฅ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < )) = if((๐ = 0 โจ ๐ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ))) |
19 | | simpl 109 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โค) |
20 | | simpr 110 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โค) |
21 | | c0ex 7950 |
. . . 4
โข 0 โ
V |
22 | 21 | a1i 9 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โจ ๐ = 0)) โ 0 โ V) |
23 | | 1zzd 9279 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ 1 โ
โค) |
24 | | nnuz 9562 |
. . . . . 6
โข โ =
(โคโฅโ1) |
25 | | rabeq 2729 |
. . . . . 6
โข (โ
= (โคโฅโ1) โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)} = {๐ โ (โคโฅโ1)
โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}) |
26 | 24, 25 | ax-mp 5 |
. . . . 5
โข {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)} = {๐ โ (โคโฅโ1)
โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)} |
27 | | dvdsmul1 11819 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) |
28 | 27 | adantr 276 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โฅ (๐ ยท ๐)) |
29 | | simpll 527 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โ โค) |
30 | | simplr 528 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โ โค) |
31 | 29, 30 | zmulcld 9380 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐ ยท ๐) โ โค) |
32 | | dvdsabsb 11816 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ ยท ๐) โ โค) โ (๐ โฅ (๐ ยท ๐) โ ๐ โฅ (absโ(๐ ยท ๐)))) |
33 | 29, 31, 32 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐ โฅ (๐ ยท ๐) โ ๐ โฅ (absโ(๐ ยท ๐)))) |
34 | 28, 33 | mpbid 147 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โฅ (absโ(๐ ยท ๐))) |
35 | | dvdsmul2 11820 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) |
36 | 35 | adantr 276 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โฅ (๐ ยท ๐)) |
37 | | dvdsabsb 11816 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ ยท ๐) โ โค) โ (๐ โฅ (๐ ยท ๐) โ ๐ โฅ (absโ(๐ ยท ๐)))) |
38 | 30, 31, 37 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐ โฅ (๐ ยท ๐) โ ๐ โฅ (absโ(๐ ยท ๐)))) |
39 | 36, 38 | mpbid 147 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โฅ (absโ(๐ ยท ๐))) |
40 | 29 | zcnd 9375 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โ โ) |
41 | 30 | zcnd 9375 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โ โ) |
42 | 40, 41 | absmuld 11202 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (absโ(๐ ยท ๐)) = ((absโ๐) ยท (absโ๐))) |
43 | | simpr 110 |
. . . . . . . . . . . . 13
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ยฌ (๐ = 0 โจ ๐ = 0)) |
44 | | ioran 752 |
. . . . . . . . . . . . 13
โข (ยฌ
(๐ = 0 โจ ๐ = 0) โ (ยฌ ๐ = 0 โง ยฌ ๐ = 0)) |
45 | 43, 44 | sylib 122 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (ยฌ ๐ = 0 โง ยฌ ๐ = 0)) |
46 | 45 | simpld 112 |
. . . . . . . . . . 11
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ยฌ ๐ = 0) |
47 | 46 | neqned 2354 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โ 0) |
48 | | nnabscl 11108 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
49 | 29, 47, 48 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (absโ๐) โ
โ) |
50 | 45 | simprd 114 |
. . . . . . . . . . 11
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ยฌ ๐ = 0) |
51 | 50 | neqned 2354 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ๐ โ 0) |
52 | | nnabscl 11108 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
53 | 30, 51, 52 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (absโ๐) โ
โ) |
54 | 49, 53 | nnmulcld 8967 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ((absโ๐) ยท (absโ๐)) โ
โ) |
55 | 42, 54 | eqeltrd 2254 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (absโ(๐ ยท ๐)) โ โ) |
56 | | breq2 4007 |
. . . . . . . . 9
โข (๐ = (absโ(๐ ยท ๐)) โ (๐ โฅ ๐ โ ๐ โฅ (absโ(๐ ยท ๐)))) |
57 | | breq2 4007 |
. . . . . . . . 9
โข (๐ = (absโ(๐ ยท ๐)) โ (๐ โฅ ๐ โ ๐ โฅ (absโ(๐ ยท ๐)))) |
58 | 56, 57 | anbi12d 473 |
. . . . . . . 8
โข (๐ = (absโ(๐ ยท ๐)) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (๐ โฅ (absโ(๐ ยท ๐)) โง ๐ โฅ (absโ(๐ ยท ๐))))) |
59 | 58 | elrab3 2894 |
. . . . . . 7
โข
((absโ(๐
ยท ๐)) โ โ
โ ((absโ(๐
ยท ๐)) โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)} โ (๐ โฅ (absโ(๐ ยท ๐)) โง ๐ โฅ (absโ(๐ ยท ๐))))) |
60 | 55, 59 | syl 14 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ ((absโ(๐ ยท ๐)) โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)} โ (๐ โฅ (absโ(๐ ยท ๐)) โง ๐ โฅ (absโ(๐ ยท ๐))))) |
61 | 34, 39, 60 | mpbir2and 944 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (absโ(๐ ยท ๐)) โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}) |
62 | | elfzelz 10024 |
. . . . . . 7
โข (๐ โ (1...(absโ(๐ ยท ๐))) โ ๐ โ โค) |
63 | | zdvdsdc 11818 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ
DECID ๐
โฅ ๐) |
64 | 29, 62, 63 | syl2an 289 |
. . . . . 6
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โง ๐ โ (1...(absโ(๐ ยท ๐)))) โ DECID ๐ โฅ ๐) |
65 | | zdvdsdc 11818 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ
DECID ๐
โฅ ๐) |
66 | 30, 62, 65 | syl2an 289 |
. . . . . 6
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โง ๐ โ (1...(absโ(๐ ยท ๐)))) โ DECID ๐ โฅ ๐) |
67 | | dcan2 934 |
. . . . . 6
โข
(DECID ๐ โฅ ๐ โ (DECID ๐ โฅ ๐ โ DECID (๐ โฅ ๐ โง ๐ โฅ ๐))) |
68 | 64, 66, 67 | sylc 62 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โง ๐ โ (1...(absโ(๐ ยท ๐)))) โ DECID (๐ โฅ ๐ โง ๐ โฅ ๐)) |
69 | 23, 26, 61, 68 | infssuzcldc 11951 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ) โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}) |
70 | 69 | elexd 2750 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ) โ
V) |
71 | | lcmmndc 12061 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ
DECID (๐ = 0
โจ ๐ =
0)) |
72 | 22, 70, 71 | ifcldadc 3563 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ
if((๐ = 0 โจ ๐ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < )) โ
V) |
73 | 2, 18, 19, 20, 72 | ovmpod 6001 |
1
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) = if((๐ = 0 โจ ๐ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ))) |