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	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	modexp2m1d.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	modexp2m1d.g	⊢ ( 𝜑 → 1 < 𝐸 )
	modexp2m1d.m	⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( - 1 mod 𝐸 ) )
Assertion	modexp2m1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) mod 𝐸 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		modexp2m1d.a	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2		modexp2m1d.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
3		modexp2m1d.g	⊢ ( 𝜑 → 1 < 𝐸 )
4		modexp2m1d.m	⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( - 1 mod 𝐸 ) )
5	1	zcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6	5	sqvald	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
7	6	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) mod 𝐸 ) = ( ( 𝐴 · 𝐴 ) mod 𝐸 ) )
8		neg1z	⊢ - 1 ∈ ℤ
9	8	a1i	⊢ ( 𝜑 → - 1 ∈ ℤ )
10	1 9 1 9 2 4 4	modmul12d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐴 ) mod 𝐸 ) = ( ( - 1 · - 1 ) mod 𝐸 ) )
11	7 10	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) mod 𝐸 ) = ( ( - 1 · - 1 ) mod 𝐸 ) )
12		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
13	12	a1i	⊢ ( 𝜑 → ( - 1 · - 1 ) = 1 )
14	13	oveq1d	⊢ ( 𝜑 → ( ( - 1 · - 1 ) mod 𝐸 ) = ( 1 mod 𝐸 ) )
15	2	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
16		1mod	⊢ ( ( 𝐸 ∈ ℝ ∧ 1 < 𝐸 ) → ( 1 mod 𝐸 ) = 1 )
17	15 3 16	syl2anc	⊢ ( 𝜑 → ( 1 mod 𝐸 ) = 1 )
18	14 17	eqtrd	⊢ ( 𝜑 → ( ( - 1 · - 1 ) mod 𝐸 ) = 1 )
19	11 18	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) mod 𝐸 ) = 1 )