lgsval - Intuitionistic Logic Explorer

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

Theorem lgsval 13699

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 9239	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 1 ∈ ℤ)
2		0zd 9224	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ∈ ℤ)
3		zsqcl 10546	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
4	3	ad2antrr 485	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
5		zdceq 9287	. . . . 5 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
6	4, 1, 5	syl2anc 409	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → DECID (𝐴↑2) = 1)
7	1, 2, 6	ifcldcd 3561	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → if((𝐴↑2) = 1, 1, 0) ∈ ℤ)
8		neg1z 9244	. . . . . 6 ⊢ -1 ∈ ℤ
9	8	a1i 9	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → -1 ∈ ℤ)
10		1zzd 9239	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 1 ∈ ℤ)
11		simpr 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
12		0zd 9224	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 0 ∈ ℤ)
13		zdclt 9289	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
14	11, 12, 13	syl2an2r 590	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝑁 < 0)
15		simpl 108	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
16		zdclt 9289	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
17	15, 12, 16	syl2an2r 590	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝐴 < 0)
18		dcan2 929	. . . . . 6 ⊢ (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
19	14, 17, 18	sylc 62	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
20	9, 10, 19	ifcldcd 3561	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
21		nnuz 9522	. . . . . 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 2231	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
24		eqeq1 2177	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑛 = 2 ↔ 𝑘 = 2))
25		oveq1 5860	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1))
26	25	oveq1d 5868	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑛 − 1) / 2) = ((𝑘 − 1) / 2))
27	26	oveq2d 5869	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (𝐴↑((𝑛 − 1) / 2)) = (𝐴↑((𝑘 − 1) / 2)))
28	27	oveq1d 5868	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → ((𝐴↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑘 − 1) / 2)) + 1))
29		id 19	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
30	28, 29	oveq12d 5871	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘))
31	30	oveq1d 5868	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))
32	24, 31	ifbieq2d 3550	. . . . . . . . . 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 5860	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
34	32, 33	oveq12d 5871	. . . . . . . . 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 3548	. . . . . . . 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 109	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
37		0zd 9224	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 0 ∈ ℤ)
38		1zzd 9239	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 1 ∈ ℤ)
39	38	znegcld 9336	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → -1 ∈ ℤ)
40		id 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ)
41		8nn 9045	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 ∈ ℕ
42	41	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 8 ∈ ℕ)
43	40, 42	zmodcld 10301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ₀)
44	43	nn0zd 9332	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
45		1zzd 9239	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 1 ∈ ℤ)
46		zdceq 9287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
47	44, 45, 46	syl2anc 409	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
48		7nn 9044	. . . . . . . . . . . . . . . . . 18 ⊢ 7 ∈ ℕ
49	48	nnzi 9233	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℤ
50		zdceq 9287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
51	44, 49, 50	sylancl 411	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 7)
52		dcor 930	. . . . . . . . . . . . . . . 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 3603	. . . . . . . . . . . . . . . . 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 833	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℤ → (DECID (𝐴 mod 8) ∈ {1, 7} ↔ DECID ((𝐴 mod 8) = 1 ∨ (𝐴 mod 8) = 7)))
57	53, 56	mpbird 166	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) ∈ {1, 7})
58	57	ad5antr 493	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID (𝐴 mod 8) ∈ {1, 7})
59	38, 39, 58	ifcldcd 3561	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ∈ ℤ)
60		2nn 9039	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
61	60	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 2 ∈ ℕ)
62		simp-5l 538	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 𝐴 ∈ ℤ)
63		dvdsdc 11760	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 2 ∥ 𝐴)
64	61, 62, 63	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID 2 ∥ 𝐴)
65	37, 59, 64	ifcldcd 3561	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) ∈ ℤ)
66		simp-5l 538	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝐴 ∈ ℤ)
67		simpr 109	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 𝑘 = 2)
68		prm2orodd 12080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → (𝑘 = 2 ∨ ¬ 2 ∥ 𝑘))
69	68	orcomd 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
70	69	ad2antlr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
71	67, 70	ecased 1344	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 2 ∥ 𝑘)
72		prmnn 12064	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
73	72	nnnn0d 9188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ₀)
74		nn0oddm1d2 11868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ₀))
75	73, 74	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ₀))
76	75	ad2antlr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ↔ ((𝑘 − 1) / 2) ∈ ℕ₀))
77	71, 76	mpbid 146	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝑘 − 1) / 2) ∈ ℕ₀)
78		zexpcl 10491	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
79	66, 77, 78	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
80	79	peano2zd 9337	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝐴↑((𝑘 − 1) / 2)) + 1) ∈ ℤ)
81	36	ad2antrr 485	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝑘 ∈ ℕ)
82	80, 81	zmodcld 10301	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℕ₀)
83	82	nn0zd 9332	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℤ)
84		1zzd 9239	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 1 ∈ ℤ)
85	83, 84	zsubcld 9339	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1) ∈ ℤ)
86		nnz 9231	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
87	86	ad2antlr 486	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
88		2z 9240	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
89		zdceq 9287	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
90	87, 88, 89	sylancl 411	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → DECID 𝑘 = 2)
91	65, 85, 90	ifcldadc 3555	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1)) ∈ ℤ)
92		simpr 109	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
93		simp-4r 537	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
94		neqne 2348	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 = 0 → 𝑁 ≠ 0)
95	94	ad3antlr 490	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
96		pczcl 12252	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
97	92, 93, 95, 96	syl12anc 1231	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
98		zexpcl 10491	. . . . . . . . . 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 409	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (if(𝑘 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))↑(𝑘 pCnt 𝑁)) ∈ ℤ)
100		1zzd 9239	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
101		prmdc 12084	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
102	101	adantl 275	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
103	99, 100, 102	ifcldadc 3555	. . . . . . . 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 5589	. . . . . . 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 2247	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℤ)
106		zmulcl 9265	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
107	106	adantl 275	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
108	21, 10, 105, 107	seqf 10417	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → seq1( · , 𝐹):ℕ⟶ℤ)
109		simplr 525	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ)
110	94	adantl 275	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
111		nnabscl 11064	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
112	109, 110, 111	syl2anc 409	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (abs‘𝑁) ∈ ℕ)
113	108, 112	ffvelrnd 5632	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (seq1( · , 𝐹)‘(abs‘𝑁)) ∈ ℤ)
114	20, 113	zmulcld 9340	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) ∈ ℤ)
115		0zd 9224	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
116		zdceq 9287	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
117	11, 115, 116	syl2anc 409	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
118	7, 114, 117	ifcldadc 3555	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ)
119		simpr 109	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑚 = 𝑁)
120	119	eqeq1d 2179	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0))
121		simpl 108	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑎 = 𝐴)
122	121	oveq1d 5868	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2))
123	122	eqeq1d 2179	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1))
124	123	ifbid 3547	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0))
125	119	breq1d 3999	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0))
126	121	breq1d 3999	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0))
127	125, 126	anbi12d 470	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
128	127	ifbid 3547	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
129	121	breq2d 4001	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴))
130	121	oveq1d 5868	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8))
131	130	eleq1d 2239	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
132	131	ifbid 3547	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
133	129, 132	ifbieq2d 3550	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
134	121	oveq1d 5868	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2)))
135	134	oveq1d 5868	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1))
136	135	oveq1d 5868	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛))
137	136	oveq1d 5868	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))
138	133, 137	ifeq12d 3545	. . . . . . . . . . 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 5869	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁))
140	138, 139	oveq12d 5871	. . . . . . . . . 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 3543	. . . . . . . . 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 4080	. . . . . . . 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 2221	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹)
144	143	seqeq3d 10409	. . . . . 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 5500	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁))
146	144, 145	fveq12d 5503	. . . . 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 5871	. . . 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 3552	. . 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 13693	. . 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 5982	. 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 1333	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 103 ↔ wb 104 ∨ wo 703 DECID wdc 829 = wceq 1348 ∈ wcel 2141 ≠ wne 2340 ifcif 3526 {cpr 3584 class class class wbr 3989 ↦ cmpt 4050 ‘cfv 5198 (class class class)co 5853 0cc0 7774 1c1 7775 + caddc 7777 · cmul 7779 < clt 7954 − cmin 8090 -cneg 8091 / cdiv 8589 ℕcn 8878 2c2 8929 7c7 8934 8c8 8935 ℕ₀cn0 9135 ℤcz 9212 mod cmo 10278 seqcseq 10401 ↑cexp 10475 abscabs 10961 ∥ cdvds 11749 ℙcprime 12061 pCnt cpc 12238 /_L clgs 13692

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-xor 1371 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-1o 6395 df-2o 6396 df-er 6513 df-en 6719 df-fin 6721 df-sup 6961 df-inf 6962 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-5 8940 df-6 8941 df-7 8942 df-8 8943 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-fz 9966 df-fzo 10099 df-fl 10226 df-mod 10279 df-seqfrec 10402 df-exp 10476 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-dvds 11750 df-gcd 11898 df-prm 12062 df-pc 12239 df-lgs 13693

This theorem is referenced by: lgscllem 13702 lgsval2lem 13705 lgs0 13708 lgsval4 13715

W3C validator