Metamath Proof Explorer

Theorem lgsmod

Description: The Legendre (Jacobi) symbol is preserved under reduction mod n when n is odd. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsmod ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zmodcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod 𝑁 ) ∈ ℕ0 )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℕ0 )
3 2 nn0zd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℤ )
4 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℤ )
5 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → 𝑛 ∈ ℙ )
6 5 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℙ )
7 simpl3 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ¬ 2 ∥ 𝑁 )
8 breq1 ⊢ ( 𝑛 = 2 → ( 𝑛 ∥ 𝑁 ↔ 2 ∥ 𝑁 ) )
9 8 notbid ⊢ ( 𝑛 = 2 → ( ¬ 𝑛 ∥ 𝑁 ↔ ¬ 2 ∥ 𝑁 ) )
10 7 9 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 = 2 → ¬ 𝑛 ∥ 𝑁 ) )
11 10 necon2ad ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ( 𝑛 ∥ 𝑁 → 𝑛 ≠ 2 ) )
12 11 imp ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ≠ 2 )
13 eldifsn ⊢ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑛 ∈ ℙ ∧ 𝑛 ≠ 2 ) )
14 6 12 13 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ( ℙ ∖ { 2 } ) )
15 oddprm ⊢ ( 𝑛 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ )
16 14 15 syl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ )
17 16 nnnn0d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ0 )
18 zexpcl ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℤ )
19 4 17 18 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℤ )
20 19 zred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℝ )
21 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝐴 ∈ ℤ )
22 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℤ )
23 21 17 22 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℤ )
24 23 zred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℝ )
25 1red ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 1 ∈ ℝ )
26 prmnn ⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℕ )
27 26 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℕ )
28 27 nnrpd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℝ+ )
29 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∥ 𝑁 )
30 21 zred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝐴 ∈ ℝ )
31 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
32 31 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
33 32 nnrpd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∈ ℝ+ )
34 modabs2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )
35 30 33 34 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )
36 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
37 32 4 21 36 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
38 35 37 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) )
39 prmz ⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℤ )
40 39 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℤ )
41 32 nnzd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
42 4 21 zsubcld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ∈ ℤ )
43 dvdstr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ∈ ℤ ) → ( ( 𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) → 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
44 40 41 42 43 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝑛 ∥ 𝑁 ∧ 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) → 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
45 29 38 44 mp2and ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) )
46 moddvds ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) ↔ 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
47 27 4 21 46 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) ↔ 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
48 45 47 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) )
49 modexp ⊢ ( ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ0 ∧ 𝑛 ∈ ℝ+ ) ∧ ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) ) → ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) )
50 4 21 17 28 48 49 syl221anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) )
51 modadd1 ⊢ ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℝ ∧ ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℝ ) ∧ ( 1 ∈ ℝ ∧ 𝑛 ∈ ℝ+ ) ∧ ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) ) → ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) )
52 20 24 25 28 50 51 syl221anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) )
53 52 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
54 lgsval3 ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝑛 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) = ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
55 4 14 54 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) = ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
56 lgsval3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 /L 𝑛 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
57 21 14 56 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( 𝐴 /L 𝑛 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
58 53 55 57 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) = ( 𝐴 /L 𝑛 ) )
59 58 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
60 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℤ )
61 39 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℤ )
62 lgscl ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ∈ ℤ )
63 60 61 62 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ∈ ℤ )
64 63 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ∈ ℂ )
65 64 exp0d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ 0 ) = 1 )
66 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → 𝐴 ∈ ℤ )
67 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝐴 /L 𝑛 ) ∈ ℤ )
68 66 61 67 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝐴 /L 𝑛 ) ∈ ℤ )
69 68 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝐴 /L 𝑛 ) ∈ ℂ )
70 69 exp0d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 /L 𝑛 ) ↑ 0 ) = 1 )
71 65 70 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ 0 ) = ( ( 𝐴 /L 𝑛 ) ↑ 0 ) )
72 31 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → 𝑁 ∈ ℕ )
73 pceq0 ⊢ ( ( 𝑛 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑛 pCnt 𝑁 ) = 0 ↔ ¬ 𝑛 ∥ 𝑁 ) )
74 5 72 73 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 pCnt 𝑁 ) = 0 ↔ ¬ 𝑛 ∥ 𝑁 ) )
75 74 biimpar ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝑛 pCnt 𝑁 ) = 0 )
76 75 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ 0 ) )
77 75 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ 0 ) )
78 71 76 77 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
79 59 78 pm2.61dan ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
80 79 ifeq1da ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
81 80 mpteq2dv ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) )
82 81 seqeq3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) )
83 82 fveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
84 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
85 84 lgsval4a ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
86 3 31 85 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
87 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
88 87 lgsval4a ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
89 88 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝐴 /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
90 83 86 89 3eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )