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	|- ( ph -> A e. ZZ )
	modexp2m1d.e	|- ( ph -> E e. RR+ )
	modexp2m1d.g	|- ( ph -> 1 < E )
	modexp2m1d.m	|- ( ph -> ( A mod E ) = ( -u 1 mod E ) )
Assertion	modexp2m1d	|- ( ph -> ( ( A ^ 2 ) mod E ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		modexp2m1d.a	|- ( ph -> A e. ZZ )
2		modexp2m1d.e	|- ( ph -> E e. RR+ )
3		modexp2m1d.g	|- ( ph -> 1 < E )
4		modexp2m1d.m	|- ( ph -> ( A mod E ) = ( -u 1 mod E ) )
5	1	zcnd	|- ( ph -> A e. CC )
6	5	sqvald	|- ( ph -> ( A ^ 2 ) = ( A x. A ) )
7	6	oveq1d	|- ( ph -> ( ( A ^ 2 ) mod E ) = ( ( A x. A ) mod E ) )
8		neg1z	|- -u 1 e. ZZ
9	8	a1i	|- ( ph -> -u 1 e. ZZ )
10	1 9 1 9 2 4 4	modmul12d	|- ( ph -> ( ( A x. A ) mod E ) = ( ( -u 1 x. -u 1 ) mod E ) )
11	7 10	eqtrd	|- ( ph -> ( ( A ^ 2 ) mod E ) = ( ( -u 1 x. -u 1 ) mod E ) )
12		neg1mulneg1e1	|- ( -u 1 x. -u 1 ) = 1
13	12	a1i	|- ( ph -> ( -u 1 x. -u 1 ) = 1 )
14	13	oveq1d	|- ( ph -> ( ( -u 1 x. -u 1 ) mod E ) = ( 1 mod E ) )
15	2	rpred	|- ( ph -> E e. RR )
16		1mod	|- ( ( E e. RR /\ 1 < E ) -> ( 1 mod E ) = 1 )
17	15 3 16	syl2anc	|- ( ph -> ( 1 mod E ) = 1 )
18	14 17	eqtrd	|- ( ph -> ( ( -u 1 x. -u 1 ) mod E ) = 1 )
19	11 18	eqtrd	|- ( ph -> ( ( A ^ 2 ) mod E ) = 1 )