Metamath Proof Explorer

Theorem mod42tp1mod8

Description: If a number is 3 modulo 4 , twice the number plus 1 is 7 modulo 8 . (Contributed by AV, 19-Aug-2021)

Ref Expression
Assertion mod42tp1mod8 
|- ( ( N e. ZZ /\ ( N mod 4 ) = 3 ) -> ( ( ( 2 x. N ) + 1 ) mod 8 ) = 7 )

Proof

Step Hyp Ref Expression
1 4nn 
 |-  4 e. NN
2 1 a1i 
 |-  ( N e. ZZ -> 4 e. NN )
3 3nn0 
 |-  3 e. NN0
4 3 a1i 
 |-  ( N e. ZZ -> 3 e. NN0 )
5 3lt4 
 |-  3 < 4
6 4 5 jctir 
 |-  ( N e. ZZ -> ( 3 e. NN0 /\ 3 < 4 ) )
7 modremain 
 |-  ( ( N e. ZZ /\ 4 e. NN /\ ( 3 e. NN0 /\ 3 < 4 ) ) -> ( ( N mod 4 ) = 3 <-> E. z e. ZZ ( ( z x. 4 ) + 3 ) = N ) )
8 2 6 7 mpd3an23 
 |-  ( N e. ZZ -> ( ( N mod 4 ) = 3 <-> E. z e. ZZ ( ( z x. 4 ) + 3 ) = N ) )
9 2cnd 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> 2 e. CC )
10 simpr 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> z e. ZZ )
11 4z 
 |-  4 e. ZZ
12 11 a1i 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> 4 e. ZZ )
13 10 12 zmulcld 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( z x. 4 ) e. ZZ )
14 13 zcnd 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( z x. 4 ) e. CC )
15 3cn 
 |-  3 e. CC
16 15 a1i 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> 3 e. CC )
17 9 14 16 adddid 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( 2 x. ( ( z x. 4 ) + 3 ) ) = ( ( 2 x. ( z x. 4 ) ) + ( 2 x. 3 ) ) )
18 10 zcnd 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> z e. CC )
19 4cn 
 |-  4 e. CC
20 19 a1i 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> 4 e. CC )
21 9 18 20 mul12d 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( 2 x. ( z x. 4 ) ) = ( z x. ( 2 x. 4 ) ) )
22 2cn 
 |-  2 e. CC
23 4t2e8 
 |-  ( 4 x. 2 ) = 8
24 19 22 23 mulcomli 
 |-  ( 2 x. 4 ) = 8
25 24 oveq2i 
 |-  ( z x. ( 2 x. 4 ) ) = ( z x. 8 )
26 21 25 eqtrdi 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( 2 x. ( z x. 4 ) ) = ( z x. 8 ) )
27 3t2e6 
 |-  ( 3 x. 2 ) = 6
28 15 22 27 mulcomli 
 |-  ( 2 x. 3 ) = 6
29 28 a1i 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( 2 x. 3 ) = 6 )
30 26 29 oveq12d 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( 2 x. ( z x. 4 ) ) + ( 2 x. 3 ) ) = ( ( z x. 8 ) + 6 ) )
31 17 30 eqtrd 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( 2 x. ( ( z x. 4 ) + 3 ) ) = ( ( z x. 8 ) + 6 ) )
32 31 oveq1d 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) = ( ( ( z x. 8 ) + 6 ) + 1 ) )
33 id 
 |-  ( z e. ZZ -> z e. ZZ )
34 8nn 
 |-  8 e. NN
35 34 nnzi 
 |-  8 e. ZZ
36 35 a1i 
 |-  ( z e. ZZ -> 8 e. ZZ )
37 33 36 zmulcld 
 |-  ( z e. ZZ -> ( z x. 8 ) e. ZZ )
38 37 zcnd 
 |-  ( z e. ZZ -> ( z x. 8 ) e. CC )
39 6cn 
 |-  6 e. CC
40 39 a1i 
 |-  ( z e. ZZ -> 6 e. CC )
41 1cnd 
 |-  ( z e. ZZ -> 1 e. CC )
42 38 40 41 addassd 
 |-  ( z e. ZZ -> ( ( ( z x. 8 ) + 6 ) + 1 ) = ( ( z x. 8 ) + ( 6 + 1 ) ) )
43 6p1e7 
 |-  ( 6 + 1 ) = 7
44 43 a1i 
 |-  ( z e. ZZ -> ( 6 + 1 ) = 7 )
45 44 oveq2d 
 |-  ( z e. ZZ -> ( ( z x. 8 ) + ( 6 + 1 ) ) = ( ( z x. 8 ) + 7 ) )
46 42 45 eqtrd 
 |-  ( z e. ZZ -> ( ( ( z x. 8 ) + 6 ) + 1 ) = ( ( z x. 8 ) + 7 ) )
47 46 adantl 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( ( z x. 8 ) + 6 ) + 1 ) = ( ( z x. 8 ) + 7 ) )
48 32 47 eqtrd 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) = ( ( z x. 8 ) + 7 ) )
49 48 oveq1d 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) mod 8 ) = ( ( ( z x. 8 ) + 7 ) mod 8 ) )
50 nnrp 
 |-  ( 8 e. NN -> 8 e. RR+ )
51 34 50 mp1i 
 |-  ( z e. ZZ -> 8 e. RR+ )
52 0xr 
 |-  0 e. RR*
53 52 a1i 
 |-  ( z e. ZZ -> 0 e. RR* )
54 8re 
 |-  8 e. RR
55 54 rexri 
 |-  8 e. RR*
56 55 a1i 
 |-  ( z e. ZZ -> 8 e. RR* )
57 7re 
 |-  7 e. RR
58 57 rexri 
 |-  7 e. RR*
59 58 a1i 
 |-  ( z e. ZZ -> 7 e. RR* )
60 0re 
 |-  0 e. RR
61 7pos 
 |-  0 < 7
62 60 57 61 ltleii 
 |-  0 <_ 7
63 62 a1i 
 |-  ( z e. ZZ -> 0 <_ 7 )
64 7lt8 
 |-  7 < 8
65 64 a1i 
 |-  ( z e. ZZ -> 7 < 8 )
66 53 56 59 63 65 elicod 
 |-  ( z e. ZZ -> 7 e. ( 0 [,) 8 ) )
67 muladdmodid 
 |-  ( ( z e. ZZ /\ 8 e. RR+ /\ 7 e. ( 0 [,) 8 ) ) -> ( ( ( z x. 8 ) + 7 ) mod 8 ) = 7 )
68 51 66 67 mpd3an23 
 |-  ( z e. ZZ -> ( ( ( z x. 8 ) + 7 ) mod 8 ) = 7 )
69 68 adantl 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( ( z x. 8 ) + 7 ) mod 8 ) = 7 )
70 49 69 eqtrd 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) mod 8 ) = 7 )
71 oveq2 
 |-  ( ( ( z x. 4 ) + 3 ) = N -> ( 2 x. ( ( z x. 4 ) + 3 ) ) = ( 2 x. N ) )
72 71 oveq1d 
 |-  ( ( ( z x. 4 ) + 3 ) = N -> ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) = ( ( 2 x. N ) + 1 ) )
73 72 oveq1d 
 |-  ( ( ( z x. 4 ) + 3 ) = N -> ( ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) mod 8 ) = ( ( ( 2 x. N ) + 1 ) mod 8 ) )
74 73 eqeq1d 
 |-  ( ( ( z x. 4 ) + 3 ) = N -> ( ( ( ( 2 x. ( ( z x. 4 ) + 3 ) ) + 1 ) mod 8 ) = 7 <-> ( ( ( 2 x. N ) + 1 ) mod 8 ) = 7 ) )
75 70 74 syl5ibcom 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( ( ( z x. 4 ) + 3 ) = N -> ( ( ( 2 x. N ) + 1 ) mod 8 ) = 7 ) )
76 75 rexlimdva 
 |-  ( N e. ZZ -> ( E. z e. ZZ ( ( z x. 4 ) + 3 ) = N -> ( ( ( 2 x. N ) + 1 ) mod 8 ) = 7 ) )
77 8 76 sylbid 
 |-  ( N e. ZZ -> ( ( N mod 4 ) = 3 -> ( ( ( 2 x. N ) + 1 ) mod 8 ) = 7 ) )
78 77 imp 
 |-  ( ( N e. ZZ /\ ( N mod 4 ) = 3 ) -> ( ( ( 2 x. N ) + 1 ) mod 8 ) = 7 )