Step | Hyp | Ref
| Expression |
1 | | dvdsnprmd.d |
. 2
โข (๐ โ ๐ด โฅ ๐) |
2 | | dvdszrcl 16148 |
. . . 4
โข (๐ด โฅ ๐ โ (๐ด โ โค โง ๐ โ โค)) |
3 | | divides 16145 |
. . . 4
โข ((๐ด โ โค โง ๐ โ โค) โ (๐ด โฅ ๐ โ โ๐ โ โค (๐ ยท ๐ด) = ๐)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
โข (๐ โ (๐ด โฅ ๐ โ โ๐ โ โค (๐ ยท ๐ด) = ๐)) |
5 | | 2z 12542 |
. . . . . . . 8
โข 2 โ
โค |
6 | 5 | a1i 11 |
. . . . . . 7
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ 2 โ โค) |
7 | | simplr 768 |
. . . . . . 7
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ๐ โ โค) |
8 | | dvdsnprmd.l |
. . . . . . . . . . . 12
โข (๐ โ ๐ด < ๐) |
9 | 8 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โค) โ ๐ด < ๐) |
10 | 9 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ๐ด < ๐) |
11 | | breq2 5114 |
. . . . . . . . . . 11
โข ((๐ ยท ๐ด) = ๐ โ (๐ด < (๐ ยท ๐ด) โ ๐ด < ๐)) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ (๐ด < (๐ ยท ๐ด) โ ๐ด < ๐)) |
13 | 10, 12 | mpbird 257 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ๐ด < (๐ ยท ๐ด)) |
14 | | dvdsnprmd.g |
. . . . . . . . . . . . 13
โข (๐ โ 1 < ๐ด) |
15 | | zre 12510 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โค โ ๐ด โ
โ) |
16 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง 1 <
๐ด โง ๐ โ โค) โ ๐ด โ โ) |
17 | | zre 12510 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ๐ โ
โ) |
18 | 17 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง 1 <
๐ด โง ๐ โ โค) โ ๐ โ โ) |
19 | | 0lt1 11684 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 <
1 |
20 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด โ โค โ 0 โ
โ) |
21 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด โ โค โ 1 โ
โ) |
22 | | lttr 11238 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((0
โ โ โง 1 โ โ โง ๐ด โ โ) โ ((0 < 1 โง 1
< ๐ด) โ 0 < ๐ด)) |
23 | 20, 21, 15, 22 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ด โ โค โ ((0 <
1 โง 1 < ๐ด) โ 0
< ๐ด)) |
24 | 19, 23 | mpani 695 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โค โ (1 <
๐ด โ 0 < ๐ด)) |
25 | 24 | imp 408 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โค โง 1 <
๐ด) โ 0 < ๐ด) |
26 | 25 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง 1 <
๐ด โง ๐ โ โค) โ 0 < ๐ด) |
27 | 16, 18, 26 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง 1 <
๐ด โง ๐ โ โค) โ (๐ด โ โ โง ๐ โ โ โง 0 < ๐ด)) |
28 | 27 | 3exp 1120 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โค โ (1 <
๐ด โ (๐ โ โค โ (๐ด โ โ โง ๐ โ โ โง 0 <
๐ด)))) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ โ โค) โ (1 <
๐ด โ (๐ โ โค โ (๐ด โ โ โง ๐ โ โ โง 0 <
๐ด)))) |
30 | 1, 2, 29 | 3syl 18 |
. . . . . . . . . . . . 13
โข (๐ โ (1 < ๐ด โ (๐ โ โค โ (๐ด โ โ โง ๐ โ โ โง 0 < ๐ด)))) |
31 | 14, 30 | mpd 15 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ โค โ (๐ด โ โ โง ๐ โ โ โง 0 < ๐ด))) |
32 | 31 | imp 408 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โค) โ (๐ด โ โ โง ๐ โ โ โง 0 < ๐ด)) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ (๐ด โ โ โง ๐ โ โ โง 0 < ๐ด)) |
34 | | ltmulgt12 12023 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐ด) โ (1 < ๐ โ ๐ด < (๐ ยท ๐ด))) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ (1 < ๐ โ ๐ด < (๐ ยท ๐ด))) |
36 | 13, 35 | mpbird 257 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ 1 < ๐) |
37 | | df-2 12223 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
38 | 37 | breq1i 5117 |
. . . . . . . . 9
โข (2 โค
๐ โ (1 + 1) โค ๐) |
39 | | 1zzd 12541 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ 1 โ
โค) |
40 | | zltp1le 12560 |
. . . . . . . . . . . . 13
โข ((1
โ โค โง ๐
โ โค) โ (1 < ๐ โ (1 + 1) โค ๐)) |
41 | 39, 40 | mpancom 687 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (1 <
๐ โ (1 + 1) โค ๐)) |
42 | 41 | bicomd 222 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((1 + 1)
โค ๐ โ 1 < ๐)) |
43 | 42 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โค) โ ((1 + 1) โค ๐ โ 1 < ๐)) |
44 | 43 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ((1 + 1) โค ๐ โ 1 < ๐)) |
45 | 38, 44 | bitrid 283 |
. . . . . . . 8
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ (2 โค ๐ โ 1 < ๐)) |
46 | 36, 45 | mpbird 257 |
. . . . . . 7
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ 2 โค ๐) |
47 | | eluz2 12776 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ (2 โ โค โง ๐ โ โค โง 2 โค
๐)) |
48 | 6, 7, 46, 47 | syl3anbrc 1344 |
. . . . . 6
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ๐ โ
(โคโฅโ2)) |
49 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง 1 <
๐ด) โ 2 โ
โค) |
50 | | simpl 484 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง 1 <
๐ด) โ ๐ด โ โค) |
51 | | 1zzd 12541 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โค โ 1 โ
โค) |
52 | | zltp1le 12560 |
. . . . . . . . . . . . . . . . 17
โข ((1
โ โค โง ๐ด
โ โค) โ (1 < ๐ด โ (1 + 1) โค ๐ด)) |
53 | 51, 52 | mpancom 687 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โค โ (1 <
๐ด โ (1 + 1) โค ๐ด)) |
54 | 53 | biimpa 478 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง 1 <
๐ด) โ (1 + 1) โค
๐ด) |
55 | 37 | breq1i 5117 |
. . . . . . . . . . . . . . 15
โข (2 โค
๐ด โ (1 + 1) โค ๐ด) |
56 | 54, 55 | sylibr 233 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง 1 <
๐ด) โ 2 โค ๐ด) |
57 | 49, 50, 56 | 3jca 1129 |
. . . . . . . . . . . . 13
โข ((๐ด โ โค โง 1 <
๐ด) โ (2 โ โค
โง ๐ด โ โค
โง 2 โค ๐ด)) |
58 | 57 | ex 414 |
. . . . . . . . . . . 12
โข (๐ด โ โค โ (1 <
๐ด โ (2 โ โค
โง ๐ด โ โค
โง 2 โค ๐ด))) |
59 | 58 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง ๐ โ โค) โ (1 <
๐ด โ (2 โ โค
โง ๐ด โ โค
โง 2 โค ๐ด))) |
60 | 1, 2, 59 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ (1 < ๐ด โ (2 โ โค โง ๐ด โ โค โง 2 โค
๐ด))) |
61 | 14, 60 | mpd 15 |
. . . . . . . . 9
โข (๐ โ (2 โ โค โง
๐ด โ โค โง 2
โค ๐ด)) |
62 | | eluz2 12776 |
. . . . . . . . 9
โข (๐ด โ
(โคโฅโ2) โ (2 โ โค โง ๐ด โ โค โง 2 โค
๐ด)) |
63 | 61, 62 | sylibr 233 |
. . . . . . . 8
โข (๐ โ ๐ด โ
(โคโฅโ2)) |
64 | 63 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ ๐ด โ
(โคโฅโ2)) |
65 | 64 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ๐ด โ
(โคโฅโ2)) |
66 | | nprm 16571 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง ๐ด โ (โคโฅโ2))
โ ยฌ (๐ ยท
๐ด) โ
โ) |
67 | 48, 65, 66 | syl2anc 585 |
. . . . 5
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ยฌ (๐ ยท ๐ด) โ โ) |
68 | | eleq1 2826 |
. . . . . . 7
โข ((๐ ยท ๐ด) = ๐ โ ((๐ ยท ๐ด) โ โ โ ๐ โ โ)) |
69 | 68 | notbid 318 |
. . . . . 6
โข ((๐ ยท ๐ด) = ๐ โ (ยฌ (๐ ยท ๐ด) โ โ โ ยฌ ๐ โ
โ)) |
70 | 69 | adantl 483 |
. . . . 5
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ (ยฌ (๐ ยท ๐ด) โ โ โ ยฌ ๐ โ
โ)) |
71 | 67, 70 | mpbid 231 |
. . . 4
โข (((๐ โง ๐ โ โค) โง (๐ ยท ๐ด) = ๐) โ ยฌ ๐ โ โ) |
72 | 71 | rexlimdva2 3155 |
. . 3
โข (๐ โ (โ๐ โ โค (๐ ยท ๐ด) = ๐ โ ยฌ ๐ โ โ)) |
73 | 4, 72 | sylbid 239 |
. 2
โข (๐ โ (๐ด โฅ ๐ โ ยฌ ๐ โ โ)) |
74 | 1, 73 | mpd 15 |
1
โข (๐ โ ยฌ ๐ โ โ) |