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 ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 mod 4 ) = 3 ) → ( ( ( 2 · 𝑁 ) + 1 ) mod 8 ) = 7 )

Proof

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