Proof of Theorem fvmptnn04if
Step | Hyp | Ref
| Expression |
1 | | fvmptnn04if.n |
. . 3
   |
2 | | csbif 3942 |
. . . . 5
  ![]_ ]_](_urbrack.gif)        
           ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)             |
3 | | eqsbc3 3318 |
. . . . . . 7

   ![]. ].](_drbrack.gif)
   |
4 | 1, 3 | syl 17 |
. . . . . 6
    ![]. ].](_drbrack.gif)    |
5 | | csbif 3942 |
. . . . . . 7
  ![]_ ]_](_urbrack.gif)    
          ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)        |
6 | | eqsbc3 3318 |
. . . . . . . . 9

   ![]. ].](_drbrack.gif)
   |
7 | 1, 6 | syl 17 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)    |
8 | | csbif 3942 |
. . . . . . . . 9
  ![]_ ]_](_urbrack.gif)          ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)   |
9 | | sbcbr2g 4471 |
. . . . . . . . . . . 12

   ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
10 | 1, 9 | syl 17 |
. . . . . . . . . . 11
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)    |
11 | | csbvarg 3803 |
. . . . . . . . . . . . 13

  ![]_ ]_](_urbrack.gif)   |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)
  |
13 | 12 | breq2d 4427 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
   |
14 | 10, 13 | bitrd 261 |
. . . . . . . . . 10
    ![]. ].](_drbrack.gif)    |
15 | 14 | ifbid 3914 |
. . . . . . . . 9
     ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
16 | 8, 15 | syl5eq 2507 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
17 | 7, 16 | ifbieq2d 3917 |
. . . . . . 7
     ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     |
18 | 5, 17 | syl5eq 2507 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)              
 ![]_ ]_](_urbrack.gif)     
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     |
19 | 4, 18 | ifbieq2d 3917 |
. . . . 5
     ![]. ].](_drbrack.gif)    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)     
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      |
20 | 2, 19 | syl5eq 2507 |
. . . 4
   ![]_ ]_](_urbrack.gif)          
          ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)     
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      |
21 | | fvmptnn04if.a |
. . . . . 6
 
   ![]_ ]_](_urbrack.gif)   |
22 | | fvmptnn04if.y |
. . . . . . 7
   |
23 | 22 | adantr 471 |
. . . . . 6
 
   |
24 | 21, 23 | eqeltrrd 2540 |
. . . . 5
 
   ![]_ ]_](_urbrack.gif)   |
25 | | fvmptnn04if.c |
. . . . . . . . 9
 
   ![]_ ]_](_urbrack.gif)   |
26 | 25 | eqcomd 2467 |
. . . . . . . 8
 
   ![]_ ]_](_urbrack.gif)   |
27 | 26 | adantlr 726 |
. . . . . . 7
  
 
  ![]_ ]_](_urbrack.gif)   |
28 | 22 | ad2antrr 737 |
. . . . . . 7
  
 
  |
29 | 27, 28 | eqeltrd 2539 |
. . . . . 6
  
 
  ![]_ ]_](_urbrack.gif)   |
30 | | fvmptnn04if.d |
. . . . . . . . . . . 12
 

  ![]_ ]_](_urbrack.gif)   |
31 | 30 | eqcomd 2467 |
. . . . . . . . . . 11
 

  ![]_ ]_](_urbrack.gif)   |
32 | 31 | ex 440 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
   |
33 | 32 | ad2antrr 737 |
. . . . . . . . 9
  
     ![]_ ]_](_urbrack.gif)    |
34 | 33 | imp 435 |
. . . . . . . 8
   

    ![]_ ]_](_urbrack.gif)   |
35 | 22 | ad3antrrr 741 |
. . . . . . . 8
   

    |
36 | 34, 35 | eqeltrd 2539 |
. . . . . . 7
   

    ![]_ ]_](_urbrack.gif)   |
37 | | simplll 773 |
. . . . . . . . 9
   

    |
38 | | ancom 456 |
. . . . . . . . . . . . 13
  
    |
39 | 38 | anbi2i 705 |
. . . . . . . . . . . 12
    
 
 
      |
40 | | ancom 456 |
. . . . . . . . . . . . 13
 


     
     |
41 | | anass 659 |
. . . . . . . . . . . . . . 15
    


    |
42 | 41 | bicomi 207 |
. . . . . . . . . . . . . 14
  
 
 
    |
43 | 42 | anbi1i 706 |
. . . . . . . . . . . . 13
   
     
 
   |
44 | | anass 659 |
. . . . . . . . . . . . 13
   
 

 
      |
45 | 40, 43, 44 | 3bitri 279 |
. . . . . . . . . . . 12
 


    
 
    |
46 | | anass 659 |
. . . . . . . . . . . 12
   
  
 
      |
47 | 39, 45, 46 | 3bitr4i 285 |
. . . . . . . . . . 11
 


           |
48 | | an32 812 |
. . . . . . . . . . . . 13
           |
49 | | ancom 456 |
. . . . . . . . . . . . . 14
  
    |
50 | 49 | anbi1i 706 |
. . . . . . . . . . . . 13
           |
51 | 48, 50 | bitri 257 |
. . . . . . . . . . . 12
      

   |
52 | 51 | anbi1i 706 |
. . . . . . . . . . 11
   
  
  


   |
53 | 47, 52 | bitri 257 |
. . . . . . . . . 10
 


           |
54 | | df-ne 2634 |
. . . . . . . . . . . . 13

  |
55 | | elnnne0 10911 |
. . . . . . . . . . . . . . 15

    |
56 | | nngt0 10665 |
. . . . . . . . . . . . . . 15
   |
57 | 55, 56 | sylbir 218 |
. . . . . . . . . . . . . 14
  
  |
58 | 57 | expcom 441 |
. . . . . . . . . . . . 13
 
   |
59 | 54, 58 | sylbir 218 |
. . . . . . . . . . . 12
     |
60 | 59 | adantr 471 |
. . . . . . . . . . 11
  
      |
61 | 1, 60 | mpan9 476 |
. . . . . . . . . 10
 


     |
62 | 53, 61 | sylbir 218 |
. . . . . . . . 9
   

 
  |
63 | 1 | nn0red 10954 |
. . . . . . . . . . . . . . . 16
   |
64 | | fvmptnn04if.s |
. . . . . . . . . . . . . . . . 17
   |
65 | 64 | nnred 10651 |
. . . . . . . . . . . . . . . 16
   |
66 | 63, 65 | lenltd 9806 |
. . . . . . . . . . . . . . 15
     |
67 | 66 | biimprd 231 |
. . . . . . . . . . . . . 14
 
   |
68 | 67 | adantld 473 |
. . . . . . . . . . . . 13
  
    |
69 | 68 | adantld 473 |
. . . . . . . . . . . 12
   
     |
70 | 69 | imp 435 |
. . . . . . . . . . 11
 


     |
71 | | nesym 2691 |
. . . . . . . . . . . . . 14

  |
72 | 71 | biimpri 211 |
. . . . . . . . . . . . 13
   |
73 | 72 | adantr 471 |
. . . . . . . . . . . 12
     |
74 | 73 | ad2antll 740 |
. . . . . . . . . . 11
 


     |
75 | 63 | adantr 471 |
. . . . . . . . . . . 12
 


     |
76 | 65 | adantr 471 |
. . . . . . . . . . . 12
 


     |
77 | 75, 76 | ltlend 9805 |
. . . . . . . . . . 11
 


         |
78 | 70, 74, 77 | mpbir2and 938 |
. . . . . . . . . 10
 


     |
79 | 53, 78 | sylbir 218 |
. . . . . . . . 9
   

    |
80 | | fvmptnn04if.b |
. . . . . . . . . 10
 

  ![]_ ]_](_urbrack.gif)   |
81 | 80 | eqcomd 2467 |
. . . . . . . . 9
 

  ![]_ ]_](_urbrack.gif)   |
82 | 37, 62, 79, 81 | syl3anc 1276 |
. . . . . . . 8
   

  
 ![]_ ]_](_urbrack.gif)
  |
83 | 22 | ad3antrrr 741 |
. . . . . . . 8
   

 
  |
84 | 82, 83 | eqeltrd 2539 |
. . . . . . 7
   

  
 ![]_ ]_](_urbrack.gif)
  |
85 | 36, 84 | ifclda 3924 |
. . . . . 6
  
   
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
86 | 29, 85 | ifclda 3924 |
. . . . 5
 
      ![]_ ]_](_urbrack.gif)   
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     |
87 | 24, 86 | ifclda 3924 |
. . . 4
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      |
88 | 20, 87 | eqeltrd 2539 |
. . 3
   ![]_ ]_](_urbrack.gif)          
       |
89 | | fvmptnn04if.g |
. . . 4
      
           |
90 | 89 | fvmpts 5973 |
. . 3
    ![]_ ]_](_urbrack.gif)      
         
      ![]_ ]_](_urbrack.gif)  
     
         |
91 | 1, 88, 90 | syl2anc 671 |
. 2
       ![]_ ]_](_urbrack.gif)        
         |
92 | 21 | eqcomd 2467 |
. . 3
 
   ![]_ ]_](_urbrack.gif)   |
93 | 34, 82 | ifeqda 3925 |
. . . 4
  
   
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
94 | 27, 93 | ifeqda 3925 |
. . 3
 
      ![]_ ]_](_urbrack.gif)   
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     |
95 | 92, 94 | ifeqda 3925 |
. 2
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      |
96 | 91, 20, 95 | 3eqtrd 2499 |
1
       |