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 ∈ ℤ ∧ N mod 4 = 3 → 2 ⋅ N + 1 mod 8 = 7

Proof

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