Step | Hyp | Ref
| Expression |
1 | | eqeq2 2748 |
. 2
โข
((ฯโ(๐ /
๐)) = if(๐ โฅ ๐, (ฯโ(๐ / ๐)), 0) โ ((โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = (ฯโ(๐ / ๐)) โ (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = if(๐ โฅ ๐, (ฯโ(๐ / ๐)), 0))) |
2 | | eqeq2 2748 |
. 2
โข (0 =
if(๐ โฅ ๐, (ฯโ(๐ / ๐)), 0) โ ((โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = 0 โ (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = if(๐ โฅ ๐, (ฯโ(๐ / ๐)), 0))) |
3 | | nndivdvds 16145 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ (๐ / ๐) โ โ)) |
4 | 3 | biimpa 477 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โฅ ๐) โ (๐ / ๐) โ โ) |
5 | | dfphi2 16646 |
. . . 4
โข ((๐ / ๐) โ โ โ (ฯโ(๐ / ๐)) = (โฏโ{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1})) |
6 | 4, 5 | syl 17 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โฅ ๐) โ (ฯโ(๐ / ๐)) = (โฏโ{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1})) |
7 | | eqid 2736 |
. . . . . 6
โข {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} = {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} |
8 | | eqid 2736 |
. . . . . 6
โข {๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐} = {๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐} |
9 | | eqid 2736 |
. . . . . 6
โข (๐ง โ {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โฆ (๐ง ยท ๐)) = (๐ง โ {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โฆ (๐ง ยท ๐)) |
10 | 7, 8, 9 | hashgcdlem 16660 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ โง ๐ โฅ ๐) โ (๐ง โ {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โฆ (๐ง ยท ๐)):{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1}โ1-1-ontoโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) |
11 | 10 | 3expa 1118 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โฅ ๐) โ (๐ง โ {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โฆ (๐ง ยท ๐)):{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1}โ1-1-ontoโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) |
12 | | ovex 7390 |
. . . . . 6
โข
(0..^(๐ / ๐)) โ V |
13 | 12 | rabex 5289 |
. . . . 5
โข {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โ V |
14 | 13 | f1oen 8913 |
. . . 4
โข ((๐ง โ {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โฆ (๐ง ยท ๐)):{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1}โ1-1-ontoโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐} โ {๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โ {๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) |
15 | | hasheni 14248 |
. . . 4
โข ({๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1} โ {๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐} โ (โฏโ{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1}) = (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐})) |
16 | 11, 14, 15 | 3syl 18 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โฅ ๐) โ (โฏโ{๐ฆ โ (0..^(๐ / ๐)) โฃ (๐ฆ gcd (๐ / ๐)) = 1}) = (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐})) |
17 | 6, 16 | eqtr2d 2777 |
. 2
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โฅ ๐) โ (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = (ฯโ(๐ / ๐))) |
18 | | simprr 771 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ (0..^๐) โง (๐ฅ gcd ๐) = ๐)) โ (๐ฅ gcd ๐) = ๐) |
19 | | elfzoelz 13572 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (0..^๐) โ ๐ฅ โ โค) |
20 | 19 | ad2antrl 726 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ (0..^๐) โง (๐ฅ gcd ๐) = ๐)) โ ๐ฅ โ โค) |
21 | | nnz 12520 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โค) |
22 | 21 | ad2antrr 724 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ (0..^๐) โง (๐ฅ gcd ๐) = ๐)) โ ๐ โ โค) |
23 | | gcddvds 16383 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง ๐ โ โค) โ ((๐ฅ gcd ๐) โฅ ๐ฅ โง (๐ฅ gcd ๐) โฅ ๐)) |
24 | 20, 22, 23 | syl2anc 584 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ (0..^๐) โง (๐ฅ gcd ๐) = ๐)) โ ((๐ฅ gcd ๐) โฅ ๐ฅ โง (๐ฅ gcd ๐) โฅ ๐)) |
25 | 24 | simprd 496 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ (0..^๐) โง (๐ฅ gcd ๐) = ๐)) โ (๐ฅ gcd ๐) โฅ ๐) |
26 | 18, 25 | eqbrtrrd 5129 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ (0..^๐) โง (๐ฅ gcd ๐) = ๐)) โ ๐ โฅ ๐) |
27 | 26 | expr 457 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฅ โ (0..^๐)) โ ((๐ฅ gcd ๐) = ๐ โ ๐ โฅ ๐)) |
28 | 27 | con3d 152 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ฅ โ (0..^๐)) โ (ยฌ ๐ โฅ ๐ โ ยฌ (๐ฅ gcd ๐) = ๐)) |
29 | 28 | impancom 452 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ยฌ
๐ โฅ ๐) โ (๐ฅ โ (0..^๐) โ ยฌ (๐ฅ gcd ๐) = ๐)) |
30 | 29 | ralrimiv 3142 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ยฌ
๐ โฅ ๐) โ โ๐ฅ โ (0..^๐) ยฌ (๐ฅ gcd ๐) = ๐) |
31 | | rabeq0 4344 |
. . . . 5
โข ({๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐} = โ
โ โ๐ฅ โ (0..^๐) ยฌ (๐ฅ gcd ๐) = ๐) |
32 | 30, 31 | sylibr 233 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ยฌ
๐ โฅ ๐) โ {๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐} = โ
) |
33 | 32 | fveq2d 6846 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ยฌ
๐ โฅ ๐) โ (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) =
(โฏโโ
)) |
34 | | hash0 14267 |
. . 3
โข
(โฏโโ
) = 0 |
35 | 33, 34 | eqtrdi 2792 |
. 2
โข (((๐ โ โ โง ๐ โ โ) โง ยฌ
๐ โฅ ๐) โ (โฏโ{๐ฅ โ (0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = 0) |
36 | 1, 2, 17, 35 | ifbothda 4524 |
1
โข ((๐ โ โ โง ๐ โ โ) โ
(โฏโ{๐ฅ โ
(0..^๐) โฃ (๐ฅ gcd ๐) = ๐}) = if(๐ โฅ ๐, (ฯโ(๐ / ๐)), 0)) |