Step | Hyp | Ref
| Expression |
1 | | divides 16139 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
2 | 1 | 3adant2 1132 |
. 2
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
3 | | zcn 12505 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
4 | 3 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ โ โ) |
5 | 4 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
6 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
7 | 6 | adantl 483 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
8 | | zcn 12505 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
9 | 8 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ โ โ) |
10 | 9 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
11 | | simpl2 1193 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ 0) |
12 | 5, 7, 10, 11 | divmul3d 11966 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ((๐ / ๐) = ๐ โ ๐ = (๐ ยท ๐))) |
13 | | eqcom 2744 |
. . . . . . . 8
โข (๐ = (๐ ยท ๐) โ (๐ ยท ๐) = ๐) |
14 | 12, 13 | bitrdi 287 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ((๐ / ๐) = ๐ โ (๐ ยท ๐) = ๐)) |
15 | 14 | biimprd 248 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ((๐ ยท ๐) = ๐ โ (๐ / ๐) = ๐)) |
16 | 15 | impr 456 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ โ โค โง (๐ ยท ๐) = ๐)) โ (๐ / ๐) = ๐) |
17 | | simprl 770 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ โ โค โง (๐ ยท ๐) = ๐)) โ ๐ โ โค) |
18 | 16, 17 | eqeltrd 2838 |
. . . 4
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ โ โค โง (๐ ยท ๐) = ๐)) โ (๐ / ๐) โ โค) |
19 | 18 | rexlimdvaa 3154 |
. . 3
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |
20 | | simpr 486 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ / ๐) โ โค) โ (๐ / ๐) โ โค) |
21 | | simp2 1138 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ โ 0) |
22 | 4, 9, 21 | divcan1d 11933 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ((๐ / ๐) ยท ๐) = ๐) |
23 | 22 | adantr 482 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ / ๐) โ โค) โ ((๐ / ๐) ยท ๐) = ๐) |
24 | | oveq1 7365 |
. . . . . . 7
โข (๐ = (๐ / ๐) โ (๐ ยท ๐) = ((๐ / ๐) ยท ๐)) |
25 | 24 | eqeq1d 2739 |
. . . . . 6
โข (๐ = (๐ / ๐) โ ((๐ ยท ๐) = ๐ โ ((๐ / ๐) ยท ๐) = ๐)) |
26 | 25 | rspcev 3582 |
. . . . 5
โข (((๐ / ๐) โ โค โง ((๐ / ๐) ยท ๐) = ๐) โ โ๐ โ โค (๐ ยท ๐) = ๐) |
27 | 20, 23, 26 | syl2anc 585 |
. . . 4
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ / ๐) โ โค) โ โ๐ โ โค (๐ ยท ๐) = ๐) |
28 | 27 | ex 414 |
. . 3
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ((๐ / ๐) โ โค โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
29 | 19, 28 | impbid 211 |
. 2
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |
30 | 2, 29 | bitrd 279 |
1
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ / ๐) โ โค)) |