lgsval - Intuitionistic Logic Explorer

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

Theorem lgsval 15245

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 9353	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 1 ∈ ℤ)
2		0zd 9338	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → 0 ∈ ℤ)
3		zsqcl 10702	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
4	3	ad2antrr 488	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → (𝐴↑2) ∈ ℤ)
5		zdceq 9401	. . . . 5 ⊢ (((𝐴↑2) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴↑2) = 1)
6	4, 1, 5	syl2anc 411	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → DECID (𝐴↑2) = 1)
7	1, 2, 6	ifcldcd 3597	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 = 0) → if((𝐴↑2) = 1, 1, 0) ∈ ℤ)
8		neg1z 9358	. . . . . 6 ⊢ -1 ∈ ℤ
9	8	a1i 9	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → -1 ∈ ℤ)
10		1zzd 9353	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 1 ∈ ℤ)
11		simpr 110	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
12		0zd 9338	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 0 ∈ ℤ)
13		zdclt 9403	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 < 0)
14	11, 12, 13	syl2an2r 595	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝑁 < 0)
15		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐴 ∈ ℤ)
16		zdclt 9403	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝐴 < 0)
17	15, 12, 16	syl2an2r 595	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID 𝐴 < 0)
18		dcan2 936	. . . . . 6 ⊢ (DECID 𝑁 < 0 → (DECID 𝐴 < 0 → DECID (𝑁 < 0 ∧ 𝐴 < 0)))
19	14, 17, 18	sylc 62	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → DECID (𝑁 < 0 ∧ 𝐴 < 0))
20	9, 10, 19	ifcldcd 3597	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℤ)
21		nnuz 9637	. . . . . 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 2257	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
24		eqeq1 2203	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑛 = 2 ↔ 𝑘 = 2))
25		oveq1 5929	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1))
26	25	oveq1d 5937	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑛 − 1) / 2) = ((𝑘 − 1) / 2))
27	26	oveq2d 5938	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → (𝐴↑((𝑛 − 1) / 2)) = (𝐴↑((𝑘 − 1) / 2)))
28	27	oveq1d 5937	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → ((𝐴↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑘 − 1) / 2)) + 1))
29		id 19	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘)
30	28, 29	oveq12d 5940	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘))
31	30	oveq1d 5937	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1))
32	24, 31	ifbieq2d 3585	. . . . . . . . . 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 5929	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑁) = (𝑘 pCnt 𝑁))
34	32, 33	oveq12d 5940	. . . . . . . . 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 3583	. . . . . . . 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 9338	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 0 ∈ ℤ)
38		1zzd 9353	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 1 ∈ ℤ)
39	38	znegcld 9450	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → -1 ∈ ℤ)
40		id 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ)
41		8nn 9158	. . . . . . . . . . . . . . . . . . . 20 ⊢ 8 ∈ ℕ
42	41	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 8 ∈ ℕ)
43	40, 42	zmodcld 10437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℕ₀)
44	43	nn0zd 9446	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → (𝐴 mod 8) ∈ ℤ)
45		1zzd 9353	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℤ → 1 ∈ ℤ)
46		zdceq 9401	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝐴 mod 8) = 1)
47	44, 45, 46	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 1)
48		7nn 9157	. . . . . . . . . . . . . . . . . 18 ⊢ 7 ∈ ℕ
49	48	nnzi 9347	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℤ
50		zdceq 9401	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 mod 8) ∈ ℤ ∧ 7 ∈ ℤ) → DECID (𝐴 mod 8) = 7)
51	44, 49, 50	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℤ → DECID (𝐴 mod 8) = 7)
52		dcor 937	. . . . . . . . . . . . . . . 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 3642	. . . . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . . . 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 3597	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → if((𝐴 mod 8) ∈ {1, 7}, 1, -1) ∈ ℤ)
60		2nn 9152	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
61	60	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 2 ∈ ℕ)
62		simp-5l 543	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → 𝐴 ∈ ℤ)
63		dvdsdc 11963	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 2 ∥ 𝐴)
64	61, 62, 63	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ 𝑘 = 2) → DECID 2 ∥ 𝐴)
65	37, 59, 64	ifcldcd 3597	. . . . . . . . . . 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 12294	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → (𝑘 = 2 ∨ ¬ 2 ∥ 𝑘))
69	68	orcomd 730	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
70	69	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (¬ 2 ∥ 𝑘 ∨ 𝑘 = 2))
71	67, 70	ecased 1360	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ¬ 2 ∥ 𝑘)
72		prmnn 12278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ)
73	72	nnnn0d 9302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℕ₀)
74		nn0oddm1d2 12074	. . . . . . . . . . . . . . . . . . 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 10646	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℤ ∧ ((𝑘 − 1) / 2) ∈ ℕ₀) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
79	66, 77, 78	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (𝐴↑((𝑘 − 1) / 2)) ∈ ℤ)
80	79	peano2zd 9451	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((𝐴↑((𝑘 − 1) / 2)) + 1) ∈ ℤ)
81	36	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 𝑘 ∈ ℕ)
82	80, 81	zmodcld 10437	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℕ₀)
83	82	nn0zd 9446	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → (((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) ∈ ℤ)
84		1zzd 9353	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → 1 ∈ ℤ)
85	83, 84	zsubcld 9453	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) ∧ ¬ 𝑘 = 2) → ((((𝐴↑((𝑘 − 1) / 2)) + 1) mod 𝑘) − 1) ∈ ℤ)
86		nnz 9345	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
87	86	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
88		2z 9354	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
89		zdceq 9401	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 2 ∈ ℤ) → DECID 𝑘 = 2)
90	87, 88, 89	sylancl 413	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → DECID 𝑘 = 2)
91	65, 85, 90	ifcldadc 3590	. . . . . . . . . 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 2375	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 = 0 → 𝑁 ≠ 0)
95	94	ad3antlr 493	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → 𝑁 ≠ 0)
96		pczcl 12467	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
97	92, 93, 95, 96	syl12anc 1247	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑁) ∈ ℕ₀)
98		zexpcl 10646	. . . . . . . . . 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 9353	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) ∧ ¬ 𝑘 ∈ ℙ) → 1 ∈ ℤ)
101		prmdc 12298	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → DECID 𝑘 ∈ ℙ)
102	101	adantl 277	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → DECID 𝑘 ∈ ℙ)
103	99, 100, 102	ifcldadc 3590	. . . . . . . 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 5655	. . . . . . 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 2273	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℤ)
106		zmulcl 9379	. . . . . . 7 ⊢ ((𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ) → (𝑘 · 𝑣) ∈ ℤ)
107	106	adantl 277	. . . . . 6 ⊢ ((((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) ∧ (𝑘 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝑘 · 𝑣) ∈ ℤ)
108	21, 10, 105, 107	seqf 10556	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → seq1( · , 𝐹):ℕ⟶ℤ)
109		simplr 528	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ)
110	94	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
111		nnabscl 11265	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
112	109, 110, 111	syl2anc 411	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (abs‘𝑁) ∈ ℕ)
113	108, 112	ffvelcdmd 5698	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (seq1( · , 𝐹)‘(abs‘𝑁)) ∈ ℤ)
114	20, 113	zmulcld 9454	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) ∈ ℤ)
115		0zd 9338	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈ ℤ)
116		zdceq 9401	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
117	11, 115, 116	syl2anc 411	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑁 = 0)
118	7, 114, 117	ifcldadc 3590	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ ℤ)
119		simpr 110	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑚 = 𝑁)
120	119	eqeq1d 2205	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0))
121		simpl 109	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → 𝑎 = 𝐴)
122	121	oveq1d 5937	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2))
123	122	eqeq1d 2205	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1))
124	123	ifbid 3582	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0))
125	119	breq1d 4043	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0))
126	121	breq1d 4043	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0))
127	125, 126	anbi12d 473	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
128	127	ifbid 3582	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
129	121	breq2d 4045	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴))
130	121	oveq1d 5937	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8))
131	130	eleq1d 2265	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
132	131	ifbid 3582	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
133	129, 132	ifbieq2d 3585	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
134	121	oveq1d 5937	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2)))
135	134	oveq1d 5937	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1))
136	135	oveq1d 5937	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛))
137	136	oveq1d 5937	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))
138	133, 137	ifeq12d 3580	. . . . . . . . . . 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 5938	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁))
140	138, 139	oveq12d 5940	. . . . . . . . . 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 3578	. . . . . . . . 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 4124	. . . . . . . 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 2247	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹)
144	143	seqeq3d 10547	. . . . . 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 5562	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁))
146	144, 145	fveq12d 5565	. . . . 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 5940	. . . 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 3587	. . 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 15239	. . 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 6052	. 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 1349	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 709 DECID wdc 835 = wceq 1364 ∈ wcel 2167 ≠ wne 2367 ifcif 3561 {cpr 3623 class class class wbr 4033 ↦ cmpt 4094 ‘cfv 5258 (class class class)co 5922 0cc0 7879 1c1 7880 + caddc 7882 · cmul 7884 < clt 8061 − cmin 8197 -cneg 8198 / cdiv 8699 ℕcn 8990 2c2 9041 7c7 9046 8c8 9047 ℕ₀cn0 9249 ℤcz 9326 mod cmo 10414 seqcseq 10539 ↑cexp 10630 abscabs 11162 ∥ cdvds 11952 ℙcprime 12275 pCnt cpc 12453 /_L clgs 15238

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-1o 6474 df-2o 6475 df-er 6592 df-en 6800 df-fin 6802 df-sup 7050 df-inf 7051 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-5 9052 df-6 9053 df-7 9054 df-8 9055 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-dvds 11953 df-gcd 12121 df-prm 12276 df-pc 12454 df-lgs 15239

This theorem is referenced by: lgscllem 15248 lgsval2lem 15251 lgs0 15254 lgsval4 15261

W3C validator