Proof of Theorem lcmneg
Step | Hyp | Ref
| Expression |
1 | | lcm0val 10447 |
. . . . . . . 8
lcm |
2 | | znegcl 8382 |
. . . . . . . . 9
|
3 | | lcm0val 10447 |
. . . . . . . . 9
lcm
|
4 | 2, 3 | syl 14 |
. . . . . . . 8
lcm |
5 | 1, 4 | eqtr4d 2116 |
. . . . . . 7
lcm lcm
|
6 | 5 | ad2antlr 472 |
. . . . . 6
lcm lcm
|
7 | | oveq2 5540 |
. . . . . . . 8
lcm lcm |
8 | | oveq2 5540 |
. . . . . . . 8
lcm lcm |
9 | 7, 8 | eqeq12d 2095 |
. . . . . . 7
lcm lcm lcm lcm |
10 | 9 | adantl 271 |
. . . . . 6
lcm lcm
lcm lcm |
11 | 6, 10 | mpbird 165 |
. . . . 5
lcm lcm |
12 | | lcmcom 10446 |
. . . . . . 7
lcm lcm |
13 | | lcmcom 10446 |
. . . . . . . 8
lcm lcm |
14 | 2, 13 | sylan2 280 |
. . . . . . 7
lcm lcm |
15 | 12, 14 | eqeq12d 2095 |
. . . . . 6
lcm lcm
lcm lcm |
16 | 15 | adantr 270 |
. . . . 5
lcm lcm
lcm lcm |
17 | 11, 16 | mpbird 165 |
. . . 4
lcm lcm |
18 | | neg0 7354 |
. . . . . . . 8
|
19 | 18 | oveq2i 5543 |
. . . . . . 7
lcm lcm |
20 | 19 | eqcomi 2085 |
. . . . . 6
lcm lcm |
21 | | oveq2 5540 |
. . . . . 6
lcm lcm |
22 | | negeq 7301 |
. . . . . . 7
|
23 | 22 | oveq2d 5548 |
. . . . . 6
lcm lcm |
24 | 20, 21, 23 | 3eqtr4a 2139 |
. . . . 5
lcm lcm |
25 | 24 | adantl 271 |
. . . 4
lcm lcm |
26 | 17, 25 | jaodan 743 |
. . 3
lcm lcm |
27 | | dvdslcm 10451 |
. . . . . . . 8
lcm lcm |
28 | 2, 27 | sylan2 280 |
. . . . . . 7
lcm lcm |
29 | | simpr 108 |
. . . . . . . . 9
|
30 | | lcmcl 10454 |
. . . . . . . . . . 11
lcm |
31 | 2, 30 | sylan2 280 |
. . . . . . . . . 10
lcm |
32 | 31 | nn0zd 8467 |
. . . . . . . . 9
lcm |
33 | | negdvdsb 10211 |
. . . . . . . . 9
lcm lcm
lcm |
34 | 29, 32, 33 | syl2anc 403 |
. . . . . . . 8
lcm
lcm |
35 | 34 | anbi2d 451 |
. . . . . . 7
lcm lcm lcm lcm |
36 | 28, 35 | mpbird 165 |
. . . . . 6
lcm lcm |
37 | 36 | adantr 270 |
. . . . 5
lcm lcm |
38 | | zcn 8356 |
. . . . . . . . . . . . 13
|
39 | 38 | negeq0d 7411 |
. . . . . . . . . . . 12
|
40 | 39 | orbi2d 736 |
. . . . . . . . . . 11
|
41 | 40 | notbid 624 |
. . . . . . . . . 10
|
42 | 41 | biimpa 290 |
. . . . . . . . 9
|
43 | 42 | adantll 459 |
. . . . . . . 8
|
44 | | lcmn0cl 10450 |
. . . . . . . . 9
lcm |
45 | 2, 44 | sylanl2 395 |
. . . . . . . 8
lcm |
46 | 43, 45 | syldan 276 |
. . . . . . 7
lcm |
47 | | simpl 107 |
. . . . . . 7
|
48 | | 3anass 923 |
. . . . . . 7
lcm
lcm |
49 | 46, 47, 48 | sylanbrc 408 |
. . . . . 6
lcm
|
50 | | simpr 108 |
. . . . . 6
|
51 | | lcmledvds 10452 |
. . . . . 6
lcm
lcm lcm lcm lcm |
52 | 49, 50, 51 | syl2anc 403 |
. . . . 5
lcm
lcm lcm
lcm |
53 | 37, 52 | mpd 13 |
. . . 4
lcm
lcm |
54 | | dvdslcm 10451 |
. . . . . 6
lcm lcm |
55 | 54 | adantr 270 |
. . . . 5
lcm
lcm |
56 | | simplr 496 |
. . . . . . . 8
|
57 | | lcmn0cl 10450 |
. . . . . . . . 9
lcm |
58 | 57 | nnzd 8468 |
. . . . . . . 8
lcm |
59 | | negdvdsb 10211 |
. . . . . . . 8
lcm lcm lcm |
60 | 56, 58, 59 | syl2anc 403 |
. . . . . . 7
lcm lcm |
61 | 60 | anbi2d 451 |
. . . . . 6
lcm
lcm
lcm lcm |
62 | | lcmledvds 10452 |
. . . . . . . . . 10
lcm
lcm lcm
lcm lcm |
63 | 62 | ex 113 |
. . . . . . . . 9
lcm
lcm
lcm
lcm lcm |
64 | 2, 63 | syl3an3 1204 |
. . . . . . . 8
lcm
lcm
lcm
lcm lcm |
65 | 64 | 3expib 1141 |
. . . . . . 7
lcm
lcm
lcm
lcm lcm |
66 | 57, 47, 43, 65 | syl3c 62 |
. . . . . 6
lcm
lcm
lcm lcm |
67 | 61, 66 | sylbid 148 |
. . . . 5
lcm
lcm lcm
lcm |
68 | 55, 67 | mpd 13 |
. . . 4
lcm
lcm |
69 | | lcmcl 10454 |
. . . . . . 7
lcm |
70 | 69 | nn0red 8342 |
. . . . . 6
lcm |
71 | 30 | nn0red 8342 |
. . . . . . 7
lcm |
72 | 2, 71 | sylan2 280 |
. . . . . 6
lcm |
73 | 70, 72 | letri3d 7226 |
. . . . 5
lcm lcm
lcm lcm
lcm lcm |
74 | 73 | adantr 270 |
. . . 4
lcm lcm
lcm lcm
lcm lcm |
75 | 53, 68, 74 | mpbir2and 885 |
. . 3
lcm lcm |
76 | | lcmmndc 10444 |
. . . 4
DECID |
77 | | exmiddc 777 |
. . . 4
DECID
|
78 | 76, 77 | syl 14 |
. . 3
|
79 | 26, 75, 78 | mpjaodan 744 |
. 2
lcm lcm |
80 | 79 | eqcomd 2086 |
1
lcm lcm |