ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lgsquad3 Unicode version

Theorem lgsquad3 16088
Description: Extend lgsquad2 16087 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015.)
Assertion
Ref Expression
lgsquad3  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( M  /L
N )  =  ( ( -u 1 ^ ( ( ( M  -  1 )  / 
2 )  x.  (
( N  -  1 )  /  2 ) ) )  x.  ( N  /L M ) ) )

Proof of Theorem lgsquad3
StepHypRef Expression
1 simplrl 537 . . . . . . . . . 10  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  N  e.  NN )
21nnzd 9721 . . . . . . . . 9  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  N  e.  ZZ )
3 nnz 9617 . . . . . . . . . 10  |-  ( M  e.  NN  ->  M  e.  ZZ )
43ad3antrrr 492 . . . . . . . . 9  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  M  e.  ZZ )
5 lgscl 16018 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( N  /L
M )  e.  ZZ )
62, 4, 5syl2anc 411 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( N  /L M )  e.  ZZ )
76zred 9722 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( N  /L M )  e.  RR )
8 absresq 11793 . . . . . . 7  |-  ( ( N  /L M )  e.  RR  ->  ( ( abs `  ( N  /L M ) ) ^ 2 )  =  ( ( N  /L M ) ^ 2 ) )
97, 8syl 14 . . . . . 6  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( abs `  ( N  /L
M ) ) ^
2 )  =  ( ( N  /L
M ) ^ 2 ) )
102, 4gcdcomd 12700 . . . . . . . . . 10  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( N  gcd  M )  =  ( M  gcd  N ) )
11 simpr 110 . . . . . . . . . 10  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( M  gcd  N )  =  1 )
1210, 11eqtrd 2267 . . . . . . . . 9  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( N  gcd  M )  =  1 )
13 lgsabs1 16043 . . . . . . . . . 10  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( abs `  ( N  /L M ) )  =  1  <->  ( N  gcd  M )  =  1 ) )
142, 4, 13syl2anc 411 . . . . . . . . 9  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( abs `  ( N  /L
M ) )  =  1  <->  ( N  gcd  M )  =  1 ) )
1512, 14mpbird 167 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( abs `  ( N  /L M ) )  =  1 )
1615oveq1d 6074 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( abs `  ( N  /L
M ) ) ^
2 )  =  ( 1 ^ 2 ) )
17 sq1 11023 . . . . . . 7  |-  ( 1 ^ 2 )  =  1
1816, 17eqtrdi 2283 . . . . . 6  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( abs `  ( N  /L
M ) ) ^
2 )  =  1 )
196zcnd 9723 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( N  /L M )  e.  CC )
2019sqvald 11061 . . . . . 6  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( N  /L M ) ^ 2 )  =  ( ( N  /L M )  x.  ( N  /L
M ) ) )
219, 18, 203eqtr3d 2275 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  1  =  ( ( N  /L
M )  x.  ( N  /L M ) ) )
2221oveq2d 6075 . . . 4  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( M  /L N )  x.  1 )  =  ( ( M  /L N )  x.  ( ( N  /L M )  x.  ( N  /L
M ) ) ) )
23 lgscl 16018 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  /L
N )  e.  ZZ )
244, 2, 23syl2anc 411 . . . . . 6  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( M  /L N )  e.  ZZ )
2524zcnd 9723 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( M  /L N )  e.  CC )
2625, 19, 19mulassd 8314 . . . 4  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( ( M  /L N )  x.  ( N  /L M ) )  x.  ( N  /L M ) )  =  ( ( M  /L N )  x.  ( ( N  /L M )  x.  ( N  /L M ) ) ) )
2722, 26eqtr4d 2270 . . 3  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( M  /L N )  x.  1 )  =  ( ( ( M  /L N )  x.  ( N  /L M ) )  x.  ( N  /L M ) ) )
2825mulridd 8308 . . 3  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( M  /L N )  x.  1 )  =  ( M  /L
N ) )
29 simplll 535 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  M  e.  NN )
30 simpllr 536 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  -.  2  ||  M )
31 simplrr 538 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  -.  2  ||  N )
3229, 30, 1, 31, 11lgsquad2 16087 . . . 4  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( M  /L N )  x.  ( N  /L M ) )  =  ( -u 1 ^ ( ( ( M  -  1 )  /  2 )  x.  ( ( N  - 
1 )  /  2
) ) ) )
3332oveq1d 6074 . . 3  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( ( ( M  /L N )  x.  ( N  /L M ) )  x.  ( N  /L M ) )  =  ( (
-u 1 ^ (
( ( M  - 
1 )  /  2
)  x.  ( ( N  -  1 )  /  2 ) ) )  x.  ( N  /L M ) ) )
3427, 28, 333eqtr3d 2275 . 2  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  ( M  gcd  N )  =  1 )  ->  ( M  /L N )  =  ( ( -u 1 ^ ( ( ( M  -  1 )  /  2 )  x.  ( ( N  - 
1 )  /  2
) ) )  x.  ( N  /L
M ) ) )
35 neg1cn 9363 . . . . . 6  |-  -u 1  e.  CC
3635a1i 9 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  -u 1  e.  CC )
37 neg1ap0 9367 . . . . . 6  |-  -u 1 #  0
3837a1i 9 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  -u 1 #  0 )
393ad3antrrr 492 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  M  e.  ZZ )
40 simpllr 536 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  -.  2  ||  M )
41 1zzd 9625 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  1  e.  ZZ )
42 2prm 12854 . . . . . . . . 9  |-  2  e.  Prime
43 nprmdvds1 12867 . . . . . . . . 9  |-  ( 2  e.  Prime  ->  -.  2  ||  1 )
4442, 43mp1i 10 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  -.  2  ||  1 )
45 omoe 12612 . . . . . . . 8  |-  ( ( ( M  e.  ZZ  /\ 
-.  2  ||  M
)  /\  ( 1  e.  ZZ  /\  -.  2  ||  1 ) )  ->  2  ||  ( M  -  1 ) )
4639, 40, 41, 44, 45syl22anc 1275 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  2  ||  ( M  -  1 ) )
47 2z 9626 . . . . . . . 8  |-  2  e.  ZZ
48 2ne0 9350 . . . . . . . 8  |-  2  =/=  0
49 peano2zm 9636 . . . . . . . . 9  |-  ( M  e.  ZZ  ->  ( M  -  1 )  e.  ZZ )
5039, 49syl 14 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  ( M  -  1 )  e.  ZZ )
51 dvdsval2 12506 . . . . . . . 8  |-  ( ( 2  e.  ZZ  /\  2  =/=  0  /\  ( M  -  1 )  e.  ZZ )  -> 
( 2  ||  ( M  -  1 )  <-> 
( ( M  - 
1 )  /  2
)  e.  ZZ ) )
5247, 48, 50, 51mp3an12i 1378 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
2  ||  ( M  -  1 )  <->  ( ( M  -  1 )  /  2 )  e.  ZZ ) )
5346, 52mpbid 147 . . . . . 6  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
( M  -  1 )  /  2 )  e.  ZZ )
54 nnz 9617 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  e.  ZZ )
5554adantr 276 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  -.  2  ||  N )  ->  N  e.  ZZ )
5655ad2antlr 489 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  N  e.  ZZ )
57 simplrr 538 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  -.  2  ||  N )
58 omoe 12612 . . . . . . . 8  |-  ( ( ( N  e.  ZZ  /\ 
-.  2  ||  N
)  /\  ( 1  e.  ZZ  /\  -.  2  ||  1 ) )  ->  2  ||  ( N  -  1 ) )
5956, 57, 41, 44, 58syl22anc 1275 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  2  ||  ( N  -  1 ) )
60 peano2zm 9636 . . . . . . . . 9  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
6156, 60syl 14 . . . . . . . 8  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  ( N  -  1 )  e.  ZZ )
62 dvdsval2 12506 . . . . . . . 8  |-  ( ( 2  e.  ZZ  /\  2  =/=  0  /\  ( N  -  1 )  e.  ZZ )  -> 
( 2  ||  ( N  -  1 )  <-> 
( ( N  - 
1 )  /  2
)  e.  ZZ ) )
6347, 48, 61, 62mp3an12i 1378 . . . . . . 7  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
2  ||  ( N  -  1 )  <->  ( ( N  -  1 )  /  2 )  e.  ZZ ) )
6459, 63mpbid 147 . . . . . 6  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
( N  -  1 )  /  2 )  e.  ZZ )
6553, 64zmulcld 9728 . . . . 5  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
( ( M  - 
1 )  /  2
)  x.  ( ( N  -  1 )  /  2 ) )  e.  ZZ )
6636, 38, 65expclzapd 11069 . . . 4  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  ( -u 1 ^ ( ( ( M  -  1 )  /  2 )  x.  ( ( N  -  1 )  / 
2 ) ) )  e.  CC )
6766mul01d 8685 . . 3  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
( -u 1 ^ (
( ( M  - 
1 )  /  2
)  x.  ( ( N  -  1 )  /  2 ) ) )  x.  0 )  =  0 )
6854, 3, 5syl2anr 290 . . . . . . . 8  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( N  /L
M )  e.  ZZ )
69 0zd 9610 . . . . . . . 8  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  0  e.  ZZ )
70 zdceq 9674 . . . . . . . 8  |-  ( ( ( N  /L
M )  e.  ZZ  /\  0  e.  ZZ )  -> DECID 
( N  /L
M )  =  0 )
7168, 69, 70syl2anc 411 . . . . . . 7  |-  ( ( M  e.  NN  /\  N  e.  NN )  -> DECID  ( N  /L M )  =  0 )
72 lgsne0 16042 . . . . . . . . . . 11  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( N  /L M )  =/=  0  <->  ( N  gcd  M )  =  1 ) )
73 gcdcom 12699 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( N  gcd  M
)  =  ( M  gcd  N ) )
7473eqeq1d 2243 . . . . . . . . . . 11  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( N  gcd  M )  =  1  <->  ( M  gcd  N )  =  1 ) )
7572, 74bitrd 188 . . . . . . . . . 10  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( ( N  /L M )  =/=  0  <->  ( M  gcd  N )  =  1 ) )
7654, 3, 75syl2anr 290 . . . . . . . . 9  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( ( N  /L M )  =/=  0  <->  ( M  gcd  N )  =  1 ) )
7776a1d 22 . . . . . . . 8  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  (DECID  ( N  /L
M )  =  0  ->  ( ( N  /L M )  =/=  0  <->  ( M  gcd  N )  =  1 ) ) )
7877necon1bbiddc 2477 . . . . . . 7  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  (DECID  ( N  /L
M )  =  0  ->  ( -.  ( M  gcd  N )  =  1  <->  ( N  /L M )  =  0 ) ) )
7971, 78mpd 13 . . . . . 6  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( -.  ( M  gcd  N )  =  1  <->  ( N  /L M )  =  0 ) )
8079ad2ant2r 509 . . . . 5  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( -.  ( M  gcd  N )  =  1  <->  ( N  /L M )  =  0 ) )
8180biimpa 296 . . . 4  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  ( N  /L M )  =  0 )
8281oveq2d 6075 . . 3  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  (
( -u 1 ^ (
( ( M  - 
1 )  /  2
)  x.  ( ( N  -  1 )  /  2 ) ) )  x.  ( N  /L M ) )  =  ( (
-u 1 ^ (
( ( M  - 
1 )  /  2
)  x.  ( ( N  -  1 )  /  2 ) ) )  x.  0 ) )
83 0zd 9610 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  0  e.  ZZ )
84 zdceq 9674 . . . . . . . 8  |-  ( ( ( M  /L
N )  e.  ZZ  /\  0  e.  ZZ )  -> DECID 
( M  /L
N )  =  0 )
8523, 83, 84syl2anc 411 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  -> DECID  ( M  /L N )  =  0 )
86 lgsne0 16042 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( M  /L N )  =/=  0  <->  ( M  gcd  N )  =  1 ) )
8786a1d 22 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  (DECID  ( M  /L
N )  =  0  ->  ( ( M  /L N )  =/=  0  <->  ( M  gcd  N )  =  1 ) ) )
8887necon1bbiddc 2477 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  (DECID  ( M  /L
N )  =  0  ->  ( -.  ( M  gcd  N )  =  1  <->  ( M  /L N )  =  0 ) ) )
8985, 88mpd 13 . . . . . 6  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( -.  ( M  gcd  N )  =  1  <->  ( M  /L N )  =  0 ) )
903, 54, 89syl2an 289 . . . . 5  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( -.  ( M  gcd  N )  =  1  <->  ( M  /L N )  =  0 ) )
9190ad2ant2r 509 . . . 4  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( -.  ( M  gcd  N )  =  1  <->  ( M  /L N )  =  0 ) )
9291biimpa 296 . . 3  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  ( M  /L N )  =  0 )
9367, 82, 923eqtr4rd 2278 . 2  |-  ( ( ( ( M  e.  NN  /\  -.  2  ||  M )  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  /\  -.  ( M  gcd  N )  =  1 )  ->  ( M  /L N )  =  ( ( -u
1 ^ ( ( ( M  -  1 )  /  2 )  x.  ( ( N  -  1 )  / 
2 ) ) )  x.  ( N  /L M ) ) )
94 gcdnncl 12693 . . . . . 6  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( M  gcd  N
)  e.  NN )
9594ad2ant2r 509 . . . . 5  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( M  gcd  N
)  e.  NN )
9695nnzd 9721 . . . 4  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( M  gcd  N
)  e.  ZZ )
97 1zzd 9625 . . . 4  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
1  e.  ZZ )
98 zdceq 9674 . . . 4  |-  ( ( ( M  gcd  N
)  e.  ZZ  /\  1  e.  ZZ )  -> DECID  ( M  gcd  N )  =  1 )
9996, 97, 98syl2anc 411 . . 3  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> DECID  ( M  gcd  N )  =  1 )
100 exmiddc 844 . . 3  |-  (DECID  ( M  gcd  N )  =  1  ->  ( ( M  gcd  N )  =  1  \/  -.  ( M  gcd  N )  =  1 ) )
10199, 100syl 14 . 2  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( ( M  gcd  N )  =  1  \/ 
-.  ( M  gcd  N )  =  1 ) )
10234, 93, 101mpjaodan 806 1  |-  ( ( ( M  e.  NN  /\ 
-.  2  ||  M
)  /\  ( N  e.  NN  /\  -.  2  ||  N ) )  -> 
( M  /L
N )  =  ( ( -u 1 ^ ( ( ( M  -  1 )  / 
2 )  x.  (
( N  -  1 )  /  2 ) ) )  x.  ( N  /L M ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 716  DECID wdc 842    = wceq 1398    e. wcel 2205    =/= wne 2414   class class class wbr 4115   ` cfv 5358  (class class class)co 6059   CCcc 8142   RRcr 8143   0cc0 8144   1c1 8145    x. cmul 8149    - cmin 8462   -ucneg 8463   # cap 8874    / cdiv 8967   NNcn 9258   2c2 9309   ZZcz 9598   ^cexp 10928   abscabs 11712    || cdvds 12503    gcd cgcd 12679   Primecprime 12834    /Lclgs 16001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4231  ax-sep 4234  ax-nul 4242  ax-pow 4293  ax-pr 4328  ax-un 4560  ax-setind 4665  ax-iinf 4716  ax-cnex 8235  ax-resscn 8236  ax-1cn 8237  ax-1re 8238  ax-icn 8239  ax-addcl 8240  ax-addrcl 8241  ax-mulcl 8242  ax-mulrcl 8243  ax-addcom 8244  ax-mulcom 8245  ax-addass 8246  ax-mulass 8247  ax-distr 8248  ax-i2m1 8249  ax-0lt1 8250  ax-1rid 8251  ax-0id 8252  ax-rnegex 8253  ax-precex 8254  ax-cnre 8255  ax-pre-ltirr 8256  ax-pre-ltwlin 8257  ax-pre-lttrn 8258  ax-pre-apti 8259  ax-pre-ltadd 8260  ax-pre-mulgt0 8261  ax-pre-mulext 8262  ax-arch 8263  ax-caucvg 8264  ax-addf 8266  ax-mulf 8267
This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-xor 1421  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rmo 2530  df-rab 2531  df-v 2817  df-sbc 3046  df-csb 3142  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-nul 3513  df-if 3626  df-pw 3677  df-sn 3701  df-pr 3702  df-tp 3703  df-op 3704  df-uni 3921  df-int 3956  df-iun 3999  df-disj 4092  df-br 4116  df-opab 4178  df-mpt 4179  df-tr 4215  df-id 4420  df-po 4423  df-iso 4424  df-iord 4493  df-on 4495  df-ilim 4496  df-suc 4498  df-iom 4719  df-xp 4761  df-rel 4762  df-cnv 4763  df-co 4764  df-dm 4765  df-rn 4766  df-res 4767  df-ima 4768  df-iota 5318  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-isom 5367  df-riota 6012  df-ov 6062  df-oprab 6063  df-mpo 6064  df-of 6276  df-1st 6348  df-2nd 6349  df-tpos 6490  df-recs 6550  df-irdg 6615  df-frec 6636  df-1o 6661  df-2o 6662  df-oadd 6665  df-er 6781  df-ec 6783  df-qs 6787  df-map 6898  df-en 6990  df-dom 6991  df-fin 6992  df-sup 7289  df-inf 7290  df-pnf 8327  df-mnf 8328  df-xr 8329  df-ltxr 8330  df-le 8331  df-sub 8464  df-neg 8465  df-reap 8868  df-ap 8875  df-div 8968  df-inn 9259  df-2 9317  df-3 9318  df-4 9319  df-5 9320  df-6 9321  df-7 9322  df-8 9323  df-9 9324  df-n0 9518  df-z 9599  df-dec 9732  df-uz 9876  df-q 9974  df-rp 10009  df-fz 10366  df-fzo 10503  df-fl 10658  df-mod 10713  df-seqfrec 10838  df-exp 10929  df-ihash 11168  df-cj 11556  df-re 11557  df-im 11558  df-rsqrt 11713  df-abs 11714  df-clim 11994  df-sumdc 12069  df-proddc 12267  df-dvds 12504  df-gcd 12680  df-prm 12835  df-phi 12938  df-pc 13013  df-struct 13303  df-ndx 13304  df-slot 13305  df-base 13307  df-sets 13308  df-iress 13309  df-plusg 13392  df-mulr 13393  df-starv 13394  df-sca 13395  df-vsca 13396  df-ip 13397  df-tset 13398  df-ple 13399  df-ds 13401  df-unif 13402  df-0g 13560  df-igsum 13561  df-topgen 13562  df-iimas 13572  df-qus 13573  df-mgm 13624  df-sgrp 13670  df-mnd 13683  df-mhm 13719  df-submnd 13720  df-grp 13763  df-minusg 13764  df-sbg 13765  df-mulg 13878  df-subg 13928  df-nsg 13929  df-eqg 13930  df-ghm 13999  df-cmn 14044  df-abl 14045  df-mgp 14165  df-rng 14177  df-ur 14208  df-srg 14212  df-ring 14246  df-cring 14247  df-oppr 14316  df-dvdsr 14338  df-unit 14339  df-invr 14371  df-dvr 14382  df-rhm 14402  df-nzr 14430  df-subrg 14470  df-domn 14510  df-idom 14511  df-lmod 14568  df-lssm 14632  df-lsp 14666  df-sra 14714  df-rgmod 14715  df-lidl 14748  df-rsp 14749  df-2idl 14779  df-bl 14825  df-mopn 14826  df-fg 14828  df-metu 14829  df-cnfld 14836  df-zring 14870  df-zrh 14893  df-zn 14895  df-lgs 16002
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator