Step | Hyp | Ref
| Expression |
1 | | oveq2 5882 |
. . . . . 6
โข (๐ = 1 โ (๐ดโ๐) = (๐ดโ1)) |
2 | 1 | breq1d 4013 |
. . . . 5
โข (๐ = 1 โ ((๐ดโ๐) # 0 โ (๐ดโ1) # 0)) |
3 | 2 | bibi1d 233 |
. . . 4
โข (๐ = 1 โ (((๐ดโ๐) # 0 โ ๐ด # 0) โ ((๐ดโ1) # 0 โ ๐ด # 0))) |
4 | 3 | imbi2d 230 |
. . 3
โข (๐ = 1 โ ((๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (๐ด โ โ โ ((๐ดโ1) # 0 โ ๐ด # 0)))) |
5 | | oveq2 5882 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | 5 | breq1d 4013 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ๐) # 0 โ (๐ดโ๐) # 0)) |
7 | 6 | bibi1d 233 |
. . . 4
โข (๐ = ๐ โ (((๐ดโ๐) # 0 โ ๐ด # 0) โ ((๐ดโ๐) # 0 โ ๐ด # 0))) |
8 | 7 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)))) |
9 | | oveq2 5882 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | 9 | breq1d 4013 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ๐) # 0 โ (๐ดโ(๐ + 1)) # 0)) |
11 | 10 | bibi1d 233 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ดโ๐) # 0 โ ๐ด # 0) โ ((๐ดโ(๐ + 1)) # 0 โ ๐ด # 0))) |
12 | 11 | imbi2d 230 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (๐ด โ โ โ ((๐ดโ(๐ + 1)) # 0 โ ๐ด # 0)))) |
13 | | oveq2 5882 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | 13 | breq1d 4013 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ๐) # 0 โ (๐ดโ๐) # 0)) |
15 | 14 | bibi1d 233 |
. . . 4
โข (๐ = ๐ โ (((๐ดโ๐) # 0 โ ๐ด # 0) โ ((๐ดโ๐) # 0 โ ๐ด # 0))) |
16 | 15 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)))) |
17 | | exp1 10525 |
. . . 4
โข (๐ด โ โ โ (๐ดโ1) = ๐ด) |
18 | 17 | breq1d 4013 |
. . 3
โข (๐ด โ โ โ ((๐ดโ1) # 0 โ ๐ด # 0)) |
19 | | nnnn0 9182 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
20 | | expp1 10526 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
21 | 20 | breq1d 4013 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ(๐ + 1)) # 0 โ ((๐ดโ๐) ยท ๐ด) # 0)) |
22 | 21 | ancoms 268 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ด โ โ)
โ ((๐ดโ(๐ + 1)) # 0 โ ((๐ดโ๐) ยท ๐ด) # 0)) |
23 | 19, 22 | sylan 283 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ ((๐ดโ(๐ + 1)) # 0 โ ((๐ดโ๐) ยท ๐ด) # 0)) |
24 | 23 | adantr 276 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ ((๐ดโ(๐ + 1)) # 0 โ ((๐ดโ๐) ยท ๐ด) # 0)) |
25 | | simplr 528 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ ๐ด โ โ) |
26 | 19 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ ๐ โ โ0) |
27 | | expcl 10537 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
28 | 25, 26, 27 | syl2anc 411 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (๐ดโ๐) โ โ) |
29 | 28, 25 | mulap0bd 8613 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (((๐ดโ๐) # 0 โง ๐ด # 0) โ ((๐ดโ๐) ยท ๐ด) # 0)) |
30 | | anbi1 466 |
. . . . . . . 8
โข (((๐ดโ๐) # 0 โ ๐ด # 0) โ (((๐ดโ๐) # 0 โง ๐ด # 0) โ (๐ด # 0 โง ๐ด # 0))) |
31 | 30 | adantl 277 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (((๐ดโ๐) # 0 โง ๐ด # 0) โ (๐ด # 0 โง ๐ด # 0))) |
32 | 24, 29, 31 | 3bitr2d 216 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ ((๐ดโ(๐ + 1)) # 0 โ (๐ด # 0 โง ๐ด # 0))) |
33 | | anidm 396 |
. . . . . 6
โข ((๐ด # 0 โง ๐ด # 0) โ ๐ด # 0) |
34 | 32, 33 | bitrdi 196 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โ) โง ((๐ดโ๐) # 0 โ ๐ด # 0)) โ ((๐ดโ(๐ + 1)) # 0 โ ๐ด # 0)) |
35 | 34 | exp31 364 |
. . . 4
โข (๐ โ โ โ (๐ด โ โ โ (((๐ดโ๐) # 0 โ ๐ด # 0) โ ((๐ดโ(๐ + 1)) # 0 โ ๐ด # 0)))) |
36 | 35 | a2d 26 |
. . 3
โข (๐ โ โ โ ((๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0)) โ (๐ด โ โ โ ((๐ดโ(๐ + 1)) # 0 โ ๐ด # 0)))) |
37 | 4, 8, 12, 16, 18, 36 | nnind 8934 |
. 2
โข (๐ โ โ โ (๐ด โ โ โ ((๐ดโ๐) # 0 โ ๐ด # 0))) |
38 | 37 | impcom 125 |
1
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ดโ๐) # 0 โ ๐ด # 0)) |