Step | Hyp | Ref
| Expression |
1 | | divrngidl.1 |
. . 3
     |
2 | | divrngidl.2 |
. . 3
     |
3 | | divrngidl.4 |
. . 3
GId   |
4 | | divrngidl.3 |
. . 3
 |
5 | | eqid 2451 |
. . 3
GId  GId   |
6 | 1, 2, 3, 4, 5 | isdrngo2 32198 |
. 2
   GId                  GId      |
7 | 1, 3 | idl0cl 32252 |
. . . . . . . . . . 11
         |
8 | 7 | adantr 471 |
. . . . . . . . . 10
  
                     GId  
  |
9 | | fvex 5857 |
. . . . . . . . . . . . . 14
GId   |
10 | 3, 9 | eqeltri 2525 |
. . . . . . . . . . . . 13
 |
11 | 10 | snss 4064 |
. . . . . . . . . . . 12

    |
12 | | necom 2676 |
. . . . . . . . . . . 12
       |
13 | | pssdifn0 3794 |
. . . . . . . . . . . . 13
       
     |
14 | | n0 3708 |
. . . . . . . . . . . . 13
    
       |
15 | 13, 14 | sylib 201 |
. . . . . . . . . . . 12
              |
16 | 11, 12, 15 | syl2anb 486 |
. . . . . . . . . . 11
    
       |
17 | 1, 4 | idlss 32250 |
. . . . . . . . . . . . . . . . 17
         |
18 | | ssdif 3535 |
. . . . . . . . . . . . . . . . . 18
 
         |
19 | 18 | sselda 3399 |
. . . . . . . . . . . . . . . . 17
 
    

     |
20 | 17, 19 | sylan 478 |
. . . . . . . . . . . . . . . 16
  
    
    

     |
21 | | oveq2 6283 |
. . . . . . . . . . . . . . . . . . 19
           |
22 | 21 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . 18
      GId 
    GId     |
23 | 22 | rexbidv 2872 |
. . . . . . . . . . . . . . . . 17
  
         GId 
          GId     |
24 | 23 | rspcva 3115 |
. . . . . . . . . . . . . . . 16
     
                GId  
          GId    |
25 | 20, 24 | sylan 478 |
. . . . . . . . . . . . . . 15
                              GId  
          GId    |
26 | | eldifi 3522 |
. . . . . . . . . . . . . . . . . . . 20
       |
27 | | eldifi 3522 |
. . . . . . . . . . . . . . . . . . . 20
       |
28 | 26, 27 | anim12i 574 |
. . . . . . . . . . . . . . . . . . 19
     

        |
29 | 1, 2, 4 | idllmulcl 32254 |
. . . . . . . . . . . . . . . . . . . 20
  
              |
30 | 1, 2, 4, 5 | 1idl 32260 |
. . . . . . . . . . . . . . . . . . . . . . 23
        GId 
   |
31 | 30 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . 22
        GId 
   |
32 | 31 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
  
         GId 
   |
33 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . 22
     GId 
    
GId     |
34 | 33 | imbi1d 323 |
. . . . . . . . . . . . . . . . . . . . 21
     GId 
        GId      |
35 | 32, 34 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . . . . 20
  
             GId           |
36 | 29, 35 | mpid 42 |
. . . . . . . . . . . . . . . . . . 19
  
             GId     |
37 | 28, 36 | sylan2 481 |
. . . . . . . . . . . . . . . . . 18
  
                     GId     |
38 | 37 | anassrs 658 |
. . . . . . . . . . . . . . . . 17
             
    
     GId 
   |
39 | 38 | rexlimdva 2851 |
. . . . . . . . . . . . . . . 16
  
    
    
 
         GId     |
40 | 39 | imp 435 |
. . . . . . . . . . . . . . 15
                        GId     |
41 | 25, 40 | syldan 477 |
. . . . . . . . . . . . . 14
                              GId  
  |
42 | 41 | an32s 818 |
. . . . . . . . . . . . 13
                         GId  
       |
43 | 42 | ex 440 |
. . . . . . . . . . . 12
  
                     GId  
        |
44 | 43 | exlimdv 1782 |
. . . . . . . . . . 11
  
                     GId  
 

      |
45 | 16, 44 | syl5 33 |
. . . . . . . . . 10
  
                     GId  
 
  
   |
46 | 8, 45 | mpand 686 |
. . . . . . . . 9
  
                     GId  
      |
47 | 46 | an32s 818 |
. . . . . . . 8
                   GId  
    
      |
48 | | neor 2714 |
. . . . . . . 8
   

      |
49 | 47, 48 | sylibr 217 |
. . . . . . 7
                   GId  
    
  
   |
50 | 49 | ex 440 |
. . . . . 6
  
               GId  
    
  
    |
51 | 1, 3 | 0idl 32259 |
. . . . . . . . 9
         |
52 | | eleq1 2517 |
. . . . . . . . 9
                 |
53 | 51, 52 | syl5ibrcom 230 |
. . . . . . . 8
           |
54 | 1, 4 | rngoidl 32258 |
. . . . . . . . 9
       |
55 | | eleq1 2517 |
. . . . . . . . 9
     
       |
56 | 54, 55 | syl5ibrcom 230 |
. . . . . . . 8
 
       |
57 | 53, 56 | jaod 386 |
. . . . . . 7
    

       |
58 | 57 | adantr 471 |
. . . . . 6
  
               GId  
   
        |
59 | 50, 58 | impbid 195 |
. . . . 5
  
               GId  
       
    |
60 | | vex 3015 |
. . . . . 6
 |
61 | 60 | elpr 3953 |
. . . . 5
    
   
   |
62 | 59, 61 | syl6bbr 271 |
. . . 4
  
               GId  
             |
63 | 62 | eqrdv 2449 |
. . 3
  
               GId  
           |
64 | 63 | adantrl 727 |
. 2
   GId                  GId               |
65 | 6, 64 | sylbi 200 |
1
            |