Step | Hyp | Ref
| Expression |
1 | | eqeq2 2187 |
. . . 4
โข (๐ = 0 โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = 0)) |
2 | 1 | rexbidv 2478 |
. . 3
โข (๐ = 0 โ (โ๐ โ โค ((2 ยท
๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท
๐) + 1) =
0)) |
3 | | eqeq2 2187 |
. . . 4
โข (๐ = 0 โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = 0)) |
4 | 3 | rexbidv 2478 |
. . 3
โข (๐ = 0 โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) =
0)) |
5 | 2, 4 | orbi12d 793 |
. 2
โข (๐ = 0 โ ((โ๐ โ โค ((2 ยท
๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = 0 โจ โ๐ โ โค (๐ ยท 2) =
0))) |
6 | | eqeq2 2187 |
. . . . 5
โข (๐ = ๐ โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = ๐)) |
7 | 6 | rexbidv 2478 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
8 | | oveq2 5886 |
. . . . . . 7
โข (๐ = ๐ฅ โ (2 ยท ๐) = (2 ยท ๐ฅ)) |
9 | 8 | oveq1d 5893 |
. . . . . 6
โข (๐ = ๐ฅ โ ((2 ยท ๐) + 1) = ((2 ยท ๐ฅ) + 1)) |
10 | 9 | eqeq1d 2186 |
. . . . 5
โข (๐ = ๐ฅ โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐ฅ) + 1) = ๐)) |
11 | 10 | cbvrexv 2706 |
. . . 4
โข
(โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โ โ๐ฅ โ โค ((2 ยท
๐ฅ) + 1) = ๐) |
12 | 7, 11 | bitrdi 196 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ฅ โ โค ((2 ยท ๐ฅ) + 1) = ๐)) |
13 | | eqeq2 2187 |
. . . . 5
โข (๐ = ๐ โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = ๐)) |
14 | 13 | rexbidv 2478 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
15 | | oveq1 5885 |
. . . . . 6
โข (๐ = ๐ฆ โ (๐ ยท 2) = (๐ฆ ยท 2)) |
16 | 15 | eqeq1d 2186 |
. . . . 5
โข (๐ = ๐ฆ โ ((๐ ยท 2) = ๐ โ (๐ฆ ยท 2) = ๐)) |
17 | 16 | cbvrexv 2706 |
. . . 4
โข
(โ๐ โ
โค (๐ ยท 2) =
๐ โ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐) |
18 | 14, 17 | bitrdi 196 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐)) |
19 | 12, 18 | orbi12d 793 |
. 2
โข (๐ = ๐ โ ((โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ฅ โ โค ((2 ยท ๐ฅ) + 1) = ๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐))) |
20 | | eqeq2 2187 |
. . . 4
โข (๐ = (๐ + 1) โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = (๐ + 1))) |
21 | 20 | rexbidv 2478 |
. . 3
โข (๐ = (๐ + 1) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = (๐ + 1))) |
22 | | eqeq2 2187 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = (๐ + 1))) |
23 | 22 | rexbidv 2478 |
. . 3
โข (๐ = (๐ + 1) โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) = (๐ + 1))) |
24 | 21, 23 | orbi12d 793 |
. 2
โข (๐ = (๐ + 1) โ ((โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = (๐ + 1) โจ โ๐ โ โค (๐ ยท 2) = (๐ + 1)))) |
25 | | eqeq2 2187 |
. . . 4
โข (๐ = ๐ โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท ๐) + 1) = ๐)) |
26 | 25 | rexbidv 2478 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
27 | | eqeq2 2187 |
. . . 4
โข (๐ = ๐ โ ((๐ ยท 2) = ๐ โ (๐ ยท 2) = ๐)) |
28 | 27 | rexbidv 2478 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
29 | 26, 28 | orbi12d 793 |
. 2
โข (๐ = ๐ โ ((โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐))) |
30 | | 0z 9267 |
. . . 4
โข 0 โ
โค |
31 | | 2cn 8993 |
. . . . 5
โข 2 โ
โ |
32 | 31 | mul02i 8350 |
. . . 4
โข (0
ยท 2) = 0 |
33 | | oveq1 5885 |
. . . . . 6
โข (๐ = 0 โ (๐ ยท 2) = (0 ยท
2)) |
34 | 33 | eqeq1d 2186 |
. . . . 5
โข (๐ = 0 โ ((๐ ยท 2) = 0 โ (0 ยท 2) =
0)) |
35 | 34 | rspcev 2843 |
. . . 4
โข ((0
โ โค โง (0 ยท 2) = 0) โ โ๐ โ โค (๐ ยท 2) = 0) |
36 | 30, 32, 35 | mp2an 426 |
. . 3
โข
โ๐ โ
โค (๐ ยท 2) =
0 |
37 | 36 | olci 732 |
. 2
โข
(โ๐ โ
โค ((2 ยท ๐) +
1) = 0 โจ โ๐ โ
โค (๐ ยท 2) =
0) |
38 | | orcom 728 |
. . 3
โข
((โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = ๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐) โ (โ๐ฆ โ โค (๐ฆ ยท 2) = ๐ โจ โ๐ฅ โ โค ((2 ยท ๐ฅ) + 1) = ๐)) |
39 | | zcn 9261 |
. . . . . . . . 9
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
40 | | mulcom 7943 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง 2 โ
โ) โ (๐ฆ ยท
2) = (2 ยท ๐ฆ)) |
41 | 39, 31, 40 | sylancl 413 |
. . . . . . . 8
โข (๐ฆ โ โค โ (๐ฆ ยท 2) = (2 ยท ๐ฆ)) |
42 | 41 | adantl 277 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ (๐ฆ ยท 2) = (2
ยท ๐ฆ)) |
43 | 42 | eqeq1d 2186 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ ((๐ฆ ยท 2) =
๐ โ (2 ยท ๐ฆ) = ๐)) |
44 | | eqid 2177 |
. . . . . . . . 9
โข ((2
ยท ๐ฆ) + 1) = ((2
ยท ๐ฆ) +
1) |
45 | | oveq2 5886 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (2 ยท ๐) = (2 ยท ๐ฆ)) |
46 | 45 | oveq1d 5893 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ ((2 ยท ๐) + 1) = ((2 ยท ๐ฆ) + 1)) |
47 | 46 | eqeq1d 2186 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (((2 ยท ๐) + 1) = ((2 ยท ๐ฆ) + 1) โ ((2 ยท ๐ฆ) + 1) = ((2 ยท ๐ฆ) + 1))) |
48 | 47 | rspcev 2843 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง ((2
ยท ๐ฆ) + 1) = ((2
ยท ๐ฆ) + 1)) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ((2
ยท ๐ฆ) +
1)) |
49 | 44, 48 | mpan2 425 |
. . . . . . . 8
โข (๐ฆ โ โค โ
โ๐ โ โค ((2
ยท ๐) + 1) = ((2
ยท ๐ฆ) +
1)) |
50 | | oveq1 5885 |
. . . . . . . . . 10
โข ((2
ยท ๐ฆ) = ๐ โ ((2 ยท ๐ฆ) + 1) = (๐ + 1)) |
51 | 50 | eqeq2d 2189 |
. . . . . . . . 9
โข ((2
ยท ๐ฆ) = ๐ โ (((2 ยท ๐) + 1) = ((2 ยท ๐ฆ) + 1) โ ((2 ยท ๐) + 1) = (๐ + 1))) |
52 | 51 | rexbidv 2478 |
. . . . . . . 8
โข ((2
ยท ๐ฆ) = ๐ โ (โ๐ โ โค ((2 ยท
๐) + 1) = ((2 ยท
๐ฆ) + 1) โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
53 | 49, 52 | syl5ibcom 155 |
. . . . . . 7
โข (๐ฆ โ โค โ ((2
ยท ๐ฆ) = ๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
54 | 53 | adantl 277 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ ((2 ยท ๐ฆ) =
๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
55 | 43, 54 | sylbid 150 |
. . . . 5
โข ((๐ โ โ0
โง ๐ฆ โ โค)
โ ((๐ฆ ยท 2) =
๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
56 | 55 | rexlimdva 2594 |
. . . 4
โข (๐ โ โ0
โ (โ๐ฆ โ
โค (๐ฆ ยท 2) =
๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1))) |
57 | | peano2z 9292 |
. . . . . . . 8
โข (๐ฅ โ โค โ (๐ฅ + 1) โ
โค) |
58 | 57 | adantl 277 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (๐ฅ + 1) โ
โค) |
59 | | zcn 9261 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
60 | | mulcom 7943 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง 2 โ
โ) โ (๐ฅ ยท
2) = (2 ยท ๐ฅ)) |
61 | 31, 60 | mpan2 425 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (๐ฅ ยท 2) = (2 ยท ๐ฅ)) |
62 | 31 | mullidi 7963 |
. . . . . . . . . . . . 13
โข (1
ยท 2) = 2 |
63 | 62 | a1i 9 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (1
ยท 2) = 2) |
64 | 61, 63 | oveq12d 5896 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ ((๐ฅ ยท 2) + (1 ยท 2)) =
((2 ยท ๐ฅ) +
2)) |
65 | | df-2 8981 |
. . . . . . . . . . . 12
โข 2 = (1 +
1) |
66 | 65 | oveq2i 5889 |
. . . . . . . . . . 11
โข ((2
ยท ๐ฅ) + 2) = ((2
ยท ๐ฅ) + (1 +
1)) |
67 | 64, 66 | eqtrdi 2226 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ ((๐ฅ ยท 2) + (1 ยท 2)) =
((2 ยท ๐ฅ) + (1 +
1))) |
68 | | ax-1cn 7907 |
. . . . . . . . . . 11
โข 1 โ
โ |
69 | | adddir 7951 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง 1 โ
โ โง 2 โ โ) โ ((๐ฅ + 1) ยท 2) = ((๐ฅ ยท 2) + (1 ยท
2))) |
70 | 68, 31, 69 | mp3an23 1329 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ ((๐ฅ + 1) ยท 2) = ((๐ฅ ยท 2) + (1 ยท
2))) |
71 | | mulcl 7941 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยท ๐ฅ) โ โ) |
72 | 31, 71 | mpan 424 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
โ) |
73 | | addass 7944 |
. . . . . . . . . . . 12
โข (((2
ยท ๐ฅ) โ โ
โง 1 โ โ โง 1 โ โ) โ (((2 ยท ๐ฅ) + 1) + 1) = ((2 ยท ๐ฅ) + (1 + 1))) |
74 | 68, 68, 73 | mp3an23 1329 |
. . . . . . . . . . 11
โข ((2
ยท ๐ฅ) โ โ
โ (((2 ยท ๐ฅ) +
1) + 1) = ((2 ยท ๐ฅ) +
(1 + 1))) |
75 | 72, 74 | syl 14 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ (((2
ยท ๐ฅ) + 1) + 1) = ((2
ยท ๐ฅ) + (1 +
1))) |
76 | 67, 70, 75 | 3eqtr4d 2220 |
. . . . . . . . 9
โข (๐ฅ โ โ โ ((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) +
1)) |
77 | 59, 76 | syl 14 |
. . . . . . . 8
โข (๐ฅ โ โค โ ((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) +
1)) |
78 | 77 | adantl 277 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ ((๐ฅ + 1) ยท 2)
= (((2 ยท ๐ฅ) + 1) +
1)) |
79 | | oveq1 5885 |
. . . . . . . . 9
โข (๐ = (๐ฅ + 1) โ (๐ ยท 2) = ((๐ฅ + 1) ยท 2)) |
80 | 79 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ = (๐ฅ + 1) โ ((๐ ยท 2) = (((2 ยท ๐ฅ) + 1) + 1) โ ((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) +
1))) |
81 | 80 | rspcev 2843 |
. . . . . . 7
โข (((๐ฅ + 1) โ โค โง
((๐ฅ + 1) ยท 2) = (((2
ยท ๐ฅ) + 1) + 1))
โ โ๐ โ
โค (๐ ยท 2) =
(((2 ยท ๐ฅ) + 1) +
1)) |
82 | 58, 78, 81 | syl2anc 411 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ โ๐ โ
โค (๐ ยท 2) =
(((2 ยท ๐ฅ) + 1) +
1)) |
83 | | oveq1 5885 |
. . . . . . . 8
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (((2 ยท ๐ฅ) + 1) + 1) = (๐ + 1)) |
84 | 83 | eqeq2d 2189 |
. . . . . . 7
โข (((2
ยท ๐ฅ) + 1) = ๐ โ ((๐ ยท 2) = (((2 ยท ๐ฅ) + 1) + 1) โ (๐ ยท 2) = (๐ + 1))) |
85 | 84 | rexbidv 2478 |
. . . . . 6
โข (((2
ยท ๐ฅ) + 1) = ๐ โ (โ๐ โ โค (๐ ยท 2) = (((2 ยท
๐ฅ) + 1) + 1) โ
โ๐ โ โค
(๐ ยท 2) = (๐ + 1))) |
86 | 82, 85 | syl5ibcom 155 |
. . . . 5
โข ((๐ โ โ0
โง ๐ฅ โ โค)
โ (((2 ยท ๐ฅ) +
1) = ๐ โ โ๐ โ โค (๐ ยท 2) = (๐ + 1))) |
87 | 86 | rexlimdva 2594 |
. . . 4
โข (๐ โ โ0
โ (โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = ๐ โ โ๐ โ โค (๐ ยท 2) = (๐ + 1))) |
88 | 56, 87 | orim12d 786 |
. . 3
โข (๐ โ โ0
โ ((โ๐ฆ โ
โค (๐ฆ ยท 2) =
๐ โจ โ๐ฅ โ โค ((2 ยท
๐ฅ) + 1) = ๐) โ (โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1) โจ โ๐ โ โค (๐ ยท 2) = (๐ + 1)))) |
89 | 38, 88 | biimtrid 152 |
. 2
โข (๐ โ โ0
โ ((โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = ๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท
๐) + 1) = (๐ + 1) โจ โ๐ โ โค (๐ ยท 2) = (๐ + 1)))) |
90 | 5, 19, 24, 29, 37, 89 | nn0ind 9370 |
1
โข (๐ โ โ0
โ (โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |