Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . . 12
           |
2 | | rpssre 11312 |
. . . . . . . . . . . . 13
 |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
       |
4 | 1, 3 | fssd 5738 |
. . . . . . . . . . 11
           |
5 | 4 | 3ad2ant3 1031 |
. . . . . . . . . 10
 
               |
6 | 5 | adantr 467 |
. . . . . . . . 9
            
 
      |
7 | 6 | ffvelrnda 6022 |
. . . . . . . 8
               
       |
8 | | simplrr 771 |
. . . . . . . 8
               
   |
9 | | simpl2 1012 |
. . . . . . . . . 10
            
 
      |
10 | 9 | ffvelrnda 6022 |
. . . . . . . . 9
               
       |
11 | 10 | rpregt0d 11347 |
. . . . . . . 8
               
             |
12 | 7, 8, 11 | 3jca 1188 |
. . . . . . 7
               
                   |
13 | | ledivmul2 10484 |
. . . . . . . 8
     
                         
         |
14 | 13 | bicomd 205 |
. . . . . . 7
     
                                   |
15 | 12, 14 | syl 17 |
. . . . . 6
               
                     
   |
16 | | id 22 |
. . . . . . . . . . . . 13
           |
17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
       |
18 | 16, 17 | fssd 5738 |
. . . . . . . . . . . 12
           |
19 | 18 | 3ad2ant2 1030 |
. . . . . . . . . . 11
 
               |
20 | | reex 9630 |
. . . . . . . . . . . . 13
 |
21 | 20 | ssex 4547 |
. . . . . . . . . . . 12

  |
22 | 21 | 3ad2ant1 1029 |
. . . . . . . . . . 11
 
           |
23 | 5, 19, 22 | 3jca 1188 |
. . . . . . . . . 10
 
                 
   |
24 | 23 | adantr 467 |
. . . . . . . . 9
            
 
            |
25 | 24 | adantr 467 |
. . . . . . . 8
               
             |
26 | | ffun 5731 |
. . . . . . . . . . . . . . . 16
       |
27 | 26 | adantl 468 |
. . . . . . . . . . . . . . 15
 
       |
28 | 21 | anim1i 572 |
. . . . . . . . . . . . . . . . 17
 
     
       |
29 | 28 | ancomd 453 |
. . . . . . . . . . . . . . . 16
 
             |
30 | | fex 6138 |
. . . . . . . . . . . . . . . 16
         |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
 
       |
32 | | 0red 9644 |
. . . . . . . . . . . . . . 15
 
       |
33 | | frn 5735 |
. . . . . . . . . . . . . . . . 17
    
  |
34 | | 0nrp 11334 |
. . . . . . . . . . . . . . . . . . 19
 |
35 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20

  |
36 | 35 | ssneld 3434 |
. . . . . . . . . . . . . . . . . . 19


   |
37 | 34, 36 | mpi 20 |
. . . . . . . . . . . . . . . . . 18

  |
38 | | df-nel 2625 |
. . . . . . . . . . . . . . . . . 18

  |
39 | 37, 38 | sylibr 216 |
. . . . . . . . . . . . . . . . 17

  |
40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
41 | 40 | adantl 468 |
. . . . . . . . . . . . . . 15
 
       |
42 | | suppdm 40357 |
. . . . . . . . . . . . . . 15
  
   supp
   |
43 | 27, 31, 32, 41, 42 | syl31anc 1271 |
. . . . . . . . . . . . . 14
 
      supp    |
44 | | fdm 5733 |
. . . . . . . . . . . . . . 15
       |
45 | 44 | adantl 468 |
. . . . . . . . . . . . . 14
 
       |
46 | 43, 45 | eqtrd 2485 |
. . . . . . . . . . . . 13
 
      supp    |
47 | 46 | 3adant3 1028 |
. . . . . . . . . . . 12
 
          supp    |
48 | 47 | eqcomd 2457 |
. . . . . . . . . . 11
 
          supp    |
49 | 48 | adantr 467 |
. . . . . . . . . 10
            
 

supp    |
50 | 49 | eleq2d 2514 |
. . . . . . . . 9
            
 

 supp     |
51 | 50 | biimpa 487 |
. . . . . . . 8
               
  supp    |
52 | | refdivmptfv 40410 |
. . . . . . . 8
             supp     /_f                 |
53 | 25, 51, 52 | syl2anc 667 |
. . . . . . 7
               
   /_f                 |
54 | 53 | breq1d 4412 |
. . . . . 6
               
    /_f    
             |
55 | 15, 54 | bitr4d 260 |
. . . . 5
               
              /_f        |
56 | 55 | imbi2d 318 |
. . . 4
               
  
           
  /_f    
    |
57 | 56 | ralbidva 2824 |
. . 3
            
 
 

          


  /_f    
    |
58 | 57 | 2rexbidva 2907 |
. 2
 
          
 

          
   
  /_f    
    |
59 | | simp1 1008 |
. . 3
 
           |
60 | | ssid 3451 |
. . . 4
 |
61 | 60 | a1i 11 |
. . 3
 
           |
62 | | elbigo2 40416 |
. . 3
                _O 
   
              |
63 | 19, 59, 5, 61, 62 | syl22anc 1269 |
. 2
 
         
_O    

              |
64 | | refdivmptf 40406 |
. . . . 5
         
  /_f     supp      |
65 | 23, 64 | syl 17 |
. . . 4
 
          /_f     supp      |
66 | 44 | eqcomd 2457 |
. . . . . . 7
       |
67 | 66 | 3ad2ant2 1030 |
. . . . . 6
 
           |
68 | | simpr 463 |
. . . . . . . . 9
 
           |
69 | 21 | adantr 467 |
. . . . . . . . 9
 
       |
70 | 68, 69, 30 | syl2anc 667 |
. . . . . . . 8
 
       |
71 | 27, 70, 32, 41, 42 | syl31anc 1271 |
. . . . . . 7
 
      supp    |
72 | 71 | 3adant3 1028 |
. . . . . 6
 
          supp    |
73 | 67, 72 | eqtr4d 2488 |
. . . . 5
 
          supp    |
74 | 73 | feq2d 5715 |
. . . 4
 
           /_f     
 /_f     supp       |
75 | 65, 74 | mpbird 236 |
. . 3
 
          /_f        |
76 | | ello12 13580 |
. . 3
   /_f         /_f      
  
  /_f    
    |
77 | 75, 59, 76 | syl2anc 667 |
. 2
 
           /_f        

  /_f         |
78 | 58, 63, 77 | 3bitr4d 289 |
1
 
         
_O   /_f         |