Step | Hyp | Ref
| Expression |
1 | | elq 12874 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ด = (๐ฅ / ๐ฆ)) |
2 | | nnne0 12186 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ 0) |
3 | 2 | ancli 549 |
. . . . . 6
โข (๐ฆ โ โ โ (๐ฆ โ โ โง ๐ฆ โ 0)) |
4 | | neeq1 3006 |
. . . . . . . . . 10
โข (๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (๐ฅ / ๐ฆ) โ 0)) |
5 | | zcn 12503 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
6 | | nncn 12160 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
7 | 5, 6 | anim12i 613 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ (๐ฅ โ โ โง ๐ฆ โ
โ)) |
8 | | divne0b 11823 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฆ โ 0) โ (๐ฅ โ 0 โ (๐ฅ / ๐ฆ) โ 0)) |
9 | 8 | 3expa 1118 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ฆ โ 0) โ (๐ฅ โ 0 โ (๐ฅ / ๐ฆ) โ 0)) |
10 | 7, 9 | sylan 580 |
. . . . . . . . . . 11
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โ (๐ฅ โ 0 โ (๐ฅ / ๐ฆ) โ 0)) |
11 | 10 | bicomd 222 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โ ((๐ฅ / ๐ฆ) โ 0 โ ๐ฅ โ 0)) |
12 | 4, 11 | sylan9bbr 511 |
. . . . . . . . 9
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โง ๐ด = (๐ฅ / ๐ฆ)) โ (๐ด โ 0 โ ๐ฅ โ 0)) |
13 | | nnz 12519 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
14 | | zmulcl 12551 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ ยท ๐ฆ) โ โค) |
15 | 13, 14 | sylan2 593 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) โ โค) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฅ โ 0) โ (๐ฅ ยท ๐ฆ) โ โค) |
17 | | msqznn 12584 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ๐ฅ โ 0) โ (๐ฅ ยท ๐ฅ) โ โ) |
18 | 17 | adantlr 713 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฅ โ 0) โ (๐ฅ ยท ๐ฅ) โ โ) |
19 | 16, 18 | jca 512 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฅ โ 0) โ ((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ)) |
20 | 19 | adantlr 713 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โง ๐ฅ โ 0) โ ((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ)) |
21 | 20 | adantlr 713 |
. . . . . . . . . . 11
โข
(((((๐ฅ โ
โค โง ๐ฆ โ
โ) โง ๐ฆ โ 0)
โง ๐ด = (๐ฅ / ๐ฆ)) โง ๐ฅ โ 0) โ ((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ)) |
22 | | oveq2 7364 |
. . . . . . . . . . . . 13
โข (๐ด = (๐ฅ / ๐ฆ) โ (1 / ๐ด) = (1 / (๐ฅ / ๐ฆ))) |
23 | | divid 11841 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ โ โง ๐ฅ โ 0) โ (๐ฅ / ๐ฅ) = 1) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ (๐ฅ / ๐ฅ) = 1) |
25 | 24 | oveq1d 7371 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ ((๐ฅ / ๐ฅ) / (๐ฅ / ๐ฆ)) = (1 / (๐ฅ / ๐ฆ))) |
26 | | simpll 765 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ ๐ฅ โ
โ) |
27 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ (๐ฅ โ โ โง ๐ฅ โ 0)) |
28 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ (๐ฆ โ โ โง ๐ฆ โ 0)) |
29 | | divdivdiv 11855 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฅ โ โ โง (๐ฅ โ โ โง ๐ฅ โ 0)) โง ((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0))) โ ((๐ฅ / ๐ฅ) / (๐ฅ / ๐ฆ)) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
30 | 26, 27, 27, 28, 29 | syl22anc 837 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ ((๐ฅ / ๐ฅ) / (๐ฅ / ๐ฆ)) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
31 | 25, 30 | eqtr3d 2778 |
. . . . . . . . . . . . . . . 16
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ (1 / (๐ฅ / ๐ฆ)) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
32 | 31 | an4s 658 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ฅ โ 0 โง ๐ฆ โ 0)) โ (1 / (๐ฅ / ๐ฆ)) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
33 | 7, 32 | sylan 580 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ฅ โ 0 โง ๐ฆ โ 0)) โ (1 / (๐ฅ / ๐ฆ)) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
34 | 33 | anass1rs 653 |
. . . . . . . . . . . . 13
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โง ๐ฅ โ 0) โ (1 / (๐ฅ / ๐ฆ)) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
35 | 22, 34 | sylan9eqr 2798 |
. . . . . . . . . . . 12
โข
(((((๐ฅ โ
โค โง ๐ฆ โ
โ) โง ๐ฆ โ 0)
โง ๐ฅ โ 0) โง ๐ด = (๐ฅ / ๐ฆ)) โ (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
36 | 35 | an32s 650 |
. . . . . . . . . . 11
โข
(((((๐ฅ โ
โค โง ๐ฆ โ
โ) โง ๐ฆ โ 0)
โง ๐ด = (๐ฅ / ๐ฆ)) โง ๐ฅ โ 0) โ (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) |
37 | 21, 36 | jca 512 |
. . . . . . . . . 10
โข
(((((๐ฅ โ
โค โง ๐ฆ โ
โ) โง ๐ฆ โ 0)
โง ๐ด = (๐ฅ / ๐ฆ)) โง ๐ฅ โ 0) โ (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ)))) |
38 | 37 | ex 413 |
. . . . . . . . 9
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โง ๐ด = (๐ฅ / ๐ฆ)) โ (๐ฅ โ 0 โ (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))))) |
39 | 12, 38 | sylbid 239 |
. . . . . . . 8
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โง ๐ด = (๐ฅ / ๐ฆ)) โ (๐ด โ 0 โ (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))))) |
40 | 39 | ex 413 |
. . . . . . 7
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ฆ โ 0) โ (๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ)))))) |
41 | 40 | anasss 467 |
. . . . . 6
โข ((๐ฅ โ โค โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ (๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ)))))) |
42 | 3, 41 | sylan2 593 |
. . . . 5
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ (๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ)))))) |
43 | | rspceov 7403 |
. . . . . . 7
โข (((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) โ โ๐ง โ โค โ๐ค โ โ (1 / ๐ด) = (๐ง / ๐ค)) |
44 | 43 | 3expa 1118 |
. . . . . 6
โข ((((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) โ โ๐ง โ โค โ๐ค โ โ (1 / ๐ด) = (๐ง / ๐ค)) |
45 | | elq 12874 |
. . . . . 6
โข ((1 /
๐ด) โ โ โ
โ๐ง โ โค
โ๐ค โ โ (1
/ ๐ด) = (๐ง / ๐ค)) |
46 | 44, 45 | sylibr 233 |
. . . . 5
โข ((((๐ฅ ยท ๐ฆ) โ โค โง (๐ฅ ยท ๐ฅ) โ โ) โง (1 / ๐ด) = ((๐ฅ ยท ๐ฆ) / (๐ฅ ยท ๐ฅ))) โ (1 / ๐ด) โ โ) |
47 | 42, 46 | syl8 76 |
. . . 4
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ (๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (1 / ๐ด) โ โ))) |
48 | 47 | rexlimivv 3196 |
. . 3
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (1 / ๐ด) โ โ)) |
49 | 1, 48 | sylbi 216 |
. 2
โข (๐ด โ โ โ (๐ด โ 0 โ (1 / ๐ด) โ
โ)) |
50 | 49 | imp 407 |
1
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ
โ) |