Theorem modexp2m1d

Description: The square of an integer which is -1 modulo a number greater than 1 is 1 modulo the same modulus. (Contributed by AV, 5-Jul-2020)

	Ref	Expression
Hypotheses	modexp2m1d.a	$$⊢\phi \to A\in \mathbb{Z}$$
	modexp2m1d.e	$$⊢\phi \to E\in {ℝ}^{+}$$
	modexp2m1d.g	$$⊢\phi \to 1<E$$
	modexp2m1d.m	$$⊢\phi \to A\mathrm{mod}E=-1\mathrm{mod}E$$
Assertion	modexp2m1d	$$⊢\phi \to A^2\mathrm{mod}E=1$$

Proof

Step	Hyp	Ref	Expression
1		modexp2m1d.a	$$⊢\phi \to A\in \mathbb{Z}$$
2		modexp2m1d.e	$$⊢\phi \to E\in {ℝ}^{+}$$
3		modexp2m1d.g	$$⊢\phi \to 1<E$$
4		modexp2m1d.m	$$⊢\phi \to A\mathrm{mod}E=-1\mathrm{mod}E$$
5	1	zcnd	$$⊢\phi \to A\in ℂ$$
6	5	sqvald	$$⊢\phi \to A^2=AA$$
7	6	oveq1d	$$⊢\phi \to A^2\mathrm{mod}E=AA\mathrm{mod}E$$
8		neg1z	$$⊢-1\in \mathbb{Z}$$
9	8	a1i	$$⊢\phi \to -1\in \mathbb{Z}$$
10	1 9 1 9 2 4 4	modmul12d	$$⊢\phi \to AA\mathrm{mod}E=-1-1\mathrm{mod}E$$
11	7 10	eqtrd	$$⊢\phi \to A^2\mathrm{mod}E=-1-1\mathrm{mod}E$$
12		neg1mulneg1e1	$$⊢-1-1=1$$
13	12	a1i	$$⊢\phi \to -1-1=1$$
14	13	oveq1d	$$⊢\phi \to -1-1\mathrm{mod}E=1\mathrm{mod}E$$
15	2	rpred	$$⊢\phi \to E\in ℝ$$
16		1mod	$$⊢\left(E\in ℝ\wedge 1<E\right)\to 1\mathrm{mod}E=1$$
17	15 3 16	syl2anc	$$⊢\phi \to 1\mathrm{mod}E=1$$
18	14 17	eqtrd	$$⊢\phi \to -1-1\mathrm{mod}E=1$$
19	11 18	eqtrd	$$⊢\phi \to A^2\mathrm{mod}E=1$$