Step | Hyp | Ref
| Expression |
1 | | divides 16073 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐พ) = ๐)) |
2 | 1 | 3adant3 1133 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โ (๐พ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐พ) = ๐)) |
3 | | simpl1 1192 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐พ โ
โค) |
4 | | nnnn0 12354 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
5 | 4 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โ ๐ โ
โ0) |
6 | 5 | adantr 482 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐ โ
โ0) |
7 | | zexpcl 13911 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โ0)
โ (๐พโ๐) โ
โค) |
8 | 3, 6, 7 | syl2anc 585 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ (๐พโ๐) โ โค) |
9 | | simpr 486 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐ โ
โค) |
10 | | zexpcl 13911 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ0)
โ (๐โ๐) โ
โค) |
11 | 9, 6, 10 | syl2anc 585 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ (๐โ๐) โ โค) |
12 | 11, 8 | zmulcld 12546 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ((๐โ๐) ยท (๐พโ๐)) โ โค) |
13 | | simpl3 1194 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐ โ
โ) |
14 | | iddvdsexp 16097 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โ) โ ๐พ โฅ (๐พโ๐)) |
15 | 3, 13, 14 | syl2anc 585 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐พ โฅ (๐พโ๐)) |
16 | | dvdsmul2 16096 |
. . . . . . 7
โข (((๐โ๐) โ โค โง (๐พโ๐) โ โค) โ (๐พโ๐) โฅ ((๐โ๐) ยท (๐พโ๐))) |
17 | 11, 8, 16 | syl2anc 585 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ (๐พโ๐) โฅ ((๐โ๐) ยท (๐พโ๐))) |
18 | 3, 8, 12, 15, 17 | dvdstrd 16112 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐พ โฅ ((๐โ๐) ยท (๐พโ๐))) |
19 | | zcn 12438 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
20 | 19 | adantl 483 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐ โ
โ) |
21 | | zcn 12438 |
. . . . . . . 8
โข (๐พ โ โค โ ๐พ โ
โ) |
22 | 21 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โ ๐พ โ
โ) |
23 | 22 | adantr 482 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐พ โ
โ) |
24 | 20, 23, 6 | mulexpd 13993 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ((๐ ยท ๐พ)โ๐) = ((๐โ๐) ยท (๐พโ๐))) |
25 | 18, 24 | breqtrrd 5132 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ๐พ โฅ ((๐ ยท ๐พ)โ๐)) |
26 | | oveq1 7357 |
. . . . 5
โข ((๐ ยท ๐พ) = ๐ โ ((๐ ยท ๐พ)โ๐) = (๐โ๐)) |
27 | 26 | breq2d 5116 |
. . . 4
โข ((๐ ยท ๐พ) = ๐ โ (๐พ โฅ ((๐ ยท ๐พ)โ๐) โ ๐พ โฅ (๐โ๐))) |
28 | 25, 27 | syl5ibcom 245 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โง ๐ โ โค) โ ((๐ ยท ๐พ) = ๐ โ ๐พ โฅ (๐โ๐))) |
29 | 28 | rexlimdva 3151 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โ
(โ๐ โ โค
(๐ ยท ๐พ) = ๐ โ ๐พ โฅ (๐โ๐))) |
30 | 2, 29 | sylbid 239 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐โ๐))) |