Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
โข (0
โฅ ๐พ โ 0 โฅ
๐พ) |
2 | | breq1 5109 |
. . . . . . . 8
โข (๐ = 0 โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
3 | 2 | adantl 483 |
. . . . . . 7
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
4 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ lcm ๐) = (0 lcm ๐)) |
5 | | 0z 12515 |
. . . . . . . . . . 11
โข 0 โ
โค |
6 | | lcmcom 16474 |
. . . . . . . . . . 11
โข ((0
โ โค โง ๐
โ โค) โ (0 lcm ๐) = (๐ lcm 0)) |
7 | 5, 6 | mpan 689 |
. . . . . . . . . 10
โข (๐ โ โค โ (0 lcm
๐) = (๐ lcm 0)) |
8 | | lcm0val 16475 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ lcm 0) = 0) |
9 | 7, 8 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ โค โ (0 lcm
๐) = 0) |
10 | 4, 9 | sylan9eqr 2795 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ = 0) โ (๐ lcm ๐) = 0) |
11 | 10 | breq1d 5116 |
. . . . . . 7
โข ((๐ โ โค โง ๐ = 0) โ ((๐ lcm ๐) โฅ ๐พ โ 0 โฅ ๐พ)) |
12 | 3, 11 | imbi12d 345 |
. . . . . 6
โข ((๐ โ โค โง ๐ = 0) โ ((๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ) โ (0 โฅ ๐พ โ 0 โฅ ๐พ))) |
13 | 1, 12 | mpbiri 258 |
. . . . 5
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
14 | 13 | 3ad2antl3 1188 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
15 | 14 | adantrd 493 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
16 | 15 | ex 414 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ = 0 โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
17 | | breq1 5109 |
. . . . . . . 8
โข (๐ = 0 โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
18 | 17 | adantl 483 |
. . . . . . 7
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
19 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ lcm ๐) = (๐ lcm 0)) |
20 | | lcm0val 16475 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ lcm 0) = 0) |
21 | 19, 20 | sylan9eqr 2795 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ = 0) โ (๐ lcm ๐) = 0) |
22 | 21 | breq1d 5116 |
. . . . . . 7
โข ((๐ โ โค โง ๐ = 0) โ ((๐ lcm ๐) โฅ ๐พ โ 0 โฅ ๐พ)) |
23 | 18, 22 | imbi12d 345 |
. . . . . 6
โข ((๐ โ โค โง ๐ = 0) โ ((๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ) โ (0 โฅ ๐พ โ 0 โฅ ๐พ))) |
24 | 1, 23 | mpbiri 258 |
. . . . 5
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
25 | 24 | 3ad2antl2 1187 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
26 | 25 | adantld 492 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
27 | 26 | ex 414 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ = 0 โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
28 | | neanior 3034 |
. . . . . 6
โข ((๐ โ 0 โง ๐ โ 0) โ ยฌ (๐ = 0 โจ ๐ = 0)) |
29 | | lcmcl 16482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โ
โ0) |
30 | 29 | nn0zd 12530 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โ โค) |
31 | | dvds0 16159 |
. . . . . . . . . . . . . . . . 17
โข ((๐ lcm ๐) โ โค โ (๐ lcm ๐) โฅ 0) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โฅ 0) |
33 | 32 | a1d 25 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0)) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ = 0) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0)) |
35 | | breq2 5110 |
. . . . . . . . . . . . . . . . 17
โข (๐พ = 0 โ (๐ โฅ ๐พ โ ๐ โฅ 0)) |
36 | | breq2 5110 |
. . . . . . . . . . . . . . . . 17
โข (๐พ = 0 โ (๐ โฅ ๐พ โ ๐ โฅ 0)) |
37 | 35, 36 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (๐พ = 0 โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ โฅ 0 โง ๐ โฅ 0))) |
38 | | breq2 5110 |
. . . . . . . . . . . . . . . 16
โข (๐พ = 0 โ ((๐ lcm ๐) โฅ ๐พ โ (๐ lcm ๐) โฅ 0)) |
39 | 37, 38 | imbi12d 345 |
. . . . . . . . . . . . . . 15
โข (๐พ = 0 โ (((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0))) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ = 0) โ (((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0))) |
41 | 34, 40 | mpbird 257 |
. . . . . . . . . . . . 13
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
42 | 41 | adantrl 715 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ โ โค) โง (๐พ โ โค โง ๐พ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
43 | 42 | adantllr 718 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง ๐ โ 0) โง ๐ โ โค) โง (๐พ โ โค โง ๐พ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
44 | 43 | adantlrr 720 |
. . . . . . . . . 10
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
45 | 44 | anassrs 469 |
. . . . . . . . 9
โข
(((((๐ โ
โค โง ๐ โ 0)
โง (๐ โ โค
โง ๐ โ 0)) โง
๐พ โ โค) โง
๐พ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
46 | | nnabscl 15216 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
47 | | nnabscl 15216 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
48 | | nnabscl 15216 |
. . . . . . . . . . . . . 14
โข ((๐พ โ โค โง ๐พ โ 0) โ (absโ๐พ) โ
โ) |
49 | | lcmgcdlem 16487 |
. . . . . . . . . . . . . . 15
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ ((((absโ๐) lcm (absโ๐)) ยท ((absโ๐) gcd (absโ๐))) =
(absโ((absโ๐)
ยท (absโ๐)))
โง (((absโ๐พ)
โ โ โง ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ))) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ)))) |
50 | 49 | simprd 497 |
. . . . . . . . . . . . . 14
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ (((absโ๐พ) โ โ โง
((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ))) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ))) |
51 | 48, 50 | sylani 605 |
. . . . . . . . . . . . 13
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ (((๐พ โ โค โง ๐พ โ 0) โง ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ))) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ))) |
52 | 46, 47, 51 | syl2an 597 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ (((๐พ โ โค โง ๐พ โ 0) โง ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ))) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ))) |
53 | 52 | expdimp 454 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ โ 0)) โ
(((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ))) |
54 | | dvdsabsb 16163 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ ๐ โฅ (absโ๐พ))) |
55 | | zabscl 15204 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ โ โค โ
(absโ๐พ) โ
โค) |
56 | | absdvdsb 16162 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง
(absโ๐พ) โ
โค) โ (๐ โฅ
(absโ๐พ) โ
(absโ๐) โฅ
(absโ๐พ))) |
57 | 55, 56 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ (absโ๐พ) โ (absโ๐) โฅ (absโ๐พ))) |
58 | 54, 57 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
59 | 58 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
60 | | dvdsabsb 16163 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ ๐ โฅ (absโ๐พ))) |
61 | | absdvdsb 16162 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง
(absโ๐พ) โ
โค) โ (๐ โฅ
(absโ๐พ) โ
(absโ๐) โฅ
(absโ๐พ))) |
62 | 55, 61 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ (absโ๐พ) โ (absโ๐) โฅ (absโ๐พ))) |
63 | 60, 62 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
64 | 63 | adantll 713 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
65 | 59, 64 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ)))) |
66 | 65 | bicomd 222 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
(((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
(๐ โฅ ๐พ โง ๐ โฅ ๐พ))) |
67 | | lcmabs 16486 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ๐) lcm
(absโ๐)) = (๐ lcm ๐)) |
68 | 67 | breq1d 5116 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ
(((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ) โ (๐ lcm ๐) โฅ (absโ๐พ))) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
(((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ) โ (๐ lcm ๐) โฅ (absโ๐พ))) |
70 | | dvdsabsb 16163 |
. . . . . . . . . . . . . . . . 17
โข (((๐ lcm ๐) โ โค โง ๐พ โ โค) โ ((๐ lcm ๐) โฅ ๐พ โ (๐ lcm ๐) โฅ (absโ๐พ))) |
71 | 30, 70 | sylan 581 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ ((๐ lcm ๐) โฅ ๐พ โ (๐ lcm ๐) โฅ (absโ๐พ))) |
72 | 69, 71 | bitr4d 282 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
(((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
73 | 66, 72 | imbi12d 345 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
((((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ)) โ
((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
74 | 73 | adantrr 716 |
. . . . . . . . . . . . 13
โข (((๐ โ โค โง ๐ โ โค) โง (๐พ โ โค โง ๐พ โ 0)) โ
((((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ)) โ
((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
75 | 74 | adantllr 718 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง ๐ โ 0) โง ๐ โ โค) โง (๐พ โ โค โง ๐พ โ 0)) โ ((((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ)) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
76 | 75 | adantlrr 720 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ โ 0)) โ
((((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ)) โ
((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
77 | 53, 76 | mpbid 231 |
. . . . . . . . . 10
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
78 | 77 | anassrs 469 |
. . . . . . . . 9
โข
(((((๐ โ
โค โง ๐ โ 0)
โง (๐ โ โค
โง ๐ โ 0)) โง
๐พ โ โค) โง
๐พ โ 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
79 | 45, 78 | pm2.61dane 3029 |
. . . . . . . 8
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง ๐พ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
80 | 79 | ex 414 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ (๐พ โ โค โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
81 | 80 | an4s 659 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ 0 โง ๐ โ 0)) โ (๐พ โ โค โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
82 | 28, 81 | sylan2br 596 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐พ โ โค โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
83 | 82 | impancom 453 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ (ยฌ
(๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
84 | 83 | 3impa 1111 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (ยฌ
(๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
85 | 84 | 3comr 1126 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (ยฌ
(๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
86 | 16, 27, 85 | ecase3d 1033 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |