2lgsoddprmlem2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 2lgsoddprmlem2		GIF version

Theorem 2lgsoddprmlem2 16139

Description: Lemma 2 for 2lgsoddprm . (Contributed by AV, 19-Jul-2021.)

**Assertion**
Ref	Expression
2lgsoddprmlem2	⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8)))

Proof of Theorem 2lgsoddprmlem2 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		8nn 9451	. . . . . 6 ⊢ 8 ∈ ℕ
2		nnq 10012	. . . . . 6 ⊢ (8 ∈ ℕ → 8 ∈ ℚ)
3	1, 2	ax-mp 5	. . . . 5 ⊢ 8 ∈ ℚ
4		8pos 9386	. . . . 5 ⊢ 0 < 8
5		eqcom 2240	. . . . . 6 ⊢ (𝑅 = (𝑁 mod 8) ↔ (𝑁 mod 8) = 𝑅)
6		modqmuladdim 10782	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 8 ∈ ℚ ∧ 0 < 8) → ((𝑁 mod 8) = 𝑅 → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)))
7	5, 6	biimtrid 152	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 8 ∈ ℚ ∧ 0 < 8) → (𝑅 = (𝑁 mod 8) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)))
8	3, 4, 7	mp3an23 1370	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑅 = (𝑁 mod 8) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)))
9	8	imp 124	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 = (𝑁 mod 8)) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))
10	9	3adant2 1047	. 2 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))
11		zcn 9628	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
12		8cn 9369	. . . . . . . . 9 ⊢ 8 ∈ ℂ
13	12	a1i 9	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → 8 ∈ ℂ)
14	11, 13	mulcomd 8337	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 · 8) = (8 · 𝑘))
15	14	adantl 277	. . . . . 6 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑘 · 8) = (8 · 𝑘))
16	15	oveq1d 6090	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 8) + 𝑅) = ((8 · 𝑘) + 𝑅))
17	16	eqeq2d 2250	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑁 = ((𝑘 · 8) + 𝑅) ↔ 𝑁 = ((8 · 𝑘) + 𝑅)))
18		simpr 110	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ)
19	18	adantr 276	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → 𝑘 ∈ ℤ)
20		id 19	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
21	1	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → 8 ∈ ℕ)
22	20, 21	zmodcld 10760	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 mod 8) ∈ ℕ₀)
23	22	nn0zd 9745	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (𝑁 mod 8) ∈ ℤ)
24	23	3ad2ant1 1049	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℤ)
25		eleq1 2301	. . . . . . . . . . . 12 ⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℤ ↔ (𝑁 mod 8) ∈ ℤ))
26	25	3ad2ant3 1051	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℤ ↔ (𝑁 mod 8) ∈ ℤ))
27	24, 26	mpbird 167	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℤ)
28	27	adantr 276	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → 𝑅 ∈ ℤ)
29	28	adantr 276	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → 𝑅 ∈ ℤ)
30		simpr 110	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → 𝑁 = ((8 · 𝑘) + 𝑅))
31		2lgsoddprmlem1 16138	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8)))
32	19, 29, 30, 31	syl3anc 1278	. . . . . . 7 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8)))
33	32	breq2d 4137	. . . . . 6 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8))))
34		2z 9651	. . . . . . 7 ⊢ 2 ∈ ℤ
35		simp1 1028	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑁 ∈ ℤ)
36	1	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 8 ∈ ℕ)
37	35, 36	zmodcld 10760	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℕ₀)
38	37	nn0red 9600	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℝ)
39		eleq1 2301	. . . . . . . . . . 11 ⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℝ ↔ (𝑁 mod 8) ∈ ℝ))
40	39	3ad2ant3 1051	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℝ ↔ (𝑁 mod 8) ∈ ℝ))
41	38, 40	mpbird 167	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℝ)
42		resqcl 11022	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
43		peano2rem 8583	. . . . . . . . . . 11 ⊢ ((𝑅↑2) ∈ ℝ → ((𝑅↑2) − 1) ∈ ℝ)
44	42, 43	syl 14	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → ((𝑅↑2) − 1) ∈ ℝ)
45		8re 9368	. . . . . . . . . . 11 ⊢ 8 ∈ ℝ
46	45	a1i 9	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → 8 ∈ ℝ)
47	45, 4	gt0ap0ii 8946	. . . . . . . . . . 11 ⊢ 8 # 0
48	47	a1i 9	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → 8 # 0)
49	44, 46, 48	redivclapd 9155	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ → (((𝑅↑2) − 1) / 8) ∈ ℝ)
50	41, 49	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (((𝑅↑2) − 1) / 8) ∈ ℝ)
51	50	adantr 276	. . . . . . 7 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (((𝑅↑2) − 1) / 8) ∈ ℝ)
52		eleq1 2301	. . . . . . . . . . . 12 ⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℕ₀ ↔ (𝑁 mod 8) ∈ ℕ₀))
53	52	3ad2ant3 1051	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℕ₀ ↔ (𝑁 mod 8) ∈ ℕ₀))
54	37, 53	mpbird 167	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℕ₀)
55		nn0z 9643	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℕ₀ → 𝑅 ∈ ℤ)
56	1	nnzi 9644	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℤ
57	56	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 8 ∈ ℤ)
58		zsqcl 11025	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (𝑘↑2) ∈ ℤ)
59	58	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘↑2) ∈ ℤ)
60	57, 59	zmulcld 9753	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8 · (𝑘↑2)) ∈ ℤ)
61	34	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∈ ℤ)
62		zmulcl 9677	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℤ)
63	62	ancoms 268	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℤ)
64	61, 63	zmulcld 9753	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · (𝑘 · 𝑅)) ∈ ℤ)
65	60, 64	zaddcld 9751	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ)
66		4z 9653	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℤ
67	66	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 4 ∈ ℤ)
68	67, 59	zmulcld 9753	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (4 · (𝑘↑2)) ∈ ℤ)
69	68, 63	zaddcld 9751	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((4 · (𝑘↑2)) + (𝑘 · 𝑅)) ∈ ℤ)
70		dvdsmul1 12558	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ ((4 · (𝑘↑2)) + (𝑘 · 𝑅)) ∈ ℤ) → 2 ∥ (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))))
71	34, 69, 70	sylancr 418	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∥ (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))))
72		4t2e8 9442	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 · 2) = 8
73		4cn 9361	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℂ
74		2cn 9354	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
75	73, 74	mulcomi 8322	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 · 2) = (2 · 4)
76	72, 75	eqtr3i 2261	. . . . . . . . . . . . . . . . . 18 ⊢ 8 = (2 · 4)
77	76	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 8 = (2 · 4))
78	77	oveq1d 6090	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8 · (𝑘↑2)) = ((2 · 4) · (𝑘↑2)))
79	74	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∈ ℂ)
80	73	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 4 ∈ ℂ)
81	58	zcnd 9748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℤ → (𝑘↑2) ∈ ℂ)
82	81	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘↑2) ∈ ℂ)
83	79, 80, 82	mulassd 8339	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((2 · 4) · (𝑘↑2)) = (2 · (4 · (𝑘↑2))))
84	78, 83	eqtrd 2271	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8 · (𝑘↑2)) = (2 · (4 · (𝑘↑2))))
85	84	oveq1d 6090	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) = ((2 · (4 · (𝑘↑2))) + (2 · (𝑘 · 𝑅))))
86	68	zcnd 9748	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (4 · (𝑘↑2)) ∈ ℂ)
87	62	zcnd 9748	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℂ)
88	87	ancoms 268	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℂ)
89	79, 86, 88	adddid 8340	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))) = ((2 · (4 · (𝑘↑2))) + (2 · (𝑘 · 𝑅))))
90	85, 89	eqtr4d 2274	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) = (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))))
91	71, 90	breqtrrd 4153	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))))
92	65, 91	jca 306	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅)))))
93	92	ex 115	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℤ → (𝑘 ∈ ℤ → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))))))
94	54, 55, 93	3syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑘 ∈ ℤ → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))))))
95	94	imp 124	. . . . . . . 8 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅)))))
96	95	adantr 276	. . . . . . 7 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅)))))
97		dvdsaddre2b 12586	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ (((𝑅↑2) − 1) / 8) ∈ ℝ ∧ (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ ∧ 2 ∥ ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))))) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 2 ∥ (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8))))
98	34, 51, 96, 97	mp3an2ani 1385	. . . . . 6 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑅↑2) − 1) / 8) ↔ 2 ∥ (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8))))
99	33, 98	bitr4d 191	. . . . 5 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8)))
100	99	ex 115	. . . 4 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑁 = ((8 · 𝑘) + 𝑅) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8))))
101	17, 100	sylbid 150	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑁 = ((𝑘 · 8) + 𝑅) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8))))
102	101	rexlimdva 2668	. 2 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8))))
103	10, 102	mpd 13	1 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((𝑅↑2) − 1) / 8)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ∃wrex 2529 class class class wbr 4125 (class class class)co 6075 ℂcc 8167 ℝcr 8168 0cc0 8169 1c1 8170 + caddc 8172 · cmul 8174 < clt 8350 − cmin 8487 # cap 8899 / cdiv 8992 ℕcn 9283 2c2 9334 4c4 9336 8c8 9340 ℕ₀cn0 9542 ℤcz 9623 ℚcq 9998 mod cmo 10737 ↑cexp 10953 ∥ cdvds 12532

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730 ax-cnex 8260 ax-resscn 8261 ax-1cn 8262 ax-1re 8263 ax-icn 8264 ax-addcl 8265 ax-addrcl 8266 ax-mulcl 8267 ax-mulrcl 8268 ax-addcom 8269 ax-mulcom 8270 ax-addass 8271 ax-mulass 8272 ax-distr 8273 ax-i2m1 8274 ax-0lt1 8275 ax-1rid 8276 ax-0id 8277 ax-rnegex 8278 ax-precex 8279 ax-cnre 8280 ax-pre-ltirr 8281 ax-pre-ltwlin 8282 ax-pre-lttrn 8283 ax-pre-apti 8284 ax-pre-ltadd 8285 ax-pre-mulgt0 8286 ax-pre-mulext 8287 ax-arch 8288

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3636 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-id 4433 df-po 4436 df-iso 4437 df-iord 4506 df-on 4508 df-ilim 4509 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-1st 6364 df-2nd 6365 df-recs 6566 df-frec 6652 df-pnf 8352 df-mnf 8353 df-xr 8354 df-ltxr 8355 df-le 8356 df-sub 8489 df-neg 8490 df-reap 8893 df-ap 8900 df-div 8993 df-inn 9284 df-2 9342 df-3 9343 df-4 9344 df-5 9345 df-6 9346 df-7 9347 df-8 9348 df-n0 9543 df-z 9624 df-uz 9901 df-q 9999 df-rp 10034 df-ico 10275 df-fl 10683 df-mod 10738 df-seqfrec 10863 df-exp 10954 df-dvds 12533

This theorem is referenced by: 2lgsoddprmlem4 16145

W3C validator