Metamath Proof Explorer

Theorem lgsdinn0

Description: Variation on lgsdi valid for all M , N but only for positive A . (The exact location of the failure of this law is for A = -u 1 , M = 0 , and some N in which case ( -u 1 /L 0 ) = 1 but ( -u 1 /L N ) = -u 1 when -u 1 is not a quadratic residue mod N .) (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Assertion lgsdinn0 ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐴 /L 𝑥 ) = ( 𝐴 /L 𝑁 ) )
2 1 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 0 ) ) )
3 2 eqeq2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) ↔ ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 0 ) ) ) )
4 sq1 ⊢ ( 1 ↑ 2 ) = 1
5 4 eqeq2i ⊢ ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) = 1 )
6 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
7 nn0ge0 ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
8 1re ⊢ 1 ∈ ℝ
9 0le1 ⊢ 0 ≤ 1
10 sq11 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
11 8 9 10 mpanr12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
12 6 7 11 syl2anc ⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
13 12 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) = ( 1 ↑ 2 ) ↔ 𝐴 = 1 ) )
14 5 13 bitr3id ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) = 1 ↔ 𝐴 = 1 ) )
15 14 biimpa ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → 𝐴 = 1 )
16 15 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐴 /L 𝑥 ) = ( 1 /L 𝑥 ) )
17 1lgs ⊢ ( 𝑥 ∈ ℤ → ( 1 /L 𝑥 ) = 1 )
18 17 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 1 /L 𝑥 ) = 1 )
19 16 18 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐴 /L 𝑥 ) = 1 )
20 19 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) = ( 1 · ( 𝐴 /L 0 ) ) )
21 nn0z ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
22 21 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → 𝐴 ∈ ℤ )
23 0z ⊢ 0 ∈ ℤ
24 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝐴 /L 0 ) ∈ ℤ )
25 22 23 24 sylancl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐴 /L 0 ) ∈ ℤ )
26 25 zcnd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐴 /L 0 ) ∈ ℂ )
27 26 mulid2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 1 · ( 𝐴 /L 0 ) ) = ( 𝐴 /L 0 ) )
28 20 27 eqtr2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) = 1 ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) )
29 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝐴 /L 𝑥 ) ∈ ℤ )
30 21 29 sylan ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( 𝐴 /L 𝑥 ) ∈ ℤ )
31 30 zcnd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( 𝐴 /L 𝑥 ) ∈ ℂ )
32 31 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) ≠ 1 ) → ( 𝐴 /L 𝑥 ) ∈ ℂ )
33 32 mul01d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) ≠ 1 ) → ( ( 𝐴 /L 𝑥 ) · 0 ) = 0 )
34 21 adantr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ ℤ )
35 lgs0 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )
36 34 35 syl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( 𝐴 /L 0 ) = if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) )
37 ifnefalse ⊢ ( ( 𝐴 ↑ 2 ) ≠ 1 → if ( ( 𝐴 ↑ 2 ) = 1 , 1 , 0 ) = 0 )
38 36 37 sylan9eq ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) ≠ 1 ) → ( 𝐴 /L 0 ) = 0 )
39 38 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) ≠ 1 ) → ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) = ( ( 𝐴 /L 𝑥 ) · 0 ) )
40 33 39 38 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) ∧ ( 𝐴 ↑ 2 ) ≠ 1 ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) )
41 28 40 pm2.61dane ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) )
42 41 ralrimiva ⊢ ( 𝐴 ∈ ℕ0 → ∀ 𝑥 ∈ ℤ ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) )
43 42 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∀ 𝑥 ∈ ℤ ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) )
44 simp3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
45 3 43 44 rspcdva ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 0 ) ) )
46 45 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 0 ) ) )
47 21 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℤ )
48 47 23 24 sylancl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 0 ) ∈ ℤ )
49 48 zcnd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 0 ) ∈ ℂ )
50 49 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L 0 ) ∈ ℂ )
51 lgscl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
52 47 44 51 syl2anc ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
53 52 zcnd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℂ )
54 53 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L 𝑁 ) ∈ ℂ )
55 50 54 mulcomd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( ( 𝐴 /L 0 ) · ( 𝐴 /L 𝑁 ) ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 0 ) ) )
56 46 55 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 0 ) · ( 𝐴 /L 𝑁 ) ) )
57 oveq1 ⊢ ( 𝑀 = 0 → ( 𝑀 · 𝑁 ) = ( 0 · 𝑁 ) )
58 44 zcnd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
59 58 mul02d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 · 𝑁 ) = 0 )
60 57 59 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑁 ) = 0 )
61 60 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( 𝐴 /L 0 ) )
62 simpr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝑀 = 0 )
63 62 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L 𝑀 ) = ( 𝐴 /L 0 ) )
64 63 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) = ( ( 𝐴 /L 0 ) · ( 𝐴 /L 𝑁 ) ) )
65 56 61 64 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )
66 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐴 /L 𝑥 ) = ( 𝐴 /L 𝑀 ) )
67 66 oveq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 0 ) ) )
68 67 eqeq2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑥 ) · ( 𝐴 /L 0 ) ) ↔ ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 0 ) ) ) )
69 simp2 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
70 68 43 69 rspcdva ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 0 ) ) )
71 70 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝐴 /L 0 ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 0 ) ) )
72 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑀 · 𝑁 ) = ( 𝑀 · 0 ) )
73 69 zcnd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℂ )
74 73 mul01d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 0 ) = 0 )
75 72 74 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝑀 · 𝑁 ) = 0 )
76 75 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( 𝐴 /L 0 ) )
77 simpr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → 𝑁 = 0 )
78 77 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝐴 /L 𝑁 ) = ( 𝐴 /L 0 ) )
79 78 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 0 ) ) )
80 71 76 79 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 = 0 ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )
81 lgsdi ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )
82 21 81 syl3anl1 ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≠ 0 ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )
83 65 80 82 pm2.61da2ne ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 /L 𝑀 ) · ( 𝐴 /L 𝑁 ) ) )