Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . 3
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐พ โ
โค) |
2 | | simpr2 1196 |
. . 3
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐ โ
โค) |
3 | 1, 2 | jca 513 |
. 2
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ (๐พ โ โค โง ๐ โ
โค)) |
4 | | simpr3 1197 |
. . 3
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐ โ
โค) |
5 | 1, 4 | jca 513 |
. 2
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ (๐พ โ โค โง ๐ โ
โค)) |
6 | | simpll 766 |
. . . . 5
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐ผ โ
โค) |
7 | 6, 2 | zmulcld 12546 |
. . . 4
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ (๐ผ ยท ๐) โ โค) |
8 | | simplr 768 |
. . . . 5
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐ฝ โ
โค) |
9 | 8, 4 | zmulcld 12546 |
. . . 4
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ (๐ฝ ยท ๐) โ โค) |
10 | 7, 9 | zaddcld 12544 |
. . 3
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ((๐ผ ยท ๐) + (๐ฝ ยท ๐)) โ โค) |
11 | 1, 10 | jca 513 |
. 2
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ (๐พ โ โค โง ((๐ผ ยท ๐) + (๐ฝ ยท ๐)) โ โค)) |
12 | | zmulcl 12483 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ผ โ โค) โ (๐ฅ ยท ๐ผ) โ โค) |
13 | | zmulcl 12483 |
. . . . . . . 8
โข ((๐ฆ โ โค โง ๐ฝ โ โค) โ (๐ฆ ยท ๐ฝ) โ โค) |
14 | 12, 13 | anim12i 614 |
. . . . . . 7
โข (((๐ฅ โ โค โง ๐ผ โ โค) โง (๐ฆ โ โค โง ๐ฝ โ โค)) โ ((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค)) |
15 | 14 | an4s 659 |
. . . . . 6
โข (((๐ฅ โ โค โง ๐ฆ โ โค) โง (๐ผ โ โค โง ๐ฝ โ โค)) โ ((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค)) |
16 | 15 | expcom 415 |
. . . . 5
โข ((๐ผ โ โค โง ๐ฝ โ โค) โ ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค))) |
17 | 16 | adantr 482 |
. . . 4
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค))) |
18 | 17 | imp 408 |
. . 3
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค)) |
19 | | zaddcl 12474 |
. . 3
โข (((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค) โ ((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) โ โค) |
20 | 18, 19 | syl 17 |
. 2
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) โ โค) |
21 | | zcn 12438 |
. . . . . . . 8
โข ((๐ฅ ยท ๐ผ) โ โค โ (๐ฅ ยท ๐ผ) โ โ) |
22 | | zcn 12438 |
. . . . . . . 8
โข ((๐ฆ ยท ๐ฝ) โ โค โ (๐ฆ ยท ๐ฝ) โ โ) |
23 | 21, 22 | anim12i 614 |
. . . . . . 7
โข (((๐ฅ ยท ๐ผ) โ โค โง (๐ฆ ยท ๐ฝ) โ โค) โ ((๐ฅ ยท ๐ผ) โ โ โง (๐ฆ ยท ๐ฝ) โ โ)) |
24 | 18, 23 | syl 17 |
. . . . . 6
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐ผ) โ โ โง (๐ฆ ยท ๐ฝ) โ โ)) |
25 | 1 | zcnd 12541 |
. . . . . . 7
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐พ โ
โ) |
26 | 25 | adantr 482 |
. . . . . 6
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐พ โ
โ) |
27 | | adddir 11080 |
. . . . . . 7
โข (((๐ฅ ยท ๐ผ) โ โ โง (๐ฆ ยท ๐ฝ) โ โ โง ๐พ โ โ) โ (((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) ยท ๐พ) = (((๐ฅ ยท ๐ผ) ยท ๐พ) + ((๐ฆ ยท ๐ฝ) ยท ๐พ))) |
28 | 27 | 3expa 1119 |
. . . . . 6
โข ((((๐ฅ ยท ๐ผ) โ โ โง (๐ฆ ยท ๐ฝ) โ โ) โง ๐พ โ โ) โ (((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) ยท ๐พ) = (((๐ฅ ยท ๐ผ) ยท ๐พ) + ((๐ฆ ยท ๐ฝ) ยท ๐พ))) |
29 | 24, 26, 28 | syl2anc 585 |
. . . . 5
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) ยท ๐พ) = (((๐ฅ ยท ๐ผ) ยท ๐พ) + ((๐ฆ ยท ๐ฝ) ยท ๐พ))) |
30 | | zcn 12438 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
31 | 30 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ๐ฅ โ
โ) |
32 | 31 | adantl 483 |
. . . . . . 7
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ
โ) |
33 | | zcn 12438 |
. . . . . . . 8
โข (๐ผ โ โค โ ๐ผ โ
โ) |
34 | 33 | ad3antrrr 729 |
. . . . . . 7
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ผ โ
โ) |
35 | 32, 34, 26 | mul32d 11299 |
. . . . . 6
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐ผ) ยท ๐พ) = ((๐ฅ ยท ๐พ) ยท ๐ผ)) |
36 | | zcn 12438 |
. . . . . . . . 9
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
37 | 36 | adantl 483 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ๐ฆ โ
โ) |
38 | 37 | adantl 483 |
. . . . . . 7
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ
โ) |
39 | 8 | zcnd 12541 |
. . . . . . . 8
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ๐ฝ โ
โ) |
40 | 39 | adantr 482 |
. . . . . . 7
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฝ โ
โ) |
41 | 38, 40, 26 | mul32d 11299 |
. . . . . 6
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฆ ยท ๐ฝ) ยท ๐พ) = ((๐ฆ ยท ๐พ) ยท ๐ฝ)) |
42 | 35, 41 | oveq12d 7368 |
. . . . 5
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐ผ) ยท ๐พ) + ((๐ฆ ยท ๐ฝ) ยท ๐พ)) = (((๐ฅ ยท ๐พ) ยท ๐ผ) + ((๐ฆ ยท ๐พ) ยท ๐ฝ))) |
43 | 32, 26 | mulcld 11109 |
. . . . . . 7
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ๐พ) โ โ) |
44 | 43, 34 | mulcomd 11110 |
. . . . . 6
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐พ) ยท ๐ผ) = (๐ผ ยท (๐ฅ ยท ๐พ))) |
45 | 38, 26 | mulcld 11109 |
. . . . . . 7
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฆ ยท ๐พ) โ โ) |
46 | 45, 40 | mulcomd 11110 |
. . . . . 6
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฆ ยท ๐พ) ยท ๐ฝ) = (๐ฝ ยท (๐ฆ ยท ๐พ))) |
47 | 44, 46 | oveq12d 7368 |
. . . . 5
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐พ) ยท ๐ผ) + ((๐ฆ ยท ๐พ) ยท ๐ฝ)) = ((๐ผ ยท (๐ฅ ยท ๐พ)) + (๐ฝ ยท (๐ฆ ยท ๐พ)))) |
48 | 29, 42, 47 | 3eqtrd 2782 |
. . . 4
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) ยท ๐พ) = ((๐ผ ยท (๐ฅ ยท ๐พ)) + (๐ฝ ยท (๐ฆ ยท ๐พ)))) |
49 | | oveq2 7358 |
. . . . 5
โข ((๐ฅ ยท ๐พ) = ๐ โ (๐ผ ยท (๐ฅ ยท ๐พ)) = (๐ผ ยท ๐)) |
50 | | oveq2 7358 |
. . . . 5
โข ((๐ฆ ยท ๐พ) = ๐ โ (๐ฝ ยท (๐ฆ ยท ๐พ)) = (๐ฝ ยท ๐)) |
51 | 49, 50 | oveqan12d 7369 |
. . . 4
โข (((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ผ ยท (๐ฅ ยท ๐พ)) + (๐ฝ ยท (๐ฆ ยท ๐พ))) = ((๐ผ ยท ๐) + (๐ฝ ยท ๐))) |
52 | 48, 51 | sylan9eq 2798 |
. . 3
โข
(((((๐ผ โ
โค โง ๐ฝ โ
โค) โง (๐พ โ
โค โง ๐ โ
โค โง ๐ โ
โค)) โง (๐ฅ โ
โค โง ๐ฆ โ
โค)) โง ((๐ฅ
ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐)) โ (((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) ยท ๐พ) = ((๐ผ ยท ๐) + (๐ฝ ยท ๐))) |
53 | 52 | ex 414 |
. 2
โข ((((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ (((๐ฅ ยท ๐ผ) + (๐ฆ ยท ๐ฝ)) ยท ๐พ) = ((๐ผ ยท ๐) + (๐ฝ ยท ๐)))) |
54 | 3, 5, 11, 20, 53 | dvds2lem 16086 |
1
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ ((๐ผ ยท ๐) + (๐ฝ ยท ๐)))) |