Step | Hyp | Ref
| Expression |
1 | | modqexp.c |
. 2
โข (๐ โ ๐ถ โ
โ0) |
2 | | oveq2 5882 |
. . . . . 6
โข (๐ค = 0 โ (๐ดโ๐ค) = (๐ดโ0)) |
3 | 2 | oveq1d 5889 |
. . . . 5
โข (๐ค = 0 โ ((๐ดโ๐ค) mod ๐ท) = ((๐ดโ0) mod ๐ท)) |
4 | | oveq2 5882 |
. . . . . 6
โข (๐ค = 0 โ (๐ตโ๐ค) = (๐ตโ0)) |
5 | 4 | oveq1d 5889 |
. . . . 5
โข (๐ค = 0 โ ((๐ตโ๐ค) mod ๐ท) = ((๐ตโ0) mod ๐ท)) |
6 | 3, 5 | eqeq12d 2192 |
. . . 4
โข (๐ค = 0 โ (((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท) โ ((๐ดโ0) mod ๐ท) = ((๐ตโ0) mod ๐ท))) |
7 | 6 | imbi2d 230 |
. . 3
โข (๐ค = 0 โ ((๐ โ ((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท)) โ (๐ โ ((๐ดโ0) mod ๐ท) = ((๐ตโ0) mod ๐ท)))) |
8 | | oveq2 5882 |
. . . . . 6
โข (๐ค = ๐ โ (๐ดโ๐ค) = (๐ดโ๐)) |
9 | 8 | oveq1d 5889 |
. . . . 5
โข (๐ค = ๐ โ ((๐ดโ๐ค) mod ๐ท) = ((๐ดโ๐) mod ๐ท)) |
10 | | oveq2 5882 |
. . . . . 6
โข (๐ค = ๐ โ (๐ตโ๐ค) = (๐ตโ๐)) |
11 | 10 | oveq1d 5889 |
. . . . 5
โข (๐ค = ๐ โ ((๐ตโ๐ค) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) |
12 | 9, 11 | eqeq12d 2192 |
. . . 4
โข (๐ค = ๐ โ (((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท) โ ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท))) |
13 | 12 | imbi2d 230 |
. . 3
โข (๐ค = ๐ โ ((๐ โ ((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท)) โ (๐ โ ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)))) |
14 | | oveq2 5882 |
. . . . . 6
โข (๐ค = (๐ + 1) โ (๐ดโ๐ค) = (๐ดโ(๐ + 1))) |
15 | 14 | oveq1d 5889 |
. . . . 5
โข (๐ค = (๐ + 1) โ ((๐ดโ๐ค) mod ๐ท) = ((๐ดโ(๐ + 1)) mod ๐ท)) |
16 | | oveq2 5882 |
. . . . . 6
โข (๐ค = (๐ + 1) โ (๐ตโ๐ค) = (๐ตโ(๐ + 1))) |
17 | 16 | oveq1d 5889 |
. . . . 5
โข (๐ค = (๐ + 1) โ ((๐ตโ๐ค) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท)) |
18 | 15, 17 | eqeq12d 2192 |
. . . 4
โข (๐ค = (๐ + 1) โ (((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท) โ ((๐ดโ(๐ + 1)) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท))) |
19 | 18 | imbi2d 230 |
. . 3
โข (๐ค = (๐ + 1) โ ((๐ โ ((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท)) โ (๐ โ ((๐ดโ(๐ + 1)) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท)))) |
20 | | oveq2 5882 |
. . . . . 6
โข (๐ค = ๐ถ โ (๐ดโ๐ค) = (๐ดโ๐ถ)) |
21 | 20 | oveq1d 5889 |
. . . . 5
โข (๐ค = ๐ถ โ ((๐ดโ๐ค) mod ๐ท) = ((๐ดโ๐ถ) mod ๐ท)) |
22 | | oveq2 5882 |
. . . . . 6
โข (๐ค = ๐ถ โ (๐ตโ๐ค) = (๐ตโ๐ถ)) |
23 | 22 | oveq1d 5889 |
. . . . 5
โข (๐ค = ๐ถ โ ((๐ตโ๐ค) mod ๐ท) = ((๐ตโ๐ถ) mod ๐ท)) |
24 | 21, 23 | eqeq12d 2192 |
. . . 4
โข (๐ค = ๐ถ โ (((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท) โ ((๐ดโ๐ถ) mod ๐ท) = ((๐ตโ๐ถ) mod ๐ท))) |
25 | 24 | imbi2d 230 |
. . 3
โข (๐ค = ๐ถ โ ((๐ โ ((๐ดโ๐ค) mod ๐ท) = ((๐ตโ๐ค) mod ๐ท)) โ (๐ โ ((๐ดโ๐ถ) mod ๐ท) = ((๐ตโ๐ถ) mod ๐ท)))) |
26 | | modqexp.a |
. . . . . . 7
โข (๐ โ ๐ด โ โค) |
27 | 26 | zcnd 9375 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
28 | | exp0 10523 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ0) = 1) |
29 | 27, 28 | syl 14 |
. . . . 5
โข (๐ โ (๐ดโ0) = 1) |
30 | | modqexp.b |
. . . . . . 7
โข (๐ โ ๐ต โ โค) |
31 | 30 | zcnd 9375 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
32 | | exp0 10523 |
. . . . . 6
โข (๐ต โ โ โ (๐ตโ0) = 1) |
33 | 31, 32 | syl 14 |
. . . . 5
โข (๐ โ (๐ตโ0) = 1) |
34 | 29, 33 | eqtr4d 2213 |
. . . 4
โข (๐ โ (๐ดโ0) = (๐ตโ0)) |
35 | 34 | oveq1d 5889 |
. . 3
โข (๐ โ ((๐ดโ0) mod ๐ท) = ((๐ตโ0) mod ๐ท)) |
36 | | zexpcl 10534 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ โ0)
โ (๐ดโ๐) โ
โค) |
37 | 26, 36 | sylan 283 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โค) |
38 | 37 | adantr 276 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (๐ดโ๐) โ โค) |
39 | | zexpcl 10534 |
. . . . . . . . . 10
โข ((๐ต โ โค โง ๐ โ โ0)
โ (๐ตโ๐) โ
โค) |
40 | 30, 39 | sylan 283 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ตโ๐) โ โค) |
41 | 40 | adantr 276 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (๐ตโ๐) โ โค) |
42 | 26 | ad2antrr 488 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ๐ด โ โค) |
43 | 30 | ad2antrr 488 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ๐ต โ โค) |
44 | | modqexp.dq |
. . . . . . . . 9
โข (๐ โ ๐ท โ โ) |
45 | 44 | ad2antrr 488 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ๐ท โ โ) |
46 | | modqexp.dgt0 |
. . . . . . . . 9
โข (๐ โ 0 < ๐ท) |
47 | 46 | ad2antrr 488 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ 0 < ๐ท) |
48 | | simpr 110 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) |
49 | | modqexp.mod |
. . . . . . . . 9
โข (๐ โ (๐ด mod ๐ท) = (๐ต mod ๐ท)) |
50 | 49 | ad2antrr 488 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (๐ด mod ๐ท) = (๐ต mod ๐ท)) |
51 | 38, 41, 42, 43, 45, 47, 48, 50 | modqmul12d 10377 |
. . . . . . 7
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (((๐ดโ๐) ยท ๐ด) mod ๐ท) = (((๐ตโ๐) ยท ๐ต) mod ๐ท)) |
52 | 27 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ๐ด โ โ) |
53 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
54 | 53 | adantr 276 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ๐ โ โ0) |
55 | | expp1 10526 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
56 | 52, 54, 55 | syl2anc 411 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
57 | 56 | oveq1d 5889 |
. . . . . . 7
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ((๐ดโ(๐ + 1)) mod ๐ท) = (((๐ดโ๐) ยท ๐ด) mod ๐ท)) |
58 | 31 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ๐ต โ โ) |
59 | | expp1 10526 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
60 | 58, 54, 59 | syl2anc 411 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
61 | 60 | oveq1d 5889 |
. . . . . . 7
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ((๐ตโ(๐ + 1)) mod ๐ท) = (((๐ตโ๐) ยท ๐ต) mod ๐ท)) |
62 | 51, 57, 61 | 3eqtr4d 2220 |
. . . . . 6
โข (((๐ โง ๐ โ โ0) โง ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ ((๐ดโ(๐ + 1)) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท)) |
63 | 62 | ex 115 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท) โ ((๐ดโ(๐ + 1)) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท))) |
64 | 63 | expcom 116 |
. . . 4
โข (๐ โ โ0
โ (๐ โ (((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท) โ ((๐ดโ(๐ + 1)) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท)))) |
65 | 64 | a2d 26 |
. . 3
โข (๐ โ โ0
โ ((๐ โ ((๐ดโ๐) mod ๐ท) = ((๐ตโ๐) mod ๐ท)) โ (๐ โ ((๐ดโ(๐ + 1)) mod ๐ท) = ((๐ตโ(๐ + 1)) mod ๐ท)))) |
66 | 7, 13, 19, 25, 35, 65 | nn0ind 9366 |
. 2
โข (๐ถ โ โ0
โ (๐ โ ((๐ดโ๐ถ) mod ๐ท) = ((๐ตโ๐ถ) mod ๐ท))) |
67 | 1, 66 | mpcom 36 |
1
โข (๐ โ ((๐ดโ๐ถ) mod ๐ท) = ((๐ตโ๐ถ) mod ๐ท)) |