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 prmz ⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℤ )
30 29 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℤ )
31 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
32 31 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
33 32 nnzd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
34 4 21 zsubcld ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ∈ ℤ )
35 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∥ 𝑁 )
36 21 zred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝐴 ∈ ℝ )
37 32 nnrpd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∈ ℝ+ )
38 modabs2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )
39 36 37 38 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) )
40 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
41 32 4 21 40 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
42 39 41 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑁 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) )
43 30 33 34 35 42 dvdstrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) )
44 moddvds ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) ↔ 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
45 27 4 21 44 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) ↔ 𝑛 ∥ ( ( 𝐴 mod 𝑁 ) − 𝐴 ) ) )
46 43 45 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) )
47 modexp ⊢ ( ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( ( ( 𝑛 − 1 ) / 2 ) ∈ ℕ0 ∧ 𝑛 ∈ ℝ+ ) ∧ ( ( 𝐴 mod 𝑁 ) mod 𝑛 ) = ( 𝐴 mod 𝑛 ) ) → ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) )
48 4 21 17 28 46 47 syl221anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) )
49 modadd1 ⊢ ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℝ ∧ ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) ∈ ℝ ) ∧ ( 1 ∈ ℝ ∧ 𝑛 ∈ ℝ+ ) ∧ ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) = ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) mod 𝑛 ) ) → ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) )
50 20 24 25 28 48 49 syl221anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) = ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) )
51 50 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
52 lgsval3 ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝑛 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) = ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
53 4 14 52 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) = ( ( ( ( ( 𝐴 mod 𝑁 ) ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
54 lgsval3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 /L 𝑛 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
55 21 14 54 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( 𝐴 /L 𝑛 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑛 − 1 ) / 2 ) ) + 1 ) mod 𝑛 ) − 1 ) )
56 51 53 55 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) = ( 𝐴 /L 𝑛 ) )
57 56 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
58 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝐴 mod 𝑁 ) ∈ ℤ )
59 29 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → 𝑛 ∈ ℤ )
60 lgscl ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ∈ ℤ )
61 58 59 60 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ∈ ℤ )
62 61 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ∈ ℂ )
63 62 exp0d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ 0 ) = 1 )
64 simpll1 ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → 𝐴 ∈ ℤ )
65 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝐴 /L 𝑛 ) ∈ ℤ )
66 64 59 65 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝐴 /L 𝑛 ) ∈ ℤ )
67 66 zcnd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝐴 /L 𝑛 ) ∈ ℂ )
68 67 exp0d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 /L 𝑛 ) ↑ 0 ) = 1 )
69 63 68 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ 0 ) = ( ( 𝐴 /L 𝑛 ) ↑ 0 ) )
70 31 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → 𝑁 ∈ ℕ )
71 pceq0 ⊢ ( ( 𝑛 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑛 pCnt 𝑁 ) = 0 ↔ ¬ 𝑛 ∥ 𝑁 ) )
72 5 70 71 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ( ( 𝑛 pCnt 𝑁 ) = 0 ↔ ¬ 𝑛 ∥ 𝑁 ) )
73 72 biimpar ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( 𝑛 pCnt 𝑁 ) = 0 )
74 73 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ 0 ) )
75 73 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ 0 ) )
76 69 74 75 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) ∧ ¬ 𝑛 ∥ 𝑁 ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
77 57 76 pm2.61dan ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑛 ∈ ℙ ) → ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) = ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) )
78 77 ifeq1da ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) = if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
79 78 mpteq2dv ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) )
80 79 seqeq3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) )
81 80 fveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
82 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
83 82 lgsval4a ⊢ ( ( ( 𝐴 mod 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
84 3 31 83 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( ( 𝐴 mod 𝑁 ) /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
85 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
86 85 lgsval4a ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
87 86 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝐴 /L 𝑁 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( ( 𝐴 /L 𝑛 ) ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) ) ) ‘ 𝑁 ) )
88 81 84 87 3eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) )