Step | Hyp | Ref
| Expression |
1 | | oddpwdc.j |
. . . . . . . . 9
โข ๐ฝ = {๐ง โ โ โฃ ยฌ 2 โฅ ๐ง} |
2 | | oddpwdc.f |
. . . . . . . . 9
โข ๐น = (๐ฅ โ ๐ฝ, ๐ฆ โ โ0 โฆ
((2โ๐ฆ) ยท ๐ฅ)) |
3 | 1, 2 | oddpwdc 12176 |
. . . . . . . 8
โข ๐น:(๐ฝ ร โ0)โ1-1-ontoโโ |
4 | | f1ocnv 5476 |
. . . . . . . 8
โข (๐น:(๐ฝ ร โ0)โ1-1-ontoโโ โ โก๐น:โโ1-1-ontoโ(๐ฝ ร
โ0)) |
5 | | f1of 5463 |
. . . . . . . 8
โข (โก๐น:โโ1-1-ontoโ(๐ฝ ร โ0) โ โก๐น:โโถ(๐ฝ ร
โ0)) |
6 | 3, 4, 5 | mp2b 8 |
. . . . . . 7
โข โก๐น:โโถ(๐ฝ ร
โ0) |
7 | 6 | ffvelcdmi 5652 |
. . . . . 6
โข (๐ด โ โ โ (โก๐นโ๐ด) โ (๐ฝ ร
โ0)) |
8 | | xp2nd 6169 |
. . . . . 6
โข ((โก๐นโ๐ด) โ (๐ฝ ร โ0) โ
(2nd โ(โก๐นโ๐ด)) โ
โ0) |
9 | 7, 8 | syl 14 |
. . . . 5
โข (๐ด โ โ โ
(2nd โ(โก๐นโ๐ด)) โ
โ0) |
10 | 9 | nn0zd 9375 |
. . . 4
โข (๐ด โ โ โ
(2nd โ(โก๐นโ๐ด)) โ โค) |
11 | | 2nn 9082 |
. . . . . 6
โข 2 โ
โ |
12 | 11 | a1i 9 |
. . . . 5
โข (๐ด โ โ โ 2 โ
โ) |
13 | 12 | nnzd 9376 |
. . . 4
โข (๐ด โ โ โ 2 โ
โค) |
14 | 10, 13 | zmulcld 9383 |
. . 3
โข (๐ด โ โ โ
((2nd โ(โก๐นโ๐ด)) ยท 2) โ
โค) |
15 | | dvdsmul2 11823 |
. . . 4
โข
(((2nd โ(โก๐นโ๐ด)) โ โค โง 2 โ โค)
โ 2 โฅ ((2nd โ(โก๐นโ๐ด)) ยท 2)) |
16 | 10, 13, 15 | syl2anc 411 |
. . 3
โข (๐ด โ โ โ 2 โฅ
((2nd โ(โก๐นโ๐ด)) ยท 2)) |
17 | | oddp1even 11883 |
. . . . 5
โข
(((2nd โ(โก๐นโ๐ด)) ยท 2) โ โค โ (ยฌ
2 โฅ ((2nd โ(โก๐นโ๐ด)) ยท 2) โ 2 โฅ
(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1))) |
18 | 17 | biimprd 158 |
. . . 4
โข
(((2nd โ(โก๐นโ๐ด)) ยท 2) โ โค โ (2
โฅ (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1) โ ยฌ 2 โฅ
((2nd โ(โก๐นโ๐ด)) ยท 2))) |
19 | 18 | con2d 624 |
. . 3
โข
(((2nd โ(โก๐นโ๐ด)) ยท 2) โ โค โ (2
โฅ ((2nd โ(โก๐นโ๐ด)) ยท 2) โ ยฌ 2 โฅ
(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1))) |
20 | 14, 16, 19 | sylc 62 |
. 2
โข (๐ด โ โ โ ยฌ 2
โฅ (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) |
21 | | xp1st 6168 |
. . . . . . . . . . 11
โข ((โก๐นโ๐ด) โ (๐ฝ ร โ0) โ
(1st โ(โก๐นโ๐ด)) โ ๐ฝ) |
22 | 7, 21 | syl 14 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(1st โ(โก๐นโ๐ด)) โ ๐ฝ) |
23 | | breq2 4009 |
. . . . . . . . . . . . 13
โข (๐ง = (1st โ(โก๐นโ๐ด)) โ (2 โฅ ๐ง โ 2 โฅ (1st
โ(โก๐นโ๐ด)))) |
24 | 23 | notbid 667 |
. . . . . . . . . . . 12
โข (๐ง = (1st โ(โก๐นโ๐ด)) โ (ยฌ 2 โฅ ๐ง โ ยฌ 2 โฅ
(1st โ(โก๐นโ๐ด)))) |
25 | 24, 1 | elrab2 2898 |
. . . . . . . . . . 11
โข
((1st โ(โก๐นโ๐ด)) โ ๐ฝ โ ((1st โ(โก๐นโ๐ด)) โ โ โง ยฌ 2 โฅ
(1st โ(โก๐นโ๐ด)))) |
26 | 25 | simplbi 274 |
. . . . . . . . . 10
โข
((1st โ(โก๐นโ๐ด)) โ ๐ฝ โ (1st โ(โก๐นโ๐ด)) โ โ) |
27 | 22, 26 | syl 14 |
. . . . . . . . 9
โข (๐ด โ โ โ
(1st โ(โก๐นโ๐ด)) โ โ) |
28 | 27 | nnsqcld 10677 |
. . . . . . . 8
โข (๐ด โ โ โ
((1st โ(โก๐นโ๐ด))โ2) โ โ) |
29 | 25 | simprbi 275 |
. . . . . . . . . . 11
โข
((1st โ(โก๐นโ๐ด)) โ ๐ฝ โ ยฌ 2 โฅ (1st
โ(โก๐นโ๐ด))) |
30 | 22, 29 | syl 14 |
. . . . . . . . . 10
โข (๐ด โ โ โ ยฌ 2
โฅ (1st โ(โก๐นโ๐ด))) |
31 | | 2prm 12129 |
. . . . . . . . . . 11
โข 2 โ
โ |
32 | 27 | nnzd 9376 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(1st โ(โก๐นโ๐ด)) โ โค) |
33 | | euclemma 12148 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (1st โ(โก๐นโ๐ด)) โ โค โง (1st
โ(โก๐นโ๐ด)) โ โค) โ (2 โฅ
((1st โ(โก๐นโ๐ด)) ยท (1st โ(โก๐นโ๐ด))) โ (2 โฅ (1st
โ(โก๐นโ๐ด)) โจ 2 โฅ (1st
โ(โก๐นโ๐ด))))) |
34 | | oridm 757 |
. . . . . . . . . . . 12
โข ((2
โฅ (1st โ(โก๐นโ๐ด)) โจ 2 โฅ (1st
โ(โก๐นโ๐ด))) โ 2 โฅ (1st
โ(โก๐นโ๐ด))) |
35 | 33, 34 | bitrdi 196 |
. . . . . . . . . . 11
โข ((2
โ โ โง (1st โ(โก๐นโ๐ด)) โ โค โง (1st
โ(โก๐นโ๐ด)) โ โค) โ (2 โฅ
((1st โ(โก๐นโ๐ด)) ยท (1st โ(โก๐นโ๐ด))) โ 2 โฅ (1st
โ(โก๐นโ๐ด)))) |
36 | 31, 32, 32, 35 | mp3an2i 1342 |
. . . . . . . . . 10
โข (๐ด โ โ โ (2
โฅ ((1st โ(โก๐นโ๐ด)) ยท (1st โ(โก๐นโ๐ด))) โ 2 โฅ (1st
โ(โก๐นโ๐ด)))) |
37 | 30, 36 | mtbird 673 |
. . . . . . . . 9
โข (๐ด โ โ โ ยฌ 2
โฅ ((1st โ(โก๐นโ๐ด)) ยท (1st โ(โก๐นโ๐ด)))) |
38 | 27 | nncnd 8935 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(1st โ(โก๐นโ๐ด)) โ โ) |
39 | 38 | sqvald 10653 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((1st โ(โก๐นโ๐ด))โ2) = ((1st โ(โก๐นโ๐ด)) ยท (1st โ(โก๐นโ๐ด)))) |
40 | 39 | breq2d 4017 |
. . . . . . . . 9
โข (๐ด โ โ โ (2
โฅ ((1st โ(โก๐นโ๐ด))โ2) โ 2 โฅ ((1st
โ(โก๐นโ๐ด)) ยท (1st โ(โก๐นโ๐ด))))) |
41 | 37, 40 | mtbird 673 |
. . . . . . . 8
โข (๐ด โ โ โ ยฌ 2
โฅ ((1st โ(โก๐นโ๐ด))โ2)) |
42 | | breq2 4009 |
. . . . . . . . . 10
โข (๐ง = ((1st
โ(โก๐นโ๐ด))โ2) โ (2 โฅ ๐ง โ 2 โฅ
((1st โ(โก๐นโ๐ด))โ2))) |
43 | 42 | notbid 667 |
. . . . . . . . 9
โข (๐ง = ((1st
โ(โก๐นโ๐ด))โ2) โ (ยฌ 2 โฅ ๐ง โ ยฌ 2 โฅ
((1st โ(โก๐นโ๐ด))โ2))) |
44 | 43, 1 | elrab2 2898 |
. . . . . . . 8
โข
(((1st โ(โก๐นโ๐ด))โ2) โ ๐ฝ โ (((1st โ(โก๐นโ๐ด))โ2) โ โ โง ยฌ 2
โฅ ((1st โ(โก๐นโ๐ด))โ2))) |
45 | 28, 41, 44 | sylanbrc 417 |
. . . . . . 7
โข (๐ด โ โ โ
((1st โ(โก๐นโ๐ด))โ2) โ ๐ฝ) |
46 | 12 | nnnn0d 9231 |
. . . . . . . . 9
โข (๐ด โ โ โ 2 โ
โ0) |
47 | 9, 46 | nn0mulcld 9236 |
. . . . . . . 8
โข (๐ด โ โ โ
((2nd โ(โก๐นโ๐ด)) ยท 2) โ
โ0) |
48 | | peano2nn0 9218 |
. . . . . . . 8
โข
(((2nd โ(โก๐นโ๐ด)) ยท 2) โ โ0
โ (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1) โ
โ0) |
49 | 47, 48 | syl 14 |
. . . . . . 7
โข (๐ด โ โ โ
(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1) โ
โ0) |
50 | | opelxp 4658 |
. . . . . . 7
โข
(โจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ โ (๐ฝ ร โ0)
โ (((1st โ(โก๐นโ๐ด))โ2) โ ๐ฝ โง (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1) โ
โ0)) |
51 | 45, 49, 50 | sylanbrc 417 |
. . . . . 6
โข (๐ด โ โ โ
โจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ โ (๐ฝ ร
โ0)) |
52 | 12 | nncnd 8935 |
. . . . . . . . . . 11
โข (๐ด โ โ โ 2 โ
โ) |
53 | 52, 47 | expp1d 10657 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) =
((2โ((2nd โ(โก๐นโ๐ด)) ยท 2)) ยท
2)) |
54 | 52, 47 | expcld 10656 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(2โ((2nd โ(โก๐นโ๐ด)) ยท 2)) โ
โ) |
55 | 54, 52 | mulcomd 7981 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((2โ((2nd โ(โก๐นโ๐ด)) ยท 2)) ยท 2) = (2 ยท
(2โ((2nd โ(โก๐นโ๐ด)) ยท 2)))) |
56 | 52, 46, 9 | expmuld 10659 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(2โ((2nd โ(โก๐นโ๐ด)) ยท 2)) = ((2โ(2nd
โ(โก๐นโ๐ด)))โ2)) |
57 | 56 | oveq2d 5893 |
. . . . . . . . . 10
โข (๐ด โ โ โ (2
ยท (2โ((2nd โ(โก๐นโ๐ด)) ยท 2))) = (2 ยท
((2โ(2nd โ(โก๐นโ๐ด)))โ2))) |
58 | 53, 55, 57 | 3eqtrd 2214 |
. . . . . . . . 9
โข (๐ด โ โ โ
(2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) = (2 ยท
((2โ(2nd โ(โก๐นโ๐ด)))โ2))) |
59 | 58 | oveq1d 5892 |
. . . . . . . 8
โข (๐ด โ โ โ
((2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) ยท
((1st โ(โก๐นโ๐ด))โ2)) = ((2 ยท
((2โ(2nd โ(โก๐นโ๐ด)))โ2)) ยท ((1st
โ(โก๐นโ๐ด))โ2))) |
60 | 12, 49 | nnexpcld 10678 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) โ
โ) |
61 | 60, 28 | nnmulcld 8970 |
. . . . . . . . 9
โข (๐ด โ โ โ
((2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) ยท
((1st โ(โก๐นโ๐ด))โ2)) โ โ) |
62 | | oveq2 5885 |
. . . . . . . . . 10
โข (๐ฅ = ((1st
โ(โก๐นโ๐ด))โ2) โ ((2โ๐ฆ) ยท ๐ฅ) = ((2โ๐ฆ) ยท ((1st โ(โก๐นโ๐ด))โ2))) |
63 | | oveq2 5885 |
. . . . . . . . . . 11
โข (๐ฆ = (((2nd
โ(โก๐นโ๐ด)) ยท 2) + 1) โ (2โ๐ฆ) = (2โ(((2nd
โ(โก๐นโ๐ด)) ยท 2) + 1))) |
64 | 63 | oveq1d 5892 |
. . . . . . . . . 10
โข (๐ฆ = (((2nd
โ(โก๐นโ๐ด)) ยท 2) + 1) โ ((2โ๐ฆ) ยท ((1st
โ(โก๐นโ๐ด))โ2)) = ((2โ(((2nd
โ(โก๐นโ๐ด)) ยท 2) + 1)) ยท
((1st โ(โก๐นโ๐ด))โ2))) |
65 | 62, 64, 2 | ovmpog 6011 |
. . . . . . . . 9
โข
((((1st โ(โก๐นโ๐ด))โ2) โ ๐ฝ โง (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1) โ
โ0 โง ((2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) ยท
((1st โ(โก๐นโ๐ด))โ2)) โ โ) โ
(((1st โ(โก๐นโ๐ด))โ2)๐น(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) =
((2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) ยท
((1st โ(โก๐นโ๐ด))โ2))) |
66 | 45, 49, 61, 65 | syl3anc 1238 |
. . . . . . . 8
โข (๐ด โ โ โ
(((1st โ(โก๐นโ๐ด))โ2)๐น(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) =
((2โ(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) ยท
((1st โ(โก๐นโ๐ด))โ2))) |
67 | | f1ocnvfv2 5781 |
. . . . . . . . . . . . . . . 16
โข ((๐น:(๐ฝ ร โ0)โ1-1-ontoโโ โง ๐ด โ โ) โ (๐นโ(โก๐นโ๐ด)) = ๐ด) |
68 | 3, 67 | mpan 424 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ (๐นโ(โก๐นโ๐ด)) = ๐ด) |
69 | | 1st2nd2 6178 |
. . . . . . . . . . . . . . . . 17
โข ((โก๐นโ๐ด) โ (๐ฝ ร โ0) โ (โก๐นโ๐ด) = โจ(1st โ(โก๐นโ๐ด)), (2nd โ(โก๐นโ๐ด))โฉ) |
70 | 7, 69 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ โ (โก๐นโ๐ด) = โจ(1st โ(โก๐นโ๐ด)), (2nd โ(โก๐นโ๐ด))โฉ) |
71 | 70 | fveq2d 5521 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ (๐นโ(โก๐นโ๐ด)) = (๐นโโจ(1st โ(โก๐นโ๐ด)), (2nd โ(โก๐นโ๐ด))โฉ)) |
72 | 68, 71 | eqtr3d 2212 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ๐ด = (๐นโโจ(1st โ(โก๐นโ๐ด)), (2nd โ(โก๐นโ๐ด))โฉ)) |
73 | | df-ov 5880 |
. . . . . . . . . . . . . 14
โข
((1st โ(โก๐นโ๐ด))๐น(2nd โ(โก๐นโ๐ด))) = (๐นโโจ(1st โ(โก๐นโ๐ด)), (2nd โ(โก๐นโ๐ด))โฉ) |
74 | 72, 73 | eqtr4di 2228 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ ๐ด = ((1st
โ(โก๐นโ๐ด))๐น(2nd โ(โก๐นโ๐ด)))) |
75 | 12, 9 | nnexpcld 10678 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ
(2โ(2nd โ(โก๐นโ๐ด))) โ โ) |
76 | 75, 27 | nnmulcld 8970 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ
((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด))) โ โ) |
77 | | oveq2 5885 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (1st โ(โก๐นโ๐ด)) โ ((2โ๐ฆ) ยท ๐ฅ) = ((2โ๐ฆ) ยท (1st โ(โก๐นโ๐ด)))) |
78 | | oveq2 5885 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = (2nd โ(โก๐นโ๐ด)) โ (2โ๐ฆ) = (2โ(2nd โ(โก๐นโ๐ด)))) |
79 | 78 | oveq1d 5892 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = (2nd โ(โก๐นโ๐ด)) โ ((2โ๐ฆ) ยท (1st โ(โก๐นโ๐ด))) = ((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด)))) |
80 | 77, 79, 2 | ovmpog 6011 |
. . . . . . . . . . . . . 14
โข
(((1st โ(โก๐นโ๐ด)) โ ๐ฝ โง (2nd โ(โก๐นโ๐ด)) โ โ0 โง
((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด))) โ โ) โ ((1st
โ(โก๐นโ๐ด))๐น(2nd โ(โก๐นโ๐ด))) = ((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด)))) |
81 | 22, 9, 76, 80 | syl3anc 1238 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ
((1st โ(โก๐นโ๐ด))๐น(2nd โ(โก๐นโ๐ด))) = ((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด)))) |
82 | 74, 81 | eqtrd 2210 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด = ((2โ(2nd
โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด)))) |
83 | 82 | oveq1d 5892 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (๐ดโ2) =
(((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด)))โ2)) |
84 | 75 | nncnd 8935 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(2โ(2nd โ(โก๐นโ๐ด))) โ โ) |
85 | 84, 38 | sqmuld 10668 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(((2โ(2nd โ(โก๐นโ๐ด))) ยท (1st โ(โก๐นโ๐ด)))โ2) = (((2โ(2nd
โ(โก๐นโ๐ด)))โ2) ยท ((1st
โ(โก๐นโ๐ด))โ2))) |
86 | 83, 85 | eqtrd 2210 |
. . . . . . . . . 10
โข (๐ด โ โ โ (๐ดโ2) =
(((2โ(2nd โ(โก๐นโ๐ด)))โ2) ยท ((1st
โ(โก๐นโ๐ด))โ2))) |
87 | 86 | oveq2d 5893 |
. . . . . . . . 9
โข (๐ด โ โ โ (2
ยท (๐ดโ2)) = (2
ยท (((2โ(2nd โ(โก๐นโ๐ด)))โ2) ยท ((1st
โ(โก๐นโ๐ด))โ2)))) |
88 | 56, 54 | eqeltrrd 2255 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((2โ(2nd โ(โก๐นโ๐ด)))โ2) โ โ) |
89 | 28 | nncnd 8935 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((1st โ(โก๐นโ๐ด))โ2) โ โ) |
90 | 52, 88, 89 | mulassd 7983 |
. . . . . . . . 9
โข (๐ด โ โ โ ((2
ยท ((2โ(2nd โ(โก๐นโ๐ด)))โ2)) ยท ((1st
โ(โก๐นโ๐ด))โ2)) = (2 ยท
(((2โ(2nd โ(โก๐นโ๐ด)))โ2) ยท ((1st
โ(โก๐นโ๐ด))โ2)))) |
91 | 87, 90 | eqtr4d 2213 |
. . . . . . . 8
โข (๐ด โ โ โ (2
ยท (๐ดโ2)) = ((2
ยท ((2โ(2nd โ(โก๐นโ๐ด)))โ2)) ยท ((1st
โ(โก๐นโ๐ด))โ2))) |
92 | 59, 66, 91 | 3eqtr4rd 2221 |
. . . . . . 7
โข (๐ด โ โ โ (2
ยท (๐ดโ2)) =
(((1st โ(โก๐นโ๐ด))โ2)๐น(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1))) |
93 | | df-ov 5880 |
. . . . . . 7
โข
(((1st โ(โก๐นโ๐ด))โ2)๐น(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) = (๐นโโจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) |
94 | 92, 93 | eqtr2di 2227 |
. . . . . 6
โข (๐ด โ โ โ (๐นโโจ((1st
โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) = (2 ยท
(๐ดโ2))) |
95 | | f1ocnvfv 5782 |
. . . . . . 7
โข ((๐น:(๐ฝ ร โ0)โ1-1-ontoโโ โง โจ((1st
โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ โ (๐ฝ ร โ0))
โ ((๐นโโจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) = (2 ยท
(๐ดโ2)) โ (โก๐นโ(2 ยท (๐ดโ2))) = โจ((1st
โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ)) |
96 | 3, 95 | mpan 424 |
. . . . . 6
โข
(โจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ โ (๐ฝ ร โ0)
โ ((๐นโโจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) = (2 ยท
(๐ดโ2)) โ (โก๐นโ(2 ยท (๐ดโ2))) = โจ((1st
โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ)) |
97 | 51, 94, 96 | sylc 62 |
. . . . 5
โข (๐ด โ โ โ (โก๐นโ(2 ยท (๐ดโ2))) = โจ((1st
โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) |
98 | 97 | fveq2d 5521 |
. . . 4
โข (๐ด โ โ โ
(2nd โ(โก๐นโ(2 ยท (๐ดโ2)))) = (2nd
โโจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ)) |
99 | | op2ndg 6154 |
. . . . 5
โข
((((1st โ(โก๐นโ๐ด))โ2) โ ๐ฝ โง (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1) โ
โ0) โ (2nd โโจ((1st
โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) =
(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) |
100 | 45, 49, 99 | syl2anc 411 |
. . . 4
โข (๐ด โ โ โ
(2nd โโจ((1st โ(โก๐นโ๐ด))โ2), (((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)โฉ) =
(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1)) |
101 | 98, 100 | eqtrd 2210 |
. . 3
โข (๐ด โ โ โ
(2nd โ(โก๐นโ(2 ยท (๐ดโ2)))) = (((2nd
โ(โก๐นโ๐ด)) ยท 2) + 1)) |
102 | 101 | breq2d 4017 |
. 2
โข (๐ด โ โ โ (2
โฅ (2nd โ(โก๐นโ(2 ยท (๐ดโ2)))) โ 2 โฅ
(((2nd โ(โก๐นโ๐ด)) ยท 2) + 1))) |
103 | 20, 102 | mtbird 673 |
1
โข (๐ด โ โ โ ยฌ 2
โฅ (2nd โ(โก๐นโ(2 ยท (๐ดโ2))))) |