lgsneg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgsneg		Structured version Visualization version GIF version

Theorem lgsneg 26813

Description: The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.)

**Assertion**
Ref	Expression
lgsneg	⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L -𝑁) = (if(𝐴 < 0, -1, 1) · (𝐴 /_L 𝑁)))

Proof of Theorem lgsneg Dummy variables 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 4533	. . . . . . . . 9 ⊢ (𝐴 < 0 → if(𝐴 < 0, -1, 1) = -1)
2	1	adantl 482	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝐴 < 0, -1, 1) = -1)
3	2	oveq1d 7420	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (-1 · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)))
4		oveq2 7413	. . . . . . . . . 10 ⊢ (if(𝑁 < 0, -1, 1) = -1 → (-1 · if(𝑁 < 0, -1, 1)) = (-1 · -1))
5		neg1mulneg1e1 12421	. . . . . . . . . 10 ⊢ (-1 · -1) = 1
6	4, 5	eqtrdi 2788	. . . . . . . . 9 ⊢ (if(𝑁 < 0, -1, 1) = -1 → (-1 · if(𝑁 < 0, -1, 1)) = 1)
7		oveq2 7413	. . . . . . . . . 10 ⊢ (if(𝑁 < 0, -1, 1) = 1 → (-1 · if(𝑁 < 0, -1, 1)) = (-1 · 1))
8		ax-1cn 11164	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
9	8	mulm1i 11655	. . . . . . . . . 10 ⊢ (-1 · 1) = -1
10	7, 9	eqtrdi 2788	. . . . . . . . 9 ⊢ (if(𝑁 < 0, -1, 1) = 1 → (-1 · if(𝑁 < 0, -1, 1)) = -1)
11	6, 10	ifsb 4540	. . . . . . . 8 ⊢ (-1 · if(𝑁 < 0, -1, 1)) = if(𝑁 < 0, 1, -1)
12		simpr 485	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝐴 < 0)
13	12	biantrud 532	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
14	13	ifbid 4550	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝑁 < 0, -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
15	14	oveq2d 7421	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (-1 · if(𝑁 < 0, -1, 1)) = (-1 · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)))
16		simpl3 1193	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝑁 ≠ 0)
17	16	necomd 2996	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 0 ≠ 𝑁)
18		simpl2 1192	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝑁 ∈ ℤ)
19	18	zred 12662	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → 𝑁 ∈ ℝ)
20		0re 11212	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
21		ltlen 11311	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
22	19, 20, 21	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
23	17, 22	mpbiran2d 706	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ 𝑁 ≤ 0))
24	19	le0neg1d 11781	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 ≤ 0 ↔ 0 ≤ -𝑁))
25	19	renegcld 11637	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → -𝑁 ∈ ℝ)
26		lenlt 11288	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝑁 ∈ ℝ) → (0 ≤ -𝑁 ↔ ¬ -𝑁 < 0))
27	20, 25, 26	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (0 ≤ -𝑁 ↔ ¬ -𝑁 < 0))
28	23, 24, 27	3bitrd 304	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (𝑁 < 0 ↔ ¬ -𝑁 < 0))
29	28	ifbid 4550	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝑁 < 0, 1, -1) = if(¬ -𝑁 < 0, 1, -1))
30		ifnot 4579	. . . . . . . . 9 ⊢ if(¬ -𝑁 < 0, 1, -1) = if(-𝑁 < 0, -1, 1)
31	29, 30	eqtrdi 2788	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(𝑁 < 0, 1, -1) = if(-𝑁 < 0, -1, 1))
32	11, 15, 31	3eqtr3a 2796	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (-1 · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if(-𝑁 < 0, -1, 1))
33	12	biantrud 532	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (-𝑁 < 0 ↔ (-𝑁 < 0 ∧ 𝐴 < 0)))
34	33	ifbid 4550	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → if(-𝑁 < 0, -1, 1) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
35	3, 32, 34	3eqtrd 2776	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
36		1t1e1 12370	. . . . . . 7 ⊢ (1 · 1) = 1
37		iffalse 4536	. . . . . . . . 9 ⊢ (¬ 𝐴 < 0 → if(𝐴 < 0, -1, 1) = 1)
38	37	adantl 482	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → if(𝐴 < 0, -1, 1) = 1)
39		simpr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → ¬ 𝐴 < 0)
40	39	intnand 489	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → ¬ (𝑁 < 0 ∧ 𝐴 < 0))
41	40	iffalsed 4538	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1)
42	38, 41	oveq12d 7423	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = (1 · 1))
43	39	intnand 489	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → ¬ (-𝑁 < 0 ∧ 𝐴 < 0))
44	43	iffalsed 4538	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = 1)
45	36, 42, 44	3eqtr4a 2798	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ ¬ 𝐴 < 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
46	35, 45	pm2.61dan 811	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) = if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
47	46	eqcomd 2738	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) = (if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)))
48		simpr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
49		simpl2 1192	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → 𝑁 ∈ ℤ)
50		zq 12934	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℚ)
51	49, 50	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → 𝑁 ∈ ℚ)
52		pcneg 16803	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑛 pCnt -𝑁) = (𝑛 pCnt 𝑁))
53	48, 51, 52	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt -𝑁) = (𝑛 pCnt 𝑁))
54	53	oveq2d 7421	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑛 ∈ ℙ) → ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)) = ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)))
55	54	ifeq1da 4558	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1) = if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
56	55	mpteq2dv 5249	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))
57	56	seqeq3d 13970	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))))
58		zcn 12559	. . . . . . 7 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
59	58	3ad2ant2 1134	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℂ)
60	59	absnegd 15392	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘-𝑁) = (abs‘𝑁))
61	57, 60	fveq12d 6895	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))
62	47, 61	oveq12d 7423	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁))) = ((if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
63		neg1cn 12322	. . . . . 6 ⊢ -1 ∈ ℂ
64	63, 8	ifcli 4574	. . . . 5 ⊢ if(𝐴 < 0, -1, 1) ∈ ℂ
65	64	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if(𝐴 < 0, -1, 1) ∈ ℂ)
66	63, 8	ifcli 4574	. . . . 5 ⊢ if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ
67	66	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) ∈ ℂ)
68		nnabscl 15268	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
69	68	3adant1 1130	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
70		nnuz 12861	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
71	69, 70	eleqtrdi 2843	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ (ℤ_≥‘1))
72		eqid 2732	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))
73	72	lgsfcl3 26810	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ)
74		elfznn 13526	. . . . . . 7 ⊢ (𝑥 ∈ (1...(abs‘𝑁)) → 𝑥 ∈ ℕ)
75		ffvelcdm 7080	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)):ℕ⟶ℤ ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑥) ∈ ℤ)
76	73, 74, 75	syl2an 596	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑥 ∈ (1...(abs‘𝑁))) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1))‘𝑥) ∈ ℤ)
77		zmulcl 12607	. . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ)
78	77	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 · 𝑦) ∈ ℤ)
79	71, 76, 78	seqcl 13984	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℤ)
80	79	zcnd 12663	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)) ∈ ℂ)
81	65, 67, 80	mulassd 11233	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((if(𝐴 < 0, -1, 1) · if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1)) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))) = (if(𝐴 < 0, -1, 1) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
82	62, 81	eqtrd 2772	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁))) = (if(𝐴 < 0, -1, 1) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
83		simp1 1136	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
84		znegcl 12593	. . . 4 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
85	84	3ad2ant2 1134	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → -𝑁 ∈ ℤ)
86		simp3 1138	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
87	59, 86	negne0d 11565	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → -𝑁 ≠ 0)
88		eqid 2732	. . . 4 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1))
89	88	lgsval4 26809	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ -𝑁 ∈ ℤ ∧ -𝑁 ≠ 0) → (𝐴 /_L -𝑁) = (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁))))
90	83, 85, 87, 89	syl3anc 1371	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L -𝑁) = (if((-𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt -𝑁)), 1)))‘(abs‘-𝑁))))
91	72	lgsval4 26809	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁))))
92	91	oveq2d 7421	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (if(𝐴 < 0, -1, 1) · (𝐴 /_L 𝑁)) = (if(𝐴 < 0, -1, 1) · (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /_L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))‘(abs‘𝑁)))))
93	82, 90, 92	3eqtr4d 2782	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /_L -𝑁) = (if(𝐴 < 0, -1, 1) · (𝐴 /_L 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ifcif 4527 class class class wbr 5147 ↦ cmpt 5230 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 · cmul 11111 < clt 11244 ≤ cle 11245 -cneg 11441 ℕcn 12208 ℤcz 12554 ℤ_≥cuz 12818 ℚcq 12928 ...cfz 13480 seqcseq 13962 ↑cexp 14023 abscabs 15177 ℙcprime 16604 pCnt cpc 16765 /_L clgs 26786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-oadd 8466 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-xnn0 12541 df-z 12555 df-uz 12819 df-q 12929 df-rp 12971 df-fz 13481 df-fzo 13624 df-fl 13753 df-mod 13831 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-dvds 16194 df-gcd 16432 df-prm 16605 df-phi 16695 df-pc 16766 df-lgs 26787

This theorem is referenced by: lgsneg1 26814

W3C validator