Step | Hyp | Ref
| Expression |
1 | | 2cnd 12238 |
. . . . . . . . . 10
โข (๐ โ โ โ 2 โ
โ) |
2 | | nnnn0 12427 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
3 | 1, 2 | expcld 14058 |
. . . . . . . . 9
โข (๐ โ โ โ
(2โ๐) โ
โ) |
4 | 3 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
5 | | 1cnd 11157 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ 1 โ โ) |
6 | | eldifi 4091 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
7 | | prmnn 16557 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
8 | | nncn 12168 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
10 | 9 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ) |
11 | | nnnn0 12427 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
12 | 11 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ0) |
13 | 10, 12 | expcld 14058 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐โ๐) โ
โ) |
14 | 4, 5, 13 | 3jca 1129 |
. . . . . . 7
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((2โ๐) โ
โ โง 1 โ โ โง (๐โ๐) โ โ)) |
15 | 14 | adantr 482 |
. . . . . 6
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ ((2โ๐) โ
โ โง 1 โ โ โง (๐โ๐) โ โ)) |
16 | | subadd2 11412 |
. . . . . 6
โข
(((2โ๐) โ
โ โง 1 โ โ โง (๐โ๐) โ โ) โ (((2โ๐) โ 1) = (๐โ๐) โ ((๐โ๐) + 1) = (2โ๐))) |
17 | 15, 16 | syl 17 |
. . . . 5
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (((2โ๐) โ
1) = (๐โ๐) โ ((๐โ๐) + 1) = (2โ๐))) |
18 | 10 | adantr 482 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ ๐ โ
โ) |
19 | | simpl2 1193 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ ๐ โ
โ) |
20 | | simpr 486 |
. . . . . . . 8
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ ยฌ 2 โฅ ๐) |
21 | 18, 19, 20 | oddpwp1fsum 16281 |
. . . . . . 7
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ ((๐โ๐) + 1) = ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)))) |
22 | 21 | eqeq1d 2739 |
. . . . . 6
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (((๐โ๐) + 1) = (2โ๐) โ ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐))) |
23 | | peano2nn 12172 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ + 1) โ
โ) |
24 | 23 | nnzd 12533 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ + 1) โ
โค) |
25 | 6, 7, 24 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ (๐ + 1) โ
โค) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ + 1) โ
โค) |
27 | | fzfid 13885 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (0...(๐ โ 1))
โ Fin) |
28 | | neg1z 12546 |
. . . . . . . . . . . . . . 15
โข -1 โ
โค |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ -1 โ โค) |
30 | | elfznn0 13541 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
31 | | zexpcl 13989 |
. . . . . . . . . . . . . 14
โข ((-1
โ โค โง ๐
โ โ0) โ (-1โ๐) โ โค) |
32 | 29, 30, 31 | syl2an 597 |
. . . . . . . . . . . . 13
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ
(-1โ๐) โ
โค) |
33 | | nnz 12527 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โค) |
34 | 6, 7, 33 | 3syl 18 |
. . . . . . . . . . . . . . 15
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โค) |
36 | | zexpcl 13989 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ๐ โ โ0)
โ (๐โ๐) โ
โค) |
37 | 35, 30, 36 | syl2an 597 |
. . . . . . . . . . . . 13
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) โ โค) |
38 | 32, 37 | zmulcld 12620 |
. . . . . . . . . . . 12
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ
((-1โ๐) ยท
(๐โ๐)) โ โค) |
39 | 27, 38 | fsumzcl 15627 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โ โค) |
40 | 26, 39 | jca 513 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((๐ + 1) โ
โค โง ฮฃ๐
โ (0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โ โค)) |
41 | 40 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โง ((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐)) โ ((๐ + 1) โ โค โง ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ โค)) |
42 | | dvdsmul2 16168 |
. . . . . . . . 9
โข (((๐ + 1) โ โค โง
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ โค) โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)))) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โง ((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐)) โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)))) |
44 | | breq2 5114 |
. . . . . . . . . 10
โข (((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐) โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ (2โ๐))) |
45 | 44 | adantl 483 |
. . . . . . . . 9
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โง ((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐)) โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ (2โ๐))) |
46 | | 2a1 28 |
. . . . . . . . . . 11
โข (๐ = 1 โ (((๐ โ (โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง ยฌ 2
โฅ ๐) โ
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ ๐ = 1))) |
47 | | 2prm 16575 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โ |
48 | | prmuz2 16579 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
49 | 6, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ ๐ โ
(โคโฅโ2)) |
50 | 49 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
(โคโฅโ2)) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
๐ โ
(โคโฅโ2)) |
52 | | df-ne 2945 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 1 โ ยฌ ๐ = 1) |
53 | | eluz2b3 12854 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ
(โคโฅโ2) โ (๐ โ โ โง ๐ โ 1)) |
54 | 53 | simplbi2 502 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ โ 1 โ ๐ โ
(โคโฅโ2))) |
55 | 52, 54 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (ยฌ
๐ = 1 โ ๐ โ
(โคโฅโ2))) |
56 | 55 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (ยฌ ๐ = 1 โ
๐ โ
(โคโฅโ2))) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
โข (ยฌ
๐ = 1 โ ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
(โคโฅโ2))) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((ยฌ
๐ = 1 โง ยฌ 2 โฅ
๐) โ ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
(โคโฅโ2))) |
59 | 58 | impcom 409 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
๐ โ
(โคโฅโ2)) |
60 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
ยฌ 2 โฅ ๐) |
61 | | lighneallem4b 45875 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ
(โคโฅโ2) โง ๐ โ (โคโฅโ2)
โง ยฌ 2 โฅ ๐)
โ ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โ
(โคโฅโ2)) |
62 | 51, 59, 60, 61 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ
(โคโฅโ2)) |
63 | 2 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ โ
โ0) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
๐ โ
โ0) |
65 | | dvdsprmpweqnn 16764 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ โง ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ (โคโฅโ2)
โง ๐ โ
โ0) โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ (2โ๐) โ โ๐ โ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) = (2โ๐))) |
66 | 47, 62, 64, 65 | mp3an2i 1467 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ โ๐ โ โ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) = (2โ๐))) |
67 | | 2z 12542 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โค |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
2 โ โค) |
69 | | iddvdsexp 16169 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โค โง ๐
โ โ) โ 2 โฅ (2โ๐)) |
70 | 68, 69 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ 2
โฅ (2โ๐)) |
71 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . 20
โข
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) = (2โ๐) โ (2 โฅ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ 2 โฅ (2โ๐))) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง (ยฌ ๐ = 1 โง ยฌ 2 โฅ ๐)) โง ๐ โ โ) โง ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) = (2โ๐)) โ (2 โฅ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ 2 โฅ (2โ๐))) |
73 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
(0...(๐ โ 1)) โ
Fin) |
74 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ -1 โ
โค) |
75 | 74, 31 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง ๐ โ โ0)
โ (-1โ๐) โ
โค) |
76 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ ๐ โ
โ0) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ0) |
78 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ0) |
79 | 77, 78 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ0) |
80 | 79 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โค) |
81 | 75, 80 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ โ โง ๐ โ โ0)
โ ((-1โ๐)
ยท (๐โ๐)) โ
โค) |
82 | 81 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ (๐ โ โ0
โ ((-1โ๐)
ยท (๐โ๐)) โ
โค)) |
83 | 6, 7, 82 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (โ โ {2})
โ (๐ โ
โ0 โ ((-1โ๐) ยท (๐โ๐)) โ โค)) |
84 | 83 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โ
โ0 โ ((-1โ๐) ยท (๐โ๐)) โ โค)) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
(๐ โ
โ0 โ ((-1โ๐) ยท (๐โ๐)) โ โค)) |
86 | 85, 30 | impel 507 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง (ยฌ ๐ = 1 โง ยฌ 2 โฅ ๐)) โง ๐ โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((-1โ๐) ยท (๐โ๐)) โ โค) |
87 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ0
โ ๐ โ
โค) |
88 | | m1expcl2 13998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โค โ
(-1โ๐) โ {-1,
1}) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ0
โ (-1โ๐) โ
{-1, 1}) |
90 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข
(-1โ๐) โ
V |
91 | 90 | elpr 4614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
((-1โ๐) โ
{-1, 1} โ ((-1โ๐)
= -1 โจ (-1โ๐) =
1)) |
92 | | n2dvdsm1 16258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ยฌ 2
โฅ -1 |
93 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
((-1โ๐) = -1
โ (2 โฅ (-1โ๐) โ 2 โฅ -1)) |
94 | 92, 93 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข
((-1โ๐) = -1
โ ยฌ 2 โฅ (-1โ๐)) |
95 | | n2dvds1 16257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ยฌ 2
โฅ 1 |
96 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข
((-1โ๐) = 1
โ (2 โฅ (-1โ๐) โ 2 โฅ 1)) |
97 | 95, 96 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข
((-1โ๐) = 1
โ ยฌ 2 โฅ (-1โ๐)) |
98 | 94, 97 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข
(((-1โ๐) = -1
โจ (-1โ๐) = 1)
โ ยฌ 2 โฅ (-1โ๐)) |
99 | 98 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข
(((-1โ๐) = -1
โจ (-1โ๐) = 1)
โ (๐ โ
โ0 โ ยฌ 2 โฅ (-1โ๐))) |
100 | 91, 99 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
((-1โ๐) โ
{-1, 1} โ (๐ โ
โ0 โ ยฌ 2 โฅ (-1โ๐))) |
101 | 89, 100 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ0
โ ยฌ 2 โฅ (-1โ๐)) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ ยฌ 2 โฅ (-1โ๐)) |
103 | | elnn0 12422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
104 | | oddn2prm 16691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ (โ โ {2})
โ ยฌ 2 โฅ ๐) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ยฌ 2 โฅ ๐) |
106 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ) |
107 | | prmdvdsexp 16598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((2
โ โ โง ๐
โ โค โง ๐
โ โ) โ (2 โฅ (๐โ๐) โ 2 โฅ ๐)) |
108 | 47, 34, 106, 107 | mp3an2ani 1469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2 โฅ (๐โ๐) โ 2 โฅ ๐)) |
109 | 105, 108 | mtbird 325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ยฌ 2 โฅ (๐โ๐)) |
110 | 109 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ (๐ โ (โ โ {2})
โ ยฌ 2 โฅ (๐โ๐))) |
111 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข (๐ = 0 โ (๐โ๐) = (๐โ0)) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ (๐โ๐) = (๐โ0)) |
113 | 9 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ ๐ โ
โ) |
114 | 113 | exp0d 14052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ (๐โ0) = 1) |
115 | 112, 114 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ (๐โ๐) = 1) |
116 | 115 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ (2
โฅ (๐โ๐) โ 2 โฅ
1)) |
117 | 95, 116 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ = 0 โง ๐ โ (โ โ {2})) โ ยฌ
2 โฅ (๐โ๐)) |
118 | 117 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ = 0 โ (๐ โ (โ โ {2}) โ ยฌ 2
โฅ (๐โ๐))) |
119 | 110, 118 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โจ ๐ = 0) โ (๐ โ (โ โ {2}) โ ยฌ 2
โฅ (๐โ๐))) |
120 | 103, 119 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ0
โ (๐ โ (โ
โ {2}) โ ยฌ 2 โฅ (๐โ๐))) |
121 | 120 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ ยฌ 2 โฅ (๐โ๐)) |
122 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (ยฌ (2
โฅ (-1โ๐) โจ 2
โฅ (๐โ๐)) โ (ยฌ 2 โฅ
(-1โ๐) โง ยฌ 2
โฅ (๐โ๐))) |
123 | 102, 121,
122 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ ยฌ (2 โฅ (-1โ๐) โจ 2 โฅ (๐โ๐))) |
124 | 28, 31 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ0
โ (-1โ๐) โ
โค) |
125 | 124 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ (-1โ๐) โ โค) |
126 | 6, 7, 76 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ (โ โ {2})
โ ๐ โ
โ0) |
127 | 126 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ ๐ โ
โ0) |
128 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ ๐ โ โ0) |
129 | 127, 128 | nn0expcld 14156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ (๐โ๐) โ
โ0) |
130 | 129 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ (๐โ๐) โ โค) |
131 | | euclemma 16596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((2
โ โ โง (-1โ๐) โ โค โง (๐โ๐) โ โค) โ (2 โฅ
((-1โ๐) ยท
(๐โ๐)) โ (2 โฅ (-1โ๐) โจ 2 โฅ (๐โ๐)))) |
132 | 47, 125, 130, 131 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ (2 โฅ ((-1โ๐) ยท (๐โ๐)) โ (2 โฅ (-1โ๐) โจ 2 โฅ (๐โ๐)))) |
133 | 123, 132 | mtbird 325 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ (โ โ {2})
โง ๐ โ
โ0) โ ยฌ 2 โฅ ((-1โ๐) ยท (๐โ๐))) |
134 | 133 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (โ โ {2})
โ (๐ โ
โ0 โ ยฌ 2 โฅ ((-1โ๐) ยท (๐โ๐)))) |
135 | 134 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ โ
โ0 โ ยฌ 2 โฅ ((-1โ๐) ยท (๐โ๐)))) |
136 | 135 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
(๐ โ
โ0 โ ยฌ 2 โฅ ((-1โ๐) ยท (๐โ๐)))) |
137 | 136, 30 | impel 507 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง (ยฌ ๐ = 1 โง ยฌ 2 โฅ ๐)) โง ๐ โ โ) โง ๐ โ (0...(๐ โ 1))) โ ยฌ 2 โฅ
((-1โ๐) ยท
(๐โ๐))) |
138 | | nnm1nn0 12461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
139 | | hashfz0 14339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ 1) โ
โ0 โ (โฏโ(0...(๐ โ 1))) = ((๐ โ 1) + 1)) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ
(โฏโ(0...(๐
โ 1))) = ((๐ โ
1) + 1)) |
141 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ ๐ โ
โ) |
142 | | npcan1 11587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ โ โ ((๐ โ 1) + 1) = ๐) |
144 | 140, 143 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ ๐ = (โฏโ(0...(๐ โ 1)))) |
145 | 144 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ๐ =
(โฏโ(0...(๐
โ 1)))) |
146 | 145 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
๐ =
(โฏโ(0...(๐
โ 1)))) |
147 | 146 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(2 โฅ ๐ โ 2
โฅ (โฏโ(0...(๐ โ 1))))) |
148 | 147 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(ยฌ 2 โฅ ๐ โ
ยฌ 2 โฅ (โฏโ(0...(๐ โ 1))))) |
149 | 148 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ ๐ = 1) โ
(ยฌ 2 โฅ ๐ โ
ยฌ 2 โฅ (โฏโ(0...(๐ โ 1))))) |
150 | 149 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
ยฌ 2 โฅ (โฏโ(0...(๐ โ 1)))) |
151 | 150 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
ยฌ 2 โฅ (โฏโ(0...(๐ โ 1)))) |
152 | 73, 86, 137, 151 | oddsumodd 16279 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
ยฌ 2 โฅ ฮฃ๐
โ (0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐))) |
153 | 152 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ (2
โฅ ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โ ๐ = 1)) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง (ยฌ ๐ = 1 โง ยฌ 2 โฅ ๐)) โง ๐ โ โ) โง ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) = (2โ๐)) โ (2 โฅ ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โ ๐ = 1)) |
155 | 72, 154 | sylbird 260 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โ
(โ โ {2}) โง ๐ โ โ โง ๐ โ โ) โง (ยฌ ๐ = 1 โง ยฌ 2 โฅ ๐)) โง ๐ โ โ) โง ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) = (2โ๐)) โ (2 โฅ (2โ๐) โ ๐ = 1)) |
156 | 155 | ex 414 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) = (2โ๐) โ (2 โฅ (2โ๐) โ ๐ = 1))) |
157 | 70, 156 | mpid 44 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โง
๐ โ โ) โ
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) = (2โ๐) โ ๐ = 1)) |
158 | 157 | rexlimdva 3153 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
(โ๐ โ โ
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) = (2โ๐) โ ๐ = 1)) |
159 | 66, 158 | syld 47 |
. . . . . . . . . . . . . 14
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ ๐ = 1 โง
ยฌ 2 โฅ ๐)) โ
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ ๐ = 1)) |
160 | 159 | exp32 422 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (ยฌ ๐ = 1 โ
(ยฌ 2 โฅ ๐ โ
(ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ ๐ = 1)))) |
161 | 160 | com12 32 |
. . . . . . . . . . . 12
โข (ยฌ
๐ = 1 โ ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (ยฌ 2 โฅ ๐
โ (ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ ๐ = 1)))) |
162 | 161 | impd 412 |
. . . . . . . . . . 11
โข (ยฌ
๐ = 1 โ (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ ๐ = 1))) |
163 | 46, 162 | pm2.61i 182 |
. . . . . . . . . 10
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (ฮฃ๐ โ
(0...(๐ โ
1))((-1โ๐) ยท
(๐โ๐)) โฅ (2โ๐) โ ๐ = 1)) |
164 | 163 | adantr 482 |
. . . . . . . . 9
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โง ((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐)) โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ (2โ๐) โ ๐ = 1)) |
165 | 45, 164 | sylbid 239 |
. . . . . . . 8
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โง ((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐)) โ (ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐)) โฅ ((๐ + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) โ ๐ = 1)) |
166 | 43, 165 | mpd 15 |
. . . . . . 7
โข ((((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โง ((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐)) โ ๐ = 1) |
167 | 166 | ex 414 |
. . . . . 6
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (((๐ + 1) ยท
ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐โ๐))) = (2โ๐) โ ๐ = 1)) |
168 | 22, 167 | sylbid 239 |
. . . . 5
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (((๐โ๐) + 1) = (2โ๐) โ ๐ = 1)) |
169 | 17, 168 | sylbid 239 |
. . . 4
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง ยฌ 2 โฅ ๐)
โ (((2โ๐) โ
1) = (๐โ๐) โ ๐ = 1)) |
170 | 169 | ex 414 |
. . 3
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ (ยฌ 2 โฅ ๐
โ (((2โ๐) โ
1) = (๐โ๐) โ ๐ = 1))) |
171 | 170 | adantld 492 |
. 2
โข ((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โ ((ยฌ 2 โฅ ๐
โง ยฌ 2 โฅ ๐)
โ (((2โ๐) โ
1) = (๐โ๐) โ ๐ = 1))) |
172 | 171 | 3imp 1112 |
1
โข (((๐ โ (โ โ {2})
โง ๐ โ โ
โง ๐ โ โ)
โง (ยฌ 2 โฅ ๐
โง ยฌ 2 โฅ ๐)
โง ((2โ๐) โ
1) = (๐โ๐)) โ ๐ = 1) |