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 \in ℤ \land N \mod 4 = 3) \to (2 \cdot N + 1) \mod 8 = 7$

Proof

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

Metamath Proof Explorer

Theorem mod42tp1mod8

Proof