lgsval - Intuitionistic Logic Explorer

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

Theorem lgsval 13976

Description: Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)

**Hypothesis**
Ref	Expression
lgsval.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))

**Assertion**
Ref	Expression
lgsval	⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /_L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))

Distinct variable groups: 𝐴,𝑛 𝑛,𝑁 Allowed substitution hint: 𝐹(𝑛)

Proof of Theorem lgsval Dummy variables 𝑎 𝑚 𝑘 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1zzd 9253	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 1 ∈ ℤ)
2		0zd 9238	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ∈ ℤ)
3		zsqcl 10560	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
4	3	ad2antrr 488	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
5		zdceq 9301	. . . . 5 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
6	4, 1, 5	syl2anc 411	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → DECID (𝐴↑2) = 1)
7	1, 2, 6	ifcldcd 3567	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → if((𝐴↑2) = 1, 1, 0) ∈ ℤ)
8		neg1z 9258	. . . . . 6 ⊢ -1 ∈ ℤ
9	8	a1i 9	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → -1 ∈ ℤ)
10		1zzd 9253	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 1 ∈ ℤ)
11		simpr 110	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
12		0zd 9238	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 0 ∈ ℤ)
13		zdclt 9303	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
14	11, 12, 13	syl2an2r 595	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝑁 < 0)
15		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
16		zdclt 9303	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
17	15, 12, 16	syl2an2r 595	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝐴 < 0)
18		dcan2 934	. . . . . 6 ⊢ (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
19	14, 17, 18	sylc 62	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
20	9, 10, 19	ifcldcd 3567	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
21		nnuz 9536	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
22		lgsval.1	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
23		eleq1w 2236	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
24		eqeq1 2182	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑛 = 2 ↔ 𝑘 = 2))
25		oveq1 5872	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1))
26	25	oveq1d 5880	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑛 − 1) / 2) = ((𝑘 − 1) / 2))
27	26	oveq2d 5881	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (𝐴↑((𝑛 − 1) / 2)) = (𝐴↑((𝑘 − 1) / 2)))
28	27	oveq1d 5880	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → ((𝐴↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑘 − 1) / 2)) + 1))
29		id 19	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
30	28, 29	oveq12d 5883	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘))
31	30	oveq1d 5880	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))
32	24, 31	ifbieq2d 3556	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) = if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)))
33		oveq1 5872	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
34	32, 33	oveq12d 5883	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)) = (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)))
35	23, 34	ifbieq1d 3554	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1) = if(𝑘 ∈ ℙ, (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)), 1))
36		simpr 110	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
37		0zd 9238	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 0 ∈ ℤ)
38		1zzd 9253	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 1 ∈ ℤ)
39	38	znegcld 9350	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → -1 ∈ ℤ)
40		id 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ)
41		8nn 9059	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 ∈ ℕ
42	41	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 8 ∈ ℕ)
43	40, 42	zmodcld 10315	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ₀)
44	43	nn0zd 9346	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
45		1zzd 9253	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 1 ∈ ℤ)
46		zdceq 9301	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
47	44, 45, 46	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
48		7nn 9058	. . . . . . . . . . . . . . . . . 18 ⊢ 7 ∈ ℕ
49	48	nnzi 9247	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℤ
50		zdceq 9301	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
51	44, 49, 50	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 7)
52		dcor 935	. . . . . . . . . . . . . . . 16 ⊢ (DECID (𝐴 mod 8) = 1 → (DECID (𝐴 mod 8) = 7 → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
53	47, 51, 52	sylc 62	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℤ → DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7))
54		elprg 3609	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 mod 8) ∈ ℕ₀ → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
55	43, 54	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → ((𝐴 mod 8) ∈ {1, 7} ↔ ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
56	55	dcbid 838	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℤ → (DECID (𝐴 mod 8) ∈ {1, 7} ↔ DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
57	53, 56	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) ∈ {1, 7})
58	57	ad5antr 496	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID (𝐴 mod 8) ∈ {1, 7})
59	38, 39, 58	ifcldcd 3567	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ∈ ℤ)
60		2nn 9053	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
61	60	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 2 ∈ ℕ)
62		simp-5l 543	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 𝐴 ∈ ℤ)
63		dvdsdc 11773	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 2 ∥ 𝐴)
64	61, 62, 63	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID 2 ∥ 𝐴)
65	37, 59, 64	ifcldcd 3567	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) ∈ ℤ)
66		simp-5l 543	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝐴 ∈ ℤ)
67		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 𝑘 = 2)
68		prm2orodd 12093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → (𝑘 = 2 ∨ ¬ 2 ∥ 𝑘))
69	68	orcomd 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
70	69	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
71	67, 70	ecased 1349	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 2 ∥ 𝑘)
72		prmnn 12077	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
73	72	nnnn0d 9202	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ₀)
74		nn0oddm1d2 11881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ₀))
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ₀))
76	75	ad2antlr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ₀))
77	71, 76	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝑘 − 1) / 2) ∈ ℕ₀)
78		zexpcl 10505	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
79	66, 77, 78	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
80	79	peano2zd 9351	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝐴↑((𝑘 − 1) / 2)) + 1) ∈ ℤ)
81	36	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝑘 ∈ ℕ)
82	80, 81	zmodcld 10315	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℕ₀)
83	82	nn0zd 9346	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℤ)
84		1zzd 9253	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 1 ∈ ℤ)
85	83, 84	zsubcld 9353	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1) ∈ ℤ)
86		nnz 9245	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
87	86	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
88		2z 9254	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
89		zdceq 9301	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
90	87, 88, 89	sylancl 413	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → DECID 𝑘 = 2)
91	65, 85, 90	ifcldadc 3561	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)) ∈ ℤ)
92		simpr 110	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
93		simp-4r 542	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
94		neqne 2353	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 = 0 → 𝑁 ≠ 0)
95	94	ad3antlr 493	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
96		pczcl 12265	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
97	92, 93, 95, 96	syl12anc 1236	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
98		zexpcl 10505	. . . . . . . . . 10 ⊢ ((if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)) ∈ ℤ ∧ (𝑘 pCnt 𝑁) ∈ ℕ₀) → (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)) ∈ ℤ)
99	91, 97, 98	syl2anc 411	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)) ∈ ℤ)
100		1zzd 9253	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
101		prmdc 12097	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
102	101	adantl 277	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
103	99, 100, 102	ifcldadc 3561	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → if(𝑘 ∈ ℙ, (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)), 1) ∈ ℤ)
104	22, 35, 36, 103	fvmptd3 5601	. . . . . . 7 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)), 1))
105	104, 103	eqeltrd 2252	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℤ)
106		zmulcl 9279	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
107	106	adantl 277	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
108	21, 10, 105, 107	seqf 10431	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → seq1( · , 𝐹):ℕ⟶ℤ)
109		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ)
110	94	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
111		nnabscl 11077	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
112	109, 110, 111	syl2anc 411	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (abs‘𝑁) ∈ ℕ)
113	108, 112	ffvelcdmd 5644	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (seq1( · , 𝐹)‘(abs‘𝑁)) ∈ ℤ)
114	20, 113	zmulcld 9354	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) ∈ ℤ)
115		0zd 9238	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
116		zdceq 9301	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
117	11, 115, 116	syl2anc 411	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
118	7, 114, 117	ifcldadc 3561	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ)
119		simpr 110	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑚 = 𝑁)
120	119	eqeq1d 2184	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0))
121		simpl 109	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑎 = 𝐴)
122	121	oveq1d 5880	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2))
123	122	eqeq1d 2184	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1))
124	123	ifbid 3553	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0))
125	119	breq1d 4008	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0))
126	121	breq1d 4008	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0))
127	125, 126	anbi12d 473	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
128	127	ifbid 3553	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
129	121	breq2d 4010	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴))
130	121	oveq1d 5880	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8))
131	130	eleq1d 2244	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
132	131	ifbid 3553	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
133	129, 132	ifbieq2d 3556	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
134	121	oveq1d 5880	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2)))
135	134	oveq1d 5880	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1))
136	135	oveq1d 5880	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛))
137	136	oveq1d 5880	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))
138	133, 137	ifeq12d 3551	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) = if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)))
139	119	oveq2d 5881	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁))
140	138, 139	oveq12d 5883	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)) = (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)))
141	140	ifeq1d 3549	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1) = if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
142	141	mpteq2dv 4089	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)))
143	142, 22	eqtr4di 2226	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹)
144	143	seqeq3d 10423	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1))) = seq1( · , 𝐹))
145	119	fveq2d 5511	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁))
146	144, 145	fveq12d 5514	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)) = (seq1( · , 𝐹)‘(abs‘𝑁)))
147	128, 146	oveq12d 5883	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚))) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
148	120, 124, 147	ifbieq12d 3558	. . 3 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
149		df-lgs 13970	. . 3 ⊢ /_L = (𝑎 ∈ ℤ, 𝑚 ∈ ℤ ↦ if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))))
150	148, 149	ovmpoga 5994	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ) → (𝐴 /_L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
151	118, 150	mpd3an3 1338	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /_L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 DECID wdc 834 = wceq 1353 ∈ wcel 2146 ≠ wne 2345 ifcif 3532 {cpr 3590 class class class wbr 3998 ↦ cmpt 4059 ‘cfv 5208 (class class class)co 5865 0cc0 7786 1c1 7787 + caddc 7789 · cmul 7791 < clt 7966 − cmin 8102 -cneg 8103 / cdiv 8602 ℕcn 8892 2c2 8943 7c7 8948 8c8 8949 ℕ₀cn0 9149 ℤcz 9226 mod cmo 10292 seqcseq 10415 ↑cexp 10489 abscabs 10974 ∥ cdvds 11762 ℙcprime 12074 pCnt cpc 12251 /_L clgs 13969

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 614 ax-in2 615 ax-io 709 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-13 2148 ax-14 2149 ax-ext 2157 ax-coll 4113 ax-sep 4116 ax-nul 4124 ax-pow 4169 ax-pr 4203 ax-un 4427 ax-setind 4530 ax-iinf 4581 ax-cnex 7877 ax-resscn 7878 ax-1cn 7879 ax-1re 7880 ax-icn 7881 ax-addcl 7882 ax-addrcl 7883 ax-mulcl 7884 ax-mulrcl 7885 ax-addcom 7886 ax-mulcom 7887 ax-addass 7888 ax-mulass 7889 ax-distr 7890 ax-i2m1 7891 ax-0lt1 7892 ax-1rid 7893 ax-0id 7894 ax-rnegex 7895 ax-precex 7896 ax-cnre 7897 ax-pre-ltirr 7898 ax-pre-ltwlin 7899 ax-pre-lttrn 7900 ax-pre-apti 7901 ax-pre-ltadd 7902 ax-pre-mulgt0 7903 ax-pre-mulext 7904 ax-arch 7905 ax-caucvg 7906

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-xor 1376 df-nf 1459 df-sb 1761 df-eu 2027 df-mo 2028 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ne 2346 df-nel 2441 df-ral 2458 df-rex 2459 df-reu 2460 df-rmo 2461 df-rab 2462 df-v 2737 df-sbc 2961 df-csb 3056 df-dif 3129 df-un 3131 df-in 3133 df-ss 3140 df-nul 3421 df-if 3533 df-pw 3574 df-sn 3595 df-pr 3596 df-op 3598 df-uni 3806 df-int 3841 df-iun 3884 df-br 3999 df-opab 4060 df-mpt 4061 df-tr 4097 df-id 4287 df-po 4290 df-iso 4291 df-iord 4360 df-on 4362 df-ilim 4363 df-suc 4365 df-iom 4584 df-xp 4626 df-rel 4627 df-cnv 4628 df-co 4629 df-dm 4630 df-rn 4631 df-res 4632 df-ima 4633 df-iota 5170 df-fun 5210 df-fn 5211 df-f 5212 df-f1 5213 df-fo 5214 df-f1o 5215 df-fv 5216 df-isom 5217 df-riota 5821 df-ov 5868 df-oprab 5869 df-mpo 5870 df-1st 6131 df-2nd 6132 df-recs 6296 df-frec 6382 df-1o 6407 df-2o 6408 df-er 6525 df-en 6731 df-fin 6733 df-sup 6973 df-inf 6974 df-pnf 7968 df-mnf 7969 df-xr 7970 df-ltxr 7971 df-le 7972 df-sub 8104 df-neg 8105 df-reap 8506 df-ap 8513 df-div 8603 df-inn 8893 df-2 8951 df-3 8952 df-4 8953 df-5 8954 df-6 8955 df-7 8956 df-8 8957 df-n0 9150 df-z 9227 df-uz 9502 df-q 9593 df-rp 9625 df-fz 9980 df-fzo 10113 df-fl 10240 df-mod 10293 df-seqfrec 10416 df-exp 10490 df-cj 10819 df-re 10820 df-im 10821 df-rsqrt 10975 df-abs 10976 df-dvds 11763 df-gcd 11911 df-prm 12075 df-pc 12252 df-lgs 13970

This theorem is referenced by: lgscllem 13979 lgsval2lem 13982 lgs0 13985 lgsval4 13992

W3C validator