Step | Hyp | Ref
| Expression |
1 | | elznn0nn 12521 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ
โ))) |
2 | | elnn0 12423 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
3 | | elnn1uz2 12858 |
. . . . . . 7
โข (๐ โ โ โ (๐ = 1 โจ ๐ โ
(โคโฅโ2))) |
4 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (๐ ยท ๐ด) = (1 ยท ๐ด)) |
5 | 4 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ = 1 โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ ยท ๐ด) = (1 ยท ๐ด)) |
6 | 5 | eqeq1d 2735 |
. . . . . . . . . 10
โข ((๐ = 1 โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ ยท ๐ด) = ๐ต โ (1 ยท ๐ด) = ๐ต)) |
7 | | prmz 16559 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ โ ๐ด โ
โค) |
8 | 7 | zcnd 12616 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ ๐ด โ
โ) |
9 | 8 | mullidd 11181 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ (1
ยท ๐ด) = ๐ด) |
10 | 9 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ๐ด) = ๐ด) |
11 | 10 | eqeq1d 2735 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1
ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |
12 | 11 | biimpd 228 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1
ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |
13 | 12 | adantl 483 |
. . . . . . . . . 10
โข ((๐ = 1 โง (๐ด โ โ โง ๐ต โ โ)) โ ((1 ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |
14 | 6, 13 | sylbid 239 |
. . . . . . . . 9
โข ((๐ = 1 โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |
15 | 14 | ex 414 |
. . . . . . . 8
โข (๐ = 1 โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
16 | | prmuz2 16580 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
(โคโฅโ2)) |
17 | 16 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
(โคโฅโ2)) |
18 | | nprm 16572 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง ๐ด โ (โคโฅโ2))
โ ยฌ (๐ ยท
๐ด) โ
โ) |
19 | 17, 18 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ด โ โ โง ๐ต โ โ)) โ ยฌ (๐ ยท ๐ด) โ โ) |
20 | | eleq1 2822 |
. . . . . . . . . . . . 13
โข ((๐ ยท ๐ด) = ๐ต โ ((๐ ยท ๐ด) โ โ โ ๐ต โ โ)) |
21 | 20 | notbid 318 |
. . . . . . . . . . . 12
โข ((๐ ยท ๐ด) = ๐ต โ (ยฌ (๐ ยท ๐ด) โ โ โ ยฌ ๐ต โ
โ)) |
22 | | pm2.24 124 |
. . . . . . . . . . . . . . 15
โข (๐ต โ โ โ (ยฌ
๐ต โ โ โ
๐ด = ๐ต)) |
23 | 22 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ (ยฌ
๐ต โ โ โ
๐ด = ๐ต)) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ด โ โ โง ๐ต โ โ)) โ (ยฌ ๐ต โ โ โ ๐ด = ๐ต)) |
25 | 24 | com12 32 |
. . . . . . . . . . . 12
โข (ยฌ
๐ต โ โ โ
((๐ โ
(โคโฅโ2) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ด = ๐ต)) |
26 | 21, 25 | syl6bi 253 |
. . . . . . . . . . 11
โข ((๐ ยท ๐ด) = ๐ต โ (ยฌ (๐ ยท ๐ด) โ โ โ ((๐ โ (โคโฅโ2)
โง (๐ด โ โ
โง ๐ต โ โ))
โ ๐ด = ๐ต))) |
27 | 26 | com3l 89 |
. . . . . . . . . 10
โข (ยฌ
(๐ ยท ๐ด) โ โ โ ((๐ โ
(โคโฅโ2) โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
28 | 19, 27 | mpcom 38 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |
29 | 28 | ex 414 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
30 | 15, 29 | jaoi 856 |
. . . . . . 7
โข ((๐ = 1 โจ ๐ โ (โคโฅโ2))
โ ((๐ด โ โ
โง ๐ต โ โ)
โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
31 | 3, 30 | sylbi 216 |
. . . . . 6
โข (๐ โ โ โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
32 | | oveq1 7368 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ ยท ๐ด) = (0 ยท ๐ด)) |
33 | 32 | eqeq1d 2735 |
. . . . . . . 8
โข (๐ = 0 โ ((๐ ยท ๐ด) = ๐ต โ (0 ยท ๐ด) = ๐ต)) |
34 | | prmnn 16558 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ๐ด โ
โ) |
35 | 34 | nnred 12176 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ ๐ด โ
โ) |
36 | | mul02lem2 11340 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ (0
ยท ๐ด) =
0) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ (0
ยท ๐ด) =
0) |
38 | 37 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (0
ยท ๐ด) =
0) |
39 | 38 | eqeq1d 2735 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0
ยท ๐ด) = ๐ต โ 0 = ๐ต)) |
40 | | prmnn 16558 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ๐ต โ
โ) |
41 | | elnnne0 12435 |
. . . . . . . . . . . . 13
โข (๐ต โ โ โ (๐ต โ โ0
โง ๐ต โ
0)) |
42 | | eqneqall 2951 |
. . . . . . . . . . . . . . . 16
โข (๐ต = 0 โ (๐ต โ 0 โ ๐ด = ๐ต)) |
43 | 42 | eqcoms 2741 |
. . . . . . . . . . . . . . 15
โข (0 =
๐ต โ (๐ต โ 0 โ ๐ด = ๐ต)) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . 14
โข (๐ต โ 0 โ (0 = ๐ต โ ๐ด = ๐ต)) |
45 | 44 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ต โ โ0
โง ๐ต โ 0) โ (0 =
๐ต โ ๐ด = ๐ต)) |
46 | 41, 45 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ (0 =
๐ต โ ๐ด = ๐ต)) |
47 | 40, 46 | syl 17 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (0 =
๐ต โ ๐ด = ๐ต)) |
48 | 47 | adantl 483 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 =
๐ต โ ๐ด = ๐ต)) |
49 | 39, 48 | sylbid 239 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0
ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |
50 | 49 | com12 32 |
. . . . . . . 8
โข ((0
ยท ๐ด) = ๐ต โ ((๐ด โ โ โง ๐ต โ โ) โ ๐ด = ๐ต)) |
51 | 33, 50 | syl6bi 253 |
. . . . . . 7
โข (๐ = 0 โ ((๐ ยท ๐ด) = ๐ต โ ((๐ด โ โ โง ๐ต โ โ) โ ๐ด = ๐ต))) |
52 | 51 | com23 86 |
. . . . . 6
โข (๐ = 0 โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
53 | 31, 52 | jaoi 856 |
. . . . 5
โข ((๐ โ โ โจ ๐ = 0) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
54 | 2, 53 | sylbi 216 |
. . . 4
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ต โ โ)
โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
55 | | elnnz 12517 |
. . . . . 6
โข (-๐ โ โ โ (-๐ โ โค โง 0 <
-๐)) |
56 | | lt0neg1 11669 |
. . . . . . . 8
โข (๐ โ โ โ (๐ < 0 โ 0 < -๐)) |
57 | 34 | nngt0d 12210 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ 0 <
๐ด) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 <
๐ด) |
59 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ < 0) โ ๐ < 0) |
60 | 58, 59 | anim12ci 615 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ < 0)) โ (๐ < 0 โง 0 < ๐ด)) |
61 | 60 | orcd 872 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ < 0)) โ ((๐ < 0 โง 0 < ๐ด) โจ (0 < ๐ โง ๐ด < 0))) |
62 | | simprl 770 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ < 0)) โ ๐ โ
โ) |
63 | 35 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ < 0)) โ ๐ด โ
โ) |
65 | 62, 64 | mul2lt0bi 13029 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ < 0)) โ ((๐ ยท ๐ด) < 0 โ ((๐ < 0 โง 0 < ๐ด) โจ (0 < ๐ โง ๐ด < 0)))) |
66 | 61, 65 | mpbird 257 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ < 0)) โ (๐ ยท ๐ด) < 0) |
67 | 66 | ex 414 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ โ โ โง ๐ < 0) โ (๐ ยท ๐ด) < 0)) |
68 | | breq1 5112 |
. . . . . . . . . . . . . 14
โข ((๐ ยท ๐ด) = ๐ต โ ((๐ ยท ๐ด) < 0 โ ๐ต < 0)) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ ยท ๐ด) = ๐ต) โ ((๐ ยท ๐ด) < 0 โ ๐ต < 0)) |
70 | | nnnn0 12428 |
. . . . . . . . . . . . . . . . 17
โข (๐ต โ โ โ ๐ต โ
โ0) |
71 | | nn0nlt0 12447 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ โ0
โ ยฌ ๐ต <
0) |
72 | 71 | pm2.21d 121 |
. . . . . . . . . . . . . . . . 17
โข (๐ต โ โ0
โ (๐ต < 0 โ
๐ด = ๐ต)) |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ โ โ (๐ต < 0 โ ๐ด = ๐ต)) |
74 | 40, 73 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ต โ โ โ (๐ต < 0 โ ๐ด = ๐ต)) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ต < 0 โ ๐ด = ๐ต)) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ ยท ๐ด) = ๐ต) โ (๐ต < 0 โ ๐ด = ๐ต)) |
77 | 69, 76 | sylbid 239 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ ยท ๐ด) = ๐ต) โ ((๐ ยท ๐ด) < 0 โ ๐ด = ๐ต)) |
78 | 77 | ex 414 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ((๐ ยท ๐ด) < 0 โ ๐ด = ๐ต))) |
79 | 78 | com23 86 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) < 0 โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
80 | 67, 79 | syldc 48 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ < 0) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
81 | 80 | ex 414 |
. . . . . . . 8
โข (๐ โ โ โ (๐ < 0 โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)))) |
82 | 56, 81 | sylbird 260 |
. . . . . . 7
โข (๐ โ โ โ (0 <
-๐ โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)))) |
83 | 82 | adantld 492 |
. . . . . 6
โข (๐ โ โ โ ((-๐ โ โค โง 0 <
-๐) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)))) |
84 | 55, 83 | biimtrid 241 |
. . . . 5
โข (๐ โ โ โ (-๐ โ โ โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)))) |
85 | 84 | imp 408 |
. . . 4
โข ((๐ โ โ โง -๐ โ โ) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
86 | 54, 85 | jaoi 856 |
. . 3
โข ((๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ โ)) โ
((๐ด โ โ โง
๐ต โ โ) โ
((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
87 | 1, 86 | sylbi 216 |
. 2
โข (๐ โ โค โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต))) |
88 | 87 | 3impib 1117 |
1
โข ((๐ โ โค โง ๐ด โ โ โง ๐ต โ โ) โ ((๐ ยท ๐ด) = ๐ต โ ๐ด = ๐ต)) |