2lgsoddprmlem2 - Intuitionistic Logic Explorer

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

Theorem 2lgsoddprmlem2 15501

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 9186	. . . . . 6 ⊢ 8 ∈ ℕ
2		nnq 9736	. . . . . 6 ⊢ (8 ∈ ℕ → 8 ∈ ℚ)
3	1, 2	ax-mp 5	. . . . 5 ⊢ 8 ∈ ℚ
4		8pos 9121	. . . . 5 ⊢ 0 < 8
5		eqcom 2206	. . . . . 6 ⊢ (𝑅 = (𝑁 mod 8) ↔ (𝑁 mod 8) = 𝑅)
6		modqmuladdim 10493	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 8 ∈ ℚ ∧ 0 < 8) → ((𝑁 mod 8) = 𝑅 → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)))
7	5, 6	biimtrid 152	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∧ 8 ∈ ℚ ∧ 0 < 8) → (𝑅 = (𝑁 mod 8) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)))
8	3, 4, 7	mp3an23 1341	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑅 = (𝑁 mod 8) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅)))
9	8	imp 124	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 𝑅 = (𝑁 mod 8)) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))
10	9	3adant2 1018	. 2 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → ∃𝑘 ∈ ℤ 𝑁 = ((𝑘 · 8) + 𝑅))
11		zcn 9359	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
12		8cn 9104	. . . . . . . . 9 ⊢ 8 ∈ ℂ
13	12	a1i 9	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → 8 ∈ ℂ)
14	11, 13	mulcomd 8076	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 · 8) = (8 · 𝑘))
15	14	adantl 277	. . . . . 6 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → (𝑘 · 8) = (8 · 𝑘))
16	15	oveq1d 5949	. . . . 5 ⊢ (((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) → ((𝑘 · 8) + 𝑅) = ((8 · 𝑘) + 𝑅))
17	16	eqeq2d 2216	. . . 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 10471	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁 mod 8) ∈ ℕ₀)
23	22	nn0zd 9475	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (𝑁 mod 8) ∈ ℤ)
24	23	3ad2ant1 1020	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℤ)
25		eleq1 2267	. . . . . . . . . . . 12 ⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℤ ↔ (𝑁 mod 8) ∈ ℤ))
26	25	3ad2ant3 1022	. . . . . . . . . . 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 15500	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8)))
32	19, 29, 30, 31	syl3anc 1249	. . . . . . 7 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (((𝑁↑2) − 1) / 8) = (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8)))
33	32	breq2d 4055	. . . . . 6 ⊢ ((((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) ∧ 𝑘 ∈ ℤ) ∧ 𝑁 = ((8 · 𝑘) + 𝑅)) → (2 ∥ (((𝑁↑2) − 1) / 8) ↔ 2 ∥ (((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) + (((𝑅↑2) − 1) / 8))))
34		2z 9382	. . . . . . 7 ⊢ 2 ∈ ℤ
35		simp1 999	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑁 ∈ ℤ)
36	1	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 8 ∈ ℕ)
37	35, 36	zmodcld 10471	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℕ₀)
38	37	nn0red 9331	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑁 mod 8) ∈ ℝ)
39		eleq1 2267	. . . . . . . . . . 11 ⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℝ ↔ (𝑁 mod 8) ∈ ℝ))
40	39	3ad2ant3 1022	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℝ ↔ (𝑁 mod 8) ∈ ℝ))
41	38, 40	mpbird 167	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℝ)
42		resqcl 10733	. . . . . . . . . . 11 ⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
43		peano2rem 8321	. . . . . . . . . . 11 ⊢ ((𝑅↑2) ∈ ℝ → ((𝑅↑2) − 1) ∈ ℝ)
44	42, 43	syl 14	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → ((𝑅↑2) − 1) ∈ ℝ)
45		8re 9103	. . . . . . . . . . 11 ⊢ 8 ∈ ℝ
46	45	a1i 9	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → 8 ∈ ℝ)
47	45, 4	gt0ap0ii 8683	. . . . . . . . . . 11 ⊢ 8 # 0
48	47	a1i 9	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℝ → 8 # 0)
49	44, 46, 48	redivclapd 8890	. . . . . . . . 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 2267	. . . . . . . . . . . 12 ⊢ (𝑅 = (𝑁 mod 8) → (𝑅 ∈ ℕ₀ ↔ (𝑁 mod 8) ∈ ℕ₀))
53	52	3ad2ant3 1022	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → (𝑅 ∈ ℕ₀ ↔ (𝑁 mod 8) ∈ ℕ₀))
54	37, 53	mpbird 167	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = (𝑁 mod 8)) → 𝑅 ∈ ℕ₀)
55		nn0z 9374	. . . . . . . . . 10 ⊢ (𝑅 ∈ ℕ₀ → 𝑅 ∈ ℤ)
56	1	nnzi 9375	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℤ
57	56	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 8 ∈ ℤ)
58		zsqcl 10736	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → (𝑘↑2) ∈ ℤ)
59	58	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘↑2) ∈ ℤ)
60	57, 59	zmulcld 9483	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8 · (𝑘↑2)) ∈ ℤ)
61	34	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∈ ℤ)
62		zmulcl 9408	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℤ)
63	62	ancoms 268	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℤ)
64	61, 63	zmulcld 9483	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · (𝑘 · 𝑅)) ∈ ℤ)
65	60, 64	zaddcld 9481	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) ∈ ℤ)
66		4z 9384	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℤ
67	66	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 4 ∈ ℤ)
68	67, 59	zmulcld 9483	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (4 · (𝑘↑2)) ∈ ℤ)
69	68, 63	zaddcld 9481	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((4 · (𝑘↑2)) + (𝑘 · 𝑅)) ∈ ℤ)
70		dvdsmul1 12043	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ ((4 · (𝑘↑2)) + (𝑘 · 𝑅)) ∈ ℤ) → 2 ∥ (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))))
71	34, 69, 70	sylancr 414	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∥ (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))))
72		4t2e8 9177	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 · 2) = 8
73		4cn 9096	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℂ
74		2cn 9089	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
75	73, 74	mulcomi 8060	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 · 2) = (2 · 4)
76	72, 75	eqtr3i 2227	. . . . . . . . . . . . . . . . . 18 ⊢ 8 = (2 · 4)
77	76	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 8 = (2 · 4))
78	77	oveq1d 5949	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8 · (𝑘↑2)) = ((2 · 4) · (𝑘↑2)))
79	74	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 2 ∈ ℂ)
80	73	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → 4 ∈ ℂ)
81	58	zcnd 9478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℤ → (𝑘↑2) ∈ ℂ)
82	81	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘↑2) ∈ ℂ)
83	79, 80, 82	mulassd 8078	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((2 · 4) · (𝑘↑2)) = (2 · (4 · (𝑘↑2))))
84	78, 83	eqtrd 2237	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (8 · (𝑘↑2)) = (2 · (4 · (𝑘↑2))))
85	84	oveq1d 5949	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) = ((2 · (4 · (𝑘↑2))) + (2 · (𝑘 · 𝑅))))
86	68	zcnd 9478	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (4 · (𝑘↑2)) ∈ ℂ)
87	62	zcnd 9478	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℂ)
88	87	ancoms 268	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑅) ∈ ℂ)
89	79, 86, 88	adddid 8079	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))) = ((2 · (4 · (𝑘↑2))) + (2 · (𝑘 · 𝑅))))
90	85, 89	eqtr4d 2240	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((8 · (𝑘↑2)) + (2 · (𝑘 · 𝑅))) = (2 · ((4 · (𝑘↑2)) + (𝑘 · 𝑅))))
91	71, 90	breqtrrd 4071	. . . . . . . . . . . 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 12071	. . . . . . 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 1356	. . . . . 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 2622	. 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 980 = wceq 1372 ∈ wcel 2175 ∃wrex 2484 class class class wbr 4043 (class class class)co 5934 ℂcc 7905 ℝcr 7906 0cc0 7907 1c1 7908 + caddc 7910 · cmul 7912 < clt 8089 − cmin 8225 # cap 8636 / cdiv 8727 ℕcn 9018 2c2 9069 4c4 9071 8c8 9075 ℕ₀cn0 9277 ℤcz 9354 ℚcq 9722 mod cmo 10448 ↑cexp 10664 ∥ cdvds 12017

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 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4478 ax-setind 4583 ax-iinf 4634 ax-cnex 7998 ax-resscn 7999 ax-1cn 8000 ax-1re 8001 ax-icn 8002 ax-addcl 8003 ax-addrcl 8004 ax-mulcl 8005 ax-mulrcl 8006 ax-addcom 8007 ax-mulcom 8008 ax-addass 8009 ax-mulass 8010 ax-distr 8011 ax-i2m1 8012 ax-0lt1 8013 ax-1rid 8014 ax-0id 8015 ax-rnegex 8016 ax-precex 8017 ax-cnre 8018 ax-pre-ltirr 8019 ax-pre-ltwlin 8020 ax-pre-lttrn 8021 ax-pre-apti 8022 ax-pre-ltadd 8023 ax-pre-mulgt0 8024 ax-pre-mulext 8025 ax-arch 8026

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-reu 2490 df-rmo 2491 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-if 3571 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4338 df-po 4341 df-iso 4342 df-iord 4411 df-on 4413 df-ilim 4414 df-suc 4416 df-iom 4637 df-xp 4679 df-rel 4680 df-cnv 4681 df-co 4682 df-dm 4683 df-rn 4684 df-res 4685 df-ima 4686 df-iota 5229 df-fun 5270 df-fn 5271 df-f 5272 df-f1 5273 df-fo 5274 df-f1o 5275 df-fv 5276 df-riota 5889 df-ov 5937 df-oprab 5938 df-mpo 5939 df-1st 6216 df-2nd 6217 df-recs 6381 df-frec 6467 df-pnf 8091 df-mnf 8092 df-xr 8093 df-ltxr 8094 df-le 8095 df-sub 8227 df-neg 8228 df-reap 8630 df-ap 8637 df-div 8728 df-inn 9019 df-2 9077 df-3 9078 df-4 9079 df-5 9080 df-6 9081 df-7 9082 df-8 9083 df-n0 9278 df-z 9355 df-uz 9631 df-q 9723 df-rp 9758 df-ico 9998 df-fl 10394 df-mod 10449 df-seqfrec 10574 df-exp 10665 df-dvds 12018

This theorem is referenced by: 2lgsoddprmlem4 15507

W3C validator