Metamath Proof Explorer


Theorem lgsquad3

Description: Extend lgsquad2 to integers which share a factor. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Assertion lgsquad3 M ¬ 2 M N ¬ 2 N M / L N = 1 M 1 2 N 1 2 N / L M

Proof

Step Hyp Ref Expression
1 simplrl M ¬ 2 M N ¬ 2 N M gcd N = 1 N
2 nnz N N
3 1 2 syl M ¬ 2 M N ¬ 2 N M gcd N = 1 N
4 nnz M M
5 4 ad3antrrr M ¬ 2 M N ¬ 2 N M gcd N = 1 M
6 lgscl N M N / L M
7 3 5 6 syl2anc M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M
8 7 zred M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M
9 absresq N / L M N / L M 2 = N / L M 2
10 8 9 syl M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M 2 = N / L M 2
11 gcdcom N M N gcd M = M gcd N
12 3 5 11 syl2anc M ¬ 2 M N ¬ 2 N M gcd N = 1 N gcd M = M gcd N
13 simpr M ¬ 2 M N ¬ 2 N M gcd N = 1 M gcd N = 1
14 12 13 eqtrd M ¬ 2 M N ¬ 2 N M gcd N = 1 N gcd M = 1
15 lgsabs1 N M N / L M = 1 N gcd M = 1
16 3 5 15 syl2anc M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M = 1 N gcd M = 1
17 14 16 mpbird M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M = 1
18 17 oveq1d M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M 2 = 1 2
19 sq1 1 2 = 1
20 18 19 eqtrdi M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M 2 = 1
21 7 zcnd M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M
22 21 sqvald M ¬ 2 M N ¬ 2 N M gcd N = 1 N / L M 2 = N / L M N / L M
23 10 20 22 3eqtr3d M ¬ 2 M N ¬ 2 N M gcd N = 1 1 = N / L M N / L M
24 23 oveq2d M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N 1 = M / L N N / L M N / L M
25 lgscl M N M / L N
26 5 3 25 syl2anc M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N
27 26 zcnd M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N
28 27 21 21 mulassd M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N N / L M N / L M = M / L N N / L M N / L M
29 24 28 eqtr4d M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N 1 = M / L N N / L M N / L M
30 27 mulid1d M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N 1 = M / L N
31 simplll M ¬ 2 M N ¬ 2 N M gcd N = 1 M
32 simpllr M ¬ 2 M N ¬ 2 N M gcd N = 1 ¬ 2 M
33 simplrr M ¬ 2 M N ¬ 2 N M gcd N = 1 ¬ 2 N
34 31 32 1 33 13 lgsquad2 M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N N / L M = 1 M 1 2 N 1 2
35 34 oveq1d M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N N / L M N / L M = 1 M 1 2 N 1 2 N / L M
36 29 30 35 3eqtr3d M ¬ 2 M N ¬ 2 N M gcd N = 1 M / L N = 1 M 1 2 N 1 2 N / L M
37 neg1cn 1
38 37 a1i M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 1
39 neg1ne0 1 0
40 39 a1i M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 1 0
41 4 ad3antrrr M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M
42 simpllr M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 ¬ 2 M
43 1zzd M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 1
44 2prm 2
45 nprmdvds1 2 ¬ 2 1
46 44 45 mp1i M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 ¬ 2 1
47 omoe M ¬ 2 M 1 ¬ 2 1 2 M 1
48 41 42 43 46 47 syl22anc M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 2 M 1
49 2z 2
50 2ne0 2 0
51 peano2zm M M 1
52 41 51 syl M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M 1
53 dvdsval2 2 2 0 M 1 2 M 1 M 1 2
54 49 50 52 53 mp3an12i M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 2 M 1 M 1 2
55 48 54 mpbid M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M 1 2
56 2 adantr N ¬ 2 N N
57 56 ad2antlr M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 N
58 simplrr M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 ¬ 2 N
59 omoe N ¬ 2 N 1 ¬ 2 1 2 N 1
60 57 58 43 46 59 syl22anc M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 2 N 1
61 peano2zm N N 1
62 57 61 syl M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 N 1
63 dvdsval2 2 2 0 N 1 2 N 1 N 1 2
64 49 50 62 63 mp3an12i M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 2 N 1 N 1 2
65 60 64 mpbid M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 N 1 2
66 55 65 zmulcld M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M 1 2 N 1 2
67 38 40 66 expclzd M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 1 M 1 2 N 1 2
68 67 mul01d M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 1 M 1 2 N 1 2 0 = 0
69 lgsne0 N M N / L M 0 N gcd M = 1
70 11 eqeq1d N M N gcd M = 1 M gcd N = 1
71 69 70 bitrd N M N / L M 0 M gcd N = 1
72 2 4 71 syl2anr M N N / L M 0 M gcd N = 1
73 72 necon1bbid M N ¬ M gcd N = 1 N / L M = 0
74 73 ad2ant2r M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 N / L M = 0
75 74 biimpa M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 N / L M = 0
76 75 oveq2d M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 1 M 1 2 N 1 2 N / L M = 1 M 1 2 N 1 2 0
77 lgsne0 M N M / L N 0 M gcd N = 1
78 77 necon1bbid M N ¬ M gcd N = 1 M / L N = 0
79 4 2 78 syl2an M N ¬ M gcd N = 1 M / L N = 0
80 79 ad2ant2r M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M / L N = 0
81 80 biimpa M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M / L N = 0
82 68 76 81 3eqtr4rd M ¬ 2 M N ¬ 2 N ¬ M gcd N = 1 M / L N = 1 M 1 2 N 1 2 N / L M
83 36 82 pm2.61dan M ¬ 2 M N ¬ 2 N M / L N = 1 M 1 2 N 1 2 N / L M