Step | Hyp | Ref
| Expression |
1 | | nnne0 12188 |
. . 3
โข (๐ โ โ โ ๐ โ 0) |
2 | 1 | adantr 482 |
. 2
โข ((๐ โ โ โง ๐ โ โค) โ ๐ โ 0) |
3 | | nncn 12162 |
. . 3
โข (๐ โ โ โ ๐ โ
โ) |
4 | | zcn 12505 |
. . 3
โข (๐ โ โค โ ๐ โ
โ) |
5 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
6 | | divcan3 11840 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ ((๐ ยท ๐) / ๐) = ๐) |
7 | 6 | 3coml 1128 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ 0 โง ๐ โ โ) โ ((๐ ยท ๐) / ๐) = ๐) |
8 | 7 | 3expa 1119 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ 0) โง ๐ โ โ) โ ((๐ ยท ๐) / ๐) = ๐) |
9 | 5, 8 | sylan2 594 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ 0) โง ๐ โ โค) โ ((๐ ยท ๐) / ๐) = ๐) |
10 | 9 | 3adantl2 1168 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โง ๐ โ โค) โ ((๐ ยท ๐) / ๐) = ๐) |
11 | | oveq1 7365 |
. . . . . . . 8
โข ((๐ ยท ๐) = ๐ โ ((๐ ยท ๐) / ๐) = (๐ / ๐)) |
12 | 10, 11 | sylan9req 2798 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โง ๐ โ โค) โง (๐ ยท ๐) = ๐) โ ๐ = (๐ / ๐)) |
13 | | simplr 768 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โง ๐ โ โค) โง (๐ ยท ๐) = ๐) โ ๐ โ โค) |
14 | 12, 13 | eqeltrrd 2839 |
. . . . . 6
โข ((((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โง ๐ โ โค) โง (๐ ยท ๐) = ๐) โ (๐ / ๐) โ โค) |
15 | 14 | rexlimdva2 3155 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |
16 | | divcan2 11822 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ (๐ ยท (๐ / ๐)) = ๐) |
17 | 16 | 3com12 1124 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ (๐ ยท (๐ / ๐)) = ๐) |
18 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = (๐ / ๐) โ (๐ ยท ๐) = (๐ ยท (๐ / ๐))) |
19 | 18 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ = (๐ / ๐) โ ((๐ ยท ๐) = ๐ โ (๐ ยท (๐ / ๐)) = ๐)) |
20 | 19 | rspcev 3582 |
. . . . . . 7
โข (((๐ / ๐) โ โค โง (๐ ยท (๐ / ๐)) = ๐) โ โ๐ โ โค (๐ ยท ๐) = ๐) |
21 | 20 | expcom 415 |
. . . . . 6
โข ((๐ ยท (๐ / ๐)) = ๐ โ ((๐ / ๐) โ โค โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
22 | 17, 21 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ ((๐ / ๐) โ โค โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
23 | 15, 22 | impbid 211 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ โง ๐ โ 0) โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |
24 | 23 | 3expia 1122 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ 0 โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค))) |
25 | 3, 4, 24 | syl2an 597 |
. 2
โข ((๐ โ โ โง ๐ โ โค) โ (๐ โ 0 โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค))) |
26 | 2, 25 | mpd 15 |
1
โข ((๐ โ โ โง ๐ โ โค) โ
(โ๐ โ โค
(๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |