Step | Hyp | Ref
| Expression |
1 | | fldcrng 32230 |
. . 3
 CRingOps |
2 | | flddivrng 26136 |
. . . 4
   |
3 | | isfldidl.1 |
. . . . 5
     |
4 | | isfldidl.2 |
. . . . 5
     |
5 | | isfldidl.3 |
. . . . 5
 |
6 | | isfldidl.4 |
. . . . 5
GId   |
7 | | isfldidl.5 |
. . . . 5
GId   |
8 | 3, 4, 5, 6, 7 | dvrunz 26154 |
. . . 4
   |
9 | 2, 8 | syl 17 |
. . 3
   |
10 | 3, 4, 5, 6 | divrngidl 32254 |
. . . 4
            |
11 | 2, 10 | syl 17 |
. . 3
            |
12 | 1, 9, 11 | 3jca 1187 |
. 2
 
CRingOps
            |
13 | | crngorngo 32226 |
. . . . . 6
 CRingOps   |
14 | 13 | 3ad2ant1 1028 |
. . . . 5
  CRingOps
            |
15 | | simp2 1008 |
. . . . 5
  CRingOps
            |
16 | 3 | rneqi 5060 |
. . . . . . . . . . . . . . 15
     |
17 | 5, 16 | eqtri 2472 |
. . . . . . . . . . . . . 14
     |
18 | 17, 4, 7 | rngo1cl 26150 |
. . . . . . . . . . . . 13
   |
19 | 13, 18 | syl 17 |
. . . . . . . . . . . 12
 CRingOps   |
20 | 19 | ad2antrr 731 |
. . . . . . . . . . 11
   CRingOps          
    
  |
21 | | eldif 3413 |
. . . . . . . . . . . . . . . 16
    

     |
22 | | snssi 4115 |
. . . . . . . . . . . . . . . . . . 19
     |
23 | 3, 5 | igenss 32288 |
. . . . . . . . . . . . . . . . . . 19
    
        |
24 | 22, 23 | sylan2 477 |
. . . . . . . . . . . . . . . . . 18
           |
25 | | vex 3047 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
26 | 25 | snss 4095 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
27 | 26 | biimpri 210 |
. . . . . . . . . . . . . . . . . . . 20
      

     |
28 | | eleq2 2517 |
. . . . . . . . . . . . . . . . . . . 20
           
     |
29 | 27, 28 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . . 19
      
            |
30 | 29 | con3dimp 443 |
. . . . . . . . . . . . . . . . . 18
    
  
   
       |
31 | 24, 30 | sylan 474 |
. . . . . . . . . . . . . . . . 17
  
    
       |
32 | 31 | anasss 652 |
. . . . . . . . . . . . . . . 16
  
            |
33 | 21, 32 | sylan2b 478 |
. . . . . . . . . . . . . . 15
               |
34 | 33 | adantlr 720 |
. . . . . . . . . . . . . 14
          
 

            |
35 | | eldifi 3554 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
36 | 35 | snssd 4116 |
. . . . . . . . . . . . . . . . . . . 20
         |
37 | 3, 5 | igenidl 32289 |
. . . . . . . . . . . . . . . . . . . 20
    
          |
38 | 36, 37 | sylan2 477 |
. . . . . . . . . . . . . . . . . . 19
                 |
39 | | eleq2 2517 |
. . . . . . . . . . . . . . . . . . 19
        
                      |
40 | 38, 39 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . 18
                             |
41 | 40 | imp 431 |
. . . . . . . . . . . . . . . . 17
  
                          |
42 | 41 | an32s 812 |
. . . . . . . . . . . . . . . 16
          
 

               |
43 | | ovex 6316 |
. . . . . . . . . . . . . . . . 17
     |
44 | 43 | elpr 3985 |
. . . . . . . . . . . . . . . 16
                
       |
45 | 42, 44 | sylib 200 |
. . . . . . . . . . . . . . 15
          
 

           
      |
46 | 45 | ord 379 |
. . . . . . . . . . . . . 14
          
 

                  |
47 | 34, 46 | mpd 15 |
. . . . . . . . . . . . 13
          
 

          |
48 | 13, 47 | sylanl1 655 |
. . . . . . . . . . . 12
   CRingOps          
    
      |
49 | 3, 4, 5 | prnc 32293 |
. . . . . . . . . . . . . 14
  CRingOps
      
       |
50 | 35, 49 | sylan2 477 |
. . . . . . . . . . . . 13
  CRingOps
          
       |
51 | 50 | adantlr 720 |
. . . . . . . . . . . 12
   CRingOps          
    
     
       |
52 | 48, 51 | eqtr3d 2486 |
. . . . . . . . . . 11
   CRingOps          
    
 
       |
53 | 20, 52 | eleqtrd 2530 |
. . . . . . . . . 10
   CRingOps          
    
 
       |
54 | | eqeq1 2454 |
. . . . . . . . . . . 12
     
       |
55 | 54 | rexbidv 2900 |
. . . . . . . . . . 11
  
   

       |
56 | 55 | elrab 3195 |
. . . . . . . . . 10
  
    


       |
57 | 53, 56 | sylib 200 |
. . . . . . . . 9
   CRingOps          
    


       |
58 | 57 | simprd 465 |
. . . . . . . 8
   CRingOps          
    

      |
59 | | eqcom 2457 |
. . . . . . . . 9
    
      |
60 | 59 | rexbii 2888 |
. . . . . . . 8
     

      |
61 | 58, 60 | sylibr 216 |
. . . . . . 7
   CRingOps          
    

      |
62 | 61 | ralrimiva 2801 |
. . . . . 6
  CRingOps
          
            |
63 | 62 | 3adant2 1026 |
. . . . 5
  CRingOps
                
      |
64 | 14, 15, 63 | jca32 538 |
. . . 4
  CRingOps
          
 
              |
65 | 3, 4, 6, 5, 7 | isdrngo3 32191 |
. . . 4
  
      
        |
66 | 64, 65 | sylibr 216 |
. . 3
  CRingOps
            |
67 | | simp1 1007 |
. . 3
  CRingOps
          CRingOps |
68 | | isfld2 32231 |
. . 3

 CRingOps  |
69 | 66, 67, 68 | sylanbrc 669 |
. 2
  CRingOps
            |
70 | 12, 69 | impbii 191 |
1

 CRingOps             |