This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsmodexp

Description: If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl ). (Contributed by Mario Carneiro, 28-Feb-2014) (Revised by AV, 19-Mar-2022)

Ref Expression
Assertion dvdsmodexp ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∥ 𝐴 ) → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )

Proof

Step Hyp Ref Expression
1 dvdszrcl ⊢ ( 𝑁 ∥ 𝐴 → ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
2 dvdsmod0 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝐴 ) → ( 𝐴 mod 𝑁 ) = 0 )
3 2 3ad2antl2 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∥ 𝐴 ) → ( 𝐴 mod 𝑁 ) = 0 )
4 3 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∥ 𝐴 → ( 𝐴 mod 𝑁 ) = 0 ) )
5 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → 𝐵 ∈ ℕ )
6 5 0expd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( 0 ↑ 𝐵 ) = 0 )
7 6 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ( 0 ↑ 𝐵 ) mod 𝑁 ) = ( 0 mod 𝑁 ) )
8 simpl1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → 𝐴 ∈ ℤ )
9 0zd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → 0 ∈ ℤ )
10 nnnn0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
11 10 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ0 )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → 𝐵 ∈ ℕ0 )
13 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
14 13 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝑁 ∈ ℝ+ )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → 𝑁 ∈ ℝ+ )
16 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( 𝐴 mod 𝑁 ) = 0 )
17 0mod ⊢ ( 𝑁 ∈ ℝ+ → ( 0 mod 𝑁 ) = 0 )
18 15 17 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( 0 mod 𝑁 ) = 0 )
19 16 18 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( 𝐴 mod 𝑁 ) = ( 0 mod 𝑁 ) )
20 modexp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑁 ) = ( 0 mod 𝑁 ) ) → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( ( 0 ↑ 𝐵 ) mod 𝑁 ) )
21 8 9 12 15 19 20 syl221anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( ( 0 ↑ 𝐵 ) mod 𝑁 ) )
22 7 21 19 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) = 0 ) → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )
23 22 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) = 0 → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) )
24 4 23 syld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∥ 𝐴 → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) )
25 24 3exp ⊢ ( 𝐴 ∈ ℤ → ( 𝑁 ∈ ℕ → ( 𝐵 ∈ ℕ → ( 𝑁 ∥ 𝐴 → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) ) ) )
26 25 com24 ⊢ ( 𝐴 ∈ ℤ → ( 𝑁 ∥ 𝐴 → ( 𝐵 ∈ ℕ → ( 𝑁 ∈ ℕ → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) ) ) )
27 26 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑁 ∥ 𝐴 → ( 𝐵 ∈ ℕ → ( 𝑁 ∈ ℕ → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) ) ) )
28 1 27 mpcom ⊢ ( 𝑁 ∥ 𝐴 → ( 𝐵 ∈ ℕ → ( 𝑁 ∈ ℕ → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) ) )
29 28 3imp31 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∥ 𝐴 ) → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )