Step | Hyp | Ref
| Expression |
1 | | divides 11795 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
2 | 1 | 3adant2 1016 |
. 2
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
3 | | zcn 9257 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
4 | 3 | 3ad2ant3 1020 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ โ โ) |
5 | 4 | adantr 276 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
6 | | zcn 9257 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
7 | 6 | adantl 277 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
8 | | zcn 9257 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
9 | 8 | 3ad2ant1 1018 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ โ โ) |
10 | 9 | adantr 276 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
11 | | simpl2 1001 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ 0) |
12 | | 0z 9263 |
. . . . . . . . . . . . 13
โข 0 โ
โค |
13 | | zapne 9326 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 0 โ
โค) โ (๐ # 0
โ ๐ โ
0)) |
14 | 12, 13 | mpan2 425 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ # 0 โ ๐ โ 0)) |
15 | 14 | 3ad2ant1 1018 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (๐ # 0 โ ๐ โ 0)) |
16 | 15 | adantr 276 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ (๐ # 0 โ ๐ โ 0)) |
17 | 11, 16 | mpbird 167 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ๐ # 0) |
18 | 5, 7, 10, 17 | divmulap3d 8781 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ((๐ / ๐) = ๐ โ ๐ = (๐ ยท ๐))) |
19 | | eqcom 2179 |
. . . . . . . 8
โข (๐ = (๐ ยท ๐) โ (๐ ยท ๐) = ๐) |
20 | 18, 19 | bitrdi 196 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ((๐ / ๐) = ๐ โ (๐ ยท ๐) = ๐)) |
21 | 20 | biimprd 158 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง ๐ โ โค) โ ((๐ ยท ๐) = ๐ โ (๐ / ๐) = ๐)) |
22 | 21 | impr 379 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ โ โค โง (๐ ยท ๐) = ๐)) โ (๐ / ๐) = ๐) |
23 | | simprl 529 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ โ โค โง (๐ ยท ๐) = ๐)) โ ๐ โ โค) |
24 | 22, 23 | eqeltrd 2254 |
. . . 4
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ โ โค โง (๐ ยท ๐) = ๐)) โ (๐ / ๐) โ โค) |
25 | 24 | rexlimdvaa 2595 |
. . 3
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |
26 | | simpr 110 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ / ๐) โ โค) โ (๐ / ๐) โ โค) |
27 | | simp2 998 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ โ 0) |
28 | 27, 15 | mpbird 167 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ๐ # 0) |
29 | 4, 9, 28 | divcanap1d 8747 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ((๐ / ๐) ยท ๐) = ๐) |
30 | 29 | adantr 276 |
. . . . 5
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ / ๐) โ โค) โ ((๐ / ๐) ยท ๐) = ๐) |
31 | | oveq1 5881 |
. . . . . . 7
โข (๐ = (๐ / ๐) โ (๐ ยท ๐) = ((๐ / ๐) ยท ๐)) |
32 | 31 | eqeq1d 2186 |
. . . . . 6
โข (๐ = (๐ / ๐) โ ((๐ ยท ๐) = ๐ โ ((๐ / ๐) ยท ๐) = ๐)) |
33 | 32 | rspcev 2841 |
. . . . 5
โข (((๐ / ๐) โ โค โง ((๐ / ๐) ยท ๐) = ๐) โ โ๐ โ โค (๐ ยท ๐) = ๐) |
34 | 26, 30, 33 | syl2anc 411 |
. . . 4
โข (((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โง (๐ / ๐) โ โค) โ โ๐ โ โค (๐ ยท ๐) = ๐) |
35 | 34 | ex 115 |
. . 3
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ ((๐ / ๐) โ โค โ โ๐ โ โค (๐ ยท ๐) = ๐)) |
36 | 25, 35 | impbid 129 |
. 2
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (โ๐ โ โค (๐ ยท ๐) = ๐ โ (๐ / ๐) โ โค)) |
37 | 2, 36 | bitrd 188 |
1
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ / ๐) โ โค)) |