Step | Hyp | Ref
| Expression |
1 | | elnn0 12474 |
. 2
โข (๐ต โ โ0
โ (๐ต โ โ
โจ ๐ต =
0)) |
2 | | oveq2 7417 |
. . . . . . 7
โข (๐ง = 1 โ (๐ดโ๐ง) = (๐ดโ1)) |
3 | 2 | eleq1d 2819 |
. . . . . 6
โข (๐ง = 1 โ ((๐ดโ๐ง) โ ๐น โ (๐ดโ1) โ ๐น)) |
4 | 3 | imbi2d 341 |
. . . . 5
โข (๐ง = 1 โ ((๐ด โ ๐น โ (๐ดโ๐ง) โ ๐น) โ (๐ด โ ๐น โ (๐ดโ1) โ ๐น))) |
5 | | oveq2 7417 |
. . . . . . 7
โข (๐ง = ๐ค โ (๐ดโ๐ง) = (๐ดโ๐ค)) |
6 | 5 | eleq1d 2819 |
. . . . . 6
โข (๐ง = ๐ค โ ((๐ดโ๐ง) โ ๐น โ (๐ดโ๐ค) โ ๐น)) |
7 | 6 | imbi2d 341 |
. . . . 5
โข (๐ง = ๐ค โ ((๐ด โ ๐น โ (๐ดโ๐ง) โ ๐น) โ (๐ด โ ๐น โ (๐ดโ๐ค) โ ๐น))) |
8 | | oveq2 7417 |
. . . . . . 7
โข (๐ง = (๐ค + 1) โ (๐ดโ๐ง) = (๐ดโ(๐ค + 1))) |
9 | 8 | eleq1d 2819 |
. . . . . 6
โข (๐ง = (๐ค + 1) โ ((๐ดโ๐ง) โ ๐น โ (๐ดโ(๐ค + 1)) โ ๐น)) |
10 | 9 | imbi2d 341 |
. . . . 5
โข (๐ง = (๐ค + 1) โ ((๐ด โ ๐น โ (๐ดโ๐ง) โ ๐น) โ (๐ด โ ๐น โ (๐ดโ(๐ค + 1)) โ ๐น))) |
11 | | oveq2 7417 |
. . . . . . 7
โข (๐ง = ๐ต โ (๐ดโ๐ง) = (๐ดโ๐ต)) |
12 | 11 | eleq1d 2819 |
. . . . . 6
โข (๐ง = ๐ต โ ((๐ดโ๐ง) โ ๐น โ (๐ดโ๐ต) โ ๐น)) |
13 | 12 | imbi2d 341 |
. . . . 5
โข (๐ง = ๐ต โ ((๐ด โ ๐น โ (๐ดโ๐ง) โ ๐น) โ (๐ด โ ๐น โ (๐ดโ๐ต) โ ๐น))) |
14 | | expcllem.1 |
. . . . . . . . 9
โข ๐น โ
โ |
15 | 14 | sseli 3979 |
. . . . . . . 8
โข (๐ด โ ๐น โ ๐ด โ โ) |
16 | | exp1 14033 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ดโ1) = ๐ด) |
17 | 15, 16 | syl 17 |
. . . . . . 7
โข (๐ด โ ๐น โ (๐ดโ1) = ๐ด) |
18 | 17 | eleq1d 2819 |
. . . . . 6
โข (๐ด โ ๐น โ ((๐ดโ1) โ ๐น โ ๐ด โ ๐น)) |
19 | 18 | ibir 268 |
. . . . 5
โข (๐ด โ ๐น โ (๐ดโ1) โ ๐น) |
20 | | expcllem.2 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ๐น โง ๐ฆ โ ๐น) โ (๐ฅ ยท ๐ฆ) โ ๐น) |
21 | 20 | caovcl 7601 |
. . . . . . . . . . 11
โข (((๐ดโ๐ค) โ ๐น โง ๐ด โ ๐น) โ ((๐ดโ๐ค) ยท ๐ด) โ ๐น) |
22 | 21 | ancoms 460 |
. . . . . . . . . 10
โข ((๐ด โ ๐น โง (๐ดโ๐ค) โ ๐น) โ ((๐ดโ๐ค) ยท ๐ด) โ ๐น) |
23 | 22 | adantlr 714 |
. . . . . . . . 9
โข (((๐ด โ ๐น โง ๐ค โ โ) โง (๐ดโ๐ค) โ ๐น) โ ((๐ดโ๐ค) ยท ๐ด) โ ๐น) |
24 | | nnnn0 12479 |
. . . . . . . . . . . 12
โข (๐ค โ โ โ ๐ค โ
โ0) |
25 | | expp1 14034 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ค โ โ0)
โ (๐ดโ(๐ค + 1)) = ((๐ดโ๐ค) ยท ๐ด)) |
26 | 15, 24, 25 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ด โ ๐น โง ๐ค โ โ) โ (๐ดโ(๐ค + 1)) = ((๐ดโ๐ค) ยท ๐ด)) |
27 | 26 | eleq1d 2819 |
. . . . . . . . . 10
โข ((๐ด โ ๐น โง ๐ค โ โ) โ ((๐ดโ(๐ค + 1)) โ ๐น โ ((๐ดโ๐ค) ยท ๐ด) โ ๐น)) |
28 | 27 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ ๐น โง ๐ค โ โ) โง (๐ดโ๐ค) โ ๐น) โ ((๐ดโ(๐ค + 1)) โ ๐น โ ((๐ดโ๐ค) ยท ๐ด) โ ๐น)) |
29 | 23, 28 | mpbird 257 |
. . . . . . . 8
โข (((๐ด โ ๐น โง ๐ค โ โ) โง (๐ดโ๐ค) โ ๐น) โ (๐ดโ(๐ค + 1)) โ ๐น) |
30 | 29 | exp31 421 |
. . . . . . 7
โข (๐ด โ ๐น โ (๐ค โ โ โ ((๐ดโ๐ค) โ ๐น โ (๐ดโ(๐ค + 1)) โ ๐น))) |
31 | 30 | com12 32 |
. . . . . 6
โข (๐ค โ โ โ (๐ด โ ๐น โ ((๐ดโ๐ค) โ ๐น โ (๐ดโ(๐ค + 1)) โ ๐น))) |
32 | 31 | a2d 29 |
. . . . 5
โข (๐ค โ โ โ ((๐ด โ ๐น โ (๐ดโ๐ค) โ ๐น) โ (๐ด โ ๐น โ (๐ดโ(๐ค + 1)) โ ๐น))) |
33 | 4, 7, 10, 13, 19, 32 | nnind 12230 |
. . . 4
โข (๐ต โ โ โ (๐ด โ ๐น โ (๐ดโ๐ต) โ ๐น)) |
34 | 33 | impcom 409 |
. . 3
โข ((๐ด โ ๐น โง ๐ต โ โ) โ (๐ดโ๐ต) โ ๐น) |
35 | | oveq2 7417 |
. . . . 5
โข (๐ต = 0 โ (๐ดโ๐ต) = (๐ดโ0)) |
36 | | exp0 14031 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ0) = 1) |
37 | 15, 36 | syl 17 |
. . . . 5
โข (๐ด โ ๐น โ (๐ดโ0) = 1) |
38 | 35, 37 | sylan9eqr 2795 |
. . . 4
โข ((๐ด โ ๐น โง ๐ต = 0) โ (๐ดโ๐ต) = 1) |
39 | | expcllem.3 |
. . . 4
โข 1 โ
๐น |
40 | 38, 39 | eqeltrdi 2842 |
. . 3
โข ((๐ด โ ๐น โง ๐ต = 0) โ (๐ดโ๐ต) โ ๐น) |
41 | 34, 40 | jaodan 957 |
. 2
โข ((๐ด โ ๐น โง (๐ต โ โ โจ ๐ต = 0)) โ (๐ดโ๐ต) โ ๐น) |
42 | 1, 41 | sylan2b 595 |
1
โข ((๐ด โ ๐น โง ๐ต โ โ0) โ (๐ดโ๐ต) โ ๐น) |