lgslem1

Description: When a is coprime to the prime p , a ^ ( ( p - 1 ) / 2 ) is equivalent mod p to 1 or -u 1 , and so adding 1 makes it equivalent to 0 or 2 . (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Assertion	lgslem1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ { 0 , 2 } )

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
2	1	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℙ )
3		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4	2 3	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℕ )
5		simp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝐴 ∈ ℤ )
6		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
7	2 6	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℤ )
8	5 7	gcdcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 gcd 𝑃 ) = ( 𝑃 gcd 𝐴 ) )
9		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ¬ 𝑃 ∥ 𝐴 )
10		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
11	2 5 10	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ¬ 𝑃 ∥ 𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
12	9 11	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 gcd 𝐴 ) = 1 )
13	8 12	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 gcd 𝑃 ) = 1 )
14		eulerth	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑃 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
15	4 5 13 14	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
16		phiprm	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
17	2 16	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
18		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ₀ )
19	4 18	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 1 ) ∈ ℕ₀ )
20	17 19	eqeltrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ϕ ‘ 𝑃 ) ∈ ℕ₀ )
21		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ϕ ‘ 𝑃 ) ∈ ℕ₀ ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℤ )
22	5 20 21	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℤ )
23		1zzd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 1 ∈ ℤ )
24		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) − 1 ) ) )
25	4 22 23 24	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) − 1 ) ) )
26	15 25	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∥ ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) − 1 ) )
27	19	nn0cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 1 ) ∈ ℂ )
28		2cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 ∈ ℂ )
29		2ne0	⊢ 2 ≠ 0
30	29	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 ≠ 0 )
31	27 28 30	divcan1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) = ( 𝑃 − 1 ) )
32	17 31	eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ϕ ‘ 𝑃 ) = ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) )
33	32	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) = ( 𝐴 ↑ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ) )
34	5	zcnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝐴 ∈ ℂ )
35		2nn0	⊢ 2 ∈ ℕ₀
36	35	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 ∈ ℕ₀ )
37		oddprm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
38	37	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
39	38	nnnn0d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ₀ )
40	34 36 39	expmuld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) )
41	33 40	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) )
42	41	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) − 1 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) − 1 ) )
43		sq1	⊢ ( 1 ↑ 2 ) = 1
44	43	oveq2i	⊢ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) − 1 )
45	42 44	eqtr4di	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) − 1 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) − ( 1 ↑ 2 ) ) )
46		zexpcl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ₀ ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
47	5 39 46	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
48	47	zcnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℂ )
49		ax-1cn	⊢ 1 ∈ ℂ
50		subsq	⊢ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) · ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
51	48 49 50	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) · ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
52	45 51	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑃 ) ) − 1 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) · ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
53	26 52	breqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∥ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) · ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
54	47	peano2zd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℤ )
55		peano2zm	⊢ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ∈ ℤ )
56	47 55	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ∈ ℤ )
57		euclemma	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℤ ∧ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) · ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) ↔ ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∨ 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) ) )
58	2 54 56 57	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 ∥ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) · ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) ↔ ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∨ 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) ) )
59	53 58	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∨ 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
60		dvdsval3	⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ↔ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ) )
61	4 54 60	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ↔ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ) )
62		2z	⊢ 2 ∈ ℤ
63	62	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 ∈ ℤ )
64		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = ( 2 mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 2 ) ) )
65	4 54 63 64	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = ( 2 mod 𝑃 ) ↔ 𝑃 ∥ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 2 ) ) )
66		2re	⊢ 2 ∈ ℝ
67	66	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 ∈ ℝ )
68	4	nnrpd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℝ⁺ )
69		0le2	⊢ 0 ≤ 2
70	69	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 0 ≤ 2 )
71	4	nnred	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℝ )
72		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ_≥ ‘ 2 ) )
73	2 72	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ( ℤ_≥ ‘ 2 ) )
74		eluzle	⊢ ( 𝑃 ∈ ( ℤ_≥ ‘ 2 ) → 2 ≤ 𝑃 )
75	73 74	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 ≤ 𝑃 )
76		eldifsni	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
77	76	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ≠ 2 )
78	67 71 75 77	leneltd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 2 < 𝑃 )
79		modid	⊢ ( ( ( 2 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺ ) ∧ ( 0 ≤ 2 ∧ 2 < 𝑃 ) ) → ( 2 mod 𝑃 ) = 2 )
80	67 68 70 78 79	syl22anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 2 mod 𝑃 ) = 2 )
81	80	eqeq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = ( 2 mod 𝑃 ) ↔ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) )
82		df-2	⊢ 2 = ( 1 + 1 )
83	82	oveq2i	⊢ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 2 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − ( 1 + 1 ) )
84	49	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → 1 ∈ ℂ )
85	48 84 84	pnpcan2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − ( 1 + 1 ) ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) )
86	83 85	syl5eq	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 2 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) )
87	86	breq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 ∥ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 2 ) ↔ 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
88	65 81 87	3bitr3rd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ↔ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) )
89	61 88	orbi12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∨ 𝑃 ∥ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) ↔ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ∨ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) ) )
90	59 89	mpbid	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ∨ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) )
91		ovex	⊢ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ V
92	91	elpr	⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ { 0 , 2 } ↔ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 0 ∨ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) = 2 ) )
93	90 92	sylibr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ { 0 , 2 } )

Metamath Proof Explorer

Theorem lgslem1

Proof