Step | Hyp | Ref
| Expression |
1 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = 1 โ (๐ดโ๐ค) = (๐ดโ1)) |
2 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = 1 โ (๐ตโ๐ค) = (๐ตโ1)) |
3 | 1, 2 | breq12d 4018 |
. . . . . 6
โข (๐ค = 1 โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ (๐ดโ1) # (๐ตโ1))) |
4 | 3 | imbi1d 231 |
. . . . 5
โข (๐ค = 1 โ (((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต) โ ((๐ดโ1) # (๐ตโ1) โ ๐ด # ๐ต))) |
5 | 4 | imbi2d 230 |
. . . 4
โข (๐ค = 1 โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต)) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) # (๐ตโ1) โ ๐ด # ๐ต)))) |
6 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ดโ๐ค) = (๐ดโ๐)) |
7 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ตโ๐ค) = (๐ตโ๐)) |
8 | 6, 7 | breq12d 4018 |
. . . . . 6
โข (๐ค = ๐ โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ (๐ดโ๐) # (๐ตโ๐))) |
9 | 8 | imbi1d 231 |
. . . . 5
โข (๐ค = ๐ โ (((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต))) |
10 | 9 | imbi2d 230 |
. . . 4
โข (๐ค = ๐ โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต)) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)))) |
11 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = (๐ + 1) โ (๐ดโ๐ค) = (๐ดโ(๐ + 1))) |
12 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = (๐ + 1) โ (๐ตโ๐ค) = (๐ตโ(๐ + 1))) |
13 | 11, 12 | breq12d 4018 |
. . . . . 6
โข (๐ค = (๐ + 1) โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1)))) |
14 | 13 | imbi1d 231 |
. . . . 5
โข (๐ค = (๐ + 1) โ (((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต) โ ((๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1)) โ ๐ด # ๐ต))) |
15 | 14 | imbi2d 230 |
. . . 4
โข (๐ค = (๐ + 1) โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต)) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1)) โ ๐ด # ๐ต)))) |
16 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ดโ๐ค) = (๐ดโ๐)) |
17 | | oveq2 5885 |
. . . . . . 7
โข (๐ค = ๐ โ (๐ตโ๐ค) = (๐ตโ๐)) |
18 | 16, 17 | breq12d 4018 |
. . . . . 6
โข (๐ค = ๐ โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ (๐ดโ๐) # (๐ตโ๐))) |
19 | 18 | imbi1d 231 |
. . . . 5
โข (๐ค = ๐ โ (((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต))) |
20 | 19 | imbi2d 230 |
. . . 4
โข (๐ค = ๐ โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐ค) # (๐ตโ๐ค) โ ๐ด # ๐ต)) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)))) |
21 | | simpl 109 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
22 | 21 | exp1d 10651 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ1) = ๐ด) |
23 | | simpr 110 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
24 | 23 | exp1d 10651 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ตโ1) = ๐ต) |
25 | 22, 24 | breq12d 4018 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) # (๐ตโ1) โ ๐ด # ๐ต)) |
26 | 25 | biimpd 144 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ1) # (๐ตโ1) โ ๐ด # ๐ต)) |
27 | | simpr 110 |
. . . . . . . 8
โข
(((((๐ โ
โ โง (๐ด โ
โ โง ๐ต โ
โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โง (๐ดโ๐) # (๐ตโ๐)) โ (๐ดโ๐) # (๐ตโ๐)) |
28 | | simpllr 534 |
. . . . . . . 8
โข
(((((๐ โ
โ โง (๐ด โ
โ โง ๐ต โ
โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โง (๐ดโ๐) # (๐ตโ๐)) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) |
29 | 27, 28 | mpd 13 |
. . . . . . 7
โข
(((((๐ โ
โ โง (๐ด โ
โ โง ๐ต โ
โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โง (๐ดโ๐) # (๐ตโ๐)) โ ๐ด # ๐ต) |
30 | | simpr 110 |
. . . . . . 7
โข
(((((๐ โ
โ โง (๐ด โ
โ โง ๐ต โ
โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โง ๐ด # ๐ต) โ ๐ด # ๐ต) |
31 | | simpr 110 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) |
32 | 21 | ad3antlr 493 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ ๐ด โ โ) |
33 | | nnnn0 9185 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
34 | 33 | ad3antrrr 492 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ ๐ โ โ0) |
35 | 32, 34 | expp1d 10657 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
36 | 23 | ad3antlr 493 |
. . . . . . . . . 10
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ ๐ต โ โ) |
37 | 36, 34 | expp1d 10657 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ (๐ตโ(๐ + 1)) = ((๐ตโ๐) ยท ๐ต)) |
38 | 31, 35, 37 | 3brtr3d 4036 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ ((๐ดโ๐) ยท ๐ด) # ((๐ตโ๐) ยท ๐ต)) |
39 | 32, 34 | expcld 10656 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ (๐ดโ๐) โ โ) |
40 | 36, 34 | expcld 10656 |
. . . . . . . . 9
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ (๐ตโ๐) โ โ) |
41 | | mulext 8573 |
. . . . . . . . 9
โข ((((๐ดโ๐) โ โ โง ๐ด โ โ) โง ((๐ตโ๐) โ โ โง ๐ต โ โ)) โ (((๐ดโ๐) ยท ๐ด) # ((๐ตโ๐) ยท ๐ต) โ ((๐ดโ๐) # (๐ตโ๐) โจ ๐ด # ๐ต))) |
42 | 39, 32, 40, 36, 41 | syl22anc 1239 |
. . . . . . . 8
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ (((๐ดโ๐) ยท ๐ด) # ((๐ตโ๐) ยท ๐ต) โ ((๐ดโ๐) # (๐ตโ๐) โจ ๐ด # ๐ต))) |
43 | 38, 42 | mpd 13 |
. . . . . . 7
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ ((๐ดโ๐) # (๐ตโ๐) โจ ๐ด # ๐ต)) |
44 | 29, 30, 43 | mpjaodan 798 |
. . . . . 6
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ต โ โ)) โง ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โง (๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1))) โ ๐ด # ๐ต) |
45 | 44 | exp41 370 |
. . . . 5
โข (๐ โ โ โ ((๐ด โ โ โง ๐ต โ โ) โ (((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต) โ ((๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1)) โ ๐ด # ๐ต)))) |
46 | 45 | a2d 26 |
. . . 4
โข (๐ โ โ โ (((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ(๐ + 1)) # (๐ตโ(๐ + 1)) โ ๐ด # ๐ต)))) |
47 | 5, 10, 15, 20, 26, 46 | nnind 8937 |
. . 3
โข (๐ โ โ โ ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต))) |
48 | 47 | impcom 125 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ โ โ) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) |
49 | 48 | 3impa 1194 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ดโ๐) # (๐ตโ๐) โ ๐ด # ๐ต)) |