Step | Hyp | Ref
| Expression |
1 | | 3simpa 995 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โ โค โง ๐ โ
โค)) |
2 | | 3simpb 996 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โ โค โง ๐ โ
โค)) |
3 | | zaddcl 9306 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + ๐) โ โค) |
4 | 3 | anim2i 342 |
. . 3
โข ((๐พ โ โค โง (๐ โ โค โง ๐ โ โค)) โ (๐พ โ โค โง (๐ + ๐) โ โค)) |
5 | 4 | 3impb 1200 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โ โค โง (๐ + ๐) โ โค)) |
6 | | zaddcl 9306 |
. . 3
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ + ๐ฆ) โ โค) |
7 | 6 | adantl 277 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ + ๐ฆ) โ โค) |
8 | | zcn 9271 |
. . . . . . . 8
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
9 | | zcn 9271 |
. . . . . . . 8
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
10 | | zcn 9271 |
. . . . . . . 8
โข (๐พ โ โค โ ๐พ โ
โ) |
11 | | adddir 7961 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐พ โ โ) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) + (๐ฆ ยท ๐พ))) |
12 | 8, 9, 10, 11 | syl3an 1290 |
. . . . . . 7
โข ((๐ฅ โ โค โง ๐ฆ โ โค โง ๐พ โ โค) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) + (๐ฆ ยท ๐พ))) |
13 | 12 | 3comr 1212 |
. . . . . 6
โข ((๐พ โ โค โง ๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) + (๐ฆ ยท ๐พ))) |
14 | 13 | 3expb 1205 |
. . . . 5
โข ((๐พ โ โค โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) + (๐ฆ ยท ๐พ))) |
15 | | oveq12 5897 |
. . . . 5
โข (((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ฅ ยท ๐พ) + (๐ฆ ยท ๐พ)) = (๐ + ๐)) |
16 | 14, 15 | sylan9eq 2240 |
. . . 4
โข (((๐พ โ โค โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐)) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = (๐ + ๐)) |
17 | 16 | ex 115 |
. . 3
โข ((๐พ โ โค โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = (๐ + ๐))) |
18 | 17 | 3ad2antl1 1160 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ฅ + ๐ฆ) ยท ๐พ) = (๐ + ๐))) |
19 | 1, 2, 5, 7, 18 | dvds2lem 11823 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ + ๐))) |