Step | Hyp | Ref
| Expression |
1 | | 2z 12593 |
. . . 4
โข 2 โ
โค |
2 | | divides 16198 |
. . . 4
โข ((2
โ โค โง ๐
โ โค) โ (2 โฅ ๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
3 | 1, 2 | mpan 688 |
. . 3
โข (๐ โ โค โ (2
โฅ ๐ โ
โ๐ โ โค
(๐ ยท 2) = ๐)) |
4 | 3 | notbid 317 |
. 2
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ ยฌ
โ๐ โ โค
(๐ ยท 2) = ๐)) |
5 | | elznn0 12572 |
. . . 4
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
6 | | odd2np1lem 16282 |
. . . . . 6
โข (๐ โ โ0
โ (โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |
7 | 6 | adantl 482 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ (โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |
8 | | peano2z 12602 |
. . . . . . . . . . 11
โข (๐ฅ โ โค โ (๐ฅ + 1) โ
โค) |
9 | | znegcl 12596 |
. . . . . . . . . . 11
โข ((๐ฅ + 1) โ โค โ
-(๐ฅ + 1) โ
โค) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ -(๐ฅ + 1) โ
โค) |
11 | 10 | ad2antlr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ฅ โ โค) โง ((2
ยท ๐ฅ) + 1) = -๐) โ -(๐ฅ + 1) โ โค) |
12 | | zcn 12562 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
13 | | 2cn 12286 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ |
14 | | mulcl 11193 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยท ๐ฅ) โ โ) |
15 | 13, 14 | mpan 688 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
โ) |
16 | | peano2cn 11385 |
. . . . . . . . . . . . . . 15
โข ((2
ยท ๐ฅ) โ โ
โ ((2 ยท ๐ฅ) + 1)
โ โ) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ) + 1) โ
โ) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โค โ ((2
ยท ๐ฅ) + 1) โ
โ) |
19 | 18 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฅ โ โค) โ ((2
ยท ๐ฅ) + 1) โ
โ) |
20 | | simpl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ฅ โ โค) โ ๐ โ
โ) |
21 | 20 | recnd 11241 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฅ โ โค) โ ๐ โ
โ) |
22 | | negcon2 11512 |
. . . . . . . . . . . 12
โข ((((2
ยท ๐ฅ) + 1) โ
โ โง ๐ โ
โ) โ (((2 ยท ๐ฅ) + 1) = -๐ โ ๐ = -((2 ยท ๐ฅ) + 1))) |
23 | 19, 21, 22 | syl2anc 584 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฅ โ โค) โ (((2
ยท ๐ฅ) + 1) = -๐ โ ๐ = -((2 ยท ๐ฅ) + 1))) |
24 | | eqcom 2739 |
. . . . . . . . . . . 12
โข (๐ = -((2 ยท ๐ฅ) + 1) โ -((2 ยท
๐ฅ) + 1) = ๐) |
25 | 13, 12, 14 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โค โ (2
ยท ๐ฅ) โ
โ) |
26 | | ax-1cn 11167 |
. . . . . . . . . . . . . . . . . . . . 21
โข 1 โ
โ |
27 | 13, 26 | mulcli 11220 |
. . . . . . . . . . . . . . . . . . . 20
โข (2
ยท 1) โ โ |
28 | | addsubass 11469 |
. . . . . . . . . . . . . . . . . . . 20
โข (((2
ยท ๐ฅ) โ โ
โง (2 ยท 1) โ โ โง 1 โ โ) โ (((2
ยท ๐ฅ) + (2 ยท
1)) โ 1) = ((2 ยท ๐ฅ) + ((2 ยท 1) โ
1))) |
29 | 27, 26, 28 | mp3an23 1453 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
ยท ๐ฅ) โ โ
โ (((2 ยท ๐ฅ) +
(2 ยท 1)) โ 1) = ((2 ยท ๐ฅ) + ((2 ยท 1) โ
1))) |
30 | 25, 29 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (((2
ยท ๐ฅ) + (2 ยท
1)) โ 1) = ((2 ยท ๐ฅ) + ((2 ยท 1) โ
1))) |
31 | | 2t1e2 12374 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 1) = 2 |
32 | 31 | oveq1i 7418 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
ยท 1) โ 1) = (2 โ 1) |
33 | | 2m1e1 12337 |
. . . . . . . . . . . . . . . . . . . 20
โข (2
โ 1) = 1 |
34 | 32, 33 | eqtri 2760 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
ยท 1) โ 1) = 1 |
35 | 34 | oveq2i 7419 |
. . . . . . . . . . . . . . . . . 18
โข ((2
ยท ๐ฅ) + ((2 ยท
1) โ 1)) = ((2 ยท ๐ฅ) + 1) |
36 | 30, 35 | eqtr2di 2789 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ ((2
ยท ๐ฅ) + 1) = (((2
ยท ๐ฅ) + (2 ยท
1)) โ 1)) |
37 | | adddi 11198 |
. . . . . . . . . . . . . . . . . . . 20
โข ((2
โ โ โง ๐ฅ
โ โ โง 1 โ โ) โ (2 ยท (๐ฅ + 1)) = ((2 ยท ๐ฅ) + (2 ยท 1))) |
38 | 13, 26, 37 | mp3an13 1452 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ (2
ยท (๐ฅ + 1)) = ((2
ยท ๐ฅ) + (2 ยท
1))) |
39 | 12, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (2
ยท (๐ฅ + 1)) = ((2
ยท ๐ฅ) + (2 ยท
1))) |
40 | 39 | oveq1d 7423 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ ((2
ยท (๐ฅ + 1)) โ
1) = (((2 ยท ๐ฅ) + (2
ยท 1)) โ 1)) |
41 | 36, 40 | eqtr4d 2775 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ ((2
ยท ๐ฅ) + 1) = ((2
ยท (๐ฅ + 1)) โ
1)) |
42 | 41 | negeqd 11453 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ -((2
ยท ๐ฅ) + 1) = -((2
ยท (๐ฅ + 1)) โ
1)) |
43 | 8 | zcnd 12666 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ (๐ฅ + 1) โ
โ) |
44 | | mulneg2 11650 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โ โง (๐ฅ +
1) โ โ) โ (2 ยท -(๐ฅ + 1)) = -(2 ยท (๐ฅ + 1))) |
45 | 13, 43, 44 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (2
ยท -(๐ฅ + 1)) = -(2
ยท (๐ฅ +
1))) |
46 | 45 | oveq1d 7423 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ ((2
ยท -(๐ฅ + 1)) + 1) =
(-(2 ยท (๐ฅ + 1)) +
1)) |
47 | | mulcl 11193 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โ โง (๐ฅ +
1) โ โ) โ (2 ยท (๐ฅ + 1)) โ โ) |
48 | 13, 43, 47 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โค โ (2
ยท (๐ฅ + 1)) โ
โ) |
49 | | negsubdi 11515 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท (๐ฅ + 1)) โ
โ โง 1 โ โ) โ -((2 ยท (๐ฅ + 1)) โ 1) = (-(2 ยท (๐ฅ + 1)) + 1)) |
50 | 48, 26, 49 | sylancl 586 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โค โ -((2
ยท (๐ฅ + 1)) โ
1) = (-(2 ยท (๐ฅ + 1))
+ 1)) |
51 | 46, 50 | eqtr4d 2775 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ ((2
ยท -(๐ฅ + 1)) + 1) =
-((2 ยท (๐ฅ + 1))
โ 1)) |
52 | 42, 51 | eqtr4d 2775 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โค โ -((2
ยท ๐ฅ) + 1) = ((2
ยท -(๐ฅ + 1)) +
1)) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ฅ โ โค) โ -((2
ยท ๐ฅ) + 1) = ((2
ยท -(๐ฅ + 1)) +
1)) |
54 | 53 | eqeq1d 2734 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฅ โ โค) โ (-((2
ยท ๐ฅ) + 1) = ๐ โ ((2 ยท -(๐ฅ + 1)) + 1) = ๐)) |
55 | 24, 54 | bitrid 282 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฅ โ โค) โ (๐ = -((2 ยท ๐ฅ) + 1) โ ((2 ยท
-(๐ฅ + 1)) + 1) = ๐)) |
56 | 23, 55 | bitrd 278 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฅ โ โค) โ (((2
ยท ๐ฅ) + 1) = -๐ โ ((2 ยท -(๐ฅ + 1)) + 1) = ๐)) |
57 | 56 | biimpa 477 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ฅ โ โค) โง ((2
ยท ๐ฅ) + 1) = -๐) โ ((2 ยท -(๐ฅ + 1)) + 1) = ๐) |
58 | | oveq2 7416 |
. . . . . . . . . . . 12
โข (๐ = -(๐ฅ + 1) โ (2 ยท ๐) = (2 ยท -(๐ฅ + 1))) |
59 | 58 | oveq1d 7423 |
. . . . . . . . . . 11
โข (๐ = -(๐ฅ + 1) โ ((2 ยท ๐) + 1) = ((2 ยท -(๐ฅ + 1)) + 1)) |
60 | 59 | eqeq1d 2734 |
. . . . . . . . . 10
โข (๐ = -(๐ฅ + 1) โ (((2 ยท ๐) + 1) = ๐ โ ((2 ยท -(๐ฅ + 1)) + 1) = ๐)) |
61 | 60 | rspcev 3612 |
. . . . . . . . 9
โข ((-(๐ฅ + 1) โ โค โง ((2
ยท -(๐ฅ + 1)) + 1) =
๐) โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐) |
62 | 11, 57, 61 | syl2anc 584 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ฅ โ โค) โง ((2
ยท ๐ฅ) + 1) = -๐) โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐) |
63 | 62 | rexlimdva2 3157 |
. . . . . . 7
โข (๐ โ โ โ
(โ๐ฅ โ โค
((2 ยท ๐ฅ) + 1) =
-๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
64 | | znegcl 12596 |
. . . . . . . . . 10
โข (๐ฆ โ โค โ -๐ฆ โ
โค) |
65 | 64 | ad2antlr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ฆ โ โค) โง (๐ฆ ยท 2) = -๐) โ -๐ฆ โ โค) |
66 | | zcn 12562 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
67 | | mulcl 11193 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง 2 โ
โ) โ (๐ฆ ยท
2) โ โ) |
68 | 66, 13, 67 | sylancl 586 |
. . . . . . . . . . . 12
โข (๐ฆ โ โค โ (๐ฆ ยท 2) โ
โ) |
69 | | recn 11199 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
70 | | negcon2 11512 |
. . . . . . . . . . . 12
โข (((๐ฆ ยท 2) โ โ
โง ๐ โ โ)
โ ((๐ฆ ยท 2) =
-๐ โ ๐ = -(๐ฆ ยท 2))) |
71 | 68, 69, 70 | syl2anr 597 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฆ โ โค) โ ((๐ฆ ยท 2) = -๐ โ ๐ = -(๐ฆ ยท 2))) |
72 | | eqcom 2739 |
. . . . . . . . . . . 12
โข (๐ = -(๐ฆ ยท 2) โ -(๐ฆ ยท 2) = ๐) |
73 | | mulneg1 11649 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง 2 โ
โ) โ (-๐ฆ
ยท 2) = -(๐ฆ ยท
2)) |
74 | 66, 13, 73 | sylancl 586 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โค โ (-๐ฆ ยท 2) = -(๐ฆ ยท 2)) |
75 | 74 | adantl 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ฆ โ โค) โ (-๐ฆ ยท 2) = -(๐ฆ ยท 2)) |
76 | 75 | eqeq1d 2734 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ฆ โ โค) โ ((-๐ฆ ยท 2) = ๐ โ -(๐ฆ ยท 2) = ๐)) |
77 | 72, 76 | bitr4id 289 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฆ โ โค) โ (๐ = -(๐ฆ ยท 2) โ (-๐ฆ ยท 2) = ๐)) |
78 | 71, 77 | bitrd 278 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ฆ โ โค) โ ((๐ฆ ยท 2) = -๐ โ (-๐ฆ ยท 2) = ๐)) |
79 | 78 | biimpa 477 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ฆ โ โค) โง (๐ฆ ยท 2) = -๐) โ (-๐ฆ ยท 2) = ๐) |
80 | | oveq1 7415 |
. . . . . . . . . . 11
โข (๐ = -๐ฆ โ (๐ ยท 2) = (-๐ฆ ยท 2)) |
81 | 80 | eqeq1d 2734 |
. . . . . . . . . 10
โข (๐ = -๐ฆ โ ((๐ ยท 2) = ๐ โ (-๐ฆ ยท 2) = ๐)) |
82 | 81 | rspcev 3612 |
. . . . . . . . 9
โข ((-๐ฆ โ โค โง (-๐ฆ ยท 2) = ๐) โ โ๐ โ โค (๐ ยท 2) = ๐) |
83 | 65, 79, 82 | syl2anc 584 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ฆ โ โค) โง (๐ฆ ยท 2) = -๐) โ โ๐ โ โค (๐ ยท 2) = ๐) |
84 | 83 | rexlimdva2 3157 |
. . . . . . 7
โข (๐ โ โ โ
(โ๐ฆ โ โค
(๐ฆ ยท 2) = -๐ โ โ๐ โ โค (๐ ยท 2) = ๐)) |
85 | 63, 84 | orim12d 963 |
. . . . . 6
โข (๐ โ โ โ
((โ๐ฅ โ โค
((2 ยท ๐ฅ) + 1) =
-๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = -๐) โ (โ๐ โ โค ((2 ยท
๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐))) |
86 | | odd2np1lem 16282 |
. . . . . 6
โข (-๐ โ โ0
โ (โ๐ฅ โ
โค ((2 ยท ๐ฅ) +
1) = -๐ โจ โ๐ฆ โ โค (๐ฆ ยท 2) = -๐)) |
87 | 85, 86 | impel 506 |
. . . . 5
โข ((๐ โ โ โง -๐ โ โ0)
โ (โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |
88 | 7, 87 | jaodan 956 |
. . . 4
โข ((๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0)) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |
89 | 5, 88 | sylbi 216 |
. . 3
โข (๐ โ โค โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) |
90 | | halfnz 12639 |
. . . 4
โข ยฌ (1
/ 2) โ โค |
91 | | reeanv 3226 |
. . . . 5
โข
(โ๐ โ
โค โ๐ โ
โค (((2 ยท ๐) +
1) = ๐ โง (๐ ยท 2) = ๐) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โง โ๐ โ โค (๐ ยท 2) = ๐)) |
92 | | eqtr3 2758 |
. . . . . . 7
โข ((((2
ยท ๐) + 1) = ๐ โง (๐ ยท 2) = ๐) โ ((2 ยท ๐) + 1) = (๐ ยท 2)) |
93 | | zcn 12562 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
94 | | mulcom 11195 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 2 โ
โ) โ (๐ ยท
2) = (2 ยท ๐)) |
95 | 93, 13, 94 | sylancl 586 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ ยท 2) = (2 ยท ๐)) |
96 | 95 | eqeq2d 2743 |
. . . . . . . . 9
โข (๐ โ โค โ (((2
ยท ๐) + 1) = (๐ ยท 2) โ ((2 ยท
๐) + 1) = (2 ยท ๐))) |
97 | 96 | adantl 482 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = (๐ ยท 2) โ ((2 ยท
๐) + 1) = (2 ยท ๐))) |
98 | | mulcl 11193 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
99 | 13, 93, 98 | sylancr 587 |
. . . . . . . . . 10
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
100 | | zcn 12562 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
101 | | mulcl 11193 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
102 | 13, 100, 101 | sylancr 587 |
. . . . . . . . . 10
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
103 | | subadd 11462 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
โ โง 1 โ โ) โ (((2 ยท ๐) โ (2 ยท ๐)) = 1 โ ((2 ยท ๐) + 1) = (2 ยท ๐))) |
104 | 26, 103 | mp3an3 1450 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
โ) โ (((2 ยท ๐) โ (2 ยท ๐)) = 1 โ ((2 ยท ๐) + 1) = (2 ยท ๐))) |
105 | 99, 102, 104 | syl2anr 597 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) โ (2
ยท ๐)) = 1 โ ((2
ยท ๐) + 1) = (2
ยท ๐))) |
106 | | subcl 11458 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ ๐) โ โ) |
107 | | 2cnne0 12421 |
. . . . . . . . . . . . . . 15
โข (2 โ
โ โง 2 โ 0) |
108 | | eqcom 2739 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ๐) = (1 / 2) โ (1 / 2) = (๐ โ ๐)) |
109 | | divmul 11874 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง (๐
โ ๐) โ โ
โง (2 โ โ โง 2 โ 0)) โ ((1 / 2) = (๐ โ ๐) โ (2 ยท (๐ โ ๐)) = 1)) |
110 | 108, 109 | bitrid 282 |
. . . . . . . . . . . . . . 15
โข ((1
โ โ โง (๐
โ ๐) โ โ
โง (2 โ โ โง 2 โ 0)) โ ((๐ โ ๐) = (1 / 2) โ (2 ยท (๐ โ ๐)) = 1)) |
111 | 26, 107, 110 | mp3an13 1452 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐) โ โ โ ((๐ โ ๐) = (1 / 2) โ (2 ยท (๐ โ ๐)) = 1)) |
112 | 106, 111 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ ๐) = (1 / 2) โ (2 ยท (๐ โ ๐)) = 1)) |
113 | 112 | ancoms 459 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ ๐) = (1 / 2) โ (2 ยท (๐ โ ๐)) = 1)) |
114 | | subdi 11646 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ โง ๐
โ โ โง ๐
โ โ) โ (2 ยท (๐ โ ๐)) = ((2 ยท ๐) โ (2 ยท ๐))) |
115 | 13, 114 | mp3an1 1448 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท (๐ โ ๐)) = ((2 ยท ๐) โ (2 ยท ๐))) |
116 | 115 | ancoms 459 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท (๐ โ ๐)) = ((2 ยท ๐) โ (2 ยท ๐))) |
117 | 116 | eqeq1d 2734 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ ((2
ยท (๐ โ ๐)) = 1 โ ((2 ยท ๐) โ (2 ยท ๐)) = 1)) |
118 | 113, 117 | bitrd 278 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ ๐) = (1 / 2) โ ((2 ยท ๐) โ (2 ยท ๐)) = 1)) |
119 | 100, 93, 118 | syl2an 596 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โ ๐) = (1 / 2) โ ((2 ยท ๐) โ (2 ยท ๐)) = 1)) |
120 | | zsubcl 12603 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ ๐) โ โค) |
121 | | eleq1 2821 |
. . . . . . . . . . . 12
โข ((๐ โ ๐) = (1 / 2) โ ((๐ โ ๐) โ โค โ (1 / 2) โ
โค)) |
122 | 120, 121 | syl5ibcom 244 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โ ๐) = (1 / 2) โ (1 / 2) โ
โค)) |
123 | 122 | ancoms 459 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ โ ๐) = (1 / 2) โ (1 / 2) โ
โค)) |
124 | 119, 123 | sylbird 259 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) โ (2
ยท ๐)) = 1 โ (1
/ 2) โ โค)) |
125 | 105, 124 | sylbird 259 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = (2
ยท ๐) โ (1 / 2)
โ โค)) |
126 | 97, 125 | sylbid 239 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) = (๐ ยท 2) โ (1 / 2)
โ โค)) |
127 | 92, 126 | syl5 34 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ ((((2
ยท ๐) + 1) = ๐ โง (๐ ยท 2) = ๐) โ (1 / 2) โ
โค)) |
128 | 127 | rexlimivv 3199 |
. . . . 5
โข
(โ๐ โ
โค โ๐ โ
โค (((2 ยท ๐) +
1) = ๐ โง (๐ ยท 2) = ๐) โ (1 / 2) โ
โค) |
129 | 91, 128 | sylbir 234 |
. . . 4
โข
((โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โง โ๐ โ โค (๐ ยท 2) = ๐) โ (1 / 2) โ
โค) |
130 | 90, 129 | mto 196 |
. . 3
โข ยฌ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐ โง โ๐ โ โค (๐ ยท 2) = ๐) |
131 | | pm5.17 1010 |
. . . 4
โข
(((โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โง ยฌ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โง โ๐ โ โค (๐ ยท 2) = ๐)) โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โ ยฌ โ๐ โ โค (๐ ยท 2) = ๐)) |
132 | | bicom 221 |
. . . 4
โข
((โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โ ยฌ
โ๐ โ โค
(๐ ยท 2) = ๐) โ (ยฌ โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
133 | 131, 132 | bitri 274 |
. . 3
โข
(((โ๐ โ
โค ((2 ยท ๐) +
1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐) โง ยฌ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โง โ๐ โ โค (๐ ยท 2) = ๐)) โ (ยฌ โ๐ โ โค (๐ ยท 2) = ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
134 | 89, 130, 133 | sylanblc 589 |
. 2
โข (๐ โ โค โ (ยฌ
โ๐ โ โค
(๐ ยท 2) = ๐ โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
135 | 4, 134 | bitrd 278 |
1
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |