Step | Hyp | Ref
| Expression |
1 | | eluzelcn 9541 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
2 | 1 | adantl 277 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ โ) |
3 | | simpl 109 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ด โ โค) |
4 | 3 | zcnd 9378 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ด โ โ) |
5 | 2, 4 | mulcomd 7981 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (๐ ยท ๐ด) = (๐ด ยท ๐)) |
6 | 5 | oveq1d 5892 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((๐ ยท ๐ด) mod ๐) = ((๐ด ยท ๐) mod ๐)) |
7 | | eluzelz 9539 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ ๐ โ โค) |
8 | | zq 9628 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
9 | 7, 8 | syl 14 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
10 | 9 | adantl 277 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ โ) |
11 | | 0red 7960 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 0 โ โ) |
12 | | 2re 8991 |
. . . . . . . . 9
โข 2 โ
โ |
13 | 12 | a1i 9 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 2 โ โ) |
14 | 7 | adantl 277 |
. . . . . . . . 9
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ โค) |
15 | 14 | zred 9377 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ โ โ) |
16 | | 2pos 9012 |
. . . . . . . . 9
โข 0 <
2 |
17 | 16 | a1i 9 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 0 < 2) |
18 | | eluzle 9542 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ2) โ 2 โค ๐) |
19 | 18 | adantl 277 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 2 โค ๐) |
20 | 11, 13, 15, 17, 19 | ltletrd 8382 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 0 < ๐) |
21 | | mulqmod0 10332 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ โ โง 0 <
๐) โ ((๐ด ยท ๐) mod ๐) = 0) |
22 | 3, 10, 20, 21 | syl3anc 1238 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((๐ด ยท ๐) mod ๐) = 0) |
23 | 6, 22 | eqtrd 2210 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((๐ ยท ๐ด) mod ๐) = 0) |
24 | 23 | oveq1d 5892 |
. . . 4
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (((๐ ยท ๐ด) mod ๐) + 1) = (0 + 1)) |
25 | | 0p1e1 9035 |
. . . 4
โข (0 + 1) =
1 |
26 | 24, 25 | eqtrdi 2226 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (((๐ ยท ๐ด) mod ๐) + 1) = 1) |
27 | 26 | oveq1d 5892 |
. 2
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((((๐ ยท ๐ด) mod ๐) + 1) mod ๐) = (1 mod ๐)) |
28 | | zq 9628 |
. . . . 5
โข (๐ด โ โค โ ๐ด โ
โ) |
29 | 3, 28 | syl 14 |
. . . 4
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ๐ด โ โ) |
30 | | qmulcl 9639 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ ยท ๐ด) โ โ) |
31 | 10, 29, 30 | syl2anc 411 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (๐ ยท ๐ด) โ โ) |
32 | | 1z 9281 |
. . . 4
โข 1 โ
โค |
33 | | zq 9628 |
. . . 4
โข (1 โ
โค โ 1 โ โ) |
34 | 32, 33 | mp1i 10 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 1 โ โ) |
35 | | modqaddmod 10365 |
. . 3
โข ((((๐ ยท ๐ด) โ โ โง 1 โ โ)
โง (๐ โ โ
โง 0 < ๐)) โ
((((๐ ยท ๐ด) mod ๐) + 1) mod ๐) = (((๐ ยท ๐ด) + 1) mod ๐)) |
36 | 31, 34, 10, 20, 35 | syl22anc 1239 |
. 2
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ ((((๐ ยท ๐ด) mod ๐) + 1) mod ๐) = (((๐ ยท ๐ด) + 1) mod ๐)) |
37 | | eluz2gt1 9604 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
38 | 37 | adantl 277 |
. . 3
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ 1 < ๐) |
39 | | q1mod 10358 |
. . 3
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
40 | 10, 38, 39 | syl2anc 411 |
. 2
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (1 mod ๐) = 1) |
41 | 27, 36, 40 | 3eqtr3d 2218 |
1
โข ((๐ด โ โค โง ๐ โ
(โคโฅโ2)) โ (((๐ ยท ๐ด) + 1) mod ๐) = 1) |