2lgsoddprmlem2

		Ref	Expression
	Assertion	2lgsoddprmlem2	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{R^{2} - 1}{8}))$

Proof

Step	Hyp	Ref	Expression
1		8nn	$⊢ 8 \in ℕ$
2		nnrp	$⊢ 8 \in ℕ \to 8 \in ℝ^{+}$
3	1 2	ax-mp	$⊢ 8 \in ℝ^{+}$
4		eqcom	$⊢ R = N \mod 8 \leftrightarrow N \mod 8 = R$
5		modmuladdim	$⊢ (N \in ℤ \land 8 \in ℝ^{+}) \to (N \mod 8 = R \to \exists k \in ℤ N = k \cdot 8 + R)$
6	4 5	biimtrid	$⊢ (N \in ℤ \land 8 \in ℝ^{+}) \to (R = N \mod 8 \to \exists k \in ℤ N = k \cdot 8 + R)$
7	3 6	mpan2	$⊢ N \in ℤ \to (R = N \mod 8 \to \exists k \in ℤ N = k \cdot 8 + R)$
8	7	imp	$⊢ (N \in ℤ \land R = N \mod 8) \to \exists k \in ℤ N = k \cdot 8 + R$
9	8	3adant2	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to \exists k \in ℤ N = k \cdot 8 + R$
10		zcn	$⊢ k \in ℤ \to k \in ℂ$
11		8cn	$⊢ 8 \in ℂ$
12	11	a1i	$⊢ k \in ℤ \to 8 \in ℂ$
13	10 12	mulcomd	$⊢ k \in ℤ \to k \cdot 8 = 8 k$
14	13	adantl	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to k \cdot 8 = 8 k$
15	14	oveq1d	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to k \cdot 8 + R = 8 k + R$
16	15	eqeq2d	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to (N = k \cdot 8 + R \leftrightarrow N = 8 k + R)$
17		simpr	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to k \in ℤ$
18	17	adantr	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to k \in ℤ$
19		id	$⊢ N \in ℤ \to N \in ℤ$
20	1	a1i	$⊢ N \in ℤ \to 8 \in ℕ$
21	19 20	zmodcld	$⊢ N \in ℤ \to N \mod 8 \in ℕ_{0}$
22	21	nn0zd	$⊢ N \in ℤ \to N \mod 8 \in ℤ$
23	22	3ad2ant1	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to N \mod 8 \in ℤ$
24		eleq1	$⊢ R = N \mod 8 \to (R \in ℤ \leftrightarrow N \mod 8 \in ℤ)$
25	24	3ad2ant3	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (R \in ℤ \leftrightarrow N \mod 8 \in ℤ)$
26	23 25	mpbird	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to R \in ℤ$
27	26	adantr	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to R \in ℤ$
28	27	adantr	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to R \in ℤ$
29		simpr	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to N = 8 k + R$
30		2lgsoddprmlem1	$⊢ (k \in ℤ \land R \in ℤ \land N = 8 k + R) \to \frac{N^{2} - 1}{8} = 8 k^{2} + 2 k R + (\frac{R^{2} - 1}{8})$
31	18 28 29 30	syl3anc	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to \frac{N^{2} - 1}{8} = 8 k^{2} + 2 k R + (\frac{R^{2} - 1}{8})$
32	31	breq2d	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (8 k^{2} + 2 k R + (\frac{R^{2} - 1}{8})))$
33		2z	$⊢ 2 \in ℤ$
34		simp1	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to N \in ℤ$
35	1	a1i	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to 8 \in ℕ$
36	34 35	zmodcld	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to N \mod 8 \in ℕ_{0}$
37	36	nn0red	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to N \mod 8 \in ℝ$
38		eleq1	$⊢ R = N \mod 8 \to (R \in ℝ \leftrightarrow N \mod 8 \in ℝ)$
39	38	3ad2ant3	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (R \in ℝ \leftrightarrow N \mod 8 \in ℝ)$
40	37 39	mpbird	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to R \in ℝ$
41		resqcl	$⊢ R \in ℝ \to R^{2} \in ℝ$
42		peano2rem	$⊢ R^{2} \in ℝ \to R^{2} - 1 \in ℝ$
43	41 42	syl	$⊢ R \in ℝ \to R^{2} - 1 \in ℝ$
44		8re	$⊢ 8 \in ℝ$
45	44	a1i	$⊢ R \in ℝ \to 8 \in ℝ$
46		8pos	$⊢ 0 < 8$
47	44 46	gt0ne0ii	$⊢ 8 \neq 0$
48	47	a1i	$⊢ R \in ℝ \to 8 \neq 0$
49	43 45 48	redivcld	$⊢ R \in ℝ \to \frac{R^{2} - 1}{8} \in ℝ$
50	40 49	syl	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to \frac{R^{2} - 1}{8} \in ℝ$
51	50	adantr	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to \frac{R^{2} - 1}{8} \in ℝ$
52		eleq1	$⊢ R = N \mod 8 \to (R \in ℕ_{0} \leftrightarrow N \mod 8 \in ℕ_{0})$
53	52	3ad2ant3	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (R \in ℕ_{0} \leftrightarrow N \mod 8 \in ℕ_{0})$
54	36 53	mpbird	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to R \in ℕ_{0}$
55		nn0z	$⊢ R \in ℕ_{0} \to R \in ℤ$
56	1	nnzi	$⊢ 8 \in ℤ$
57	56	a1i	$⊢ (R \in ℤ \land k \in ℤ) \to 8 \in ℤ$
58		zsqcl	$⊢ k \in ℤ \to k^{2} \in ℤ$
59	58	adantl	$⊢ (R \in ℤ \land k \in ℤ) \to k^{2} \in ℤ$
60	57 59	zmulcld	$⊢ (R \in ℤ \land k \in ℤ) \to 8 k^{2} \in ℤ$
61	33	a1i	$⊢ (R \in ℤ \land k \in ℤ) \to 2 \in ℤ$
62		zmulcl	$⊢ (k \in ℤ \land R \in ℤ) \to k R \in ℤ$
63	62	ancoms	$⊢ (R \in ℤ \land k \in ℤ) \to k R \in ℤ$
64	61 63	zmulcld	$⊢ (R \in ℤ \land k \in ℤ) \to 2 k R \in ℤ$
65	60 64	zaddcld	$⊢ (R \in ℤ \land k \in ℤ) \to 8 k^{2} + 2 k R \in ℤ$
66		4z	$⊢ 4 \in ℤ$
67	66	a1i	$⊢ (R \in ℤ \land k \in ℤ) \to 4 \in ℤ$
68	67 59	zmulcld	$⊢ (R \in ℤ \land k \in ℤ) \to 4 k^{2} \in ℤ$
69	68 63	zaddcld	$⊢ (R \in ℤ \land k \in ℤ) \to 4 k^{2} + k R \in ℤ$
70	61 69	jca	$⊢ (R \in ℤ \land k \in ℤ) \to (2 \in ℤ \land 4 k^{2} + k R \in ℤ)$
71		dvdsmul1	$⊢ (2 \in ℤ \land 4 k^{2} + k R \in ℤ) \to 2 ∥ 2 (4 k^{2} + k R)$
72	70 71	syl	$⊢ (R \in ℤ \land k \in ℤ) \to 2 ∥ 2 (4 k^{2} + k R)$
73		4t2e8	$⊢ 4 \cdot 2 = 8$
74		4cn	$⊢ 4 \in ℂ$
75		2cn	$⊢ 2 \in ℂ$
76	74 75	mulcomi	$⊢ 4 \cdot 2 = 2 \cdot 4$
77	73 76	eqtr3i	$⊢ 8 = 2 \cdot 4$
78	77	a1i	$⊢ (R \in ℤ \land k \in ℤ) \to 8 = 2 \cdot 4$
79	78	oveq1d	$⊢ (R \in ℤ \land k \in ℤ) \to 8 k^{2} = 2 \cdot 4 k^{2}$
80	75	a1i	$⊢ (R \in ℤ \land k \in ℤ) \to 2 \in ℂ$
81	74	a1i	$⊢ (R \in ℤ \land k \in ℤ) \to 4 \in ℂ$
82	58	zcnd	$⊢ k \in ℤ \to k^{2} \in ℂ$
83	82	adantl	$⊢ (R \in ℤ \land k \in ℤ) \to k^{2} \in ℂ$
84	80 81 83	mulassd	$⊢ (R \in ℤ \land k \in ℤ) \to 2 \cdot 4 k^{2} = 2 4 k^{2}$
85	79 84	eqtrd	$⊢ (R \in ℤ \land k \in ℤ) \to 8 k^{2} = 2 4 k^{2}$
86	85	oveq1d	$⊢ (R \in ℤ \land k \in ℤ) \to 8 k^{2} + 2 k R = 2 4 k^{2} + 2 k R$
87	68	zcnd	$⊢ (R \in ℤ \land k \in ℤ) \to 4 k^{2} \in ℂ$
88	62	zcnd	$⊢ (k \in ℤ \land R \in ℤ) \to k R \in ℂ$
89	88	ancoms	$⊢ (R \in ℤ \land k \in ℤ) \to k R \in ℂ$
90	80 87 89	adddid	$⊢ (R \in ℤ \land k \in ℤ) \to 2 (4 k^{2} + k R) = 2 4 k^{2} + 2 k R$
91	86 90	eqtr4d	$⊢ (R \in ℤ \land k \in ℤ) \to 8 k^{2} + 2 k R = 2 (4 k^{2} + k R)$
92	72 91	breqtrrd	$⊢ (R \in ℤ \land k \in ℤ) \to 2 ∥ (8 k^{2} + 2 k R)$
93	65 92	jca	$⊢ (R \in ℤ \land k \in ℤ) \to (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R))$
94	93	ex	$⊢ R \in ℤ \to (k \in ℤ \to (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R)))$
95	55 94	syl	$⊢ R \in ℕ_{0} \to (k \in ℤ \to (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R)))$
96	54 95	syl	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (k \in ℤ \to (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R)))$
97	96	imp	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R))$
98	97	adantr	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R))$
99		dvdsaddre2b	$⊢ (2 \in ℤ \land \frac{R^{2} - 1}{8} \in ℝ \land (8 k^{2} + 2 k R \in ℤ \land 2 ∥ (8 k^{2} + 2 k R))) \to (2 ∥ (\frac{R^{2} - 1}{8}) \leftrightarrow 2 ∥ (8 k^{2} + 2 k R + (\frac{R^{2} - 1}{8})))$
100	33 51 98 99	mp3an2ani	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to (2 ∥ (\frac{R^{2} - 1}{8}) \leftrightarrow 2 ∥ (8 k^{2} + 2 k R + (\frac{R^{2} - 1}{8})))$
101	32 100	bitr4d	$⊢ (((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \land N = 8 k + R) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{R^{2} - 1}{8}))$
102	101	ex	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to (N = 8 k + R \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{R^{2} - 1}{8})))$
103	16 102	sylbid	$⊢ ((N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \land k \in ℤ) \to (N = k \cdot 8 + R \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{R^{2} - 1}{8})))$
104	103	rexlimdva	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (\exists k \in ℤ N = k \cdot 8 + R \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{R^{2} - 1}{8})))$
105	9 104	mpd	$⊢ (N \in ℤ \land \neg 2 ∥ N \land R = N \mod 8) \to (2 ∥ (\frac{N^{2} - 1}{8}) \leftrightarrow 2 ∥ (\frac{R^{2} - 1}{8}))$

Metamath Proof Explorer

Theorem 2lgsoddprmlem2

Proof