Step | Hyp | Ref
| Expression |
1 | | eqeq2 2750 |
. . . 4
โข (๐ = 0 โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = 0)) |
2 | 1 | rexbidv 3174 |
. . 3
โข (๐ = 0 โ (โ๐ โ โค ((2 ยท
๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท
๐) + 1) =
0)) |
3 | | eqeq2 2750 |
. . . 4
โข (๐ = 0 โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = 0)) |
4 | 3 | rexbidv 3174 |
. . 3
โข (๐ = 0 โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) =
0)) |
5 | 2, 4 | orbi12d 918 |
. 2
โข (๐ = 0 โ ((โ๐ โ โค ((2 ยท
๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = 0 โจ โ๐ โ โค (๐ ยท 2) =
0))) |
6 | | eqeq2 2750 |
. . . . 5
โข (๐ = ๐ โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = ๐)) |
7 | 6 | rexbidv 3174 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
8 | | oveq2 7358 |
. . . . . . 7
โข (๐ = ๐ฅ โ (2 ยท ๐) = (2 ยท ๐ฅ)) |
9 | 8 | oveq1d 7365 |
. . . . . 6
โข (๐ = ๐ฅ โ ((2 ยท ๐) + 1) = ((2 ยท ๐ฅ) + 1)) |
10 | 9 | eqeq1d 2740 |
. . . . 5
โข (๐ = ๐ฅ โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐ฅ) + 1) = ๐)) |
11 | 10 | cbvrexvw 3225 |
. . . 4
โข
(โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โ โ๐ฅ โ โค ((2 ยท
๐ฅ) + 1) = ๐) |
12 | 7, 11 | bitrdi 287 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ฅ โ โค ((2 ยท ๐ฅ) + 1) = ๐)) |
13 | | eqeq2 2750 |
. . . . 5
โข (๐ = ๐ โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = ๐)) |
14 | 13 | rexbidv 3174 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
15 | | oveq1 7357 |
. . . . . 6
โข (๐ = ๐ฆ โ (๐ ยท 2) = (๐ฆ ยท 2)) |
16 | 15 | eqeq1d 2740 |
. . . . 5
โข (๐ = ๐ฆ โ ((๐ ยท 2) = ๐ โ (๐ฆ ยท 2) = ๐)) |
17 | 16 | cbvrexvw 3225 |
. . . 4
โข
(โ๐ โ
โค (๐ ยท 2) =
๐ โ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐) |
18 | 14, 17 | bitrdi 287 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐)) |
19 | 12, 18 | orbi12d 918 |
. 2
โข (๐ = ๐ โ ((โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ฅ โ โค ((2 ยท ๐ฅ) + 1) = ๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐))) |
20 | | eqeq2 2750 |
. . . 4
โข (๐ = (๐ + 1) โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = (๐ + 1))) |
21 | 20 | rexbidv 3174 |
. . 3
โข (๐ = (๐ + 1) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = (๐ + 1))) |
22 | | eqeq2 2750 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = (๐ + 1))) |
23 | 22 | rexbidv 3174 |
. . 3
โข (๐ = (๐ + 1) โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) = (๐ + 1))) |
24 | 21, 23 | orbi12d 918 |
. 2
โข (๐ = (๐ + 1) โ ((โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = (๐ + 1) โจ โ๐ โ โค (๐ ยท 2) = (๐ + 1)))) |
25 | | eqeq2 2750 |
. . . 4
โข (๐ = ๐ โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = ๐)) |
26 | 25 | rexbidv 3174 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
27 | | eqeq2 2750 |
. . . 4
โข (๐ = ๐ โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = ๐)) |
28 | 27 | rexbidv 3174 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
29 | 26, 28 | orbi12d 918 |
. 2
โข (๐ = ๐ โ ((โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐))) |
30 | | 0z 12444 |
. . . 4
โข 0 โ
โค |
31 | | 2cn 12162 |
. . . . 5
โข 2 โ
โ |
32 | 31 | mul02i 11278 |
. . . 4
โข (0
ยท 2) = 0 |
33 | | oveq1 7357 |
. . . . . 6
โข (๐ = 0 โ (๐ ยท 2) = (0 ยท
2)) |
34 | 33 | eqeq1d 2740 |
. . . . 5
โข (๐ = 0 โ ((๐ ยท 2) = 0 โ (0 ยท 2) =
0)) |
35 | 34 | rspcev 3580 |
. . . 4
โข ((0
โ โค โง (0 ยท 2) = 0) โ โ๐ โ โค (๐ ยท 2) = 0) |
36 | 30, 32, 35 | mp2an 691 |
. . 3
โข
โ๐ โ
โค (๐ ยท 2) =
0 |
37 | 36 | olci 865 |
. 2
โข
(โ๐ โ
โค ((2 ยท ๐) +
1) = 0 โจ โ๐ โ
โค (๐ ยท 2) =
0) |
38 | | orcom 869 |
. . 3
โข
((โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = ๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐) โ (โ๐ฆ โ โค (๐ฆ ยท 2) = ๐ โจ โ๐ฅ โ โค ((2 ยท ๐ฅ) + 1) = ๐)) |
39 | | zcn 12438 |
. . . . . . . . 9
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
40 | | mulcom 11071 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง 2 โ
โ) โ (๐ฆ ยท
2) = (2 ยท ๐ฆ)) |
41 | 39, 31, 40 | sylancl 587 |
. . . . . . . 8
โข (๐ฆ โ โค โ (๐ฆ ยท 2) = (2 ยท ๐ฆ)) |
42 | 41 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ (๐ฆ ยท 2) = (2
ยท ๐ฆ)) |
43 | 42 | eqeq1d 2740 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ ((๐ฆ ยท 2) =
๐ โ (2 ยท ๐ฆ) = ๐)) |
44 | | eqid 2738 |
. . . . . . . . 9
โข ((2
ยท ๐ฆ) + 1) = ((2
ยท ๐ฆ) +
1) |
45 | | oveq2 7358 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (2 ยท ๐) = (2 ยท ๐ฆ)) |
46 | 45 | oveq1d 7365 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ ((2 ยท ๐) + 1) = ((2 ยท ๐ฆ) + 1)) |
47 | 46 | eqeq1d 2740 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (((2 ยท ๐) + 1) = ((2 ยท ๐ฆ) + 1) โ ((2 ยท ๐ฆ) + 1) = ((2 ยท ๐ฆ) + 1))) |
48 | 47 | rspcev 3580 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง ((2
ยท ๐ฆ) + 1) = ((2
ยท ๐ฆ) + 1)) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ((2
ยท ๐ฆ) +
1)) |
49 | 44, 48 | mpan2 690 |
. . . . . . . 8
โข (๐ฆ โ โค โ
โ๐ โ โค ((2
ยท ๐) + 1) = ((2
ยท ๐ฆ) +
1)) |
50 | | oveq1 7357 |
. . . . . . . . . 10
โข ((2
ยท ๐ฆ) = ๐ โ ((2 ยท ๐ฆ) + 1) = (๐ + 1)) |
51 | 50 | eqeq2d 2749 |
. . . . . . . . 9
โข ((2
ยท ๐ฆ) = ๐ โ (((2 ยท ๐) + 1) = ((2 ยท ๐ฆ) + 1) โ ((2 ยท ๐) + 1) = (๐ + 1))) |
52 | 51 | rexbidv 3174 |
. . . . . . . 8
โข ((2
ยท ๐ฆ) = ๐ โ (โ๐ โ โค ((2 ยท
๐) + 1) = ((2 ยท
๐ฆ) + 1) โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
53 | 49, 52 | syl5ibcom 245 |
. . . . . . 7
โข (๐ฆ โ โค โ ((2
ยท ๐ฆ) = ๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
54 | 53 | adantl 483 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ ((2 ยท ๐ฆ) =
๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
55 | 43, 54 | sylbid 239 |
. . . . 5
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ ((๐ฆ ยท 2) =
๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
56 | 55 | rexlimdva 3151 |
. . . 4
โข (๐ โ โ0
โ (โ๐ฆ โ
โค (๐ฆ ยท 2) =
๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
57 | | peano2z 12475 |
. . . . . . 7
โข (๐ฅ โ โค โ (๐ฅ + 1) โ
โค) |
58 | | zcn 12438 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
59 | | mulcom 11071 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง 2 โ
โ) โ (๐ฅ ยท
2) = (2 ยท ๐ฅ)) |
60 | 31, 59 | mpan2 690 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (๐ฅ ยท 2) = (2 ยท ๐ฅ)) |
61 | 31 | mulid2i 11094 |
. . . . . . . . . . . . 13
โข (1
ยท 2) = 2 |
62 | 61 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (1
ยท 2) = 2) |
63 | 60, 62 | oveq12d 7368 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ ((๐ฅ ยท 2) + (1 ยท 2)) =
((2 ยท ๐ฅ) +
2)) |
64 | | df-2 12150 |
. . . . . . . . . . . 12
โข 2 = (1 +
1) |
65 | 64 | oveq2i 7361 |
. . . . . . . . . . 11
โข ((2
ยท ๐ฅ) + 2) = ((2
ยท ๐ฅ) + (1 +
1)) |
66 | 63, 65 | eqtrdi 2794 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ ((๐ฅ ยท 2) + (1 ยท 2)) =
((2 ยท ๐ฅ) + (1 +
1))) |
67 | | ax-1cn 11043 |
. . . . . . . . . . 11
โข 1 โ
โ |
68 | | adddir 11080 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง 1 โ
โ โง 2 โ โ) โ ((๐ฅ + 1) ยท 2) = ((๐ฅ ยท 2) + (1 ยท
2))) |
69 | 67, 31, 68 | mp3an23 1454 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ ((๐ฅ + 1) ยท 2) = ((๐ฅ ยท 2) + (1 ยท
2))) |
70 | | mulcl 11069 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยท ๐ฅ) โ โ) |
71 | 31, 70 | mpan 689 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
โ) |
72 | | addass 11072 |
. . . . . . . . . . . 12
โข (((2
ยท ๐ฅ) โ โ
โง 1 โ โ โง 1 โ โ) โ (((2 ยท ๐ฅ) + 1) + 1) = ((2 ยท ๐ฅ) + (1 + 1))) |
73 | 67, 67, 72 | mp3an23 1454 |
. . . . . . . . . . 11
โข ((2
ยท ๐ฅ) โ โ
โ (((2 ยท ๐ฅ) +
1) + 1) = ((2 ยท ๐ฅ) +
(1 + 1))) |
74 | 71, 73 | syl 17 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ (((2
ยท ๐ฅ) + 1) + 1) = ((2
ยท ๐ฅ) + (1 +
1))) |
75 | 66, 69, 74 | 3eqtr4d 2788 |
. . . . . . . . 9
โข (๐ฅ โ โ โ ((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) +
1)) |
76 | 58, 75 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โค โ ((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) +
1)) |
77 | 76 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((๐ฅ + 1) ยท 2)
= (((2 ยท ๐ฅ) + 1) +
1)) |
78 | | oveq1 7357 |
. . . . . . . . 9
โข (๐ = (๐ฅ + 1) โ (๐ ยท 2) = ((๐ฅ + 1) ยท 2)) |
79 | 78 | eqeq1d 2740 |
. . . . . . . 8
โข (๐ = (๐ฅ + 1) โ ((๐ ยท 2) = (((2 ยท ๐ฅ) + 1) + 1) โ ((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) +
1))) |
80 | 79 | rspcev 3580 |
. . . . . . 7
โข (((๐ฅ + 1) โ โค โง
((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) + 1))
โ โ๐ โ
โค (๐ ยท 2) =
(((2 ยท ๐ฅ) + 1) +
1)) |
81 | 57, 77, 80 | syl2an2 685 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ โ๐ โ
โค (๐ ยท 2) =
(((2 ยท ๐ฅ) + 1) +
1)) |
82 | | oveq1 7357 |
. . . . . . . 8
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (((2 ยท ๐ฅ) + 1) + 1) = (๐ + 1)) |
83 | 82 | eqeq2d 2749 |
. . . . . . 7
โข (((2
ยท ๐ฅ) + 1) = ๐ โ ((๐ ยท 2) = (((2 ยท ๐ฅ) + 1) + 1) โ (๐ ยท 2) = (๐ + 1))) |
84 | 83 | rexbidv 3174 |
. . . . . 6
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (โ๐ โ โค (๐ ยท 2) = (((2 ยท
๐ฅ) + 1) + 1) โ
โ๐ โ โค
(๐ ยท 2) = (๐ + 1))) |
85 | 81, 84 | syl5ibcom 245 |
. . . . 5
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (((2 ยท ๐ฅ) +
1) = ๐ โ โ๐ โ โค (๐ ยท 2) = (๐ + 1))) |
86 | 85 | rexlimdva 3151 |
. . . 4
โข (๐ โ โ0
โ (โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = ๐ โ โ๐ โ โค (๐ ยท 2) = (๐ + 1))) |
87 | 56, 86 | orim12d 964 |
. . 3
โข (๐ โ โ0
โ ((โ๐ฆ โ
โค (๐ฆ ยท 2) =
๐ โจ โ๐ฅ โ โค ((2 ยท
๐ฅ) + 1) = ๐) โ (โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1) โจ โ๐ โ โค (๐ ยท 2) = (๐ + 1)))) |
88 | 38, 87 | biimtrid 241 |
. 2
โข (๐ โ โ0
โ ((โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = ๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1) โจ โ๐ โ โค (๐ ยท 2) = (๐ + 1)))) |
89 | 5, 19, 24, 29, 37, 88 | nn0ind 12529 |
1
โข (๐ โ โ0
โ (โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |