Metamath Proof Explorer

Theorem lgsqrlem5

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

		Ref	Expression
	Assertion	lgsqrlem5	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land A /_{L} P = 1) \to \exists x \in ℤ P ∥ (x^{2} - A)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ℤ / P ℤ = ℤ / P ℤ$
2		eqid	$⊢ {Poly}_{1} (ℤ / P ℤ) = {Poly}_{1} (ℤ / P ℤ)$
3		eqid	$⊢ {Base}_{{Poly}_{1} (ℤ / P ℤ)} = {Base}_{{Poly}_{1} (ℤ / P ℤ)}$
4		eqid	$⊢ \deg_{1} (ℤ / P ℤ) = \deg_{1} (ℤ / P ℤ)$
5		eqid	$⊢ {eval}_{1} (ℤ / P ℤ) = {eval}_{1} (ℤ / P ℤ)$
6		eqid	$⊢ \cdot_{{mulGrp}_{{Poly}_{1} (ℤ / P ℤ)}} = \cdot_{{mulGrp}_{{Poly}_{1} (ℤ / P ℤ)}}$
7		eqid	$⊢ {var}_{1} (ℤ / P ℤ) = {var}_{1} (ℤ / P ℤ)$
8		eqid	$⊢ -_{{Poly}_{1} (ℤ / P ℤ)} = -_{{Poly}_{1} (ℤ / P ℤ)}$
9		eqid	$⊢ 1_{{Poly}_{1} (ℤ / P ℤ)} = 1_{{Poly}_{1} (ℤ / P ℤ)}$
10		eqid	$⊢ ((\frac{P - 1}{2}) \cdot_{{mulGrp}_{{Poly}_{1} (ℤ / P ℤ)}} {var}_{1} (ℤ / P ℤ)) -_{{Poly}_{1} (ℤ / P ℤ)} 1_{{Poly}_{1} (ℤ / P ℤ)} = ((\frac{P - 1}{2}) \cdot_{{mulGrp}_{{Poly}_{1} (ℤ / P ℤ)}} {var}_{1} (ℤ / P ℤ)) -_{{Poly}_{1} (ℤ / P ℤ)} 1_{{Poly}_{1} (ℤ / P ℤ)}$
11		eqid	$⊢ ℤRHom (ℤ / P ℤ) = ℤRHom (ℤ / P ℤ)$
12		simp2	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land A /_{L} P = 1) \to P \in (ℙ ∖ \{2\})$
13		eqid	$⊢ (y \in (1 \dots \frac{P - 1}{2}) ⟼ ℤRHom (ℤ / P ℤ) (y^{2})) = (y \in (1 \dots \frac{P - 1}{2}) ⟼ ℤRHom (ℤ / P ℤ) (y^{2}))$
14		simp1	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land A /_{L} P = 1) \to A \in ℤ$
15		simp3	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land A /_{L} P = 1) \to A /_{L} P = 1$
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	lgsqrlem4	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\}) \land A /_{L} P = 1) \to \exists x \in ℤ P ∥ (x^{2} - A)$