Proof of Theorem lcmdvds
Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . . . . 7
   |
2 | | breq1 3898 |
. . . . . . . . 9
 
   |
3 | 2 | adantl 273 |
. . . . . . . 8
 
     |
4 | | oveq1 5735 |
. . . . . . . . . 10
  lcm   lcm    |
5 | | 0z 8969 |
. . . . . . . . . . . 12
 |
6 | | lcmcom 11591 |
. . . . . . . . . . . 12
 
  lcm   lcm    |
7 | 5, 6 | mpan 418 |
. . . . . . . . . . 11
  lcm   lcm    |
8 | | lcm0val 11592 |
. . . . . . . . . . 11
  lcm    |
9 | 7, 8 | eqtrd 2147 |
. . . . . . . . . 10
  lcm    |
10 | 4, 9 | sylan9eqr 2169 |
. . . . . . . . 9
 
  lcm    |
11 | 10 | breq1d 3905 |
. . . . . . . 8
 
   lcm     |
12 | 3, 11 | imbi12d 233 |
. . . . . . 7
 
    lcm        |
13 | 1, 12 | mpbiri 167 |
. . . . . 6
 
   lcm 
   |
14 | 13 | 3ad2antl3 1128 |
. . . . 5
  



 lcm     |
15 | 14 | adantrd 275 |
. . . 4
  


    lcm     |
16 | 15 | ex 114 |
. . 3
 
 
 
  lcm 
    |
17 | | breq1 3898 |
. . . . . . . . 9
 
   |
18 | 17 | adantl 273 |
. . . . . . . 8
 
     |
19 | | oveq2 5736 |
. . . . . . . . . 10
  lcm   lcm    |
20 | | lcm0val 11592 |
. . . . . . . . . 10
  lcm    |
21 | 19, 20 | sylan9eqr 2169 |
. . . . . . . . 9
 
  lcm    |
22 | 21 | breq1d 3905 |
. . . . . . . 8
 
   lcm     |
23 | 18, 22 | imbi12d 233 |
. . . . . . 7
 
    lcm        |
24 | 1, 23 | mpbiri 167 |
. . . . . 6
 
   lcm 
   |
25 | 24 | 3ad2antl2 1127 |
. . . . 5
  



 lcm     |
26 | 25 | adantld 274 |
. . . 4
  


    lcm     |
27 | 26 | ex 114 |
. . 3
 
 
 
  lcm 
    |
28 | 16, 27 | jaod 689 |
. 2
 
   
    lcm      |
29 | | neanior 2369 |
. . . . . 6
       |
30 | | lcmcl 11599 |
. . . . . . . . . . . . . . . . . 18
 
  lcm    |
31 | 30 | nn0zd 9075 |
. . . . . . . . . . . . . . . . 17
 
  lcm    |
32 | | dvds0 11356 |
. . . . . . . . . . . . . . . . 17
  lcm 
 lcm    |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . . . . . 16
 
  lcm    |
34 | 33 | a1d 22 |
. . . . . . . . . . . . . . 15
 
   
 lcm     |
35 | 34 | adantr 272 |
. . . . . . . . . . . . . 14
    
    lcm     |
36 | | breq2 3899 |
. . . . . . . . . . . . . . . . 17
 
   |
37 | | breq2 3899 |
. . . . . . . . . . . . . . . . 17
 
   |
38 | 36, 37 | anbi12d 462 |
. . . . . . . . . . . . . . . 16
  
 
    |
39 | | breq2 3899 |
. . . . . . . . . . . . . . . 16
   lcm 
 lcm     |
40 | 38, 39 | imbi12d 233 |
. . . . . . . . . . . . . . 15
    
 lcm     
 lcm      |
41 | 40 | adantl 273 |
. . . . . . . . . . . . . 14
    
  
  lcm 
  
  lcm 
    |
42 | 35, 41 | mpbird 166 |
. . . . . . . . . . . . 13
    
    lcm     |
43 | 42 | adantrl 467 |
. . . . . . . . . . . 12
         
 lcm     |
44 | 43 | adantllr 470 |
. . . . . . . . . . 11
      
      lcm     |
45 | 44 | adantlrr 472 |
. . . . . . . . . 10
     
  
 
    lcm     |
46 | 45 | anassrs 395 |
. . . . . . . . 9
      
 


    lcm     |
47 | | nnabscl 10764 |
. . . . . . . . . . . . 13
         |
48 | | nnabscl 10764 |
. . . . . . . . . . . . 13
         |
49 | | nnabscl 10764 |
. . . . . . . . . . . . . 14
         |
50 | | lcmgcdlem 11604 |
. . . . . . . . . . . . . . 15
                  lcm          
                              
                   lcm              |
51 | 50 | simprd 113 |
. . . . . . . . . . . . . 14
                     
                   lcm             |
52 | 49, 51 | sylani 401 |
. . . . . . . . . . . . 13
                   
                   lcm             |
53 | 47, 48, 52 | syl2an 285 |
. . . . . . . . . . . 12
               
                   lcm             |
54 | 53 | expdimp 257 |
. . . . . . . . . . 11
     
  
 
     
            
     lcm             |
55 | | dvdsabsb 11360 |
. . . . . . . . . . . . . . . . . . 19
 
         |
56 | | zabscl 10750 |
. . . . . . . . . . . . . . . . . . . 20
       |
57 | | absdvdsb 11359 |
. . . . . . . . . . . . . . . . . . . 20
           
           |
58 | 56, 57 | sylan2 282 |
. . . . . . . . . . . . . . . . . . 19
 
     
           |
59 | 55, 58 | bitrd 187 |
. . . . . . . . . . . . . . . . . 18
 
             |
60 | 59 | adantlr 466 |
. . . . . . . . . . . . . . . . 17
         
       |
61 | | dvdsabsb 11360 |
. . . . . . . . . . . . . . . . . . 19
 
         |
62 | | absdvdsb 11359 |
. . . . . . . . . . . . . . . . . . . 20
           
           |
63 | 56, 62 | sylan2 282 |
. . . . . . . . . . . . . . . . . . 19
 
     
           |
64 | 61, 63 | bitrd 187 |
. . . . . . . . . . . . . . . . . 18
 
             |
65 | 64 | adantll 465 |
. . . . . . . . . . . . . . . . 17
         
       |
66 | 60, 65 | anbi12d 462 |
. . . . . . . . . . . . . . . 16
       
            
        |
67 | 66 | bicomd 140 |
. . . . . . . . . . . . . . 15
              
         
    |
68 | | lcmabs 11603 |
. . . . . . . . . . . . . . . . . 18
 
      lcm       lcm    |
69 | 68 | breq1d 3905 |
. . . . . . . . . . . . . . . . 17
 
       lcm           lcm         |
70 | 69 | adantr 272 |
. . . . . . . . . . . . . . . 16
           lcm         
 lcm         |
71 | | dvdsabsb 11360 |
. . . . . . . . . . . . . . . . 17
   lcm     lcm 
 lcm         |
72 | 31, 71 | sylan 279 |
. . . . . . . . . . . . . . . 16
       lcm   lcm         |
73 | 70, 72 | bitr4d 190 |
. . . . . . . . . . . . . . 15
           lcm         
 lcm     |
74 | 67, 73 | imbi12d 233 |
. . . . . . . . . . . . . 14
           
            
     lcm          
    lcm      |
75 | 74 | adantrr 468 |
. . . . . . . . . . . . 13
                 
              lcm               lcm      |
76 | 75 | adantllr 470 |
. . . . . . . . . . . 12
      
            
              lcm               lcm      |
77 | 76 | adantlrr 472 |
. . . . . . . . . . 11
     
  
 
      
            
     lcm          
    lcm      |
78 | 54, 77 | mpbid 146 |
. . . . . . . . . 10
     
  
 
    lcm     |
79 | 78 | anassrs 395 |
. . . . . . . . 9
      
 


    lcm     |
80 | | zdceq 9030 |
. . . . . . . . . . . . 13
 
 DECID   |
81 | 5, 80 | mpan2 419 |
. . . . . . . . . . . 12

DECID
  |
82 | | exmiddc 804 |
. . . . . . . . . . . 12
DECID

   |
83 | 81, 82 | syl 14 |
. . . . . . . . . . 11
 
   |
84 | | df-ne 2283 |
. . . . . . . . . . . 12

  |
85 | 84 | orbi2i 734 |
. . . . . . . . . . 11
       |
86 | 83, 85 | sylibr 133 |
. . . . . . . . . 10
 
   |
87 | 86 | adantl 273 |
. . . . . . . . 9
     
 
     |
88 | 46, 79, 87 | mpjaodan 770 |
. . . . . . . 8
     
 
   
 lcm     |
89 | 88 | ex 114 |
. . . . . . 7
          
 lcm      |
90 | 89 | an4s 560 |
. . . . . 6
          
 lcm      |
91 | 29, 90 | sylan2br 284 |
. . . . 5
       
    lcm      |
92 | 91 | impancom 258 |
. . . 4
      
     lcm      |
93 | 92 | 3impa 1159 |
. . 3
 
   
    lcm      |
94 | 93 | 3comr 1172 |
. 2
 
   
    lcm      |
95 | | lcmmndc 11589 |
. . . 4
 
 DECID     |
96 | | exmiddc 804 |
. . . 4
DECID      
    |
97 | 95, 96 | syl 14 |
. . 3
 
    
    |
98 | 97 | 3adant1 982 |
. 2
 
    
    |
99 | 28, 94, 98 | mpjaod 690 |
1
 
  
  lcm 
   |