Step | Hyp | Ref
| Expression |
1 | | ablsimpgfindlem1.1 |
. . . 4
โข ๐ต = (Baseโ๐บ) |
2 | | ablsimpgfindlem1.2 |
. . . 4
โข 0 =
(0gโ๐บ) |
3 | | ablsimpgfindlem1.3 |
. . . 4
โข ยท =
(.gโ๐บ) |
4 | | ablsimpgfindlem1.5 |
. . . . 5
โข (๐ โ ๐บ โ Abel) |
5 | 4 | 3ad2ant1 1134 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ ๐บ โ Abel) |
6 | | ablsimpgfindlem1.6 |
. . . . 5
โข (๐ โ ๐บ โ SimpGrp) |
7 | 6 | 3ad2ant1 1134 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ ๐บ โ SimpGrp) |
8 | 6 | simpggrpd 19965 |
. . . . . 6
โข (๐ โ ๐บ โ Grp) |
9 | 8 | 3ad2ant1 1134 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ ๐บ โ Grp) |
10 | | 2z 12594 |
. . . . . 6
โข 2 โ
โค |
11 | 10 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ 2 โ
โค) |
12 | | simp2 1138 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ ๐ฅ โ ๐ต) |
13 | 1, 3, 9, 11, 12 | mulgcld 18976 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ (2 ยท ๐ฅ) โ ๐ต) |
14 | | simp3 1139 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ (2 ยท ๐ฅ) โ 0 ) |
15 | 14 | neneqd 2946 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ ยฌ (2 ยท ๐ฅ) = 0 ) |
16 | 1, 2, 3, 5, 7, 13,
15, 12 | ablsimpg1gend 19975 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ โ๐ฆ โ โค ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ))) |
17 | | simprr 772 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ))) |
18 | | simpl2 1193 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ๐ฅ โ ๐ต) |
19 | 1, 3 | mulg1 18961 |
. . . . . . 7
โข (๐ฅ โ ๐ต โ (1 ยท ๐ฅ) = ๐ฅ) |
20 | 18, 19 | syl 17 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ (1 ยท ๐ฅ) = ๐ฅ) |
21 | 9 | adantr 482 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ๐บ โ Grp) |
22 | | simprl 770 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ๐ฆ โ โค) |
23 | 10 | a1i 11 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ 2 โ
โค) |
24 | 1, 3 | mulgassr 18992 |
. . . . . . 7
โข ((๐บ โ Grp โง (๐ฆ โ โค โง 2 โ
โค โง ๐ฅ โ
๐ต)) โ ((2 ยท
๐ฆ) ยท ๐ฅ) = (๐ฆ ยท (2 ยท ๐ฅ))) |
25 | 21, 22, 23, 18, 24 | syl13anc 1373 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ((2 ยท ๐ฆ) ยท ๐ฅ) = (๐ฆ ยท (2 ยท ๐ฅ))) |
26 | 17, 20, 25 | 3eqtr4rd 2784 |
. . . . 5
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ((2 ยท ๐ฆ) ยท ๐ฅ) = (1 ยท ๐ฅ)) |
27 | 23, 22 | zmulcld 12672 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ (2 ยท ๐ฆ) โ
โค) |
28 | | 1zzd 12593 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ 1 โ
โค) |
29 | | ablsimpgfindlem1.4 |
. . . . . . 7
โข ๐ = (odโ๐บ) |
30 | 1, 29, 3, 2 | odcong 19417 |
. . . . . 6
โข ((๐บ โ Grp โง ๐ฅ โ ๐ต โง ((2 ยท ๐ฆ) โ โค โง 1 โ โค))
โ ((๐โ๐ฅ) โฅ ((2 ยท ๐ฆ) โ 1) โ ((2 ยท
๐ฆ) ยท ๐ฅ) = (1 ยท ๐ฅ))) |
31 | 21, 18, 27, 28, 30 | syl112anc 1375 |
. . . . 5
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ((๐โ๐ฅ) โฅ ((2 ยท ๐ฆ) โ 1) โ ((2 ยท ๐ฆ) ยท ๐ฅ) = (1 ยท ๐ฅ))) |
32 | 26, 31 | mpbird 257 |
. . . 4
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ (๐โ๐ฅ) โฅ ((2 ยท ๐ฆ) โ 1)) |
33 | | 0zd 12570 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ 0 โ
โค) |
34 | | zneo 12645 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง 0 โ
โค) โ (2 ยท ๐ฆ) โ ((2 ยท 0) + 1)) |
35 | | 2t0e0 12381 |
. . . . . . . . . . . 12
โข (2
ยท 0) = 0 |
36 | 35 | oveq1i 7419 |
. . . . . . . . . . 11
โข ((2
ยท 0) + 1) = (0 + 1) |
37 | | 0p1e1 12334 |
. . . . . . . . . . 11
โข (0 + 1) =
1 |
38 | 36, 37 | eqtri 2761 |
. . . . . . . . . 10
โข ((2
ยท 0) + 1) = 1 |
39 | 38 | a1i 11 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง 0 โ
โค) โ ((2 ยท 0) + 1) = 1) |
40 | 34, 39 | neeqtrd 3011 |
. . . . . . . 8
โข ((๐ฆ โ โค โง 0 โ
โค) โ (2 ยท ๐ฆ) โ 1) |
41 | | oveq1 7416 |
. . . . . . . . . . . . 13
โข (((2
ยท ๐ฆ) โ 1) = 0
โ (((2 ยท ๐ฆ)
โ 1) + 1) = (0 + 1)) |
42 | 41, 37 | eqtr2di 2790 |
. . . . . . . . . . . 12
โข (((2
ยท ๐ฆ) โ 1) = 0
โ 1 = (((2 ยท ๐ฆ)
โ 1) + 1)) |
43 | 42 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ฆ โ โค โง ((2
ยท ๐ฆ) โ 1) = 0)
โ 1 = (((2 ยท ๐ฆ)
โ 1) + 1)) |
44 | | 2cnd 12290 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โค โ 2 โ
โ) |
45 | | zcn 12563 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
46 | 44, 45 | mulcld 11234 |
. . . . . . . . . . . 12
โข (๐ฆ โ โค โ (2
ยท ๐ฆ) โ
โ) |
47 | | 1cnd 11209 |
. . . . . . . . . . . 12
โข (((2
ยท ๐ฆ) โ 1) = 0
โ 1 โ โ) |
48 | | npcan 11469 |
. . . . . . . . . . . 12
โข (((2
ยท ๐ฆ) โ โ
โง 1 โ โ) โ (((2 ยท ๐ฆ) โ 1) + 1) = (2 ยท ๐ฆ)) |
49 | 46, 47, 48 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ฆ โ โค โง ((2
ยท ๐ฆ) โ 1) = 0)
โ (((2 ยท ๐ฆ)
โ 1) + 1) = (2 ยท ๐ฆ)) |
50 | 43, 49 | eqtr2d 2774 |
. . . . . . . . . 10
โข ((๐ฆ โ โค โง ((2
ยท ๐ฆ) โ 1) = 0)
โ (2 ยท ๐ฆ) =
1) |
51 | 50 | ex 414 |
. . . . . . . . 9
โข (๐ฆ โ โค โ (((2
ยท ๐ฆ) โ 1) = 0
โ (2 ยท ๐ฆ) =
1)) |
52 | 51 | necon3ad 2954 |
. . . . . . . 8
โข (๐ฆ โ โค โ ((2
ยท ๐ฆ) โ 1 โ
ยฌ ((2 ยท ๐ฆ)
โ 1) = 0)) |
53 | 40, 52 | syl5 34 |
. . . . . . 7
โข (๐ฆ โ โค โ ((๐ฆ โ โค โง 0 โ
โค) โ ยฌ ((2 ยท ๐ฆ) โ 1) = 0)) |
54 | 53 | anabsi5 668 |
. . . . . 6
โข ((๐ฆ โ โค โง 0 โ
โค) โ ยฌ ((2 ยท ๐ฆ) โ 1) = 0) |
55 | 22, 33, 54 | syl2anc 585 |
. . . . 5
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ยฌ ((2 ยท
๐ฆ) โ 1) =
0) |
56 | 27, 28 | zsubcld 12671 |
. . . . . 6
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ((2 ยท ๐ฆ) โ 1) โ
โค) |
57 | | 0dvds 16220 |
. . . . . 6
โข (((2
ยท ๐ฆ) โ 1)
โ โค โ (0 โฅ ((2 ยท ๐ฆ) โ 1) โ ((2 ยท ๐ฆ) โ 1) =
0)) |
58 | 56, 57 | syl 17 |
. . . . 5
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ (0 โฅ ((2
ยท ๐ฆ) โ 1)
โ ((2 ยท ๐ฆ)
โ 1) = 0)) |
59 | 55, 58 | mtbird 325 |
. . . 4
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ ยฌ 0 โฅ ((2
ยท ๐ฆ) โ
1)) |
60 | | nbrne2 5169 |
. . . 4
โข (((๐โ๐ฅ) โฅ ((2 ยท ๐ฆ) โ 1) โง ยฌ 0 โฅ ((2
ยท ๐ฆ) โ 1))
โ (๐โ๐ฅ) โ 0) |
61 | 32, 59, 60 | syl2anc 585 |
. . 3
โข (((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โง (๐ฆ โ โค โง ๐ฅ = (๐ฆ ยท (2 ยท ๐ฅ)))) โ (๐โ๐ฅ) โ 0) |
62 | 16, 61 | rexlimddv 3162 |
. 2
โข ((๐ โง ๐ฅ โ ๐ต โง (2 ยท ๐ฅ) โ 0 ) โ (๐โ๐ฅ) โ 0) |
63 | 62 | 3expa 1119 |
1
โข (((๐ โง ๐ฅ โ ๐ต) โง (2 ยท ๐ฅ) โ 0 ) โ (๐โ๐ฅ) โ 0) |