Step | Hyp | Ref
| Expression |
1 | | gausslemma2dlem0a.p |
. . . . 5
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | | eldifi 4087 |
. . . . 5
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
3 | 1, 2 | syl 17 |
. . . 4
โข (๐ โ ๐ โ โ) |
4 | | gausslemma2dlem0b.h |
. . . . . 6
โข ๐ป = ((๐ โ 1) / 2) |
5 | 1, 4 | gausslemma2dlem0b 26708 |
. . . . 5
โข (๐ โ ๐ป โ โ) |
6 | 5 | nnnn0d 12474 |
. . . 4
โข (๐ โ ๐ป โ
โ0) |
7 | 3, 6 | jca 513 |
. . 3
โข (๐ โ (๐ โ โ โง ๐ป โ
โ0)) |
8 | | prmnn 16551 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
9 | | nnre 12161 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
10 | | peano2rem 11469 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
12 | | 2re 12228 |
. . . . . . . . . 10
โข 2 โ
โ |
13 | 12 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ 2 โ
โ) |
14 | 13, 9 | remulcld 11186 |
. . . . . . . 8
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
15 | 9 | ltm1d 12088 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) < ๐) |
16 | | nnnn0 12421 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
17 | 16 | nn0ge0d 12477 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โค
๐) |
18 | | 1le2 12363 |
. . . . . . . . . 10
โข 1 โค
2 |
19 | 18 | a1i 11 |
. . . . . . . . 9
โข (๐ โ โ โ 1 โค
2) |
20 | 9, 13, 17, 19 | lemulge12d 12094 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โค (2 ยท ๐)) |
21 | 11, 9, 14, 15, 20 | ltletrd 11316 |
. . . . . . 7
โข (๐ โ โ โ (๐ โ 1) < (2 ยท
๐)) |
22 | | 2pos 12257 |
. . . . . . . . . 10
โข 0 <
2 |
23 | 12, 22 | pm3.2i 472 |
. . . . . . . . 9
โข (2 โ
โ โง 0 < 2) |
24 | 23 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ (2 โ
โ โง 0 < 2)) |
25 | | ltdivmul 12031 |
. . . . . . . 8
โข (((๐ โ 1) โ โ โง
๐ โ โ โง (2
โ โ โง 0 < 2)) โ (((๐ โ 1) / 2) < ๐ โ (๐ โ 1) < (2 ยท ๐))) |
26 | 11, 9, 24, 25 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ โ โ (((๐ โ 1) / 2) < ๐ โ (๐ โ 1) < (2 ยท ๐))) |
27 | 21, 26 | mpbird 257 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ 1) / 2) < ๐) |
28 | 2, 8, 27 | 3syl 18 |
. . . . 5
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
< ๐) |
29 | 1, 28 | syl 17 |
. . . 4
โข (๐ โ ((๐ โ 1) / 2) < ๐) |
30 | 4, 29 | eqbrtrid 5141 |
. . 3
โข (๐ โ ๐ป < ๐) |
31 | | prmndvdsfaclt 16602 |
. . 3
โข ((๐ โ โ โง ๐ป โ โ0)
โ (๐ป < ๐ โ ยฌ ๐ โฅ (!โ๐ป))) |
32 | 7, 30, 31 | sylc 65 |
. 2
โข (๐ โ ยฌ ๐ โฅ (!โ๐ป)) |
33 | 6 | faccld 14185 |
. . . . . 6
โข (๐ โ (!โ๐ป) โ โ) |
34 | 33 | nnzd 12527 |
. . . . 5
โข (๐ โ (!โ๐ป) โ โค) |
35 | | nnz 12521 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
36 | 2, 8, 35 | 3syl 18 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
37 | 1, 36 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โค) |
38 | 34, 37 | gcdcomd 16395 |
. . . 4
โข (๐ โ ((!โ๐ป) gcd ๐) = (๐ gcd (!โ๐ป))) |
39 | 38 | eqeq1d 2739 |
. . 3
โข (๐ โ (((!โ๐ป) gcd ๐) = 1 โ (๐ gcd (!โ๐ป)) = 1)) |
40 | | coprm 16588 |
. . . 4
โข ((๐ โ โ โง
(!โ๐ป) โ โค)
โ (ยฌ ๐ โฅ
(!โ๐ป) โ (๐ gcd (!โ๐ป)) = 1)) |
41 | 3, 34, 40 | syl2anc 585 |
. . 3
โข (๐ โ (ยฌ ๐ โฅ (!โ๐ป) โ (๐ gcd (!โ๐ป)) = 1)) |
42 | 39, 41 | bitr4d 282 |
. 2
โข (๐ โ (((!โ๐ป) gcd ๐) = 1 โ ยฌ ๐ โฅ (!โ๐ป))) |
43 | 32, 42 | mpbird 257 |
1
โข (๐ โ ((!โ๐ป) gcd ๐) = 1) |