Step | Hyp | Ref
| Expression |
1 | | pockthg.4 |
. . 3
โข (๐ โ ๐ = ((๐ด ยท ๐ต) + 1)) |
2 | | pockthg.1 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
3 | | pockthg.2 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
4 | 2, 3 | nnmulcld 8967 |
. . . . . 6
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
5 | | nnuz 9562 |
. . . . . 6
โข โ =
(โคโฅโ1) |
6 | 4, 5 | eleqtrdi 2270 |
. . . . 5
โข (๐ โ (๐ด ยท ๐ต) โ
(โคโฅโ1)) |
7 | | eluzp1p1 9552 |
. . . . 5
โข ((๐ด ยท ๐ต) โ (โคโฅโ1)
โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ(1 + 1))) |
8 | 6, 7 | syl 14 |
. . . 4
โข (๐ โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ(1 + 1))) |
9 | | df-2 8977 |
. . . . 5
โข 2 = (1 +
1) |
10 | 9 | fveq2i 5518 |
. . . 4
โข
(โคโฅโ2) = (โคโฅโ(1 +
1)) |
11 | 8, 10 | eleqtrrdi 2271 |
. . 3
โข (๐ โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ2)) |
12 | 1, 11 | eqeltrd 2254 |
. 2
โข (๐ โ ๐ โ
(โคโฅโ2)) |
13 | | eluzelre 9537 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
14 | 12, 13 | syl 14 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
15 | 14 | adantr 276 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
16 | 2 | nnred 8931 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
17 | 16 | resqcld 10679 |
. . . . . . . 8
โข (๐ โ (๐ดโ2) โ โ) |
18 | 17 | adantr 276 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ดโ2) โ โ) |
19 | | prmnn 12109 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
20 | 19 | ad2antrl 490 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
21 | 20 | nnred 8931 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
22 | 21 | resqcld 10679 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐โ2) โ โ) |
23 | | pockthg.3 |
. . . . . . . . . . 11
โข (๐ โ ๐ต < ๐ด) |
24 | 3 | nnred 8931 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โ) |
25 | 2 | nngt0d 8962 |
. . . . . . . . . . . 12
โข (๐ โ 0 < ๐ด) |
26 | | ltmul2 8812 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ด โ โ โง (๐ด โ โ โง 0 <
๐ด)) โ (๐ต < ๐ด โ (๐ด ยท ๐ต) < (๐ด ยท ๐ด))) |
27 | 24, 16, 16, 25, 26 | syl112anc 1242 |
. . . . . . . . . . 11
โข (๐ โ (๐ต < ๐ด โ (๐ด ยท ๐ต) < (๐ด ยท ๐ด))) |
28 | 23, 27 | mpbid 147 |
. . . . . . . . . 10
โข (๐ โ (๐ด ยท ๐ต) < (๐ด ยท ๐ด)) |
29 | 2, 2 | nnmulcld 8967 |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท ๐ด) โ โ) |
30 | | nnltp1le 9312 |
. . . . . . . . . . 11
โข (((๐ด ยท ๐ต) โ โ โง (๐ด ยท ๐ด) โ โ) โ ((๐ด ยท ๐ต) < (๐ด ยท ๐ด) โ ((๐ด ยท ๐ต) + 1) โค (๐ด ยท ๐ด))) |
31 | 4, 29, 30 | syl2anc 411 |
. . . . . . . . . 10
โข (๐ โ ((๐ด ยท ๐ต) < (๐ด ยท ๐ด) โ ((๐ด ยท ๐ต) + 1) โค (๐ด ยท ๐ด))) |
32 | 28, 31 | mpbid 147 |
. . . . . . . . 9
โข (๐ โ ((๐ด ยท ๐ต) + 1) โค (๐ด ยท ๐ด)) |
33 | 2 | nncnd 8932 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
34 | 33 | sqvald 10650 |
. . . . . . . . 9
โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
35 | 32, 1, 34 | 3brtr4d 4035 |
. . . . . . . 8
โข (๐ โ ๐ โค (๐ดโ2)) |
36 | 35 | adantr 276 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โค (๐ดโ2)) |
37 | | pockthg.5 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ โ (๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) |
38 | 37 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ โ๐ โ โ (๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) |
39 | | prmnn 12109 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
40 | 39 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โ โ) |
41 | 40 | nncnd 8932 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โ โ) |
42 | 41 | exp1d 10648 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (๐โ1) = ๐) |
43 | | nnge1 8941 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ pCnt ๐ด) โ โ โ 1 โค (๐ pCnt ๐ด)) |
44 | 43 | ad2antll 491 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ 1 โค (๐ pCnt ๐ด)) |
45 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โ โ) |
46 | 2 | nnzd 9373 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ด โ โค) |
47 | 46 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ด โ โค) |
48 | | 1nn0 9191 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
โ0 |
49 | 48 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ 1 โ
โ0) |
50 | | pcdvdsb 12318 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ด โ โค โง 1 โ
โ0) โ (1 โค (๐ pCnt ๐ด) โ (๐โ1) โฅ ๐ด)) |
51 | 45, 47, 49, 50 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (1 โค (๐ pCnt ๐ด) โ (๐โ1) โฅ ๐ด)) |
52 | 44, 51 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (๐โ1) โฅ ๐ด) |
53 | 42, 52 | eqbrtrrd 4027 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ๐ โฅ ๐ด) |
54 | | simpl1 1000 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐) |
55 | 54, 2 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ด โ โ) |
56 | 54, 3 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ต โ โ) |
57 | 54, 23 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ต < ๐ด) |
58 | 54, 1 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ = ((๐ด ยท ๐ต) + 1)) |
59 | | simpl2l 1050 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ โ โ) |
60 | | simpl2r 1051 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ โฅ ๐) |
61 | | simpl3l 1052 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ โ โ) |
62 | | simpl3r 1053 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ (๐ pCnt ๐ด) โ โ) |
63 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ๐ฅ โ โค) |
64 | | simprrl 539 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ ((๐ฅโ(๐ โ 1)) mod ๐) = 1) |
65 | | simprrr 540 |
. . . . . . . . . . . . . . . . . . 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 12353 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โง (๐ฅ โ โค โง (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1))) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))) |
67 | 66 | rexlimdvaa 2595 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
68 | 67 | 3expa 1203 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ (โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
69 | 53, 68 | embantd 56 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ)) โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
70 | 69 | expr 375 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) โ โ โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))))) |
71 | | id 19 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ) |
72 | | prmuz2 12130 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
73 | | uz2m1nn 9604 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
75 | 74 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ โ 1) โ โ) |
76 | | pccl 12298 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ (๐ pCnt (๐ โ 1)) โ
โ0) |
77 | 71, 75, 76 | syl2anr 290 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ (๐ pCnt (๐ โ 1)) โ
โ0) |
78 | 77 | nn0ge0d 9231 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ 0 โค (๐ pCnt (๐ โ 1))) |
79 | | breq1 4006 |
. . . . . . . . . . . . . . . 16
โข ((๐ pCnt ๐ด) = 0 โ ((๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)) โ 0 โค (๐ pCnt (๐ โ 1)))) |
80 | 78, 79 | syl5ibrcom 157 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) = 0 โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
81 | 80 | a1dd 48 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) = 0 โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))))) |
82 | | simpr 110 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ๐ โ โ) |
83 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ๐ด โ โ) |
84 | 82, 83 | pccld 12299 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ (๐ pCnt ๐ด) โ
โ0) |
85 | | elnn0 9177 |
. . . . . . . . . . . . . . 15
โข ((๐ pCnt ๐ด) โ โ0 โ ((๐ pCnt ๐ด) โ โ โจ (๐ pCnt ๐ด) = 0)) |
86 | 84, 85 | sylib 122 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ pCnt ๐ด) โ โ โจ (๐ pCnt ๐ด) = 0)) |
87 | 70, 81, 86 | mpjaod 718 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โง ๐ โ โ) โ ((๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
88 | 87 | ralimdva 2544 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (โ๐ โ โ (๐ โฅ ๐ด โ โ๐ฅ โ โค (((๐ฅโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฅโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1)) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
89 | 38, 88 | mpd 13 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))) |
90 | 75 | nnzd 9373 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ โ 1) โ โค) |
91 | | pc2dvds 12328 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง (๐ โ 1) โ โค)
โ (๐ด โฅ (๐ โ 1) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
92 | 46, 90, 91 | syl2an2r 595 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด โฅ (๐ โ 1) โ โ๐ โ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)))) |
93 | 89, 92 | mpbird 167 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โฅ (๐ โ 1)) |
94 | | dvdsle 11849 |
. . . . . . . . . . 11
โข ((๐ด โ โค โง (๐ โ 1) โ โ)
โ (๐ด โฅ (๐ โ 1) โ ๐ด โค (๐ โ 1))) |
95 | 46, 75, 94 | syl2an2r 595 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด โฅ (๐ โ 1) โ ๐ด โค (๐ โ 1))) |
96 | 93, 95 | mpd 13 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โค (๐ โ 1)) |
97 | 2 | nnnn0d 9228 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ
โ0) |
98 | 20 | nnnn0d 9228 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ0) |
99 | | nn0ltlem1 9316 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ0) โ (๐ด < ๐ โ ๐ด โค (๐ โ 1))) |
100 | 97, 98, 99 | syl2an2r 595 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด < ๐ โ ๐ด โค (๐ โ 1))) |
101 | 96, 100 | mpbird 167 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด < ๐) |
102 | 16 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โ โ) |
103 | 97 | nn0ge0d 9231 |
. . . . . . . . . 10
โข (๐ โ 0 โค ๐ด) |
104 | 103 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ 0 โค ๐ด) |
105 | 98 | nn0ge0d 9231 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ 0 โค ๐) |
106 | 102, 21, 104, 105 | lt2sqd 10684 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ด < ๐ โ (๐ดโ2) < (๐โ2))) |
107 | 101, 106 | mpbid 147 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ดโ2) < (๐โ2)) |
108 | 15, 18, 22, 36, 107 | lelttrd 8081 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ < (๐โ2)) |
109 | | dvdszrcl 11798 |
. . . . . . . . 9
โข (๐ โฅ ๐ โ (๐ โ โค โง ๐ โ โค)) |
110 | 109 | simprd 114 |
. . . . . . . 8
โข (๐ โฅ ๐ โ ๐ โ โค) |
111 | 110 | ad2antll 491 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โค) |
112 | 20 | nnzd 9373 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โค) |
113 | | zsqcl 10590 |
. . . . . . . 8
โข (๐ โ โค โ (๐โ2) โ
โค) |
114 | 112, 113 | syl 14 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐โ2) โ โค) |
115 | | zltnle 9298 |
. . . . . . 7
โข ((๐ โ โค โง (๐โ2) โ โค) โ
(๐ < (๐โ2) โ ยฌ (๐โ2) โค ๐)) |
116 | 111, 114,
115 | syl2anc 411 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ < (๐โ2) โ ยฌ (๐โ2) โค ๐)) |
117 | 108, 116 | mpbid 147 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โฅ ๐)) โ ยฌ (๐โ2) โค ๐) |
118 | 117 | expr 375 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (๐ โฅ ๐ โ ยฌ (๐โ2) โค ๐)) |
119 | 118 | con2d 624 |
. . 3
โข ((๐ โง ๐ โ โ) โ ((๐โ2) โค ๐ โ ยฌ ๐ โฅ ๐)) |
120 | 119 | ralrimiva 2550 |
. 2
โข (๐ โ โ๐ โ โ ((๐โ2) โค ๐ โ ยฌ ๐ โฅ ๐)) |
121 | | isprm5 12141 |
. 2
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ โ โ ((๐โ2) โค ๐ โ ยฌ ๐ โฅ ๐))) |
122 | 12, 120, 121 | sylanbrc 417 |
1
โข (๐ โ ๐ โ โ) |