Step | Hyp | Ref
| Expression |
1 | | 8nn 12249 |
. . . . . 6
โข 8 โ
โ |
2 | | nnrp 12927 |
. . . . . 6
โข (8 โ
โ โ 8 โ โ+) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
โข 8 โ
โ+ |
4 | | eqcom 2744 |
. . . . . 6
โข (๐
= (๐ mod 8) โ (๐ mod 8) = ๐
) |
5 | | modmuladdim 13820 |
. . . . . 6
โข ((๐ โ โค โง 8 โ
โ+) โ ((๐ mod 8) = ๐
โ โ๐ โ โค ๐ = ((๐ ยท 8) + ๐
))) |
6 | 4, 5 | biimtrid 241 |
. . . . 5
โข ((๐ โ โค โง 8 โ
โ+) โ (๐
= (๐ mod 8) โ โ๐ โ โค ๐ = ((๐ ยท 8) + ๐
))) |
7 | 3, 6 | mpan2 690 |
. . . 4
โข (๐ โ โค โ (๐
= (๐ mod 8) โ โ๐ โ โค ๐ = ((๐ ยท 8) + ๐
))) |
8 | 7 | imp 408 |
. . 3
โข ((๐ โ โค โง ๐
= (๐ mod 8)) โ โ๐ โ โค ๐ = ((๐ ยท 8) + ๐
)) |
9 | 8 | 3adant2 1132 |
. 2
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ โ๐ โ โค ๐ = ((๐ ยท 8) + ๐
)) |
10 | | zcn 12505 |
. . . . . . . 8
โข (๐ โ โค โ ๐ โ
โ) |
11 | | 8cn 12251 |
. . . . . . . . 9
โข 8 โ
โ |
12 | 11 | a1i 11 |
. . . . . . . 8
โข (๐ โ โค โ 8 โ
โ) |
13 | 10, 12 | mulcomd 11177 |
. . . . . . 7
โข (๐ โ โค โ (๐ ยท 8) = (8 ยท ๐)) |
14 | 13 | adantl 483 |
. . . . . 6
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ (๐ ยท 8) = (8 ยท ๐)) |
15 | 14 | oveq1d 7373 |
. . . . 5
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ ((๐ ยท 8) + ๐
) = ((8 ยท ๐) + ๐
)) |
16 | 15 | eqeq2d 2748 |
. . . 4
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ (๐ = ((๐ ยท 8) + ๐
) โ ๐ = ((8 ยท ๐) + ๐
))) |
17 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ ๐ โ โค) |
18 | 17 | adantr 482 |
. . . . . . . 8
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ ๐ โ โค) |
19 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โค) |
20 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ 8 โ
โ) |
21 | 19, 20 | zmodcld 13798 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐ mod 8) โ
โ0) |
22 | 21 | nn0zd 12526 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ mod 8) โ
โค) |
23 | 22 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐ mod 8) โ โค) |
24 | | eleq1 2826 |
. . . . . . . . . . . 12
โข (๐
= (๐ mod 8) โ (๐
โ โค โ (๐ mod 8) โ โค)) |
25 | 24 | 3ad2ant3 1136 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐
โ โค โ (๐ mod 8) โ โค)) |
26 | 23, 25 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ ๐
โ โค) |
27 | 26 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ ๐
โ โค) |
28 | 27 | adantr 482 |
. . . . . . . 8
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ ๐
โ โค) |
29 | | simpr 486 |
. . . . . . . 8
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ ๐ = ((8 ยท ๐) + ๐
)) |
30 | | 2lgsoddprmlem1 26759 |
. . . . . . . 8
โข ((๐ โ โค โง ๐
โ โค โง ๐ = ((8 ยท ๐) + ๐
)) โ (((๐โ2) โ 1) / 8) = (((8 ยท
(๐โ2)) + (2 ยท
(๐ ยท ๐
))) + (((๐
โ2) โ 1) / 8))) |
31 | 18, 28, 29, 30 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ (((๐โ2) โ 1) / 8) = (((8 ยท
(๐โ2)) + (2 ยท
(๐ ยท ๐
))) + (((๐
โ2) โ 1) / 8))) |
32 | 31 | breq2d 5118 |
. . . . . 6
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ
(((8 ยท (๐โ2)) +
(2 ยท (๐ ยท
๐
))) + (((๐
โ2) โ 1) / 8)))) |
33 | | 2z 12536 |
. . . . . . 7
โข 2 โ
โค |
34 | | simp1 1137 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ ๐ โ โค) |
35 | 1 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ 8 โ
โ) |
36 | 34, 35 | zmodcld 13798 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐ mod 8) โ
โ0) |
37 | 36 | nn0red 12475 |
. . . . . . . . . 10
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐ mod 8) โ โ) |
38 | | eleq1 2826 |
. . . . . . . . . . 11
โข (๐
= (๐ mod 8) โ (๐
โ โ โ (๐ mod 8) โ โ)) |
39 | 38 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐
โ โ โ (๐ mod 8) โ โ)) |
40 | 37, 39 | mpbird 257 |
. . . . . . . . 9
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ ๐
โ โ) |
41 | | resqcl 14030 |
. . . . . . . . . . 11
โข (๐
โ โ โ (๐
โ2) โ
โ) |
42 | | peano2rem 11469 |
. . . . . . . . . . 11
โข ((๐
โ2) โ โ โ
((๐
โ2) โ 1)
โ โ) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
โข (๐
โ โ โ ((๐
โ2) โ 1) โ
โ) |
44 | | 8re 12250 |
. . . . . . . . . . 11
โข 8 โ
โ |
45 | 44 | a1i 11 |
. . . . . . . . . 10
โข (๐
โ โ โ 8 โ
โ) |
46 | | 8pos 12266 |
. . . . . . . . . . . 12
โข 0 <
8 |
47 | 44, 46 | gt0ne0ii 11692 |
. . . . . . . . . . 11
โข 8 โ
0 |
48 | 47 | a1i 11 |
. . . . . . . . . 10
โข (๐
โ โ โ 8 โ
0) |
49 | 43, 45, 48 | redivcld 11984 |
. . . . . . . . 9
โข (๐
โ โ โ (((๐
โ2) โ 1) / 8) โ
โ) |
50 | 40, 49 | syl 17 |
. . . . . . . 8
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (((๐
โ2) โ 1) / 8) โ
โ) |
51 | 50 | adantr 482 |
. . . . . . 7
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ (((๐
โ2) โ 1) / 8) โ
โ) |
52 | | eleq1 2826 |
. . . . . . . . . . . 12
โข (๐
= (๐ mod 8) โ (๐
โ โ0 โ (๐ mod 8) โ
โ0)) |
53 | 52 | 3ad2ant3 1136 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐
โ โ0 โ (๐ mod 8) โ
โ0)) |
54 | 36, 53 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ ๐
โ
โ0) |
55 | | nn0z 12525 |
. . . . . . . . . . 11
โข (๐
โ โ0
โ ๐
โ
โค) |
56 | 1 | nnzi 12528 |
. . . . . . . . . . . . . . . 16
โข 8 โ
โค |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ 8 โ
โค) |
58 | | zsqcl 14035 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (๐โ2) โ
โค) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ (๐โ2) โ
โค) |
60 | 57, 59 | zmulcld 12614 |
. . . . . . . . . . . . . 14
โข ((๐
โ โค โง ๐ โ โค) โ (8
ยท (๐โ2)) โ
โค) |
61 | 33 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ 2 โ
โค) |
62 | | zmulcl 12553 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐
โ โค) โ (๐ ยท ๐
) โ โค) |
63 | 62 | ancoms 460 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ (๐ ยท ๐
) โ โค) |
64 | 61, 63 | zmulcld 12614 |
. . . . . . . . . . . . . 14
โข ((๐
โ โค โง ๐ โ โค) โ (2
ยท (๐ ยท ๐
)) โ
โค) |
65 | 60, 64 | zaddcld 12612 |
. . . . . . . . . . . . 13
โข ((๐
โ โค โง ๐ โ โค) โ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))) โ
โค) |
66 | | 4z 12538 |
. . . . . . . . . . . . . . . . . . 19
โข 4 โ
โค |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐
โ โค โง ๐ โ โค) โ 4 โ
โค) |
68 | 67, 59 | zmulcld 12614 |
. . . . . . . . . . . . . . . . 17
โข ((๐
โ โค โง ๐ โ โค) โ (4
ยท (๐โ2)) โ
โค) |
69 | 68, 63 | zaddcld 12612 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ โค โง ๐ โ โค) โ ((4
ยท (๐โ2)) +
(๐ ยท ๐
)) โ
โค) |
70 | 61, 69 | jca 513 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ (2
โ โค โง ((4 ยท (๐โ2)) + (๐ ยท ๐
)) โ โค)) |
71 | | dvdsmul1 16161 |
. . . . . . . . . . . . . . 15
โข ((2
โ โค โง ((4 ยท (๐โ2)) + (๐ ยท ๐
)) โ โค) โ 2 โฅ (2
ยท ((4 ยท (๐โ2)) + (๐ ยท ๐
)))) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐
โ โค โง ๐ โ โค) โ 2
โฅ (2 ยท ((4 ยท (๐โ2)) + (๐ ยท ๐
)))) |
73 | | 4t2e8 12322 |
. . . . . . . . . . . . . . . . . . . 20
โข (4
ยท 2) = 8 |
74 | | 4cn 12239 |
. . . . . . . . . . . . . . . . . . . . 21
โข 4 โ
โ |
75 | | 2cn 12229 |
. . . . . . . . . . . . . . . . . . . . 21
โข 2 โ
โ |
76 | 74, 75 | mulcomi 11164 |
. . . . . . . . . . . . . . . . . . . 20
โข (4
ยท 2) = (2 ยท 4) |
77 | 73, 76 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . 19
โข 8 = (2
ยท 4) |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐
โ โค โง ๐ โ โค) โ 8 = (2
ยท 4)) |
79 | 78 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข ((๐
โ โค โง ๐ โ โค) โ (8
ยท (๐โ2)) = ((2
ยท 4) ยท (๐โ2))) |
80 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐
โ โค โง ๐ โ โค) โ 2 โ
โ) |
81 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐
โ โค โง ๐ โ โค) โ 4 โ
โ) |
82 | 58 | zcnd 12609 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (๐โ2) โ
โ) |
83 | 82 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข ((๐
โ โค โง ๐ โ โค) โ (๐โ2) โ
โ) |
84 | 80, 81, 83 | mulassd 11179 |
. . . . . . . . . . . . . . . . 17
โข ((๐
โ โค โง ๐ โ โค) โ ((2
ยท 4) ยท (๐โ2)) = (2 ยท (4 ยท (๐โ2)))) |
85 | 79, 84 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ โค โง ๐ โ โค) โ (8
ยท (๐โ2)) = (2
ยท (4 ยท (๐โ2)))) |
86 | 85 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))) = ((2 ยท (4 ยท
(๐โ2))) + (2 ยท
(๐ ยท ๐
)))) |
87 | 68 | zcnd 12609 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ โค โง ๐ โ โค) โ (4
ยท (๐โ2)) โ
โ) |
88 | 62 | zcnd 12609 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐
โ โค) โ (๐ ยท ๐
) โ โ) |
89 | 88 | ancoms 460 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ โค โง ๐ โ โค) โ (๐ ยท ๐
) โ โ) |
90 | 80, 87, 89 | adddid 11180 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง ๐ โ โค) โ (2
ยท ((4 ยท (๐โ2)) + (๐ ยท ๐
))) = ((2 ยท (4 ยท (๐โ2))) + (2 ยท (๐ ยท ๐
)))) |
91 | 86, 90 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
โข ((๐
โ โค โง ๐ โ โค) โ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))) = (2 ยท ((4 ยท
(๐โ2)) + (๐ ยท ๐
)))) |
92 | 72, 91 | breqtrrd 5134 |
. . . . . . . . . . . . 13
โข ((๐
โ โค โง ๐ โ โค) โ 2
โฅ ((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
)))) |
93 | 65, 92 | jca 513 |
. . . . . . . . . . . 12
โข ((๐
โ โค โง ๐ โ โค) โ (((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))) โ โค โง 2
โฅ ((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))))) |
94 | 93 | ex 414 |
. . . . . . . . . . 11
โข (๐
โ โค โ (๐ โ โค โ (((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))) โ โค โง 2
โฅ ((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
)))))) |
95 | 55, 94 | syl 17 |
. . . . . . . . . 10
โข (๐
โ โ0
โ (๐ โ โค
โ (((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))) โ โค โง 2 โฅ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
)))))) |
96 | 54, 95 | syl 17 |
. . . . . . . . 9
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (๐ โ โค โ (((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))) โ โค โง 2 โฅ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
)))))) |
97 | 96 | imp 408 |
. . . . . . . 8
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ (((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))) โ โค โง 2 โฅ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))))) |
98 | 97 | adantr 482 |
. . . . . . 7
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ (((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))) โ โค โง 2 โฅ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))))) |
99 | | dvdsaddre2b 16190 |
. . . . . . 7
โข ((2
โ โค โง (((๐
โ2) โ 1) / 8) โ โ
โง (((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))) โ โค โง 2 โฅ ((8
ยท (๐โ2)) + (2
ยท (๐ ยท ๐
))))) โ (2 โฅ (((๐
โ2) โ 1) / 8) โ
2 โฅ (((8 ยท (๐โ2)) + (2 ยท (๐ ยท ๐
))) + (((๐
โ2) โ 1) / 8)))) |
100 | 33, 51, 98, 99 | mp3an2ani 1469 |
. . . . . 6
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ (2 โฅ (((๐
โ2) โ 1) / 8) โ 2 โฅ
(((8 ยท (๐โ2)) +
(2 ยท (๐ ยท
๐
))) + (((๐
โ2) โ 1) / 8)))) |
101 | 32, 100 | bitr4d 282 |
. . . . 5
โข ((((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โง ๐ = ((8 ยท ๐) + ๐
)) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ
(((๐
โ2) โ 1) /
8))) |
102 | 101 | ex 414 |
. . . 4
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ (๐ = ((8 ยท ๐) + ๐
) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ
(((๐
โ2) โ 1) /
8)))) |
103 | 16, 102 | sylbid 239 |
. . 3
โข (((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โง ๐ โ โค) โ (๐ = ((๐ ยท 8) + ๐
) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ
(((๐
โ2) โ 1) /
8)))) |
104 | 103 | rexlimdva 3153 |
. 2
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (โ๐ โ โค ๐ = ((๐ ยท 8) + ๐
) โ (2 โฅ (((๐โ2) โ 1) / 8) โ 2 โฅ
(((๐
โ2) โ 1) /
8)))) |
105 | 9, 104 | mpd 15 |
1
โข ((๐ โ โค โง ยฌ 2
โฅ ๐ โง ๐
= (๐ mod 8)) โ (2 โฅ (((๐โ2) โ 1) / 8) โ
2 โฅ (((๐
โ2)
โ 1) / 8))) |