MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsdir2lem5 Structured version   Unicode version

Theorem lgsdir2lem5 23719
Description: Lemma for lgsdir2 23720. (Contributed by Mario Carneiro, 4-Feb-2015.)
Assertion
Ref Expression
lgsdir2lem5  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  e. 
{ 3 ,  5 }  /\  ( B  mod  8 )  e. 
{ 3 ,  5 } ) )  -> 
( ( A  x.  B )  mod  8
)  e.  { 1 ,  7 } )

Proof of Theorem lgsdir2lem5
StepHypRef Expression
1 ovex 6224 . . . . . . 7  |-  ( A  mod  8 )  e. 
_V
21elpr 3962 . . . . . 6  |-  ( ( A  mod  8 )  e.  { 3 ,  5 }  <->  ( ( A  mod  8 )  =  3  \/  ( A  mod  8 )  =  5 ) )
3 ovex 6224 . . . . . . 7  |-  ( B  mod  8 )  e. 
_V
43elpr 3962 . . . . . 6  |-  ( ( B  mod  8 )  e.  { 3 ,  5 }  <->  ( ( B  mod  8 )  =  3  \/  ( B  mod  8 )  =  5 ) )
52, 4anbi12i 695 . . . . 5  |-  ( ( ( A  mod  8
)  e.  { 3 ,  5 }  /\  ( B  mod  8
)  e.  { 3 ,  5 } )  <-> 
( ( ( A  mod  8 )  =  3  \/  ( A  mod  8 )  =  5 )  /\  (
( B  mod  8
)  =  3  \/  ( B  mod  8
)  =  5 ) ) )
6 simpll 751 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  ->  A  e.  ZZ )
7 3z 10814 . . . . . . . . . 10  |-  3  e.  ZZ
87a1i 11 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
3  e.  ZZ )
9 simplr 753 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  ->  B  e.  ZZ )
10 8re 10537 . . . . . . . . . . 11  |-  8  e.  RR
11 8pos 10553 . . . . . . . . . . 11  |-  0  <  8
1210, 11elrpii 11142 . . . . . . . . . 10  |-  8  e.  RR+
1312a1i 11 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
8  e.  RR+ )
14 simprl 754 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
( A  mod  8
)  =  3 )
15 lgsdir2lem1 23715 . . . . . . . . . . . 12  |-  ( ( ( 1  mod  8
)  =  1  /\  ( -u 1  mod  8 )  =  7 )  /\  ( ( 3  mod  8 )  =  3  /\  ( -u 3  mod  8 )  =  5 ) )
1615simpri 460 . . . . . . . . . . 11  |-  ( ( 3  mod  8 )  =  3  /\  ( -u 3  mod  8 )  =  5 )
1716simpli 456 . . . . . . . . . 10  |-  ( 3  mod  8 )  =  3
1814, 17syl6eqr 2441 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
( A  mod  8
)  =  ( 3  mod  8 ) )
19 simprr 755 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
( B  mod  8
)  =  3 )
2019, 17syl6eqr 2441 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
( B  mod  8
)  =  ( 3  mod  8 ) )
216, 8, 9, 8, 13, 18, 20modmul12d 11944 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 ) )
2221orcd 390 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 ) )  -> 
( ( ( A  x.  B )  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8 )  =  (
-u ( 3  x.  3 )  mod  8
) ) )
2322ex 432 . . . . . 6  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  3 )  ->  (
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) ) ) )
24 simpll 751 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  ->  A  e.  ZZ )
25 znegcl 10816 . . . . . . . . . . 11  |-  ( 3  e.  ZZ  ->  -u 3  e.  ZZ )
267, 25mp1i 12 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  ->  -u 3  e.  ZZ )
27 simplr 753 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  ->  B  e.  ZZ )
287a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
3  e.  ZZ )
2912a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
8  e.  RR+ )
30 simprl 754 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( A  mod  8
)  =  5 )
3116simpri 460 . . . . . . . . . . 11  |-  ( -u
3  mod  8 )  =  5
3230, 31syl6eqr 2441 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( A  mod  8
)  =  ( -u
3  mod  8 ) )
33 simprr 755 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( B  mod  8
)  =  3 )
3433, 17syl6eqr 2441 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( B  mod  8
)  =  ( 3  mod  8 ) )
3524, 26, 27, 28, 29, 32, 34modmul12d 11944 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( (
-u 3  x.  3 )  mod  8 ) )
36 3cn 10527 . . . . . . . . . . 11  |-  3  e.  CC
3736, 36mulneg1i 9920 . . . . . . . . . 10  |-  ( -u
3  x.  3 )  =  -u ( 3  x.  3 )
3837oveq1i 6206 . . . . . . . . 9  |-  ( (
-u 3  x.  3 )  mod  8 )  =  ( -u (
3  x.  3 )  mod  8 )
3935, 38syl6eq 2439 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) )
4039olcd 391 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 ) )  -> 
( ( ( A  x.  B )  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8 )  =  (
-u ( 3  x.  3 )  mod  8
) ) )
4140ex 432 . . . . . 6  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  3 )  ->  (
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) ) ) )
42 simpll 751 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  ->  A  e.  ZZ )
437a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
3  e.  ZZ )
44 simplr 753 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  ->  B  e.  ZZ )
457, 25mp1i 12 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  ->  -u 3  e.  ZZ )
4612a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
8  e.  RR+ )
47 simprl 754 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( A  mod  8
)  =  3 )
4847, 17syl6eqr 2441 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( A  mod  8
)  =  ( 3  mod  8 ) )
49 simprr 755 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( B  mod  8
)  =  5 )
5049, 31syl6eqr 2441 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( B  mod  8
)  =  ( -u
3  mod  8 ) )
5142, 43, 44, 45, 46, 48, 50modmul12d 11944 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  -u 3
)  mod  8 ) )
5236, 36mulneg2i 9921 . . . . . . . . . 10  |-  ( 3  x.  -u 3 )  = 
-u ( 3  x.  3 )
5352oveq1i 6206 . . . . . . . . 9  |-  ( ( 3  x.  -u 3
)  mod  8 )  =  ( -u (
3  x.  3 )  mod  8 )
5451, 53syl6eq 2439 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) )
5554olcd 391 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 ) )  -> 
( ( ( A  x.  B )  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8 )  =  (
-u ( 3  x.  3 )  mod  8
) ) )
5655ex 432 . . . . . 6  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( ( A  mod  8 )  =  3  /\  ( B  mod  8 )  =  5 )  ->  (
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) ) ) )
57 simpll 751 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  ->  A  e.  ZZ )
587, 25mp1i 12 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  ->  -u 3  e.  ZZ )
59 simplr 753 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  ->  B  e.  ZZ )
6012a1i 11 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
8  e.  RR+ )
61 simprl 754 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( A  mod  8
)  =  5 )
6261, 31syl6eqr 2441 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( A  mod  8
)  =  ( -u
3  mod  8 ) )
63 simprr 755 . . . . . . . . . . 11  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( B  mod  8
)  =  5 )
6463, 31syl6eqr 2441 . . . . . . . . . 10  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( B  mod  8
)  =  ( -u
3  mod  8 ) )
6557, 58, 59, 58, 60, 62, 64modmul12d 11944 . . . . . . . . 9  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( (
-u 3  x.  -u 3
)  mod  8 ) )
6636, 36mul2negi 9922 . . . . . . . . . 10  |-  ( -u
3  x.  -u 3
)  =  ( 3  x.  3 )
6766oveq1i 6206 . . . . . . . . 9  |-  ( (
-u 3  x.  -u 3
)  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )
6865, 67syl6eq 2439 . . . . . . . 8  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 ) )
6968orcd 390 . . . . . . 7  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 ) )  -> 
( ( ( A  x.  B )  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8 )  =  (
-u ( 3  x.  3 )  mod  8
) ) )
7069ex 432 . . . . . 6  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( ( A  mod  8 )  =  5  /\  ( B  mod  8 )  =  5 )  ->  (
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) ) ) )
7123, 41, 56, 70ccased 945 . . . . 5  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( ( ( A  mod  8 )  =  3  \/  ( A  mod  8 )  =  5 )  /\  (
( B  mod  8
)  =  3  \/  ( B  mod  8
)  =  5 ) )  ->  ( (
( A  x.  B
)  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  (
( A  x.  B
)  mod  8 )  =  ( -u (
3  x.  3 )  mod  8 ) ) ) )
725, 71syl5bi 217 . . . 4  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( ( A  mod  8 )  e. 
{ 3 ,  5 }  /\  ( B  mod  8 )  e. 
{ 3 ,  5 } )  ->  (
( ( A  x.  B )  mod  8
)  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8
)  =  ( -u ( 3  x.  3 )  mod  8 ) ) ) )
7372imp 427 . . 3  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  e. 
{ 3 ,  5 }  /\  ( B  mod  8 )  e. 
{ 3 ,  5 } ) )  -> 
( ( ( A  x.  B )  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  ( ( A  x.  B )  mod  8 )  =  (
-u ( 3  x.  3 )  mod  8
) ) )
74 ovex 6224 . . . 4  |-  ( ( A  x.  B )  mod  8 )  e. 
_V
7574elpr 3962 . . 3  |-  ( ( ( A  x.  B
)  mod  8 )  e.  { ( ( 3  x.  3 )  mod  8 ) ,  ( -u ( 3  x.  3 )  mod  8 ) }  <->  ( (
( A  x.  B
)  mod  8 )  =  ( ( 3  x.  3 )  mod  8 )  \/  (
( A  x.  B
)  mod  8 )  =  ( -u (
3  x.  3 )  mod  8 ) ) )
7673, 75sylibr 212 . 2  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  e. 
{ 3 ,  5 }  /\  ( B  mod  8 )  e. 
{ 3 ,  5 } ) )  -> 
( ( A  x.  B )  mod  8
)  e.  { ( ( 3  x.  3 )  mod  8 ) ,  ( -u (
3  x.  3 )  mod  8 ) } )
77 df-9 10518 . . . . . . . 8  |-  9  =  ( 8  +  1 )
78 8cn 10538 . . . . . . . . 9  |-  8  e.  CC
79 ax-1cn 9461 . . . . . . . . 9  |-  1  e.  CC
8078, 79addcomi 9682 . . . . . . . 8  |-  ( 8  +  1 )  =  ( 1  +  8 )
8177, 80eqtri 2411 . . . . . . 7  |-  9  =  ( 1  +  8 )
82 3t3e9 10605 . . . . . . 7  |-  ( 3  x.  3 )  =  9
8378mulid2i 9510 . . . . . . . 8  |-  ( 1  x.  8 )  =  8
8483oveq2i 6207 . . . . . . 7  |-  ( 1  +  ( 1  x.  8 ) )  =  ( 1  +  8 )
8581, 82, 843eqtr4i 2421 . . . . . 6  |-  ( 3  x.  3 )  =  ( 1  +  ( 1  x.  8 ) )
8685oveq1i 6206 . . . . 5  |-  ( ( 3  x.  3 )  mod  8 )  =  ( ( 1  +  ( 1  x.  8 ) )  mod  8
)
87 1re 9506 . . . . . 6  |-  1  e.  RR
88 1z 10811 . . . . . 6  |-  1  e.  ZZ
89 modcyc 11932 . . . . . 6  |-  ( ( 1  e.  RR  /\  8  e.  RR+  /\  1  e.  ZZ )  ->  (
( 1  +  ( 1  x.  8 ) )  mod  8 )  =  ( 1  mod  8 ) )
9087, 12, 88, 89mp3an 1322 . . . . 5  |-  ( ( 1  +  ( 1  x.  8 ) )  mod  8 )  =  ( 1  mod  8
)
9186, 90eqtri 2411 . . . 4  |-  ( ( 3  x.  3 )  mod  8 )  =  ( 1  mod  8
)
9215simpli 456 . . . . 5  |-  ( ( 1  mod  8 )  =  1  /\  ( -u 1  mod  8 )  =  7 )
9392simpli 456 . . . 4  |-  ( 1  mod  8 )  =  1
9491, 93eqtri 2411 . . 3  |-  ( ( 3  x.  3 )  mod  8 )  =  1
95 znegcl 10816 . . . . . . . 8  |-  ( 1  e.  ZZ  ->  -u 1  e.  ZZ )
9688, 95mp1i 12 . . . . . . 7  |-  ( T. 
->  -u 1  e.  ZZ )
97 3nn 10611 . . . . . . . . . 10  |-  3  e.  NN
9897, 97nnmulcli 10476 . . . . . . . . 9  |-  ( 3  x.  3 )  e.  NN
9998nnzi 10805 . . . . . . . 8  |-  ( 3  x.  3 )  e.  ZZ
10099a1i 11 . . . . . . 7  |-  ( T. 
->  ( 3  x.  3 )  e.  ZZ )
10188a1i 11 . . . . . . 7  |-  ( T. 
->  1  e.  ZZ )
10212a1i 11 . . . . . . 7  |-  ( T. 
->  8  e.  RR+ )
103 eqidd 2383 . . . . . . 7  |-  ( T. 
->  ( -u 1  mod  8 )  =  (
-u 1  mod  8
) )
10491a1i 11 . . . . . . 7  |-  ( T. 
->  ( ( 3  x.  3 )  mod  8
)  =  ( 1  mod  8 ) )
10596, 96, 100, 101, 102, 103, 104modmul12d 11944 . . . . . 6  |-  ( T. 
->  ( ( -u 1  x.  ( 3  x.  3 ) )  mod  8
)  =  ( (
-u 1  x.  1 )  mod  8 ) )
106105trud 1408 . . . . 5  |-  ( (
-u 1  x.  (
3  x.  3 ) )  mod  8 )  =  ( ( -u
1  x.  1 )  mod  8 )
10736, 36mulcli 9512 . . . . . . 7  |-  ( 3  x.  3 )  e.  CC
108107mulm1i 9919 . . . . . 6  |-  ( -u
1  x.  ( 3  x.  3 ) )  =  -u ( 3  x.  3 )
109108oveq1i 6206 . . . . 5  |-  ( (
-u 1  x.  (
3  x.  3 ) )  mod  8 )  =  ( -u (
3  x.  3 )  mod  8 )
11079mulm1i 9919 . . . . . 6  |-  ( -u
1  x.  1 )  =  -u 1
111110oveq1i 6206 . . . . 5  |-  ( (
-u 1  x.  1 )  mod  8 )  =  ( -u 1  mod  8 )
112106, 109, 1113eqtr3i 2419 . . . 4  |-  ( -u ( 3  x.  3 )  mod  8 )  =  ( -u 1  mod  8 )
11392simpri 460 . . . 4  |-  ( -u
1  mod  8 )  =  7
114112, 113eqtri 2411 . . 3  |-  ( -u ( 3  x.  3 )  mod  8 )  =  7
11594, 114preq12i 4028 . 2  |-  { ( ( 3  x.  3 )  mod  8 ) ,  ( -u (
3  x.  3 )  mod  8 ) }  =  { 1 ,  7 }
11676, 115syl6eleq 2480 1  |-  ( ( ( A  e.  ZZ  /\  B  e.  ZZ )  /\  ( ( A  mod  8 )  e. 
{ 3 ,  5 }  /\  ( B  mod  8 )  e. 
{ 3 ,  5 } ) )  -> 
( ( A  x.  B )  mod  8
)  e.  { 1 ,  7 } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 366    /\ wa 367    = wceq 1399   T. wtru 1400    e. wcel 1826   {cpr 3946  (class class class)co 6196   RRcr 9402   1c1 9404    + caddc 9406    x. cmul 9408   -ucneg 9719   3c3 10503   5c5 10505   7c7 10507   8c8 10508   9c9 10509   ZZcz 10781   RR+crp 11139    mod cmo 11896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480  ax-pre-sup 9481
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-recs 6960  df-rdg 6994  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-sup 7816  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-nn 10453  df-2 10511  df-3 10512  df-4 10513  df-5 10514  df-6 10515  df-7 10516  df-8 10517  df-9 10518  df-n0 10713  df-z 10782  df-uz 11002  df-rp 11140  df-fl 11828  df-mod 11897
This theorem is referenced by:  lgsdir2  23720
  Copyright terms: Public domain W3C validator