Step | Hyp | Ref
| Expression |
1 | | eluzelcn 12780 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
2 | 1 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ โ) |
3 | | zcn 12509 |
. . . . . . . . 9
โข (๐ด โ โค โ ๐ด โ
โ) |
4 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ด โ โ) |
5 | 2, 4 | mulcomd 11181 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (๐ ยท ๐ด) = (๐ด ยท ๐)) |
6 | 5 | oveq1d 7373 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((๐ ยท ๐ด) mod ๐) = ((๐ด ยท ๐) mod ๐)) |
7 | | eluz2nn 12814 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
8 | 7 | nnrpd 12960 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ ๐ โ
โ+) |
9 | | mulmod0 13788 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ โ+)
โ ((๐ด ยท ๐) mod ๐) = 0) |
10 | 8, 9 | sylan2 594 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((๐ด ยท ๐) mod ๐) = 0) |
11 | 6, 10 | eqtrd 2773 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((๐ ยท ๐ด) mod ๐) = 0) |
12 | 11 | oveq1d 7373 |
. . . 4
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (((๐ ยท ๐ด) mod ๐) + 1) = (0 + 1)) |
13 | | 0p1e1 12280 |
. . . 4
โข (0 + 1) =
1 |
14 | 12, 13 | eqtrdi 2789 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (((๐ ยท ๐ด) mod ๐) + 1) = 1) |
15 | 14 | oveq1d 7373 |
. 2
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((((๐ ยท ๐ด) mod ๐) + 1) mod ๐) = (1 mod ๐)) |
16 | | eluzelre 12779 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
17 | 16 | adantl 483 |
. . . 4
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ โ) |
18 | | zre 12508 |
. . . . 5
โข (๐ด โ โค โ ๐ด โ
โ) |
19 | 18 | adantr 482 |
. . . 4
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ด โ โ) |
20 | 17, 19 | remulcld 11190 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (๐ ยท ๐ด) โ โ) |
21 | | 1red 11161 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 1 โ โ) |
22 | 8 | adantl 483 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ
โ+) |
23 | | modaddmod 13821 |
. . 3
โข (((๐ ยท ๐ด) โ โ โง 1 โ โ
โง ๐ โ
โ+) โ ((((๐ ยท ๐ด) mod ๐) + 1) mod ๐) = (((๐ ยท ๐ด) + 1) mod ๐)) |
24 | 20, 21, 22, 23 | syl3anc 1372 |
. 2
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((((๐ ยท ๐ด) mod ๐) + 1) mod ๐) = (((๐ ยท ๐ด) + 1) mod ๐)) |
25 | | eluz2gt1 12850 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
26 | 16, 25 | jca 513 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ (๐ โ โ โง 1 < ๐)) |
27 | 26 | adantl 483 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (๐ โ โ โง 1 < ๐)) |
28 | | 1mod 13814 |
. . 3
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
29 | 27, 28 | syl 17 |
. 2
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (1 mod ๐) = 1) |
30 | 15, 24, 29 | 3eqtr3d 2781 |
1
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (((๐ ยท ๐ด) + 1) mod ๐) = 1) |