Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . . . . 7
โข (0
โฅ ๐พ โ 0 โฅ
๐พ) |
2 | | breq1 4006 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
3 | 2 | adantl 277 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
4 | | oveq1 5881 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ lcm ๐) = (0 lcm ๐)) |
5 | | 0z 9263 |
. . . . . . . . . . . 12
โข 0 โ
โค |
6 | | lcmcom 12063 |
. . . . . . . . . . . 12
โข ((0
โ โค โง ๐
โ โค) โ (0 lcm ๐) = (๐ lcm 0)) |
7 | 5, 6 | mpan 424 |
. . . . . . . . . . 11
โข (๐ โ โค โ (0 lcm
๐) = (๐ lcm 0)) |
8 | | lcm0val 12064 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐ lcm 0) = 0) |
9 | 7, 8 | eqtrd 2210 |
. . . . . . . . . 10
โข (๐ โ โค โ (0 lcm
๐) = 0) |
10 | 4, 9 | sylan9eqr 2232 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ = 0) โ (๐ lcm ๐) = 0) |
11 | 10 | breq1d 4013 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ = 0) โ ((๐ lcm ๐) โฅ ๐พ โ 0 โฅ ๐พ)) |
12 | 3, 11 | imbi12d 234 |
. . . . . . 7
โข ((๐ โ โค โง ๐ = 0) โ ((๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ) โ (0 โฅ ๐พ โ 0 โฅ ๐พ))) |
13 | 1, 12 | mpbiri 168 |
. . . . . 6
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
14 | 13 | 3ad2antl3 1161 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
15 | 14 | adantrd 279 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
16 | 15 | ex 115 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ = 0 โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
17 | | breq1 4006 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
18 | 17 | adantl 277 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ 0 โฅ ๐พ)) |
19 | | oveq2 5882 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐ lcm ๐) = (๐ lcm 0)) |
20 | | lcm0val 12064 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ lcm 0) = 0) |
21 | 19, 20 | sylan9eqr 2232 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ = 0) โ (๐ lcm ๐) = 0) |
22 | 21 | breq1d 4013 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ = 0) โ ((๐ lcm ๐) โฅ ๐พ โ 0 โฅ ๐พ)) |
23 | 18, 22 | imbi12d 234 |
. . . . . . 7
โข ((๐ โ โค โง ๐ = 0) โ ((๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ) โ (0 โฅ ๐พ โ 0 โฅ ๐พ))) |
24 | 1, 23 | mpbiri 168 |
. . . . . 6
โข ((๐ โ โค โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
25 | 24 | 3ad2antl2 1160 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ (๐ โฅ ๐พ โ (๐ lcm ๐) โฅ ๐พ)) |
26 | 25 | adantld 278 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
27 | 26 | ex 115 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ = 0 โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
28 | 16, 27 | jaod 717 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
29 | | neanior 2434 |
. . . . . 6
โข ((๐ โ 0 โง ๐ โ 0) โ ยฌ (๐ = 0 โจ ๐ = 0)) |
30 | | lcmcl 12071 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โ
โ0) |
31 | 30 | nn0zd 9372 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โ โค) |
32 | | dvds0 11812 |
. . . . . . . . . . . . . . . . 17
โข ((๐ lcm ๐) โ โค โ (๐ lcm ๐) โฅ 0) |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โฅ 0) |
34 | 33 | a1d 22 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0)) |
35 | 34 | adantr 276 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ = 0) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0)) |
36 | | breq2 4007 |
. . . . . . . . . . . . . . . . 17
โข (๐พ = 0 โ (๐ โฅ ๐พ โ ๐ โฅ 0)) |
37 | | breq2 4007 |
. . . . . . . . . . . . . . . . 17
โข (๐พ = 0 โ (๐ โฅ ๐พ โ ๐ โฅ 0)) |
38 | 36, 37 | anbi12d 473 |
. . . . . . . . . . . . . . . 16
โข (๐พ = 0 โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ โฅ 0 โง ๐ โฅ 0))) |
39 | | breq2 4007 |
. . . . . . . . . . . . . . . 16
โข (๐พ = 0 โ ((๐ lcm ๐) โฅ ๐พ โ (๐ lcm ๐) โฅ 0)) |
40 | 38, 39 | imbi12d 234 |
. . . . . . . . . . . . . . 15
โข (๐พ = 0 โ (((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0))) |
41 | 40 | adantl 277 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ = 0) โ (((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ) โ ((๐ โฅ 0 โง ๐ โฅ 0) โ (๐ lcm ๐) โฅ 0))) |
42 | 35, 41 | mpbird 167 |
. . . . . . . . . . . . 13
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
43 | 42 | adantrl 478 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ โ โค) โง (๐พ โ โค โง ๐พ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
44 | 43 | adantllr 481 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง ๐ โ 0) โง ๐ โ โค) โง (๐พ โ โค โง ๐พ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
45 | 44 | adantlrr 483 |
. . . . . . . . . 10
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
46 | 45 | anassrs 400 |
. . . . . . . . 9
โข
(((((๐ โ
โค โง ๐ โ 0)
โง (๐ โ โค
โง ๐ โ 0)) โง
๐พ โ โค) โง
๐พ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
47 | | nnabscl 11108 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
48 | | nnabscl 11108 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
49 | | nnabscl 11108 |
. . . . . . . . . . . . . 14
โข ((๐พ โ โค โง ๐พ โ 0) โ (absโ๐พ) โ
โ) |
50 | | lcmgcdlem 12076 |
. . . . . . . . . . . . . . 15
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ ((((absโ๐) lcm (absโ๐)) ยท ((absโ๐) gcd (absโ๐))) =
(absโ((absโ๐)
ยท (absโ๐)))
โง (((absโ๐พ)
โ โ โง ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ))) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ)))) |
51 | 50 | simprd 114 |
. . . . . . . . . . . . . 14
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ (((absโ๐พ) โ โ โง
((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ))) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ))) |
52 | 49, 51 | sylani 406 |
. . . . . . . . . . . . 13
โข
(((absโ๐)
โ โ โง (absโ๐) โ โ) โ (((๐พ โ โค โง ๐พ โ 0) โง ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ))) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ))) |
53 | 47, 48, 52 | syl2an 289 |
. . . . . . . . . . . 12
โข (((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ (((๐พ โ โค โง ๐พ โ 0) โง ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ))) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ))) |
54 | 53 | expdimp 259 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ โ 0)) โ
(((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ))) |
55 | | dvdsabsb 11816 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ ๐ โฅ (absโ๐พ))) |
56 | | zabscl 11094 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ โ โค โ
(absโ๐พ) โ
โค) |
57 | | absdvdsb 11815 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง
(absโ๐พ) โ
โค) โ (๐ โฅ
(absโ๐พ) โ
(absโ๐) โฅ
(absโ๐พ))) |
58 | 56, 57 | sylan2 286 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ (absโ๐พ) โ (absโ๐) โฅ (absโ๐พ))) |
59 | 55, 58 | bitrd 188 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
60 | 59 | adantlr 477 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
61 | | dvdsabsb 11816 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ ๐ โฅ (absโ๐พ))) |
62 | | absdvdsb 11815 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง
(absโ๐พ) โ
โค) โ (๐ โฅ
(absโ๐พ) โ
(absโ๐) โฅ
(absโ๐พ))) |
63 | 56, 62 | sylan2 286 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ (absโ๐พ) โ (absโ๐) โฅ (absโ๐พ))) |
64 | 61, 63 | bitrd 188 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
65 | 64 | adantll 476 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ (๐ โฅ ๐พ โ (absโ๐) โฅ (absโ๐พ))) |
66 | 60, 65 | anbi12d 473 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ ((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ)))) |
67 | 66 | bicomd 141 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
(((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
(๐ โฅ ๐พ โง ๐ โฅ ๐พ))) |
68 | | lcmabs 12075 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ๐) lcm
(absโ๐)) = (๐ lcm ๐)) |
69 | 68 | breq1d 4013 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ
(((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ) โ (๐ lcm ๐) โฅ (absโ๐พ))) |
70 | 69 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
(((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ) โ (๐ lcm ๐) โฅ (absโ๐พ))) |
71 | | dvdsabsb 11816 |
. . . . . . . . . . . . . . . . 17
โข (((๐ lcm ๐) โ โค โง ๐พ โ โค) โ ((๐ lcm ๐) โฅ ๐พ โ (๐ lcm ๐) โฅ (absโ๐พ))) |
72 | 31, 71 | sylan 283 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ ((๐ lcm ๐) โฅ ๐พ โ (๐ lcm ๐) โฅ (absโ๐พ))) |
73 | 70, 72 | bitr4d 191 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
(((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
74 | 67, 73 | imbi12d 234 |
. . . . . . . . . . . . . 14
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ
((((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ)) โ
((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
75 | 74 | adantrr 479 |
. . . . . . . . . . . . 13
โข (((๐ โ โค โง ๐ โ โค) โง (๐พ โ โค โง ๐พ โ 0)) โ
((((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ)) โ
((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
76 | 75 | adantllr 481 |
. . . . . . . . . . . 12
โข ((((๐ โ โค โง ๐ โ 0) โง ๐ โ โค) โง (๐พ โ โค โง ๐พ โ 0)) โ ((((absโ๐) โฅ (absโ๐พ) โง (absโ๐) โฅ (absโ๐พ)) โ ((absโ๐) lcm (absโ๐)) โฅ (absโ๐พ)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
77 | 76 | adantlrr 483 |
. . . . . . . . . . 11
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ โ 0)) โ
((((absโ๐) โฅ
(absโ๐พ) โง
(absโ๐) โฅ
(absโ๐พ)) โ
((absโ๐) lcm
(absโ๐)) โฅ
(absโ๐พ)) โ
((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
78 | 54, 77 | mpbid 147 |
. . . . . . . . . 10
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
79 | 78 | anassrs 400 |
. . . . . . . . 9
โข
(((((๐ โ
โค โง ๐ โ 0)
โง (๐ โ โค
โง ๐ โ 0)) โง
๐พ โ โค) โง
๐พ โ 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
80 | | zdceq 9327 |
. . . . . . . . . . . . 13
โข ((๐พ โ โค โง 0 โ
โค) โ DECID ๐พ = 0) |
81 | 5, 80 | mpan2 425 |
. . . . . . . . . . . 12
โข (๐พ โ โค โ
DECID ๐พ =
0) |
82 | | exmiddc 836 |
. . . . . . . . . . . 12
โข
(DECID ๐พ = 0 โ (๐พ = 0 โจ ยฌ ๐พ = 0)) |
83 | 81, 82 | syl 14 |
. . . . . . . . . . 11
โข (๐พ โ โค โ (๐พ = 0 โจ ยฌ ๐พ = 0)) |
84 | | df-ne 2348 |
. . . . . . . . . . . 12
โข (๐พ โ 0 โ ยฌ ๐พ = 0) |
85 | 84 | orbi2i 762 |
. . . . . . . . . . 11
โข ((๐พ = 0 โจ ๐พ โ 0) โ (๐พ = 0 โจ ยฌ ๐พ = 0)) |
86 | 83, 85 | sylibr 134 |
. . . . . . . . . 10
โข (๐พ โ โค โ (๐พ = 0 โจ ๐พ โ 0)) |
87 | 86 | adantl 277 |
. . . . . . . . 9
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง ๐พ โ โค) โ (๐พ = 0 โจ ๐พ โ 0)) |
88 | 46, 79, 87 | mpjaodan 798 |
. . . . . . . 8
โข ((((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โง ๐พ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |
89 | 88 | ex 115 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ (๐พ โ โค โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
90 | 89 | an4s 588 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ 0 โง ๐ โ 0)) โ (๐พ โ โค โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
91 | 29, 90 | sylan2br 288 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โจ ๐ = 0)) โ (๐พ โ โค โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
92 | 91 | impancom 260 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง ๐พ โ โค) โ (ยฌ
(๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
93 | 92 | 3impa 1194 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (ยฌ
(๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
94 | 93 | 3comr 1211 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (ยฌ
(๐ = 0 โจ ๐ = 0) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ))) |
95 | | lcmmndc 12061 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ
DECID (๐ = 0
โจ ๐ =
0)) |
96 | | exmiddc 836 |
. . . 4
โข
(DECID (๐ = 0 โจ ๐ = 0) โ ((๐ = 0 โจ ๐ = 0) โจ ยฌ (๐ = 0 โจ ๐ = 0))) |
97 | 95, 96 | syl 14 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ = 0 โจ ๐ = 0) โจ ยฌ (๐ = 0 โจ ๐ = 0))) |
98 | 97 | 3adant1 1015 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ = 0 โจ ๐ = 0) โจ ยฌ (๐ = 0 โจ ๐ = 0))) |
99 | 28, 94, 98 | mpjaod 718 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) |