Step | Hyp | Ref
| Expression |
1 | | df-3an 1009 |
. . . 4
    
  

    |
2 | | n0 3732 |
. . . . . . . 8
    |
3 | | n0 3732 |
. . . . . . . 8
    |
4 | 2, 3 | anbi12i 711 |
. . . . . . 7
  
 
    |
5 | | eeanv 2093 |
. . . . . . 7
     
       |
6 | 4, 5 | bitr4i 260 |
. . . . . 6
  
        |
7 | | simpll 768 |
. . . . . . . . . 10
   PCon 
   

    PCon |
8 | | simprll 780 |
. . . . . . . . . . 11
   PCon 
   

      |
9 | | simplrl 778 |
. . . . . . . . . . 11
   PCon 
   

      |
10 | | elunii 4195 |
. . . . . . . . . . 11
 
    |
11 | 8, 9, 10 | syl2anc 673 |
. . . . . . . . . 10
   PCon 
   

       |
12 | | simprlr 781 |
. . . . . . . . . . 11
   PCon 
   

      |
13 | | simplrr 779 |
. . . . . . . . . . 11
   PCon 
   

      |
14 | | elunii 4195 |
. . . . . . . . . . 11
 
    |
15 | 12, 13, 14 | syl2anc 673 |
. . . . . . . . . 10
   PCon 
   

       |
16 | | eqid 2471 |
. . . . . . . . . . 11
   |
17 | 16 | pconcn 30019 |
. . . . . . . . . 10
  PCon    

              |
18 | 7, 11, 15, 17 | syl3anc 1292 |
. . . . . . . . 9
   PCon 
   

                    |
19 | | simplrr 779 |
. . . . . . . . . . . . 13
    PCon 
   

                   
    
   |
20 | | simplrr 779 |
. . . . . . . . . . . . . . . 16
                
  
      |
21 | 20 | adantl 473 |
. . . . . . . . . . . . . . 15
    PCon 
   

                   
          |
22 | | iiuni 21991 |
. . . . . . . . . . . . . . . . 17
  ![[,] [,]](_icc.gif)    |
23 | | iicon 21997 |
. . . . . . . . . . . . . . . . . 18
 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    PCon 
   

                   
      |
25 | | simprll 780 |
. . . . . . . . . . . . . . . . 17
    PCon 
   

                   
        |
26 | 9 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    PCon 
   

                   
      |
27 | | uncom 3569 |
. . . . . . . . . . . . . . . . . . . 20
     |
28 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . 20
    PCon 
   

                   
         |
29 | 27, 28 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . . 19
    PCon 
   

                   
         |
30 | 13 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
    PCon 
   

                   
      |
31 | | elssuni 4219 |
. . . . . . . . . . . . . . . . . . . . 21
    |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    PCon 
   

                   
       |
33 | | incom 3616 |
. . . . . . . . . . . . . . . . . . . . 21
     |
34 | 33, 19 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . . . 20
    PCon 
   

                   
    
   |
35 | | uneqdifeq 3847 |
. . . . . . . . . . . . . . . . . . . 20
 
              |
36 | 32, 34, 35 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
    PCon 
   

                   
              |
37 | 29, 36 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
    PCon 
   

                   
     
   |
38 | | pcontop 30020 |
. . . . . . . . . . . . . . . . . . . 20
 PCon   |
39 | 38 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . 19
    PCon 
   

                   
      |
40 | 16 | opncld 20125 |
. . . . . . . . . . . . . . . . . . 19
 
          |
41 | 39, 30, 40 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
    PCon 
   

                   
     
       |
42 | 37, 41 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
    PCon 
   

                   
          |
43 | | 0elunit 11776 |
. . . . . . . . . . . . . . . . . 18
  ![[,] [,]](_icc.gif)   |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    PCon 
   

                   
      ![[,] [,]](_icc.gif)    |
45 | | simplrl 778 |
. . . . . . . . . . . . . . . . . . 19
                
  
      |
46 | 45 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
    PCon 
   

                   
          |
47 | 8 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
    PCon 
   

                   
      |
48 | 46, 47 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
    PCon 
   

                   
          |
49 | 22, 24, 25, 26, 42, 44, 48 | concn 20518 |
. . . . . . . . . . . . . . . 16
    PCon 
   

                   
        ![[,] [,]](_icc.gif)      |
50 | | 1elunit 11777 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)   |
51 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . 16
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)  
      |
52 | 49, 50, 51 | sylancl 675 |
. . . . . . . . . . . . . . 15
    PCon 
   

                   
          |
53 | 21, 52 | eqeltrrd 2550 |
. . . . . . . . . . . . . 14
    PCon 
   

                   
      |
54 | 12 | adantr 472 |
. . . . . . . . . . . . . 14
    PCon 
   

                   
      |
55 | | inelcm 3823 |
. . . . . . . . . . . . . 14
 
     |
56 | 53, 54, 55 | syl2anc 673 |
. . . . . . . . . . . . 13
    PCon 
   

                   
    
   |
57 | 19, 56 | pm2.21ddne 2727 |
. . . . . . . . . . . 12
    PCon 
   

                   
    
    |
58 | 57 | expr 626 |
. . . . . . . . . . 11
    PCon 
   

                      
      |
59 | 58 | pm2.01d 174 |
. . . . . . . . . 10
    PCon 
   

                        |
60 | 59 | neqned 2650 |
. . . . . . . . 9
    PCon 
   

                        |
61 | 18, 60 | rexlimddv 2875 |
. . . . . . . 8
   PCon 
   

         |
62 | 61 | exp32 616 |
. . . . . . 7
  PCon 
 
 
           |
63 | 62 | exlimdvv 1788 |
. . . . . 6
  PCon 
 
                 |
64 | 6, 63 | syl5bi 225 |
. . . . 5
  PCon 
 
             |
65 | 64 | impd 438 |
. . . 4
  PCon 
 
    
        |
66 | 1, 65 | syl5bi 225 |
. . 3
  PCon 
 
    
      |
67 | 66 | ralrimivva 2814 |
. 2
 PCon  
  
        |
68 | 16 | toptopon 20025 |
. . . 4

TopOn     |
69 | 38, 68 | sylib 201 |
. . 3
 PCon TopOn     |
70 | | dfcon2 20511 |
. . 3
 TopOn   


    
       |
71 | 69, 70 | syl 17 |
. 2
 PCon   
  
         |
72 | 67, 71 | mpbird 240 |
1
 PCon   |