Theorem lgsqrlem5

Description: Lemma for lgsqr . (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Assertion	lgsqrlem5	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℤ/nℤ ‘ 𝑃 ) = ( ℤ/nℤ ‘ 𝑃 )
2		eqid	⊢ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) )
3		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) = ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) )
4		eqid	⊢ ( deg1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( deg1 ‘ ( ℤ/nℤ ‘ 𝑃 ) )
5		eqid	⊢ ( eval1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( eval1 ‘ ( ℤ/nℤ ‘ 𝑃 ) )
6		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) )
7		eqid	⊢ ( var1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( var1 ‘ ( ℤ/nℤ ‘ 𝑃 ) )
8		eqid	⊢ ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) = ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) )
9		eqid	⊢ ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) = ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) )
10		eqid	⊢ ( ( ( ( 𝑃 − 1 ) / 2 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ) = ( ( ( ( 𝑃 − 1 ) / 2 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ) )
11		eqid	⊢ ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑃 ) ) = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑃 ) )
12		simp2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
13		eqid	⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ‘ ( 𝑦 ↑ 2 ) ) ) = ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑃 ) ) ‘ ( 𝑦 ↑ 2 ) ) )
14		simp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → 𝐴 ∈ ℤ )
15		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ( 𝐴 /L 𝑃 ) = 1 )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	lgsqrlem4	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )