Metamath Proof Explorer

Theorem powm2modprm

Description: If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018)

Ref Expression
Assertion powm2modprm ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 − 1 ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → 𝑃 ∈ ℙ )
2 simpr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℤ )
3 2 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → 𝐴 ∈ ℤ )
4 m1dvdsndvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 − 1 ) → ¬ 𝑃 ∥ 𝐴 ) )
5 4 imp ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ¬ 𝑃 ∥ 𝐴 )
6 eqid ⊢ ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
7 6 modprminv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ) )
8 simpr ⊢ ( ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ) → ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 )
9 8 eqcomd ⊢ ( ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ) → 1 = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
10 7 9 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 1 = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
11 1 3 5 10 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → 1 = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
12 modprm1div ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( 𝐴 − 1 ) ) )
13 12 biimpar ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( 𝐴 mod 𝑃 ) = 1 )
14 13 oveq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 𝐴 mod 𝑃 ) · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) = ( 1 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
15 14 oveq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( ( 𝐴 mod 𝑃 ) · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( 1 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
16 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
17 16 ad2antlr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → 𝐴 ∈ ℝ )
18 prmm2nn0 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 2 ) ∈ ℕ0 )
19 18 anim1ci ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) )
20 19 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) )
21 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
22 20 21 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
23 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
24 23 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝑃 ∈ ℕ )
25 24 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → 𝑃 ∈ ℕ )
26 22 25 zmodcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℕ0 )
27 26 nn0zd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℤ )
28 23 nnrpd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
29 28 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝑃 ∈ ℝ+ )
30 29 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → 𝑃 ∈ ℝ+ )
31 modmulmod ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑃 ) · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
32 17 27 30 31 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( ( 𝐴 mod 𝑃 ) · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
33 19 21 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
34 33 24 zmodcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℕ0 )
35 34 nn0cnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℂ )
36 35 mullidd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 1 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
37 36 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 1 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 ) )
38 37 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 1 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 ) )
39 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ )
40 16 18 39 syl2anr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ )
41 40 29 jca ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) )
42 41 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) )
43 modabs2 ⊢ ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
44 42 43 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
45 38 44 eqtrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 1 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
46 15 32 45 3eqtr3d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) )
47 11 46 eqtr2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝐴 − 1 ) ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 1 )
48 47 ex ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 − 1 ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 1 ) )