Step | Hyp | Ref
| Expression |
1 | | elfzoelz 10147 |
. . . . . . 7
โข (๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โ ๐ต โ โค) |
2 | 1 | adantr 276 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ต โ โค) |
3 | | zmodcl 10344 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ด mod ๐) โ
โ0) |
4 | 3 | adantl 277 |
. . . . . . 7
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ด mod ๐) โ
โ0) |
5 | 4 | nn0zd 9373 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ด mod ๐) โ โค) |
6 | 2, 5 | zaddcld 9379 |
. . . . 5
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ต + (๐ด mod ๐)) โ โค) |
7 | | zq 9626 |
. . . . 5
โข ((๐ต + (๐ด mod ๐)) โ โค โ (๐ต + (๐ด mod ๐)) โ โ) |
8 | 6, 7 | syl 14 |
. . . 4
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ต + (๐ด mod ๐)) โ โ) |
9 | | simprr 531 |
. . . . 5
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ โ โ) |
10 | | nnq 9633 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
11 | 9, 10 | syl 14 |
. . . 4
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ โ โ) |
12 | 9 | nngt0d 8963 |
. . . 4
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ 0 < ๐) |
13 | | elfzole1 10155 |
. . . . . 6
โข (๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โ (๐ โ (๐ด mod ๐)) โค ๐ต) |
14 | 13 | adantr 276 |
. . . . 5
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ โ (๐ด mod ๐)) โค ๐ต) |
15 | 9 | nnred 8932 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ โ โ) |
16 | 3 | nn0red 9230 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ด mod ๐) โ โ) |
17 | 16 | adantl 277 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ด mod ๐) โ โ) |
18 | 1 | zred 9375 |
. . . . . . 7
โข (๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โ ๐ต โ โ) |
19 | 18 | adantr 276 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ต โ โ) |
20 | 15, 17, 19 | lesubaddd 8499 |
. . . . 5
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ((๐ โ (๐ด mod ๐)) โค ๐ต โ ๐ โค (๐ต + (๐ด mod ๐)))) |
21 | 14, 20 | mpbid 147 |
. . . 4
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ โค (๐ต + (๐ด mod ๐))) |
22 | | elfzolt2 10156 |
. . . . . . 7
โข (๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โ ๐ต < ๐) |
23 | 22 | adantr 276 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ต < ๐) |
24 | | zq 9626 |
. . . . . . . 8
โข (๐ด โ โค โ ๐ด โ
โ) |
25 | 24 | ad2antrl 490 |
. . . . . . 7
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ด โ โ) |
26 | | modqlt 10333 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ (๐ด mod ๐) < ๐) |
27 | 25, 11, 12, 26 | syl3anc 1238 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ด mod ๐) < ๐) |
28 | 19, 17, 15, 15, 23, 27 | lt2addd 8524 |
. . . . 5
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ต + (๐ด mod ๐)) < (๐ + ๐)) |
29 | 9 | nncnd 8933 |
. . . . . 6
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ โ โ) |
30 | 29 | 2timesd 9161 |
. . . . 5
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (2 ยท ๐) = (๐ + ๐)) |
31 | 28, 30 | breqtrrd 4032 |
. . . 4
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ (๐ต + (๐ด mod ๐)) < (2 ยท ๐)) |
32 | | q2submod 10385 |
. . . 4
โข ((((๐ต + (๐ด mod ๐)) โ โ โง ๐ โ โ โง 0 < ๐) โง (๐ โค (๐ต + (๐ด mod ๐)) โง (๐ต + (๐ด mod ๐)) < (2 ยท ๐))) โ ((๐ต + (๐ด mod ๐)) mod ๐) = ((๐ต + (๐ด mod ๐)) โ ๐)) |
33 | 8, 11, 12, 21, 31, 32 | syl32anc 1246 |
. . 3
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ((๐ต + (๐ด mod ๐)) mod ๐) = ((๐ต + (๐ด mod ๐)) โ ๐)) |
34 | | zq 9626 |
. . . . 5
โข (๐ต โ โค โ ๐ต โ
โ) |
35 | 2, 34 | syl 14 |
. . . 4
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ๐ต โ โ) |
36 | | modqadd2mod 10374 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง 0 <
๐)) โ ((๐ต + (๐ด mod ๐)) mod ๐) = ((๐ต + ๐ด) mod ๐)) |
37 | 25, 35, 11, 12, 36 | syl22anc 1239 |
. . 3
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ((๐ต + (๐ด mod ๐)) mod ๐) = ((๐ต + ๐ด) mod ๐)) |
38 | 33, 37 | eqtr3d 2212 |
. 2
โข ((๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โง (๐ด โ โค โง ๐ โ โ)) โ ((๐ต + (๐ด mod ๐)) โ ๐) = ((๐ต + ๐ด) mod ๐)) |
39 | 38 | expcom 116 |
1
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ต โ ((๐ โ (๐ด mod ๐))..^๐) โ ((๐ต + (๐ด mod ๐)) โ ๐) = ((๐ต + ๐ด) mod ๐))) |