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 11530 |
. . 3
     ![]. ].](_drbrack.gif)   |
9 | | bezoutlemstep.hyp |
. . 3
   
  ![]. ].](_drbrack.gif)        ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
10 | 8, 9 | mpdan 415 |
. 2
       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
11 | | bezoutlemstep.thr |
. . 3
   |
12 | | eqidd 2116 |
. . . . . 6
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)         |
13 | 6 | nn0zd 9075 |
. . . . . . . 8

  |
14 | 13 | ad2antrr 477 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
15 | 4 | ad2antrr 477 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
16 | 13, 4 | zmodcld 10011 |
. . . . . . . 8
     |
17 | 16 | ad2antrr 477 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       |
18 | | zq 9320 |
. . . . . . . . 9
   |
19 | 14, 18 | syl 14 |
. . . . . . . 8
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
20 | 15 | nnzd 9076 |
. . . . . . . . 9
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
21 | | zq 9320 |
. . . . . . . . 9
   |
22 | 20, 21 | syl 14 |
. . . . . . . 8
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
23 | 15 | nngt0d 8674 |
. . . . . . . 8
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
24 | | modqlt 9999 |
. . . . . . . 8
 
 
   |
25 | 19, 22, 23, 24 | syl3anc 1199 |
. . . . . . 7
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       |
26 | | modremain 11474 |
. . . . . . 7
 
    
 
 
  
          |
27 | 14, 15, 17, 25, 26 | syl112anc 1203 |
. . . . . 6
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                  |
28 | 12, 27 | mpbid 146 |
. . . . 5
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            |
29 | | simplrl 507 |
. . . . . . . . . . . . . 14
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
30 | | bezoutlemstep.thx |
. . . . . . . . . . . . . . . . 17
   |
31 | | bezoutlemstep.sub-gcd |
. . . . . . . . . . . . . . . . . . 19
  
     |
32 | 31 | sbcbii 2936 |
. . . . . . . . . . . . . . . . . 18
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
 
    |
33 | | breq2 3899 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
34 | 33 | anbi2d 457 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 
    |
35 | 34 | imbi2d 229 |
. . . . . . . . . . . . . . . . . . . . 21
   
         |
36 | 35 | ralbidv 2411 |
. . . . . . . . . . . . . . . . . . . 20
  
 
    
     |
37 | 36 | sbcieg 2909 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]. ].](_drbrack.gif)   
    
     |
38 | 4, 37 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    ![]. ].](_drbrack.gif)     
        |
39 | 32, 38 | syl5bb 191 |
. . . . . . . . . . . . . . . . 17
    ![]. ].](_drbrack.gif)
        |
40 | 30, 39 | sbcbid 2934 |
. . . . . . . . . . . . . . . 16
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
    ![]. ].](_drbrack.gif)         |
41 | | breq2 3899 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
42 | 41 | anbi1d 458 |
. . . . . . . . . . . . . . . . . . . 20
    
  

    |
43 | 42 | imbi2d 229 |
. . . . . . . . . . . . . . . . . . 19
     
     
     |
44 | 43 | ralbidv 2411 |
. . . . . . . . . . . . . . . . . 18
    
 
     

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

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

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

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

   |
52 | 51 | simprd 113 |
. . . . . . . . . 10
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
  |
53 | | simplr 502 |
. . . . . . . . . . . . . . 15
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
    |
54 | 53 | nn0zd 9075 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
    |
55 | | simprl 503 |
. . . . . . . . . . . . . . 15
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
           |
56 | 55 | ad2antrr 477 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
    |
57 | 20 | ad3antrrr 481 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
  |
58 | | dvdsmultr2 11381 |
. . . . . . . . . . . . . 14
 
 
     |
59 | 54, 56, 57, 58 | syl3anc 1199 |
. . . . . . . . . . . . 13
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
        |
60 | 52, 59 | mpd 13 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
    |
61 | 51 | simpld 111 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
    |
62 | 56, 57 | zmulcld 9083 |
. . . . . . . . . . . . 13
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
      |
63 | 17 | ad3antrrr 481 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
      |
64 | 63 | nn0zd 9075 |
. . . . . . . . . . . . 13
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
      |
65 | | dvds2add 11375 |
. . . . . . . . . . . . 13
                       |
66 | 54, 62, 64, 65 | syl3anc 1199 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
     
            |
67 | 60, 61, 66 | mp2and 427 |
. . . . . . . . . . 11
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
        |
68 | | simprr 504 |
. . . . . . . . . . . 12
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
                 |
69 | 68 | ad2antrr 477 |
. . . . . . . . . . 11
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
          |
70 | 67, 69 | breqtrd 3919 |
. . . . . . . . . 10
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
 
  |
71 | 52, 70 | jca 302 |
. . . . . . . . 9
            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)           
  
   |
72 | 71 | ex 114 |
. . . . . . . 8
        
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             
     |
73 | 72 | ralrimiva 2479 |
. . . . . . 7
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
         
 
    |
74 | 31 | sbcbii 2936 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
 
    |
75 | | breq2 3899 |
. . . . . . . . . . . . . 14
 
   |
76 | 75 | anbi1d 458 |
. . . . . . . . . . . . 13
  
 
    |
77 | 76 | imbi2d 229 |
. . . . . . . . . . . 12
   
         |
78 | 77 | ralbidv 2411 |
. . . . . . . . . . 11
  
 
    
     |
79 | 78 | sbcieg 2909 |
. . . . . . . . . 10
  
 ![]. ].](_drbrack.gif)   
    
     |
80 | 4, 79 | syl 14 |
. . . . . . . . 9
    ![]. ].](_drbrack.gif)     
        |
81 | 74, 80 | syl5bb 191 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)
        |
82 | 81 | ad3antrrr 481 |
. . . . . . 7
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
            ![]. ].](_drbrack.gif)   
     |
83 | 73, 82 | mpbird 166 |
. . . . . 6
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
         
 ![]. ].](_drbrack.gif)   |
84 | | simplrr 508 |
. . . . . 6
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
           |
85 | 83, 84 | jca 302 |
. . . . 5
   
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
            ![]. ].](_drbrack.gif)    |
86 | 28, 85 | rexlimddv 2528 |
. . . 4
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)    |
87 | 86 | exp31 359 |
. . 3
     
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
 ![]. ].](_drbrack.gif)      |
88 | 11, 87 | reximdai 2504 |
. 2
     
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)     |
89 | 10, 88 | mpd 13 |
1
     ![]. ].](_drbrack.gif)    |