Metamath Proof Explorer

Theorem vfermltlALT

Description: Alternate proof of vfermltl , not using Euler's theorem. (Contributed by AV, 21-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 2m1e1 ⊢ ( 2 − 1 ) = 1
2 1 a1i ⊢ ( 𝑃 ∈ ℙ → ( 2 − 1 ) = 1 )
3 2 eqcomd ⊢ ( 𝑃 ∈ ℙ → 1 = ( 2 − 1 ) )
4 3 oveq2d ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) = ( 𝑃 − ( 2 − 1 ) ) )
5 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
6 5 zcnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
7 2cnd ⊢ ( 𝑃 ∈ ℙ → 2 ∈ ℂ )
8 1cnd ⊢ ( 𝑃 ∈ ℙ → 1 ∈ ℂ )
9 6 7 8 subsubd ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − ( 2 − 1 ) ) = ( ( 𝑃 − 2 ) + 1 ) )
10 4 9 eqtrd ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) = ( ( 𝑃 − 2 ) + 1 ) )
11 10 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 1 ) = ( ( 𝑃 − 2 ) + 1 ) )
12 11 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( 𝑃 − 1 ) ) = ( 𝐴 ↑ ( ( 𝑃 − 2 ) + 1 ) ) )
13 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
14 13 3ad2ant2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝐴 ∈ ℂ )
15 prmm2nn0 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 2 ) ∈ ℕ0 )
16 15 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝑃 − 2 ) ∈ ℕ0 )
17 14 16 expp1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( ( 𝑃 − 2 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) · 𝐴 ) )
18 12 17 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( 𝑃 − 1 ) ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) · 𝐴 ) )
19 18 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) · 𝐴 ) mod 𝑃 ) )
20 15 anim1i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝑃 − 2 ) ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) )
21 20 ancomd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) )
22 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑃 − 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
23 21 22 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℤ )
24 23 zred ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ )
25 24 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ )
26 simp2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝐴 ∈ ℤ )
27 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
28 27 nnrpd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
29 28 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → 𝑃 ∈ ℝ+ )
30 modmulmod ⊢ ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ ∧ 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) · 𝐴 ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) · 𝐴 ) mod 𝑃 ) )
31 25 26 29 30 syl3anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) · 𝐴 ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) · 𝐴 ) mod 𝑃 ) )
32 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
33 32 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℝ )
34 15 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 − 2 ) ∈ ℕ0 )
35 33 34 reexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ↑ ( 𝑃 − 2 ) ) ∈ ℝ )
36 28 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝑃 ∈ ℝ+ )
37 35 36 modcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℝ )
38 37 recnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℂ )
39 13 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℂ )
40 38 39 mulcomd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) · 𝐴 ) = ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
41 40 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) · 𝐴 ) = ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) )
42 41 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) · 𝐴 ) mod 𝑃 ) = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
43 19 31 42 3eqtr2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
44 eqid ⊢ ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
45 44 modprminv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 ) )
46 45 simprd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 · ( ( 𝐴 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = 1 )
47 43 46 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴 ) → ( ( 𝐴 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 )