lgsval - Intuitionistic Logic Explorer

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

Theorem lgsval 15739

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 9506	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 1 ∈ ℤ)
2		0zd 9491	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ∈ ℤ)
3		zsqcl 10873	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
4	3	ad2antrr 488	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
5		zdceq 9555	. . . . 5 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
6	4, 1, 5	syl2anc 411	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → DECID (𝐴↑2) = 1)
7	1, 2, 6	ifcldcd 3643	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → if((𝐴↑2) = 1, 1, 0) ∈ ℤ)
8		neg1z 9511	. . . . . 6 ⊢ -1 ∈ ℤ
9	8	a1i 9	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → -1 ∈ ℤ)
10		1zzd 9506	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 1 ∈ ℤ)
11		simpr 110	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
12		0zd 9491	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 0 ∈ ℤ)
13		zdclt 9557	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
14	11, 12, 13	syl2an2r 599	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝑁 < 0)
15		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
16		zdclt 9557	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
17	15, 12, 16	syl2an2r 599	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝐴 < 0)
18		dcan2 942	. . . . . 6 ⊢ (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
19	14, 17, 18	sylc 62	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
20	9, 10, 19	ifcldcd 3643	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
21		nnuz 9792	. . . . . 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 2292	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
24		eqeq1 2238	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑛 = 2 ↔ 𝑘 = 2))
25		oveq1 6025	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1))
26	25	oveq1d 6033	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑛 − 1) / 2) = ((𝑘 − 1) / 2))
27	26	oveq2d 6034	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (𝐴↑((𝑛 − 1) / 2)) = (𝐴↑((𝑘 − 1) / 2)))
28	27	oveq1d 6033	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → ((𝐴↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑘 − 1) / 2)) + 1))
29		id 19	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
30	28, 29	oveq12d 6036	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘))
31	30	oveq1d 6033	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))
32	24, 31	ifbieq2d 3630	. . . . . . . . . 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 6025	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
34	32, 33	oveq12d 6036	. . . . . . . . 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 3628	. . . . . . . 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 9491	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 0 ∈ ℤ)
38		1zzd 9506	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 1 ∈ ℤ)
39	38	znegcld 9604	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → -1 ∈ ℤ)
40		id 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ)
41		8nn 9311	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 ∈ ℕ
42	41	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 8 ∈ ℕ)
43	40, 42	zmodcld 10608	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ₀)
44	43	nn0zd 9600	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
45		1zzd 9506	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 1 ∈ ℤ)
46		zdceq 9555	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
47	44, 45, 46	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
48		7nn 9310	. . . . . . . . . . . . . . . . . 18 ⊢ 7 ∈ ℕ
49	48	nnzi 9500	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℤ
50		zdceq 9555	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
51	44, 49, 50	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 7)
52		dcor 943	. . . . . . . . . . . . . . . 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 3689	. . . . . . . . . . . . . . . . 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 845	. . . . . . . . . . . . . . 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 3643	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ∈ ℤ)
60		2nn 9305	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
61	60	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 2 ∈ ℕ)
62		simp-5l 545	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 𝐴 ∈ ℤ)
63		dvdsdc 12364	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 2 ∥ 𝐴)
64	61, 62, 63	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID 2 ∥ 𝐴)
65	37, 59, 64	ifcldcd 3643	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)) ∈ ℤ)
66		simp-5l 545	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝐴 ∈ ℤ)
67		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 𝑘 = 2)
68		prm2orodd 12703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → (𝑘 = 2 ∨ ¬ 2 ∥ 𝑘))
69	68	orcomd 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
70	69	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
71	67, 70	ecased 1385	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 2 ∥ 𝑘)
72		prmnn 12687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
73	72	nnnn0d 9455	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ₀)
74		nn0oddm1d2 12475	. . . . . . . . . . . . . . . . . . 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 10817	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
79	66, 77, 78	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
80	79	peano2zd 9605	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝐴↑((𝑘 − 1) / 2)) + 1) ∈ ℤ)
81	36	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝑘 ∈ ℕ)
82	80, 81	zmodcld 10608	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℕ₀)
83	82	nn0zd 9600	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℤ)
84		1zzd 9506	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 1 ∈ ℤ)
85	83, 84	zsubcld 9607	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1) ∈ ℤ)
86		nnz 9498	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
87	86	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
88		2z 9507	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
89		zdceq 9555	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
90	87, 88, 89	sylancl 413	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → DECID 𝑘 = 2)
91	65, 85, 90	ifcldadc 3635	. . . . . . . . . 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 544	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ∈ ℤ)
94		neqne 2410	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 = 0 → 𝑁 ≠ 0)
95	94	ad3antlr 493	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
96		pczcl 12876	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
97	92, 93, 95, 96	syl12anc 1271	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
98		zexpcl 10817	. . . . . . . . . 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 9506	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
101		prmdc 12707	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
102	101	adantl 277	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
103	99, 100, 102	ifcldadc 3635	. . . . . . . 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 5740	. . . . . . 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 2308	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℤ)
106		zmulcl 9533	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
107	106	adantl 277	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
108	21, 10, 105, 107	seqf 10727	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → seq1( · , 𝐹):ℕ⟶ℤ)
109		simplr 529	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ)
110	94	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
111		nnabscl 11665	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
112	109, 110, 111	syl2anc 411	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (abs‘𝑁) ∈ ℕ)
113	108, 112	ffvelcdmd 5783	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (seq1( · , 𝐹)‘(abs‘𝑁)) ∈ ℤ)
114	20, 113	zmulcld 9608	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) ∈ ℤ)
115		0zd 9491	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
116		zdceq 9555	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
117	11, 115, 116	syl2anc 411	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
118	7, 114, 117	ifcldadc 3635	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ)
119		simpr 110	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑚 = 𝑁)
120	119	eqeq1d 2240	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0))
121		simpl 109	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑎 = 𝐴)
122	121	oveq1d 6033	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2))
123	122	eqeq1d 2240	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1))
124	123	ifbid 3627	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0))
125	119	breq1d 4098	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0))
126	121	breq1d 4098	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0))
127	125, 126	anbi12d 473	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
128	127	ifbid 3627	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
129	121	breq2d 4100	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴))
130	121	oveq1d 6033	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8))
131	130	eleq1d 2300	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
132	131	ifbid 3627	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
133	129, 132	ifbieq2d 3630	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
134	121	oveq1d 6033	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2)))
135	134	oveq1d 6033	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1))
136	135	oveq1d 6033	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛))
137	136	oveq1d 6033	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))
138	133, 137	ifeq12d 3625	. . . . . . . . . . 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 6034	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁))
140	138, 139	oveq12d 6036	. . . . . . . . . 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 3623	. . . . . . . . 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 4180	. . . . . . . 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 2282	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹)
144	143	seqeq3d 10718	. . . . . 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 5643	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁))
146	144, 145	fveq12d 5646	. . . . 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 6036	. . . 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 3632	. . 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 15733	. . 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 6151	. 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 1374	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 715 DECID wdc 841 = wceq 1397 ∈ wcel 2202 ≠ wne 2402 ifcif 3605 {cpr 3670 class class class wbr 4088 ↦ cmpt 4150 ‘cfv 5326 (class class class)co 6018 0cc0 8032 1c1 8033 + caddc 8035 · cmul 8037 < clt 8214 − cmin 8350 -cneg 8351 / cdiv 8852 ℕcn 9143 2c2 9194 7c7 9199 8c8 9200 ℕ₀cn0 9402 ℤcz 9479 mod cmo 10585 seqcseq 10710 ↑cexp 10801 abscabs 11562 ∥ cdvds 12353 ℙcprime 12684 pCnt cpc 12862 /_L clgs 15732

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8123 ax-resscn 8124 ax-1cn 8125 ax-1re 8126 ax-icn 8127 ax-addcl 8128 ax-addrcl 8129 ax-mulcl 8130 ax-mulrcl 8131 ax-addcom 8132 ax-mulcom 8133 ax-addass 8134 ax-mulass 8135 ax-distr 8136 ax-i2m1 8137 ax-0lt1 8138 ax-1rid 8139 ax-0id 8140 ax-rnegex 8141 ax-precex 8142 ax-cnre 8143 ax-pre-ltirr 8144 ax-pre-ltwlin 8145 ax-pre-lttrn 8146 ax-pre-apti 8147 ax-pre-ltadd 8148 ax-pre-mulgt0 8149 ax-pre-mulext 8150 ax-arch 8151 ax-caucvg 8152

This theorem depends on definitions: df-bi 117 df-stab 838 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-xor 1420 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5971 df-ov 6021 df-oprab 6022 df-mpo 6023 df-1st 6303 df-2nd 6304 df-recs 6471 df-frec 6557 df-1o 6582 df-2o 6583 df-er 6702 df-en 6910 df-fin 6912 df-sup 7183 df-inf 7184 df-pnf 8216 df-mnf 8217 df-xr 8218 df-ltxr 8219 df-le 8220 df-sub 8352 df-neg 8353 df-reap 8755 df-ap 8762 df-div 8853 df-inn 9144 df-2 9202 df-3 9203 df-4 9204 df-5 9205 df-6 9206 df-7 9207 df-8 9208 df-n0 9403 df-z 9480 df-uz 9756 df-q 9854 df-rp 9889 df-fz 10244 df-fzo 10378 df-fl 10531 df-mod 10586 df-seqfrec 10711 df-exp 10802 df-cj 11407 df-re 11408 df-im 11409 df-rsqrt 11563 df-abs 11564 df-dvds 12354 df-gcd 12530 df-prm 12685 df-pc 12863 df-lgs 15733

This theorem is referenced by: lgscllem 15742 lgsval2lem 15745 lgs0 15748 lgsval4 15755

W3C validator