Step | Hyp | Ref
| Expression |
1 | | zre 12510 |
. . . . . 6
โข (๐ด โ โค โ ๐ด โ
โ) |
2 | | 0red 11165 |
. . . . . 6
โข (๐ด โ โค โ 0 โ
โ) |
3 | 1, 2 | leloed 11305 |
. . . . 5
โข (๐ด โ โค โ (๐ด โค 0 โ (๐ด < 0 โจ ๐ด = 0))) |
4 | | prmnn 16557 |
. . . . . . . . . 10
โข ((2
ยท ๐ด) โ โ
โ (2 ยท ๐ด)
โ โ) |
5 | | nnnn0 12427 |
. . . . . . . . . 10
โข ((2
ยท ๐ด) โ โ
โ (2 ยท ๐ด)
โ โ0) |
6 | | nn0ge0 12445 |
. . . . . . . . . . 11
โข ((2
ยท ๐ด) โ
โ0 โ 0 โค (2 ยท ๐ด)) |
7 | | 2pos 12263 |
. . . . . . . . . . . . . . . . . . 19
โข 0 <
2 |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โค โ 0 <
2) |
9 | 8 | anim1i 616 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ด < 0) โ (0 < 2 โง
๐ด < 0)) |
10 | 9 | olcd 873 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ด < 0) โ ((2 < 0 โง
0 < ๐ด) โจ (0 < 2
โง ๐ด <
0))) |
11 | | 2re 12234 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ด < 0) โ 2 โ
โ) |
13 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ด < 0) โ ๐ด โ
โ) |
14 | 12, 13 | mul2lt0bi 13028 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ด < 0) โ ((2 ยท
๐ด) < 0 โ ((2 < 0
โง 0 < ๐ด) โจ (0
< 2 โง ๐ด <
0)))) |
15 | 10, 14 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง ๐ด < 0) โ (2 ยท
๐ด) < 0) |
16 | 12, 13 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ด < 0) โ (2 ยท
๐ด) โ
โ) |
17 | | 0red 11165 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ด < 0) โ 0 โ
โ) |
18 | 16, 17 | ltnled 11309 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง ๐ด < 0) โ ((2 ยท
๐ด) < 0 โ ยฌ 0
โค (2 ยท ๐ด))) |
19 | 15, 18 | mpbid 231 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ด < 0) โ ยฌ 0 โค (2
ยท ๐ด)) |
20 | 19 | ex 414 |
. . . . . . . . . . . . 13
โข (๐ด โ โค โ (๐ด < 0 โ ยฌ 0 โค (2
ยท ๐ด))) |
21 | 20 | con2d 134 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (0 โค
(2 ยท ๐ด) โ ยฌ
๐ด < 0)) |
22 | 21 | com12 32 |
. . . . . . . . . . 11
โข (0 โค
(2 ยท ๐ด) โ
(๐ด โ โค โ
ยฌ ๐ด <
0)) |
23 | 6, 22 | syl 17 |
. . . . . . . . . 10
โข ((2
ยท ๐ด) โ
โ0 โ (๐ด โ โค โ ยฌ ๐ด < 0)) |
24 | 4, 5, 23 | 3syl 18 |
. . . . . . . . 9
โข ((2
ยท ๐ด) โ โ
โ (๐ด โ โค
โ ยฌ ๐ด <
0)) |
25 | 24 | com12 32 |
. . . . . . . 8
โข (๐ด โ โค โ ((2
ยท ๐ด) โ โ
โ ยฌ ๐ด <
0)) |
26 | 25 | con2d 134 |
. . . . . . 7
โข (๐ด โ โค โ (๐ด < 0 โ ยฌ (2 ยท
๐ด) โ
โ)) |
27 | 26 | a1dd 50 |
. . . . . 6
โข (๐ด โ โค โ (๐ด < 0 โ (ยฌ ๐ด = 1 โ ยฌ (2 ยท
๐ด) โ
โ))) |
28 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ด = 0 โ (2 ยท ๐ด) = (2 ยท
0)) |
29 | | 2t0e0 12329 |
. . . . . . . . 9
โข (2
ยท 0) = 0 |
30 | 28, 29 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ด = 0 โ (2 ยท ๐ด) = 0) |
31 | | 0nprm 16561 |
. . . . . . . . 9
โข ยฌ 0
โ โ |
32 | 31 | a1i 11 |
. . . . . . . 8
โข (๐ด = 0 โ ยฌ 0 โ
โ) |
33 | 30, 32 | eqneltrd 2858 |
. . . . . . 7
โข (๐ด = 0 โ ยฌ (2 ยท
๐ด) โ
โ) |
34 | 33 | a1i13 27 |
. . . . . 6
โข (๐ด โ โค โ (๐ด = 0 โ (ยฌ ๐ด = 1 โ ยฌ (2 ยท
๐ด) โ
โ))) |
35 | 27, 34 | jaod 858 |
. . . . 5
โข (๐ด โ โค โ ((๐ด < 0 โจ ๐ด = 0) โ (ยฌ ๐ด = 1 โ ยฌ (2 ยท ๐ด) โ
โ))) |
36 | 3, 35 | sylbid 239 |
. . . 4
โข (๐ด โ โค โ (๐ด โค 0 โ (ยฌ ๐ด = 1 โ ยฌ (2 ยท
๐ด) โ
โ))) |
37 | | 2z 12542 |
. . . . . . 7
โข 2 โ
โค |
38 | | uzid 12785 |
. . . . . . 7
โข (2 โ
โค โ 2 โ (โคโฅโ2)) |
39 | 37, 38 | ax-mp 5 |
. . . . . 6
โข 2 โ
(โคโฅโ2) |
40 | 37 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โค โง 1 โค
๐ด โง ยฌ ๐ด = 1) โ 2 โ
โค) |
41 | | simp1 1137 |
. . . . . . 7
โข ((๐ด โ โค โง 1 โค
๐ด โง ยฌ ๐ด = 1) โ ๐ด โ โค) |
42 | | df-ne 2945 |
. . . . . . . . 9
โข (๐ด โ 1 โ ยฌ ๐ด = 1) |
43 | | 1red 11163 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ 1 โ
โ) |
44 | 43, 1 | ltlend 11307 |
. . . . . . . . . . 11
โข (๐ด โ โค โ (1 <
๐ด โ (1 โค ๐ด โง ๐ด โ 1))) |
45 | | 1zzd 12541 |
. . . . . . . . . . . . . 14
โข (๐ด โ โค โ 1 โ
โค) |
46 | | zltp1le 12560 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง ๐ด
โ โค) โ (1 < ๐ด โ (1 + 1) โค ๐ด)) |
47 | 45, 46 | mpancom 687 |
. . . . . . . . . . . . 13
โข (๐ด โ โค โ (1 <
๐ด โ (1 + 1) โค ๐ด)) |
48 | 47 | biimpd 228 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (1 <
๐ด โ (1 + 1) โค ๐ด)) |
49 | | df-2 12223 |
. . . . . . . . . . . . 13
โข 2 = (1 +
1) |
50 | 49 | breq1i 5117 |
. . . . . . . . . . . 12
โข (2 โค
๐ด โ (1 + 1) โค ๐ด) |
51 | 48, 50 | syl6ibr 252 |
. . . . . . . . . . 11
โข (๐ด โ โค โ (1 <
๐ด โ 2 โค ๐ด)) |
52 | 44, 51 | sylbird 260 |
. . . . . . . . . 10
โข (๐ด โ โค โ ((1 โค
๐ด โง ๐ด โ 1) โ 2 โค ๐ด)) |
53 | 52 | expdimp 454 |
. . . . . . . . 9
โข ((๐ด โ โค โง 1 โค
๐ด) โ (๐ด โ 1 โ 2 โค ๐ด)) |
54 | 42, 53 | biimtrrid 242 |
. . . . . . . 8
โข ((๐ด โ โค โง 1 โค
๐ด) โ (ยฌ ๐ด = 1 โ 2 โค ๐ด)) |
55 | 54 | 3impia 1118 |
. . . . . . 7
โข ((๐ด โ โค โง 1 โค
๐ด โง ยฌ ๐ด = 1) โ 2 โค ๐ด) |
56 | | eluz2 12776 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ (2 โ โค โง ๐ด โ โค โง 2 โค
๐ด)) |
57 | 40, 41, 55, 56 | syl3anbrc 1344 |
. . . . . 6
โข ((๐ด โ โค โง 1 โค
๐ด โง ยฌ ๐ด = 1) โ ๐ด โ
(โคโฅโ2)) |
58 | | nprm 16571 |
. . . . . 6
โข ((2
โ (โคโฅโ2) โง ๐ด โ (โคโฅโ2))
โ ยฌ (2 ยท ๐ด)
โ โ) |
59 | 39, 57, 58 | sylancr 588 |
. . . . 5
โข ((๐ด โ โค โง 1 โค
๐ด โง ยฌ ๐ด = 1) โ ยฌ (2 ยท
๐ด) โ
โ) |
60 | 59 | 3exp 1120 |
. . . 4
โข (๐ด โ โค โ (1 โค
๐ด โ (ยฌ ๐ด = 1 โ ยฌ (2 ยท
๐ด) โ
โ))) |
61 | | zle0orge1 12523 |
. . . 4
โข (๐ด โ โค โ (๐ด โค 0 โจ 1 โค ๐ด)) |
62 | 36, 60, 61 | mpjaod 859 |
. . 3
โข (๐ด โ โค โ (ยฌ
๐ด = 1 โ ยฌ (2
ยท ๐ด) โ
โ)) |
63 | 62 | con4d 115 |
. 2
โข (๐ด โ โค โ ((2
ยท ๐ด) โ โ
โ ๐ด =
1)) |
64 | | oveq2 7370 |
. . . 4
โข (๐ด = 1 โ (2 ยท ๐ด) = (2 ยท
1)) |
65 | | 2t1e2 12323 |
. . . 4
โข (2
ยท 1) = 2 |
66 | 64, 65 | eqtrdi 2793 |
. . 3
โข (๐ด = 1 โ (2 ยท ๐ด) = 2) |
67 | | 2prm 16575 |
. . 3
โข 2 โ
โ |
68 | 66, 67 | eqeltrdi 2846 |
. 2
โข (๐ด = 1 โ (2 ยท ๐ด) โ
โ) |
69 | 63, 68 | impbid1 224 |
1
โข (๐ด โ โค โ ((2
ยท ๐ด) โ โ
โ ๐ด =
1)) |