Step | Hyp | Ref
| Expression |
1 | | pockthg.4 |
. . 3
โข (๐ โ ๐ = ((๐ด ยท ๐ต) + 1)) |
2 | | pockthg.1 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
3 | | pockthg.2 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
4 | 2, 3 | nnmulcld 12213 |
. . . . . 6
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
5 | | nnuz 12813 |
. . . . . 6
โข โ =
(โคโฅโ1) |
6 | 4, 5 | eleqtrdi 2848 |
. . . . 5
โข (๐ โ (๐ด ยท ๐ต) โ
(โคโฅโ1)) |
7 | | eluzp1p1 12798 |
. . . . 5
โข ((๐ด ยท ๐ต) โ (โคโฅโ1)
โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ(1 + 1))) |
8 | 6, 7 | syl 17 |
. . . 4
โข (๐ โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ(1 + 1))) |
9 | | df-2 12223 |
. . . . 5
โข 2 = (1 +
1) |
10 | 9 | fveq2i 6850 |
. . . 4
โข
(โคโฅโ2) = (โคโฅโ(1 +
1)) |
11 | 8, 10 | eleqtrrdi 2849 |
. . 3
โข (๐ โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ2)) |
12 | 1, 11 | eqeltrd 2838 |
. 2
โข (๐ โ ๐ โ
(โคโฅโ2)) |
13 | | eluzelre 12781 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
15 | 14 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
16 | 2 | nnred 12175 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
17 | 16 | resqcld 14037 |
. . . . . . . 8
โข (๐ โ (๐ดโ2) โ โ) |
18 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ดโ2) โ โ) |
19 | | prmnn 16557 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
20 | 19 | ad2antrl 727 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
21 | 20 | nnred 12175 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
22 | 21 | resqcld 14037 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐โ2) โ โ) |
23 | | pockthg.3 |
. . . . . . . . . . 11
โข (๐ โ ๐ต < ๐ด) |
24 | 3 | nnred 12175 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โ) |
25 | 2 | nngt0d 12209 |
. . . . . . . . . . . 12
โข (๐ โ 0 < ๐ด) |
26 | | ltmul2 12013 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ด โ โ โง (๐ด โ โ โง 0 <
๐ด)) โ (๐ต < ๐ด โ (๐ด ยท ๐ต) < (๐ด ยท ๐ด))) |
27 | 24, 16, 16, 25, 26 | syl112anc 1375 |
. . . . . . . . . . 11
โข (๐ โ (๐ต < ๐ด โ (๐ด ยท ๐ต) < (๐ด ยท ๐ด))) |
28 | 23, 27 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (๐ด ยท ๐ต) < (๐ด ยท ๐ด)) |
29 | 2, 2 | nnmulcld 12213 |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท ๐ด) โ โ) |
30 | | nnltp1le 12566 |
. . . . . . . . . . 11
โข (((๐ด ยท ๐ต) โ โ โง (๐ด ยท ๐ด) โ โ) โ ((๐ด ยท ๐ต) < (๐ด ยท ๐ด) โ ((๐ด ยท ๐ต) + 1) โค (๐ด ยท ๐ด))) |
31 | 4, 29, 30 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ ((๐ด ยท ๐ต) < (๐ด ยท ๐ด) โ ((๐ด ยท ๐ต) + 1) โค (๐ด ยท ๐ด))) |
32 | 28, 31 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ ((๐ด ยท ๐ต) + 1) โค (๐ด ยท ๐ด)) |
33 | 2 | nncnd 12176 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
34 | 33 | sqvald 14055 |
. . . . . . . . 9
โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
35 | 32, 1, 34 | 3brtr4d 5142 |
. . . . . . . 8
โข (๐ โ ๐ โค (๐ดโ2)) |
36 | 35 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โค (๐ดโ2)) |
37 | | pockthg.5 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) |
38 | 37 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ โ๐ โ โ (๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) |
39 | | prmnn 16557 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
40 | 39 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โ โ) |
41 | 40 | nncnd 12176 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โ โ) |
42 | 41 | exp1d 14053 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (๐โ1) = ๐) |
43 | | nnge1 12188 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ pCnt ๐ด) โ โ โ 1 โค (๐ pCnt ๐ด)) |
44 | 43 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ 1 โค (๐ pCnt ๐ด)) |
45 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โ โ) |
46 | 2 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ด โ โค) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ด โ โค) |
48 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
โ0 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ 1 โ
โ0) |
50 | | pcdvdsb 16748 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ด โ โค โง 1 โ
โ0) โ (1 โค (๐ pCnt ๐ด) โ (๐โ1) โฅ ๐ด)) |
51 | 45, 47, 49, 50 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (1 โค (๐ pCnt ๐ด) โ (๐โ1) โฅ ๐ด)) |
52 | 44, 51 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (๐โ1) โฅ ๐ด) |
53 | 42, 52 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โฅ ๐ด) |
54 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐) |
55 | 54, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ด โ โ) |
56 | 54, 3 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ต โ โ) |
57 | 54, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ต < ๐ด) |
58 | 54, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ = ((๐ด ยท ๐ต) + 1)) |
59 | | simpl2l 1227 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ โ โ) |
60 | | simpl2r 1228 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ โฅ ๐) |
61 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ โ โ) |
62 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ (๐ pCnt ๐ด) โ โ) |
63 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ฅ โ โค) |
64 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ((๐ฅโ(๐ โ 1)) mod ๐) = 1) |
65 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1) |
66 | 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65 | pockthlem 16784 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))) |
67 | 66 | rexlimdvaa 3154 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
68 | 67 | 3expa 1119 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
69 | 53, 68 | embantd 59 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
70 | 69 | expr 458 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) โ โ โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))))) |
71 | | id 22 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ) |
72 | | prmuz2 16579 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
73 | | uz2m1nn 12855 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
75 | 74 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ โ 1) โ โ) |
76 | | pccl 16728 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ (๐ pCnt (๐ โ 1)) โ
โ0) |
77 | 71, 75, 76 | syl2anr 598 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ (๐ pCnt (๐ โ 1)) โ
โ0) |
78 | 77 | nn0ge0d 12483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ 0 โค (๐ pCnt (๐ โ 1))) |
79 | | breq1 5113 |
. . . . . . . . . . . . . . . 16
โข ((๐ pCnt ๐ด) = 0 โ ((๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)) โ 0 โค (๐ pCnt (๐ โ 1)))) |
80 | 78, 79 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) = 0 โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
81 | 80 | a1dd 50 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) = 0 โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))))) |
82 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ๐ โ โ) |
83 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ๐ด โ โ) |
84 | 82, 83 | pccld 16729 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ (๐ pCnt ๐ด) โ
โ0) |
85 | | elnn0 12422 |
. . . . . . . . . . . . . . 15
โข ((๐ pCnt ๐ด) โ โ0 โ ((๐ pCnt ๐ด) โ โ โจ (๐ pCnt ๐ด) = 0)) |
86 | 84, 85 | sylib 217 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) โ โ โจ (๐ pCnt ๐ด) = 0)) |
87 | 70, 81, 86 | mpjaod 859 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
88 | 87 | ralimdva 3165 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
89 | 38, 88 | mpd 15 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))) |
90 | 75 | nnzd 12533 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ โ 1) โ โค) |
91 | | pc2dvds 16758 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง (๐ โ 1) โ โค)
โ (๐ด โฅ (๐ โ 1) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
92 | 46, 90, 91 | syl2an2r 684 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด โฅ (๐ โ 1) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
93 | 89, 92 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โฅ (๐ โ 1)) |
94 | | dvdsle 16199 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง (๐ โ 1) โ โ)
โ (๐ด โฅ (๐ โ 1) โ ๐ด โค (๐ โ 1))) |
95 | 46, 75, 94 | syl2an2r 684 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด โฅ (๐ โ 1) โ ๐ด โค (๐ โ 1))) |
96 | 93, 95 | mpd 15 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โค (๐ โ 1)) |
97 | 2 | nnnn0d 12480 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ
โ0) |
98 | 20 | nnnn0d 12480 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ0) |
99 | | nn0ltlem1 12570 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ0) โ (๐ด < ๐ โ ๐ด โค (๐ โ 1))) |
100 | 97, 98, 99 | syl2an2r 684 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด < ๐ โ ๐ด โค (๐ โ 1))) |
101 | 96, 100 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด < ๐) |
102 | 16 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โ โ) |
103 | 97 | nn0ge0d 12483 |
. . . . . . . . . 10
โข (๐ โ 0 โค ๐ด) |
104 | 103 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ 0 โค ๐ด) |
105 | 98 | nn0ge0d 12483 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ 0 โค ๐) |
106 | 102, 21, 104, 105 | lt2sqd 14166 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด < ๐ โ (๐ดโ2) < (๐โ2))) |
107 | 101, 106 | mpbid 231 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ดโ2) < (๐โ2)) |
108 | 15, 18, 22, 36, 107 | lelttrd 11320 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ < (๐โ2)) |
109 | 15, 22 | ltnled 11309 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ < (๐โ2) โ ยฌ (๐โ2) โค ๐)) |
110 | 108, 109 | mpbid 231 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ยฌ (๐โ2) โค ๐) |
111 | 110 | expr 458 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (๐ โฅ ๐ โ ยฌ (๐โ2) โค ๐)) |
112 | 111 | con2d 134 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐โ2) โค ๐ โ ยฌ ๐ โฅ ๐)) |
113 | 112 | ralrimiva 3144 |
. 2
โข (๐ โ โ๐ โ โ ((๐โ2) โค ๐ โ ยฌ ๐ โฅ ๐)) |
114 | | isprm5 16590 |
. 2
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ โ โ ((๐โ2) โค ๐ โ ยฌ ๐ โฅ ๐))) |
115 | 12, 113, 114 | sylanbrc 584 |
1
โข (๐ โ ๐ โ โ) |