Metamath Proof Explorer

Theorem lgsdirnn0

Description: Variation on lgsdir valid for all A , B but only for positive N . (The exact location of the failure of this law is for A = 0 , B < 0 , N = -u 1 in which case ( 0 /L -u 1 ) = 1 but ( B /L -u 1 ) = -u 1 .) (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Assertion lgsdirnn0 
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = B -> ( x /L N ) = ( B /L N ) )
2 1 oveq1d 
 |-  ( x = B -> ( ( x /L N ) x. ( 0 /L N ) ) = ( ( B /L N ) x. ( 0 /L N ) ) )
3 2 eqeq2d 
 |-  ( x = B -> ( ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) <-> ( 0 /L N ) = ( ( B /L N ) x. ( 0 /L N ) ) ) )
4 id 
 |-  ( x e. ZZ -> x e. ZZ )
5 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
6 lgscl 
 |-  ( ( x e. ZZ /\ N e. ZZ ) -> ( x /L N ) e. ZZ )
7 4 5 6 syl2anr 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( x /L N ) e. ZZ )
8 7 zcnd 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( x /L N ) e. CC )
9 8 adantr 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) = 0 ) -> ( x /L N ) e. CC )
10 9 mul01d 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) = 0 ) -> ( ( x /L N ) x. 0 ) = 0 )
11 simpr 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) = 0 ) -> ( 0 /L N ) = 0 )
12 11 oveq2d 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) = 0 ) -> ( ( x /L N ) x. ( 0 /L N ) ) = ( ( x /L N ) x. 0 ) )
13 10 12 11 3eqtr4rd 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) = 0 ) -> ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) )
14 0z 
 |-  0 e. ZZ
15 5 adantr 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> N e. ZZ )
16 lgsne0 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( ( 0 /L N ) =/= 0 <-> ( 0 gcd N ) = 1 ) )
17 14 15 16 sylancr 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( 0 /L N ) =/= 0 <-> ( 0 gcd N ) = 1 ) )
18 gcdcom 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 gcd N ) = ( N gcd 0 ) )
19 14 15 18 sylancr 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( 0 gcd N ) = ( N gcd 0 ) )
20 nn0gcdid0 
 |-  ( N e. NN0 -> ( N gcd 0 ) = N )
21 20 adantr 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( N gcd 0 ) = N )
22 19 21 eqtrd 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( 0 gcd N ) = N )
23 22 eqeq1d 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( 0 gcd N ) = 1 <-> N = 1 ) )
24 lgs1 
 |-  ( x e. ZZ -> ( x /L 1 ) = 1 )
25 24 adantl 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( x /L 1 ) = 1 )
26 oveq2 
 |-  ( N = 1 -> ( x /L N ) = ( x /L 1 ) )
27 26 eqeq1d 
 |-  ( N = 1 -> ( ( x /L N ) = 1 <-> ( x /L 1 ) = 1 ) )
28 25 27 syl5ibrcom 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( N = 1 -> ( x /L N ) = 1 ) )
29 23 28 sylbid 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( 0 gcd N ) = 1 -> ( x /L N ) = 1 ) )
30 17 29 sylbid 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( 0 /L N ) =/= 0 -> ( x /L N ) = 1 ) )
31 30 imp 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> ( x /L N ) = 1 )
32 31 oveq1d 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> ( ( x /L N ) x. ( 0 /L N ) ) = ( 1 x. ( 0 /L N ) ) )
33 5 ad2antrr 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> N e. ZZ )
34 lgscl 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 /L N ) e. ZZ )
35 14 33 34 sylancr 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> ( 0 /L N ) e. ZZ )
36 35 zcnd 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> ( 0 /L N ) e. CC )
37 36 mullidd 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> ( 1 x. ( 0 /L N ) ) = ( 0 /L N ) )
38 32 37 eqtr2d 
 |-  ( ( ( N e. NN0 /\ x e. ZZ ) /\ ( 0 /L N ) =/= 0 ) -> ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) )
39 13 38 pm2.61dane 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) )
40 39 ralrimiva 
 |-  ( N e. NN0 -> A. x e. ZZ ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) )
41 40 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> A. x e. ZZ ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) )
42 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> B e. ZZ )
43 3 41 42 rspcdva 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( 0 /L N ) = ( ( B /L N ) x. ( 0 /L N ) ) )
44 43 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( 0 /L N ) = ( ( B /L N ) x. ( 0 /L N ) ) )
45 5 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> N e. ZZ )
46 14 45 34 sylancr 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( 0 /L N ) e. ZZ )
47 46 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( 0 /L N ) e. CC )
48 47 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( 0 /L N ) e. CC )
49 lgscl 
 |-  ( ( B e. ZZ /\ N e. ZZ ) -> ( B /L N ) e. ZZ )
50 42 45 49 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( B /L N ) e. ZZ )
51 50 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( B /L N ) e. CC )
52 51 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( B /L N ) e. CC )
53 48 52 mulcomd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( ( 0 /L N ) x. ( B /L N ) ) = ( ( B /L N ) x. ( 0 /L N ) ) )
54 44 53 eqtr4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( 0 /L N ) = ( ( 0 /L N ) x. ( B /L N ) ) )
55 oveq1 
 |-  ( A = 0 -> ( A x. B ) = ( 0 x. B ) )
56 zcn 
 |-  ( B e. ZZ -> B e. CC )
57 56 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> B e. CC )
58 57 mul02d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( 0 x. B ) = 0 )
59 55 58 sylan9eqr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( A x. B ) = 0 )
60 59 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( ( A x. B ) /L N ) = ( 0 /L N ) )
61 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> A = 0 )
62 61 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( A /L N ) = ( 0 /L N ) )
63 62 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( ( A /L N ) x. ( B /L N ) ) = ( ( 0 /L N ) x. ( B /L N ) ) )
64 54 60 63 3eqtr4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ A = 0 ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
65 oveq1 
 |-  ( x = A -> ( x /L N ) = ( A /L N ) )
66 65 oveq1d 
 |-  ( x = A -> ( ( x /L N ) x. ( 0 /L N ) ) = ( ( A /L N ) x. ( 0 /L N ) ) )
67 66 eqeq2d 
 |-  ( x = A -> ( ( 0 /L N ) = ( ( x /L N ) x. ( 0 /L N ) ) <-> ( 0 /L N ) = ( ( A /L N ) x. ( 0 /L N ) ) ) )
68 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> A e. ZZ )
69 67 41 68 rspcdva 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( 0 /L N ) = ( ( A /L N ) x. ( 0 /L N ) ) )
70 69 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> ( 0 /L N ) = ( ( A /L N ) x. ( 0 /L N ) ) )
71 oveq2 
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
72 68 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> A e. CC )
73 72 mul01d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A x. 0 ) = 0 )
74 71 73 sylan9eqr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> ( A x. B ) = 0 )
75 74 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> ( ( A x. B ) /L N ) = ( 0 /L N ) )
76 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> B = 0 )
77 76 oveq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> ( B /L N ) = ( 0 /L N ) )
78 77 oveq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> ( ( A /L N ) x. ( B /L N ) ) = ( ( A /L N ) x. ( 0 /L N ) ) )
79 70 75 78 3eqtr4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ B = 0 ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
80 lgsdir 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. ZZ ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
81 5 80 syl3anl3 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )
82 64 79 81 pm2.61da2ne 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) )