Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . . 7
โข (๐ = 1 โ (๐ดโ๐) = (๐ดโ1)) |
2 | 1 | breq2d 5122 |
. . . . . 6
โข (๐ = 1 โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ (๐ดโ1))) |
3 | 2 | bibi1d 344 |
. . . . 5
โข (๐ = 1 โ ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ (๐ โฅ (๐ดโ1) โ ๐ โฅ ๐ด))) |
4 | 3 | imbi2d 341 |
. . . 4
โข (๐ = 1 โ (((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) โ ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ1) โ ๐ โฅ ๐ด)))) |
5 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | 5 | breq2d 5122 |
. . . . . 6
โข (๐ = ๐ โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ (๐ดโ๐))) |
7 | 6 | bibi1d 344 |
. . . . 5
โข (๐ = ๐ โ ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด))) |
8 | 7 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) โ ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)))) |
9 | | oveq2 7370 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | 9 | breq2d 5122 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ (๐ดโ(๐ + 1)))) |
11 | 10 | bibi1d 344 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ๐ด))) |
12 | 11 | imbi2d 341 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) โ ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ๐ด)))) |
13 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | 13 | breq2d 5122 |
. . . . . 6
โข (๐ = ๐ โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ (๐ดโ๐))) |
15 | 14 | bibi1d 344 |
. . . . 5
โข (๐ = ๐ โ ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด))) |
16 | 15 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ (((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) โ ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)))) |
17 | | zcn 12511 |
. . . . . . 7
โข (๐ด โ โค โ ๐ด โ
โ) |
18 | 17 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค) โ ๐ด โ
โ) |
19 | 18 | exp1d 14053 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ดโ1) = ๐ด) |
20 | 19 | breq2d 5122 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ1) โ ๐ โฅ ๐ด)) |
21 | | nnnn0 12427 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
22 | | expp1 13981 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
23 | 18, 21, 22 | syl2an 597 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
24 | 23 | breq2d 5122 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ((๐ดโ๐) ยท ๐ด))) |
25 | | simpll 766 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ ๐ โ
โ) |
26 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โค) โ ๐ด โ
โค) |
27 | | zexpcl 13989 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ โ โ0)
โ (๐ดโ๐) โ
โค) |
28 | 26, 21, 27 | syl2an 597 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ (๐ดโ๐) โ โค) |
29 | | simplr 768 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ ๐ด โ
โค) |
30 | | euclemma 16596 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ดโ๐) โ โค โง ๐ด โ โค) โ (๐ โฅ ((๐ดโ๐) ยท ๐ด) โ (๐ โฅ (๐ดโ๐) โจ ๐ โฅ ๐ด))) |
31 | 25, 28, 29, 30 | syl3anc 1372 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ (๐ โฅ ((๐ดโ๐) ยท ๐ด) โ (๐ โฅ (๐ดโ๐) โจ ๐ โฅ ๐ด))) |
32 | 24, 31 | bitrd 279 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ (๐ โฅ (๐ดโ(๐ + 1)) โ (๐ โฅ (๐ดโ๐) โจ ๐ โฅ ๐ด))) |
33 | | orbi1 917 |
. . . . . . . . 9
โข ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ ((๐ โฅ (๐ดโ๐) โจ ๐ โฅ ๐ด) โ (๐ โฅ ๐ด โจ ๐ โฅ ๐ด))) |
34 | | oridm 904 |
. . . . . . . . 9
โข ((๐ โฅ ๐ด โจ ๐ โฅ ๐ด) โ ๐ โฅ ๐ด) |
35 | 33, 34 | bitrdi 287 |
. . . . . . . 8
โข ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ ((๐ โฅ (๐ดโ๐) โจ ๐ โฅ ๐ด) โ ๐ โฅ ๐ด)) |
36 | 35 | bibi2d 343 |
. . . . . . 7
โข ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ ((๐ โฅ (๐ดโ(๐ + 1)) โ (๐ โฅ (๐ดโ๐) โจ ๐ โฅ ๐ด)) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ๐ด))) |
37 | 32, 36 | syl5ibcom 244 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ๐ด))) |
38 | 37 | expcom 415 |
. . . . 5
โข (๐ โ โ โ ((๐ โ โ โง ๐ด โ โค) โ ((๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ๐ด)))) |
39 | 38 | a2d 29 |
. . . 4
โข (๐ โ โ โ (((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) โ ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ(๐ + 1)) โ ๐ โฅ ๐ด)))) |
40 | 4, 8, 12, 16, 20, 39 | nnind 12178 |
. . 3
โข (๐ โ โ โ ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด))) |
41 | 40 | impcom 409 |
. 2
โข (((๐ โ โ โง ๐ด โ โค) โง ๐ โ โ) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) |
42 | 41 | 3impa 1111 |
1
โข ((๐ โ โ โง ๐ด โ โค โง ๐ โ โ) โ (๐ โฅ (๐ดโ๐) โ ๐ โฅ ๐ด)) |