Step | Hyp | Ref
| Expression |
1 | | 2zrng.e |
. . . . 5
โข ๐ธ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ)} |
2 | 1 | 2even 46821 |
. . . 4
โข 2 โ
๐ธ |
3 | 2 | a1i 11 |
. . 3
โข (๐ โ ๐ธ โ 2 โ ๐ธ) |
4 | | oveq2 7416 |
. . . . 5
โข (๐ = 2 โ (๐ ยท ๐) = (๐ ยท 2)) |
5 | | id 22 |
. . . . 5
โข (๐ = 2 โ ๐ = 2) |
6 | 4, 5 | neeq12d 3002 |
. . . 4
โข (๐ = 2 โ ((๐ ยท ๐) โ ๐ โ (๐ ยท 2) โ 2)) |
7 | 6 | adantl 482 |
. . 3
โข ((๐ โ ๐ธ โง ๐ = 2) โ ((๐ ยท ๐) โ ๐ โ (๐ ยท 2) โ 2)) |
8 | | elrabi 3677 |
. . . . . 6
โข (๐ โ {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ)} โ ๐ โ โค) |
9 | 8 | zcnd 12666 |
. . . . 5
โข (๐ โ {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ)} โ ๐ โ โ) |
10 | 9, 1 | eleq2s 2851 |
. . . 4
โข (๐ โ ๐ธ โ ๐ โ โ) |
11 | 1 | 1neven 46820 |
. . . . . . . 8
โข 1 โ
๐ธ |
12 | | elnelne2 3058 |
. . . . . . . 8
โข ((๐ โ ๐ธ โง 1 โ ๐ธ) โ ๐ โ 1) |
13 | 11, 12 | mpan2 689 |
. . . . . . 7
โข (๐ โ ๐ธ โ ๐ โ 1) |
14 | 13 | adantr 481 |
. . . . . 6
โข ((๐ โ ๐ธ โง ๐ โ โ) โ ๐ โ 1) |
15 | | simpr 485 |
. . . . . . 7
โข ((๐ โ ๐ธ โง ๐ โ โ) โ ๐ โ โ) |
16 | | 2cnd 12289 |
. . . . . . 7
โข ((๐ โ ๐ธ โง ๐ โ โ) โ 2 โ
โ) |
17 | | 2ne0 12315 |
. . . . . . . 8
โข 2 โ
0 |
18 | 17 | a1i 11 |
. . . . . . 7
โข ((๐ โ ๐ธ โง ๐ โ โ) โ 2 โ
0) |
19 | 15, 16, 18 | divcan4d 11995 |
. . . . . 6
โข ((๐ โ ๐ธ โง ๐ โ โ) โ ((๐ ยท 2) / 2) = ๐) |
20 | | 2cnne0 12421 |
. . . . . . 7
โข (2 โ
โ โง 2 โ 0) |
21 | | divid 11900 |
. . . . . . 7
โข ((2
โ โ โง 2 โ 0) โ (2 / 2) = 1) |
22 | 20, 21 | mp1i 13 |
. . . . . 6
โข ((๐ โ ๐ธ โง ๐ โ โ) โ (2 / 2) =
1) |
23 | 14, 19, 22 | 3netr4d 3018 |
. . . . 5
โข ((๐ โ ๐ธ โง ๐ โ โ) โ ((๐ ยท 2) / 2) โ (2 /
2)) |
24 | 15, 16 | mulcld 11233 |
. . . . . . . 8
โข ((๐ โ ๐ธ โง ๐ โ โ) โ (๐ ยท 2) โ โ) |
25 | 20 | a1i 11 |
. . . . . . . 8
โข ((๐ โ ๐ธ โง ๐ โ โ) โ (2 โ โ
โง 2 โ 0)) |
26 | | div11 11899 |
. . . . . . . 8
โข (((๐ ยท 2) โ โ
โง 2 โ โ โง (2 โ โ โง 2 โ 0)) โ (((๐ ยท 2) / 2) = (2 / 2)
โ (๐ ยท 2) =
2)) |
27 | 24, 16, 25, 26 | syl3anc 1371 |
. . . . . . 7
โข ((๐ โ ๐ธ โง ๐ โ โ) โ (((๐ ยท 2) / 2) = (2 / 2) โ (๐ ยท 2) =
2)) |
28 | 27 | biimprd 247 |
. . . . . 6
โข ((๐ โ ๐ธ โง ๐ โ โ) โ ((๐ ยท 2) = 2 โ ((๐ ยท 2) / 2) = (2 /
2))) |
29 | 28 | necon3d 2961 |
. . . . 5
โข ((๐ โ ๐ธ โง ๐ โ โ) โ (((๐ ยท 2) / 2) โ (2 / 2) โ (๐ ยท 2) โ
2)) |
30 | 23, 29 | mpd 15 |
. . . 4
โข ((๐ โ ๐ธ โง ๐ โ โ) โ (๐ ยท 2) โ 2) |
31 | 10, 30 | mpdan 685 |
. . 3
โข (๐ โ ๐ธ โ (๐ ยท 2) โ 2) |
32 | 3, 7, 31 | rspcedvd 3614 |
. 2
โข (๐ โ ๐ธ โ โ๐ โ ๐ธ (๐ ยท ๐) โ ๐) |
33 | 32 | rgen 3063 |
1
โข
โ๐ โ
๐ธ โ๐ โ ๐ธ (๐ ยท ๐) โ ๐ |