Step | Hyp | Ref
| Expression |
1 | | divalglem9.5 |
. . . 4
inf    |
2 | | divalglem8.1 |
. . . . 5
 |
3 | | divalglem8.2 |
. . . . 5
 |
4 | | divalglem8.3 |
. . . . 5
 |
5 | | divalglem8.4 |
. . . . 5
     |
6 | 2, 3, 4, 5 | divalglem2 14373 |
. . . 4
inf    |
7 | 1, 6 | eqeltri 2525 |
. . 3
 |
8 | 2, 3, 4, 5, 1 | divalglem5 14377 |
. . . 4
       |
9 | 8 | simpri 464 |
. . 3
     |
10 | | breq1 4405 |
. . . 4
 
   
       |
11 | 10 | rspcev 3150 |
. . 3
       
      |
12 | 7, 9, 11 | mp2an 678 |
. 2

     |
13 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
 
     |
14 | 13 | breq2d 4414 |
. . . . . . . . . . . . . 14
   

    |
15 | 14, 5 | elrab2 3198 |
. . . . . . . . . . . . 13

 
    |
16 | 15 | simplbi 462 |
. . . . . . . . . . . 12
   |
17 | 16 | nn0zd 11038 |
. . . . . . . . . . 11
   |
18 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
 
     |
19 | 18 | breq2d 4414 |
. . . . . . . . . . . . . 14
   

    |
20 | 19, 5 | elrab2 3198 |
. . . . . . . . . . . . 13

 
    |
21 | 20 | simplbi 462 |
. . . . . . . . . . . 12
   |
22 | 21 | nn0zd 11038 |
. . . . . . . . . . 11
   |
23 | | zsubcl 10979 |
. . . . . . . . . . . . 13
 
     |
24 | 2, 23 | mpan 676 |
. . . . . . . . . . . 12
 
   |
25 | | zsubcl 10979 |
. . . . . . . . . . . . 13
 
     |
26 | 2, 25 | mpan 676 |
. . . . . . . . . . . 12
 
   |
27 | 24, 26 | anim12i 570 |
. . . . . . . . . . 11
 
         |
28 | 17, 22, 27 | syl2an 480 |
. . . . . . . . . 10
 
         |
29 | 15 | simprbi 466 |
. . . . . . . . . . 11
     |
30 | 20 | simprbi 466 |
. . . . . . . . . . 11
     |
31 | 29, 30 | anim12i 570 |
. . . . . . . . . 10
 
  

     |
32 | | dvds2sub 14335 |
. . . . . . . . . . 11
  
 
            
     |
33 | 3, 32 | mp3an1 1351 |
. . . . . . . . . 10
    
            
     |
34 | 28, 31, 33 | sylc 62 |
. . . . . . . . 9
 
         |
35 | | zcn 10942 |
. . . . . . . . . . . 12
   |
36 | | zcn 10942 |
. . . . . . . . . . . 12
   |
37 | 2 | zrei 10943 |
. . . . . . . . . . . . . . . . 17
 |
38 | 37 | recni 9655 |
. . . . . . . . . . . . . . . 16
 |
39 | 38 | subidi 9945 |
. . . . . . . . . . . . . . 15
   |
40 | 39 | oveq1i 6300 |
. . . . . . . . . . . . . 14
           |
41 | | 0cn 9635 |
. . . . . . . . . . . . . . 15
 |
42 | | subsub2 9902 |
. . . . . . . . . . . . . . 15
 
           |
43 | 41, 42 | mp3an1 1351 |
. . . . . . . . . . . . . 14
 
           |
44 | 40, 43 | syl5eq 2497 |
. . . . . . . . . . . . 13
 
             |
45 | | sub4 9919 |
. . . . . . . . . . . . . 14
                     |
46 | 38, 38, 45 | mpanl12 688 |
. . . . . . . . . . . . 13
 
               |
47 | | subcl 9874 |
. . . . . . . . . . . . . . 15
 
     |
48 | 47 | ancoms 455 |
. . . . . . . . . . . . . 14
 
     |
49 | 48 | addid2d 9834 |
. . . . . . . . . . . . 13
 
         |
50 | 44, 46, 49 | 3eqtr3d 2493 |
. . . . . . . . . . . 12
 
    
      |
51 | 35, 36, 50 | syl2an 480 |
. . . . . . . . . . 11
 
    
      |
52 | 17, 22, 51 | syl2an 480 |
. . . . . . . . . 10
 
    
      |
53 | 52 | breq2d 4414 |
. . . . . . . . 9
 
       
     |
54 | 34, 53 | mpbid 214 |
. . . . . . . 8
 
     |
55 | | zsubcl 10979 |
. . . . . . . . . . 11
 
     |
56 | 55 | ancoms 455 |
. . . . . . . . . 10
 
     |
57 | | absdvdsb 14321 |
. . . . . . . . . 10
           
     |
58 | 3, 56, 57 | sylancr 669 |
. . . . . . . . 9
 
       
     |
59 | 17, 22, 58 | syl2an 480 |
. . . . . . . 8
 
       
     |
60 | 54, 59 | mpbid 214 |
. . . . . . 7
 
    
    |
61 | | nnabscl 13388 |
. . . . . . . . . . 11
         |
62 | 3, 4, 61 | mp2an 678 |
. . . . . . . . . 10
     |
63 | 62 | nnzi 10961 |
. . . . . . . . 9
     |
64 | | divides 14307 |
. . . . . . . . 9
                
           |
65 | 63, 56, 64 | sylancr 669 |
. . . . . . . 8
 
     
 
            |
66 | 17, 22, 65 | syl2an 480 |
. . . . . . 7
 
     
 
            |
67 | 60, 66 | mpbid 214 |
. . . . . 6
 
            |
68 | 67 | adantr 467 |
. . . . 5
  

    
                 |
69 | 2, 3, 4, 5 | divalglem8 14380 |
. . . . . 6
  

    
                    |
70 | 69 | rexlimdv 2877 |
. . . . 5
  

    
       
           |
71 | 68, 70 | mpd 15 |
. . . 4
  

    
        |
72 | 71 | ex 436 |
. . 3
 
      
    
   |
73 | 72 | rgen2a 2815 |
. 2


 
           |
74 | | breq1 4405 |
. . 3
 
   
       |
75 | 74 | reu4 3232 |
. 2
       
           
    
    |
76 | 12, 73, 75 | mpbir2an 931 |
1

     |