Step | Hyp | Ref
| Expression |
1 | | nnproddivdvdsd.3 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
2 | 1 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
3 | 2 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐ โ โ) |
4 | | nnproddivdvdsd.1 |
. . . . . . . . . 10
โข (๐ โ ๐พ โ โ) |
5 | 4 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ ๐พ โ โ) |
6 | 5 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐พ โ โ) |
7 | | nnproddivdvdsd.2 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
8 | 7 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
9 | 8 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐ โ โ) |
10 | 4 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐พ โ โ) |
11 | | nnne0 12194 |
. . . . . . . . 9
โข (๐พ โ โ โ ๐พ โ 0) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐พ โ 0) |
13 | 7 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐ โ โ) |
14 | 13 | nnne0d 12210 |
. . . . . . . 8
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐ โ 0) |
15 | 3, 6, 9, 12, 14 | divdiv1d 11969 |
. . . . . . 7
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ((๐ / ๐พ) / ๐) = (๐ / (๐พ ยท ๐))) |
16 | 15 | eqcomd 2743 |
. . . . . 6
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ (๐ / (๐พ ยท ๐)) = ((๐ / ๐พ) / ๐)) |
17 | 3, 6, 9, 12, 14 | divdiv32d 11963 |
. . . . . 6
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ((๐ / ๐พ) / ๐) = ((๐ / ๐) / ๐พ)) |
18 | 16, 17 | eqtrd 2777 |
. . . . 5
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ (๐ / (๐พ ยท ๐)) = ((๐ / ๐) / ๐พ)) |
19 | 4, 7 | nnmulcld 12213 |
. . . . . . . 8
โข (๐ โ (๐พ ยท ๐) โ โ) |
20 | 19, 1 | nndivdvdsd 40486 |
. . . . . . 7
โข (๐ โ ((๐พ ยท ๐) โฅ ๐ โ (๐ / (๐พ ยท ๐)) โ โ)) |
21 | 20 | biimpd 228 |
. . . . . 6
โข (๐ โ ((๐พ ยท ๐) โฅ ๐ โ (๐ / (๐พ ยท ๐)) โ โ)) |
22 | 21 | imp 408 |
. . . . 5
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ (๐ / (๐พ ยท ๐)) โ โ) |
23 | 18, 22 | eqeltrrd 2839 |
. . . 4
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ((๐ / ๐) / ๐พ) โ โ) |
24 | 4 | nnzd 12533 |
. . . . . . . . 9
โข (๐ โ ๐พ โ โค) |
25 | 7 | nnzd 12533 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
26 | 1 | nnzd 12533 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
27 | 24, 25, 26 | 3jca 1129 |
. . . . . . . 8
โข (๐ โ (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) |
28 | | muldvds2 16171 |
. . . . . . . 8
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โฅ ๐ โ ๐ โฅ ๐)) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (๐ โ ((๐พ ยท ๐) โฅ ๐ โ ๐ โฅ ๐)) |
30 | 29 | imp 408 |
. . . . . 6
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐ โฅ ๐) |
31 | 1 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐ โ โ) |
32 | 13, 31 | nndivdvdsd 40486 |
. . . . . 6
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
33 | 30, 32 | mpbid 231 |
. . . . 5
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ (๐ / ๐) โ โ) |
34 | 10, 33 | nndivdvdsd 40486 |
. . . 4
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ (๐พ โฅ (๐ / ๐) โ ((๐ / ๐) / ๐พ) โ โ)) |
35 | 23, 34 | mpbird 257 |
. . 3
โข ((๐ โง (๐พ ยท ๐) โฅ ๐) โ ๐พ โฅ (๐ / ๐)) |
36 | 35 | ex 414 |
. 2
โข (๐ โ ((๐พ ยท ๐) โฅ ๐ โ ๐พ โฅ (๐ / ๐))) |
37 | | dvdszrcl 16148 |
. . . . . . 7
โข (๐พ โฅ (๐ / ๐) โ (๐พ โ โค โง (๐ / ๐) โ โค)) |
38 | 37 | simprd 497 |
. . . . . 6
โข (๐พ โฅ (๐ / ๐) โ (๐ / ๐) โ โค) |
39 | 38 | adantl 483 |
. . . . 5
โข ((๐ โง ๐พ โฅ (๐ / ๐)) โ (๐ / ๐) โ โค) |
40 | | dvdsmulc 16173 |
. . . . . . . . 9
โข ((๐พ โ โค โง (๐ / ๐) โ โค โง ๐ โ โค) โ (๐พ โฅ (๐ / ๐) โ (๐พ ยท ๐) โฅ ((๐ / ๐) ยท ๐))) |
41 | 24, 40 | syl3an1 1164 |
. . . . . . . 8
โข ((๐ โง (๐ / ๐) โ โค โง ๐ โ โค) โ (๐พ โฅ (๐ / ๐) โ (๐พ ยท ๐) โฅ ((๐ / ๐) ยท ๐))) |
42 | 25, 41 | syl3an3 1166 |
. . . . . . 7
โข ((๐ โง (๐ / ๐) โ โค โง ๐) โ (๐พ โฅ (๐ / ๐) โ (๐พ ยท ๐) โฅ ((๐ / ๐) ยท ๐))) |
43 | 42 | 3anidm13 1421 |
. . . . . 6
โข ((๐ โง (๐ / ๐) โ โค) โ (๐พ โฅ (๐ / ๐) โ (๐พ ยท ๐) โฅ ((๐ / ๐) ยท ๐))) |
44 | 43 | impancom 453 |
. . . . 5
โข ((๐ โง ๐พ โฅ (๐ / ๐)) โ ((๐ / ๐) โ โค โ (๐พ ยท ๐) โฅ ((๐ / ๐) ยท ๐))) |
45 | 39, 44 | mpd 15 |
. . . 4
โข ((๐ โง ๐พ โฅ (๐ / ๐)) โ (๐พ ยท ๐) โฅ ((๐ / ๐) ยท ๐)) |
46 | 7 | nnne0d 12210 |
. . . . . 6
โข (๐ โ ๐ โ 0) |
47 | 2, 8, 46 | divcan1d 11939 |
. . . . 5
โข (๐ โ ((๐ / ๐) ยท ๐) = ๐) |
48 | 47 | adantr 482 |
. . . 4
โข ((๐ โง ๐พ โฅ (๐ / ๐)) โ ((๐ / ๐) ยท ๐) = ๐) |
49 | 45, 48 | breqtrd 5136 |
. . 3
โข ((๐ โง ๐พ โฅ (๐ / ๐)) โ (๐พ ยท ๐) โฅ ๐) |
50 | 49 | ex 414 |
. 2
โข (๐ โ (๐พ โฅ (๐ / ๐) โ (๐พ ยท ๐) โฅ ๐)) |
51 | 36, 50 | impbid 211 |
1
โข (๐ โ ((๐พ ยท ๐) โฅ ๐ โ ๐พ โฅ (๐ / ๐))) |