Step | Hyp | Ref
| Expression |
1 | | bezoutlemstep.is-bezout |
. . . 4
  
        |
2 | | bezoutlemstep.a |
. . . 4

  |
3 | | bezoutlemstep.b |
. . . 4

  |
4 | | bezoutlemstep.w |
. . . 4

  |
5 | | bezoutlemstep.y-is-bezout |
. . . 4
   ![] ]](rbrack.gif)   |
6 | | bezoutlemstep.y-nn0 |
. . . 4

  |
7 | | bezoutlemstep.w-is-bezout |
. . . 4
   ![]. ].](_drbrack.gif)   |
8 | 1, 2, 3, 4, 5, 6, 7 | bezoutlemnewy 12010 |
. . 3
     ![]. ].](_drbrack.gif)   |
9 | | bezoutlemstep.hyp |
. . 3
   
  ![]. ].](_drbrack.gif)        ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
10 | 8, 9 | mpdan 421 |
. 2
       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
11 | | bezoutlemstep.thr |
. . 3
   |
12 | | eqidd 2188 |
. . . . . 6
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)         |
13 | 6 | nn0zd 9386 |
. . . . . . . 8

  |
14 | 13 | ad2antrr 488 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
15 | 4 | ad2antrr 488 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
16 | 13, 4 | zmodcld 10358 |
. . . . . . . 8
     |
17 | 16 | ad2antrr 488 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       |
18 | | zq 9639 |
. . . . . . . . 9
   |
19 | 14, 18 | syl 14 |
. . . . . . . 8
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
20 | 15 | nnzd 9387 |
. . . . . . . . 9
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
21 | | zq 9639 |
. . . . . . . . 9
   |
22 | 20, 21 | syl 14 |
. . . . . . . 8
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
23 | 15 | nngt0d 8976 |
. . . . . . . 8
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
24 | | modqlt 10346 |
. . . . . . . 8
 
 
   |
25 | 19, 22, 23, 24 | syl3anc 1248 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       |
26 | | modremain 11947 |
. . . . . . 7
 
    
 
 
  
          |
27 | 14, 15, 17, 25, 26 | syl112anc 1252 |
. . . . . 6
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                  |
28 | 12, 27 | mpbid 147 |
. . . . 5
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            |
29 | | simplrl 535 |
. . . . . . . . . . . . . 14
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
30 | | bezoutlemstep.thx |
. . . . . . . . . . . . . . . . 17
   |
31 | | bezoutlemstep.sub-gcd |
. . . . . . . . . . . . . . . . . . 19
  
     |
32 | 31 | sbcbii 3034 |
. . . . . . . . . . . . . . . . . 18
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
 
    |
33 | | breq2 4019 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
34 | 33 | anbi2d 464 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 
    |
35 | 34 | imbi2d 230 |
. . . . . . . . . . . . . . . . . . . . 21
   
         |
36 | 35 | ralbidv 2487 |
. . . . . . . . . . . . . . . . . . . 20
  
 
    
     |
37 | 36 | sbcieg 3007 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]. ].](_drbrack.gif)   
    
     |
38 | 4, 37 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    ![]. ].](_drbrack.gif)     
        |
39 | 32, 38 | bitrid 192 |
. . . . . . . . . . . . . . . . 17
    ![]. ].](_drbrack.gif)
        |
40 | 30, 39 | sbcbid 3032 |
. . . . . . . . . . . . . . . 16
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
    ![]. ].](_drbrack.gif)         |
41 | | breq2 4019 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
42 | 41 | anbi1d 465 |
. . . . . . . . . . . . . . . . . . . 20
    
  

    |
43 | 42 | imbi2d 230 |
. . . . . . . . . . . . . . . . . . 19
     
     
     |
44 | 43 | ralbidv 2487 |
. . . . . . . . . . . . . . . . . 18
    
 
     

     |
45 | 44 | sbcieg 3007 |
. . . . . . . . . . . . . . . . 17
  
     ![]. ].](_drbrack.gif) 
 
     

     |
46 | 16, 45 | syl 14 |
. . . . . . . . . . . . . . . 16
      ![]. ].](_drbrack.gif)     
    
     |
47 | 40, 46 | bitrd 188 |
. . . . . . . . . . . . . . 15
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
    
     |
48 | 47 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
              ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    

     |
49 | 29, 48 | mpbid 147 |
. . . . . . . . . . . . 13
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
         
  

    |
50 | 49 | r19.21bi 2575 |
. . . . . . . . . . . 12
        
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             
       |
51 | 50 | imp 124 |
. . . . . . . . . . 11
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
   

   |
52 | 51 | simprd 114 |
. . . . . . . . . 10
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
  |
53 | | simplr 528 |
. . . . . . . . . . . . . . 15
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
    |
54 | 53 | nn0zd 9386 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
    |
55 | | simprl 529 |
. . . . . . . . . . . . . . 15
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
           |
56 | 55 | ad2antrr 488 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
    |
57 | 20 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
  |
58 | | dvdsmultr2 11853 |
. . . . . . . . . . . . . 14
 
 
     |
59 | 54, 56, 57, 58 | syl3anc 1248 |
. . . . . . . . . . . . 13
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
        |
60 | 52, 59 | mpd 13 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
    |
61 | 51 | simpld 112 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
    |
62 | 56, 57 | zmulcld 9394 |
. . . . . . . . . . . . 13
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
      |
63 | 17 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
      |
64 | 63 | nn0zd 9386 |
. . . . . . . . . . . . 13
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
      |
65 | | dvds2add 11845 |
. . . . . . . . . . . . 13
                       |
66 | 54, 62, 64, 65 | syl3anc 1248 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
     
            |
67 | 60, 61, 66 | mp2and 433 |
. . . . . . . . . . 11
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
        |
68 | | simprr 531 |
. . . . . . . . . . . 12
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
                 |
69 | 68 | ad2antrr 488 |
. . . . . . . . . . 11
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
          |
70 | 67, 69 | breqtrd 4041 |
. . . . . . . . . 10
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
  |
71 | 52, 70 | jca 306 |
. . . . . . . . 9
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
  
   |
72 | 71 | ex 115 |
. . . . . . . 8
        
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             
     |
73 | 72 | ralrimiva 2560 |
. . . . . . 7
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
         
 
    |
74 | 31 | sbcbii 3034 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
 
    |
75 | | breq2 4019 |
. . . . . . . . . . . . . 14
 
   |
76 | 75 | anbi1d 465 |
. . . . . . . . . . . . 13
  
 
    |
77 | 76 | imbi2d 230 |
. . . . . . . . . . . 12
   
         |
78 | 77 | ralbidv 2487 |
. . . . . . . . . . 11
  
 
    
     |
79 | 78 | sbcieg 3007 |
. . . . . . . . . 10
  
 ![]. ].](_drbrack.gif)   
    
     |
80 | 4, 79 | syl 14 |
. . . . . . . . 9
    ![]. ].](_drbrack.gif)     
        |
81 | 74, 80 | bitrid 192 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)
        |
82 | 81 | ad3antrrr 492 |
. . . . . . 7
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
            ![]. ].](_drbrack.gif)   
     |
83 | 73, 82 | mpbird 167 |
. . . . . 6
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
         
 ![]. ].](_drbrack.gif)   |
84 | | simplrr 536 |
. . . . . 6
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
           |
85 | 83, 84 | jca 306 |
. . . . 5
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
            ![]. ].](_drbrack.gif)    |
86 | 28, 85 | rexlimddv 2609 |
. . . 4
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)    |
87 | 86 | exp31 364 |
. . 3
     
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
 ![]. ].](_drbrack.gif)      |
88 | 11, 87 | reximdai 2585 |
. 2
     
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)     |
89 | 10, 88 | mpd 13 |
1
     ![]. ].](_drbrack.gif)    |