Proof of Theorem lcmneg
Step | Hyp | Ref
| Expression |
1 | | lcm0val 15307 |
. . . . . . . 8
lcm |
2 | | znegcl 11412 |
. . . . . . . . 9
|
3 | | lcm0val 15307 |
. . . . . . . . 9
lcm
|
4 | 2, 3 | syl 17 |
. . . . . . . 8
lcm |
5 | 1, 4 | eqtr4d 2659 |
. . . . . . 7
lcm lcm
|
6 | 5 | ad2antlr 763 |
. . . . . 6
lcm lcm
|
7 | | oveq2 6658 |
. . . . . . . 8
lcm lcm |
8 | | oveq2 6658 |
. . . . . . . 8
lcm lcm |
9 | 7, 8 | eqeq12d 2637 |
. . . . . . 7
lcm lcm lcm lcm |
10 | 9 | adantl 482 |
. . . . . 6
lcm lcm
lcm lcm |
11 | 6, 10 | mpbird 247 |
. . . . 5
lcm lcm |
12 | | lcmcom 15306 |
. . . . . . 7
lcm lcm |
13 | | lcmcom 15306 |
. . . . . . . 8
lcm lcm |
14 | 2, 13 | sylan2 491 |
. . . . . . 7
lcm lcm |
15 | 12, 14 | eqeq12d 2637 |
. . . . . 6
lcm lcm
lcm lcm |
16 | 15 | adantr 481 |
. . . . 5
lcm lcm
lcm lcm |
17 | 11, 16 | mpbird 247 |
. . . 4
lcm lcm |
18 | | neg0 10327 |
. . . . . . . 8
|
19 | 18 | oveq2i 6661 |
. . . . . . 7
lcm lcm |
20 | 19 | eqcomi 2631 |
. . . . . 6
lcm lcm |
21 | | oveq2 6658 |
. . . . . 6
lcm lcm |
22 | | negeq 10273 |
. . . . . . 7
|
23 | 22 | oveq2d 6666 |
. . . . . 6
lcm lcm |
24 | 20, 21, 23 | 3eqtr4a 2682 |
. . . . 5
lcm lcm |
25 | 24 | adantl 482 |
. . . 4
lcm lcm |
26 | 17, 25 | jaodan 826 |
. . 3
lcm lcm |
27 | | dvdslcm 15311 |
. . . . . . . 8
lcm lcm |
28 | 2, 27 | sylan2 491 |
. . . . . . 7
lcm lcm |
29 | | simpr 477 |
. . . . . . . . 9
|
30 | | lcmcl 15314 |
. . . . . . . . . . 11
lcm |
31 | 2, 30 | sylan2 491 |
. . . . . . . . . 10
lcm |
32 | 31 | nn0zd 11480 |
. . . . . . . . 9
lcm |
33 | | negdvdsb 14998 |
. . . . . . . . 9
lcm lcm
lcm |
34 | 29, 32, 33 | syl2anc 693 |
. . . . . . . 8
lcm
lcm |
35 | 34 | anbi2d 740 |
. . . . . . 7
lcm lcm lcm lcm |
36 | 28, 35 | mpbird 247 |
. . . . . 6
lcm lcm |
37 | 36 | adantr 481 |
. . . . 5
lcm lcm |
38 | | zcn 11382 |
. . . . . . . . . . . . 13
|
39 | 38 | negeq0d 10384 |
. . . . . . . . . . . 12
|
40 | 39 | orbi2d 738 |
. . . . . . . . . . 11
|
41 | 40 | notbid 308 |
. . . . . . . . . 10
|
42 | 41 | biimpa 501 |
. . . . . . . . 9
|
43 | 42 | adantll 750 |
. . . . . . . 8
|
44 | | lcmn0cl 15310 |
. . . . . . . . 9
lcm |
45 | 2, 44 | sylanl2 683 |
. . . . . . . 8
lcm |
46 | 43, 45 | syldan 487 |
. . . . . . 7
lcm |
47 | | simpl 473 |
. . . . . . 7
|
48 | | 3anass 1042 |
. . . . . . 7
lcm
lcm |
49 | 46, 47, 48 | sylanbrc 698 |
. . . . . 6
lcm
|
50 | | simpr 477 |
. . . . . 6
|
51 | | lcmledvds 15312 |
. . . . . 6
lcm
lcm lcm lcm lcm |
52 | 49, 50, 51 | syl2anc 693 |
. . . . 5
lcm
lcm lcm
lcm |
53 | 37, 52 | mpd 15 |
. . . 4
lcm
lcm |
54 | | dvdslcm 15311 |
. . . . . 6
lcm lcm |
55 | 54 | adantr 481 |
. . . . 5
lcm
lcm |
56 | | simplr 792 |
. . . . . . . 8
|
57 | | lcmn0cl 15310 |
. . . . . . . . 9
lcm |
58 | 57 | nnzd 11481 |
. . . . . . . 8
lcm |
59 | | negdvdsb 14998 |
. . . . . . . 8
lcm lcm lcm |
60 | 56, 58, 59 | syl2anc 693 |
. . . . . . 7
lcm lcm |
61 | 60 | anbi2d 740 |
. . . . . 6
lcm
lcm
lcm lcm |
62 | | lcmledvds 15312 |
. . . . . . . . . 10
lcm
lcm lcm
lcm lcm |
63 | 62 | ex 450 |
. . . . . . . . 9
lcm
lcm
lcm
lcm lcm |
64 | 2, 63 | syl3an3 1361 |
. . . . . . . 8
lcm
lcm
lcm
lcm lcm |
65 | 64 | 3expib 1268 |
. . . . . . 7
lcm
lcm
lcm
lcm lcm |
66 | 57, 47, 43, 65 | syl3c 66 |
. . . . . 6
lcm
lcm
lcm lcm |
67 | 61, 66 | sylbid 230 |
. . . . 5
lcm
lcm lcm
lcm |
68 | 55, 67 | mpd 15 |
. . . 4
lcm
lcm |
69 | | lcmcl 15314 |
. . . . . . 7
lcm |
70 | 69 | nn0red 11352 |
. . . . . 6
lcm |
71 | 30 | nn0red 11352 |
. . . . . . 7
lcm |
72 | 2, 71 | sylan2 491 |
. . . . . 6
lcm |
73 | 70, 72 | letri3d 10179 |
. . . . 5
lcm lcm
lcm lcm
lcm lcm |
74 | 73 | adantr 481 |
. . . 4
lcm lcm
lcm lcm
lcm lcm |
75 | 53, 68, 74 | mpbir2and 957 |
. . 3
lcm lcm |
76 | 26, 75 | pm2.61dan 832 |
. 2
lcm lcm |
77 | 76 | eqcomd 2628 |
1
lcm lcm |