Step | Hyp | Ref
| Expression |
1 | | bezoutlemstep.w-is-bezout |
. . 3
   ![]. ].](_drbrack.gif)   |
2 | | bezoutlemstep.is-bezout |
. . . . 5
  
        |
3 | 2 | sbcbii 3023 |
. . . 4
   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)           |
4 | | bezoutlemstep.w |
. . . . 5

  |
5 | | eqeq1 2184 |
. . . . . . 7
       
         |
6 | 5 | 2rexbidv 2502 |
. . . . . 6
  
      
           |
7 | 6 | sbcieg 2996 |
. . . . 5
  
 ![]. ].](_drbrack.gif)        
           |
8 | 4, 7 | syl 14 |
. . . 4
    ![]. ].](_drbrack.gif)         
          |
9 | 3, 8 | bitrid 192 |
. . 3
    ![]. ].](_drbrack.gif)
           |
10 | 1, 9 | mpbid 147 |
. 2
           |
11 | | bezoutlemstep.y-is-bezout |
. . . . . . 7
   ![] ]](rbrack.gif)   |
12 | | oveq2 5883 |
. . . . . . . . . . . . 13
 
     |
13 | 12 | oveq1d 5890 |
. . . . . . . . . . . 12
               |
14 | 13 | eqeq2d 2189 |
. . . . . . . . . . 11
       
         |
15 | | oveq2 5883 |
. . . . . . . . . . . . 13
 
     |
16 | 15 | oveq2d 5891 |
. . . . . . . . . . . 12
               |
17 | 16 | eqeq2d 2189 |
. . . . . . . . . . 11
       
         |
18 | 14, 17 | cbvrex2v 2718 |
. . . . . . . . . 10
  
     
          |
19 | 2, 18 | bitri 184 |
. . . . . . . . 9
  
        |
20 | 19 | sbbii 1765 |
. . . . . . . 8
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)           |
21 | | nfv 1528 |
. . . . . . . . 9
           |
22 | | eqeq1 2184 |
. . . . . . . . . 10
       
         |
23 | 22 | 2rexbidv 2502 |
. . . . . . . . 9
  
      
           |
24 | 21, 23 | sbie 1791 |
. . . . . . . 8
   ![] ]](rbrack.gif)        
          |
25 | 20, 24 | bitri 184 |
. . . . . . 7
   ![] ]](rbrack.gif)           |
26 | 11, 25 | sylib 122 |
. . . . . 6
           |
27 | 26 | ad2antrr 488 |
. . . . 5
   
 
                 |
28 | | bezoutlemstep.y-nn0 |
. . . . . . . . . . 11

  |
29 | 28 | ad4antr 494 |
. . . . . . . . . 10
       
 
       
 
       |
30 | 29 | nn0zd 9373 |
. . . . . . . . 9
       
 
       
 
       |
31 | 4 | ad4antr 494 |
. . . . . . . . 9
       
 
       
 
       |
32 | 30, 31 | zmodcld 10345 |
. . . . . . . . 9
       
 
       
 
         |
33 | | zq 9626 |
. . . . . . . . . . 11
   |
34 | 30, 33 | syl 14 |
. . . . . . . . . 10
       
 
       
 
       |
35 | 31 | nnzd 9374 |
. . . . . . . . . . 11
       
 
       
 
       |
36 | | zq 9626 |
. . . . . . . . . . 11
   |
37 | 35, 36 | syl 14 |
. . . . . . . . . 10
       
 
       
 
       |
38 | 31 | nngt0d 8963 |
. . . . . . . . . 10
       
 
       
 
       |
39 | | modqlt 10333 |
. . . . . . . . . 10
 
 
   |
40 | 34, 37, 38, 39 | syl3anc 1238 |
. . . . . . . . 9
       
 
       
 
         |
41 | | eqid 2177 |
. . . . . . . . . 10
     |
42 | | modremain 11934 |
. . . . . . . . . 10
 
    
 
 
  
          |
43 | 41, 42 | mpbii 148 |
. . . . . . . . 9
 
    
 
         |
44 | 30, 31, 32, 40, 43 | syl112anc 1242 |
. . . . . . . 8
       
 
       
 
              |
45 | | simprl 529 |
. . . . . . . . . . . . . 14
              
 
  |
46 | 45 | ad2antrr 488 |
. . . . . . . . . . . . 13
        
 
       
 
             
  |
47 | | simprl 529 |
. . . . . . . . . . . . . 14
        
 
       
 
                |
48 | | simplrl 535 |
. . . . . . . . . . . . . . 15
   
 
         |
49 | 48 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
        
 
       
 
                |
50 | 47, 49 | zmulcld 9381 |
. . . . . . . . . . . . 13
        
 
       
 
                  |
51 | 46, 50 | zsubcld 9380 |
. . . . . . . . . . . 12
        
 
       
 
                    |
52 | | simprr 531 |
. . . . . . . . . . . . . . 15
              
 
  |
53 | 52 | ad2antrr 488 |
. . . . . . . . . . . . . 14
        
 
       
 
                |
54 | | simplrr 536 |
. . . . . . . . . . . . . . . 16
   
 
         |
55 | 54 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
        
 
       
 
                |
56 | 47, 55 | zmulcld 9381 |
. . . . . . . . . . . . . 14
        
 
       
 
                  |
57 | 53, 56 | zsubcld 9380 |
. . . . . . . . . . . . 13
        
 
       
 
                    |
58 | | simplr 528 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                      |
59 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
   
 
               |
60 | 59 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
             
 
      |
61 | 60 | oveq2d 5891 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                          |
62 | 47 | zcnd 9376 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
                |
63 | | bezoutlemstep.a |
. . . . . . . . . . . . . . . . . . . . 21

  |
64 | 63 | ad5antr 496 |
. . . . . . . . . . . . . . . . . . . 20
        
 
       
 
             
  |
65 | 64 | nn0cnd 9231 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
             
  |
66 | 49 | zcnd 9376 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
                |
67 | 65, 66 | mulcld 7978 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
                  |
68 | | bezoutlemstep.b |
. . . . . . . . . . . . . . . . . . . . 21

  |
69 | 68 | ad5antr 496 |
. . . . . . . . . . . . . . . . . . . 20
        
 
       
 
             
  |
70 | 69 | nn0cnd 9231 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
             
  |
71 | 55 | zcnd 9376 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
                |
72 | 70, 71 | mulcld 7978 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
                  |
73 | 62, 67, 72 | adddid 7982 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                                  |
74 | 62, 65, 66 | mul12d 8109 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
               
        |
75 | 62, 70, 71 | mul12d 8109 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
               
        |
76 | 74, 75 | oveq12d 5893 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                                    |
77 | 61, 73, 76 | 3eqtrd 2214 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                            |
78 | 58, 77 | oveq12d 5893 |
. . . . . . . . . . . . . . 15
        
 
       
 
                                      |
79 | | simprr 531 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                      |
80 | 28 | ad5antr 496 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
                |
81 | 80 | nn0cnd 9231 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                |
82 | 31 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
             
  |
83 | 82 | nncnd 8933 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
             
  |
84 | 62, 83 | mulcld 7978 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                  |
85 | 34 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
                |
86 | 37 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
             
  |
87 | 38 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
        
 
       
 
             
  |
88 | 85, 86, 87 | modqcld 10328 |
. . . . . . . . . . . . . . . . . 18
        
 
       
 
                  |
89 | | qcn 9634 |
. . . . . . . . . . . . . . . . . 18
   
   |
90 | 88, 89 | syl 14 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                  |
91 | 81, 84, 90 | subaddd 8286 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                              |
92 | 79, 91 | mpbird 167 |
. . . . . . . . . . . . . . 15
        
 
       
 
                      |
93 | 46 | zcnd 9376 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
             
  |
94 | 65, 93 | mulcld 7978 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                  |
95 | 53 | zcnd 9376 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                |
96 | 70, 95 | mulcld 7978 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                  |
97 | 62, 66 | mulcld 7978 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                  |
98 | 65, 97 | mulcld 7978 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                    |
99 | 62, 71 | mulcld 7978 |
. . . . . . . . . . . . . . . . 17
        
 
       
 
                  |
100 | 70, 99 | mulcld 7978 |
. . . . . . . . . . . . . . . 16
        
 
       
 
                    |
101 | 94, 96, 98, 100 | addsub4d 8315 |
. . . . . . . . . . . . . . 15
        
 
       
 
                                            
       |
102 | 78, 92, 101 | 3eqtr3d 2218 |
. . . . . . . . . . . . . 14
        
 
       
 
                            
       |
103 | 65, 93, 97 | subdid 8371 |
. . . . . . . . . . . . . . 15
        
 
       
 
                              |
104 | 70, 95, 99 | subdid 8371 |
. . . . . . . . . . . . . . 15
        
 
       
 
                              |
105 | 103, 104 | oveq12d 5893 |
. . . . . . . . . . . . . 14
        
 
       
 
                
                       
       |
106 | 102, 105 | eqtr4d 2213 |
. . . . . . . . . . . . 13
        
 
       
 
                                |
107 | | oveq2 5883 |
. . . . . . . . . . . . . . . 16
     
         |
108 | 107 | oveq2d 5891 |
. . . . . . . . . . . . . . 15
                               |
109 | 108 | eqeq2d 2189 |
. . . . . . . . . . . . . 14
                 
                   |
110 | 109 | rspcev 2842 |
. . . . . . . . . . . . 13
                                      |
111 | 57, 106, 110 | syl2anc 411 |
. . . . . . . . . . . 12
        
 
       
 
              
              |
112 | | oveq2 5883 |
. . . . . . . . . . . . . . . 16
     
  
      |
113 | 112 | oveq1d 5890 |
. . . . . . . . . . . . . . 15
                       |
114 | 113 | eqeq2d 2189 |
. . . . . . . . . . . . . 14
             
               |
115 | 114 | rexbidv 2478 |
. . . . . . . . . . . . 13
      
       
                |
116 | 115 | rspcev 2842 |
. . . . . . . . . . . 12
       
            
 
         |
117 | 51, 111, 116 | syl2anc 411 |
. . . . . . . . . . 11
        
 
       
 
              
 
         |
118 | | oveq2 5883 |
. . . . . . . . . . . . . 14
 
     |
119 | 118 | oveq1d 5890 |
. . . . . . . . . . . . 13
               |
120 | 119 | eqeq2d 2189 |
. . . . . . . . . . . 12
         
           |
121 | | oveq2 5883 |
. . . . . . . . . . . . . 14
 
     |
122 | 121 | oveq2d 5891 |
. . . . . . . . . . . . 13
               |
123 | 122 | eqeq2d 2189 |
. . . . . . . . . . . 12
         
           |
124 | 120, 123 | cbvrex2v 2718 |
. . . . . . . . . . 11
  

      
            |
125 | 117, 124 | sylib 122 |
. . . . . . . . . 10
        
 
       
 
              
 
         |
126 | 32 | adantr 276 |
. . . . . . . . . . 11
        
 
       
 
                  |
127 | | eqeq1 2184 |
. . . . . . . . . . . . 13
         
           |
128 | 127 | 2rexbidv 2502 |
. . . . . . . . . . . 12
    
      
             |
129 | 128 | sbcieg 2996 |
. . . . . . . . . . 11
  
     ![]. ].](_drbrack.gif) 
      
             |
130 | 126, 129 | syl 14 |
. . . . . . . . . 10
        
 
       
 
                   ![]. ].](_drbrack.gif)        
             |
131 | 125, 130 | mpbird 167 |
. . . . . . . . 9
        
 
       
 
                  ![]. ].](_drbrack.gif) 
         |
132 | 2 | sbcbii 3023 |
. . . . . . . . 9
     ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif) 
         |
133 | 131, 132 | sylibr 134 |
. . . . . . . 8
        
 
       
 
                  ![]. ].](_drbrack.gif)   |
134 | 44, 133 | rexlimddv 2599 |
. . . . . . 7
       
 
       
 
         ![]. ].](_drbrack.gif)   |
135 | 134 | ex 115 |
. . . . . 6
              
 
        
  ![]. ].](_drbrack.gif)    |
136 | 135 | rexlimdvva 2602 |
. . . . 5
   
 
        
        
  ![]. ].](_drbrack.gif)    |
137 | 27, 136 | mpd 13 |
. . . 4
   
 
        
  ![]. ].](_drbrack.gif)   |
138 | 137 | ex 115 |
. . 3
                ![]. ].](_drbrack.gif)    |
139 | 138 | rexlimdvva 2602 |
. 2
              ![]. ].](_drbrack.gif)    |
140 | 10, 139 | mpd 13 |
1
     ![]. ].](_drbrack.gif)   |