Step | Hyp | Ref
| Expression |
1 | | 2nn 9080 |
. . . . . 6
โข 2 โ
โ |
2 | 1 | a1i 9 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ 2 โ โ) |
3 | | simplll 533 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ โ โ) |
4 | 3 | nnzd 9374 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ โ โค) |
5 | | simplr 528 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ โ
โ0) |
6 | 2, 5 | nnexpcld 10676 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ๐) โ โ) |
7 | 6 | nnzd 9374 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ๐) โ โค) |
8 | | simpr 110 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ด = ((2โ๐) ยท ๐)) |
9 | 6, 3 | nnmulcld 8968 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ((2โ๐) ยท ๐) โ โ) |
10 | 8, 9 | eqeltrd 2254 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ด โ โ) |
11 | 10 | nnzd 9374 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ด โ โค) |
12 | 6 | nncnd 8933 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ๐) โ โ) |
13 | 3 | nncnd 8933 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ โ โ) |
14 | 12, 13 | mulcomd 7979 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ((2โ๐) ยท ๐) = (๐ ยท (2โ๐))) |
15 | 8, 14 | eqtr2d 2211 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (๐ ยท (2โ๐)) = ๐ด) |
16 | | dvds0lem 11808 |
. . . . . . . 8
โข (((๐ โ โค โง
(2โ๐) โ โค
โง ๐ด โ โค)
โง (๐ ยท
(2โ๐)) = ๐ด) โ (2โ๐) โฅ ๐ด) |
17 | 4, 7, 11, 15, 16 | syl31anc 1241 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ๐) โฅ ๐ด) |
18 | | simpllr 534 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ยฌ 2 โฅ ๐) |
19 | 8 | breq2d 4016 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (((2โ๐) ยท 2) โฅ ๐ด โ ((2โ๐) ยท 2) โฅ ((2โ๐) ยท ๐))) |
20 | 2 | nnzd 9374 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ 2 โ โค) |
21 | 6 | nnne0d 8964 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ๐) โ 0) |
22 | | dvdscmulr 11827 |
. . . . . . . . . . 11
โข ((2
โ โค โง ๐
โ โค โง ((2โ๐) โ โค โง (2โ๐) โ 0)) โ
(((2โ๐) ยท 2)
โฅ ((2โ๐)
ยท ๐) โ 2
โฅ ๐)) |
23 | 20, 4, 7, 21, 22 | syl112anc 1242 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (((2โ๐) ยท 2) โฅ ((2โ๐) ยท ๐) โ 2 โฅ ๐)) |
24 | 19, 23 | bitrd 188 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (((2โ๐) ยท 2) โฅ ๐ด โ 2 โฅ ๐)) |
25 | 18, 24 | mtbird 673 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ยฌ ((2โ๐) ยท 2) โฅ ๐ด) |
26 | 2 | nncnd 8933 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ 2 โ โ) |
27 | 26, 5 | expp1d 10655 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ(๐ + 1)) = ((2โ๐) ยท 2)) |
28 | 27 | breq1d 4014 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ((2โ(๐ + 1)) โฅ ๐ด โ ((2โ๐) ยท 2) โฅ ๐ด)) |
29 | 25, 28 | mtbird 673 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ยฌ (2โ(๐ + 1)) โฅ ๐ด) |
30 | | pw2dvdseu 12168 |
. . . . . . . . 9
โข (๐ด โ โ โ
โ!๐ง โ
โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) |
31 | 10, 30 | syl 14 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ โ!๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) |
32 | | oveq2 5883 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ (2โ๐ง) = (2โ๐)) |
33 | 32 | breq1d 4014 |
. . . . . . . . . 10
โข (๐ง = ๐ โ ((2โ๐ง) โฅ ๐ด โ (2โ๐) โฅ ๐ด)) |
34 | | oveq1 5882 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ง + 1) = (๐ + 1)) |
35 | 34 | oveq2d 5891 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (2โ(๐ง + 1)) = (2โ(๐ + 1))) |
36 | 35 | breq1d 4014 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ ((2โ(๐ง + 1)) โฅ ๐ด โ (2โ(๐ + 1)) โฅ ๐ด)) |
37 | 36 | notbid 667 |
. . . . . . . . . 10
โข (๐ง = ๐ โ (ยฌ (2โ(๐ง + 1)) โฅ ๐ด โ ยฌ (2โ(๐ + 1)) โฅ ๐ด)) |
38 | 33, 37 | anbi12d 473 |
. . . . . . . . 9
โข (๐ง = ๐ โ (((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด) โ ((2โ๐) โฅ ๐ด โง ยฌ (2โ(๐ + 1)) โฅ ๐ด))) |
39 | 38 | riota2 5853 |
. . . . . . . 8
โข ((๐ โ โ0
โง โ!๐ง โ
โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) โ (((2โ๐) โฅ ๐ด โง ยฌ (2โ(๐ + 1)) โฅ ๐ด) โ (โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) = ๐)) |
40 | 5, 31, 39 | syl2anc 411 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (((2โ๐) โฅ ๐ด โง ยฌ (2โ(๐ + 1)) โฅ ๐ด) โ (โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) = ๐)) |
41 | 17, 29, 40 | mpbi2and 943 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) = ๐) |
42 | 41, 5 | eqeltrd 2254 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)) โ
โ0) |
43 | 2, 42 | nnexpcld 10676 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ(โฉ๐ง โ โ0
((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))) โ โ) |
44 | 43 | nncnd 8933 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ(โฉ๐ง โ โ0
((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))) โ โ) |
45 | 43 | nnap0d 8965 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ(โฉ๐ง โ โ0
((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))) # 0) |
46 | 41 | eqcomd 2183 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ = (โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))) |
47 | 46 | oveq2d 5891 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (2โ๐) = (2โ(โฉ๐ง โ โ0
((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)))) |
48 | 47 | oveq1d 5890 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ((2โ๐) ยท ๐) = ((2โ(โฉ๐ง โ โ0
((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))) ยท ๐)) |
49 | 8, 48 | eqtr2d 2211 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ((2โ(โฉ๐ง โ โ0
((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))) ยท ๐) = ๐ด) |
50 | 44, 13, 45, 49 | mvllmulapd 8799 |
. 2
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ ๐ = (๐ด / (2โ(โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด))))) |
51 | 50, 46 | jca 306 |
1
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง ๐ โ โ0)
โง ๐ด = ((2โ๐) ยท ๐)) โ (๐ = (๐ด / (2โ(โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)))) โง ๐ = (โฉ๐ง โ โ0 ((2โ๐ง) โฅ ๐ด โง ยฌ (2โ(๐ง + 1)) โฅ ๐ด)))) |