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 
|- ( ( A e. NN0 /\ M e. ZZ /\ N e. ZZ ) -> ( A /L ( M x. N ) ) = ( ( A /L M ) x. ( A /L N ) ) )

Proof

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