Proof of Theorem lcmdvds
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
|
2 | | breq1 4656 |
. . . . . . . 8
|
3 | 2 | adantl 482 |
. . . . . . 7
|
4 | | oveq1 6657 |
. . . . . . . . 9
lcm lcm |
5 | | 0z 11388 |
. . . . . . . . . . 11
|
6 | | lcmcom 15306 |
. . . . . . . . . . 11
lcm lcm |
7 | 5, 6 | mpan 706 |
. . . . . . . . . 10
lcm lcm |
8 | | lcm0val 15307 |
. . . . . . . . . 10
lcm |
9 | 7, 8 | eqtrd 2656 |
. . . . . . . . 9
lcm |
10 | 4, 9 | sylan9eqr 2678 |
. . . . . . . 8
lcm |
11 | 10 | breq1d 4663 |
. . . . . . 7
lcm |
12 | 3, 11 | imbi12d 334 |
. . . . . 6
lcm |
13 | 1, 12 | mpbiri 248 |
. . . . 5
lcm
|
14 | 13 | 3ad2antl3 1225 |
. . . 4
lcm |
15 | 14 | adantrd 484 |
. . 3
lcm |
16 | 15 | ex 450 |
. 2
lcm
|
17 | | breq1 4656 |
. . . . . . . 8
|
18 | 17 | adantl 482 |
. . . . . . 7
|
19 | | oveq2 6658 |
. . . . . . . . 9
lcm lcm |
20 | | lcm0val 15307 |
. . . . . . . . 9
lcm |
21 | 19, 20 | sylan9eqr 2678 |
. . . . . . . 8
lcm |
22 | 21 | breq1d 4663 |
. . . . . . 7
lcm |
23 | 18, 22 | imbi12d 334 |
. . . . . 6
lcm |
24 | 1, 23 | mpbiri 248 |
. . . . 5
lcm
|
25 | 24 | 3ad2antl2 1224 |
. . . 4
lcm |
26 | 25 | adantld 483 |
. . 3
lcm |
27 | 26 | ex 450 |
. 2
lcm
|
28 | | neanior 2886 |
. . . . . 6
|
29 | | lcmcl 15314 |
. . . . . . . . . . . . . . . . . 18
lcm |
30 | 29 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
lcm |
31 | | dvds0 14997 |
. . . . . . . . . . . . . . . . 17
lcm
lcm |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
lcm |
33 | 32 | a1d 25 |
. . . . . . . . . . . . . . 15
lcm |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . 14
lcm |
35 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
36 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
38 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
lcm
lcm |
39 | 37, 38 | imbi12d 334 |
. . . . . . . . . . . . . . 15
lcm
lcm |
40 | 39 | adantl 482 |
. . . . . . . . . . . . . 14
lcm
lcm
|
41 | 34, 40 | mpbird 247 |
. . . . . . . . . . . . 13
lcm |
42 | 41 | adantrl 752 |
. . . . . . . . . . . 12
lcm |
43 | 42 | adantllr 755 |
. . . . . . . . . . 11
lcm |
44 | 43 | adantlrr 757 |
. . . . . . . . . 10
lcm |
45 | 44 | anassrs 680 |
. . . . . . . . 9
lcm |
46 | | nnabscl 14065 |
. . . . . . . . . . . . 13
|
47 | | nnabscl 14065 |
. . . . . . . . . . . . 13
|
48 | | nnabscl 14065 |
. . . . . . . . . . . . . 14
|
49 | | lcmgcdlem 15319 |
. . . . . . . . . . . . . . 15
lcm
lcm |
50 | 49 | simprd 479 |
. . . . . . . . . . . . . 14
lcm |
51 | 48, 50 | sylani 686 |
. . . . . . . . . . . . 13
lcm |
52 | 46, 47, 51 | syl2an 494 |
. . . . . . . . . . . 12
lcm |
53 | 52 | expdimp 453 |
. . . . . . . . . . 11
lcm |
54 | | dvdsabsb 15001 |
. . . . . . . . . . . . . . . . . . 19
|
55 | | zabscl 14053 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | | absdvdsb 15000 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 55, 56 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 54, 57 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
60 | | dvdsabsb 15001 |
. . . . . . . . . . . . . . . . . . 19
|
61 | | absdvdsb 15000 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 55, 61 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 60, 62 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | adantll 750 |
. . . . . . . . . . . . . . . . 17
|
65 | 59, 64 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | bicomd 213 |
. . . . . . . . . . . . . . 15
|
67 | | lcmabs 15318 |
. . . . . . . . . . . . . . . . . 18
lcm lcm |
68 | 67 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
lcm lcm |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . 16
lcm
lcm |
70 | | dvdsabsb 15001 |
. . . . . . . . . . . . . . . . 17
lcm lcm
lcm |
71 | 30, 70 | sylan 488 |
. . . . . . . . . . . . . . . 16
lcm lcm |
72 | 69, 71 | bitr4d 271 |
. . . . . . . . . . . . . . 15
lcm
lcm |
73 | 66, 72 | imbi12d 334 |
. . . . . . . . . . . . . 14
lcm
lcm |
74 | 73 | adantrr 753 |
. . . . . . . . . . . . 13
lcm lcm |
75 | 74 | adantllr 755 |
. . . . . . . . . . . 12
lcm lcm |
76 | 75 | adantlrr 757 |
. . . . . . . . . . 11
lcm
lcm |
77 | 53, 76 | mpbid 222 |
. . . . . . . . . 10
lcm |
78 | 77 | anassrs 680 |
. . . . . . . . 9
lcm |
79 | 45, 78 | pm2.61dane 2881 |
. . . . . . . 8
lcm |
80 | 79 | ex 450 |
. . . . . . 7
lcm |
81 | 80 | an4s 869 |
. . . . . 6
lcm |
82 | 28, 81 | sylan2br 493 |
. . . . 5
lcm |
83 | 82 | impancom 456 |
. . . 4
lcm |
84 | 83 | 3impa 1259 |
. . 3
lcm |
85 | 84 | 3comr 1273 |
. 2
lcm |
86 | 16, 27, 85 | ecase3d 984 |
1
lcm
|