Proof of Theorem usgra2pthlem1
Step | Hyp | Ref
| Expression |
1 | | 0nn0 10908 |
. . . . . . . . . . . . . 14
 |
2 | | 2nn0 10910 |
. . . . . . . . . . . . . 14
 |
3 | | 0le2 10722 |
. . . . . . . . . . . . . 14
 |
4 | | elfz2nn0 11911 |
. . . . . . . . . . . . . 14
    

   |
5 | 1, 2, 3, 4 | mpbir3an 1212 |
. . . . . . . . . . . . 13
     |
6 | | ffvelrn 6035 |
. . . . . . . . . . . . 13
              
      |
7 | 5, 6 | mpan2 685 |
. . . . . . . . . . . 12
               |
8 | 7 | adantl 473 |
. . . . . . . . . . 11
       ..^                                            USGrph
         
      |
9 | | 1nn0 10909 |
. . . . . . . . . . . . . . . . . 18
 |
10 | | 1le2 10846 |
. . . . . . . . . . . . . . . . . 18
 |
11 | | elfz2nn0 11911 |
. . . . . . . . . . . . . . . . . 18
    

   |
12 | 9, 2, 10, 11 | mpbir3an 1212 |
. . . . . . . . . . . . . . . . 17
     |
13 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . 17
              
      |
14 | 12, 13 | mpan2 685 |
. . . . . . . . . . . . . . . 16
               |
15 | 14 | adantl 473 |
. . . . . . . . . . . . . . 15
       ..^                                            USGrph
         
      |
16 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
      ..^                                            USGrph  USGrph   |
17 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . 19
     |
18 | 16, 17 | jctir 547 |
. . . . . . . . . . . . . . . . . 18
      ..^                                            USGrph   USGrph        |
19 | | prcom 4041 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
20 | 19 | eqeq2i 2483 |
. . . . . . . . . . . . . . . . . . . . 21
                   
                     |
21 | 20 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
22 | 21 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
                                                              |
23 | 22 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . 18
      ..^                                            USGrph                       |
24 | | usgranloopv 25184 |
. . . . . . . . . . . . . . . . . 18
  USGrph
                                    |
25 | 18, 23, 24 | sylc 61 |
. . . . . . . . . . . . . . . . 17
      ..^                                            USGrph            |
26 | 25 | adantr 472 |
. . . . . . . . . . . . . . . 16
       ..^                                            USGrph
         
          |
27 | 17 | elsnc 3984 |
. . . . . . . . . . . . . . . . 17
                     |
28 | 27 | necon3bbii 2690 |
. . . . . . . . . . . . . . . 16
                     |
29 | 26, 28 | sylibr 217 |
. . . . . . . . . . . . . . 15
       ..^                                            USGrph
         
            |
30 | 15, 29 | eldifd 3401 |
. . . . . . . . . . . . . 14
       ..^                                            USGrph
         
              |
31 | 30 | adantr 472 |
. . . . . . . . . . . . 13
        ..^                                            USGrph
                             |
32 | | sneq 3969 |
. . . . . . . . . . . . . . . 16
      
        |
33 | 32 | difeq2d 3540 |
. . . . . . . . . . . . . . 15
                   |
34 | 33 | eleq2d 2534 |
. . . . . . . . . . . . . 14
                             |
35 | 34 | adantl 473 |
. . . . . . . . . . . . 13
        ..^                                            USGrph
                                       |
36 | 31, 35 | mpbird 240 |
. . . . . . . . . . . 12
        ..^                                            USGrph
                         |
37 | | 2re 10701 |
. . . . . . . . . . . . . . . . . . . 20
 |
38 | 37 | leidi 10169 |
. . . . . . . . . . . . . . . . . . 19
 |
39 | | elfz2nn0 11911 |
. . . . . . . . . . . . . . . . . . 19
    

   |
40 | 2, 2, 38, 39 | mpbir3an 1212 |
. . . . . . . . . . . . . . . . . 18
     |
41 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . 18
              
      |
42 | 40, 41 | mpan2 685 |
. . . . . . . . . . . . . . . . 17
               |
43 | 42 | adantl 473 |
. . . . . . . . . . . . . . . 16
       ..^                                            USGrph
         
      |
44 | | usgraf1 25166 |
. . . . . . . . . . . . . . . . . . . . . 22
 USGrph       |
45 | 44 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . 21
       ..^                                            USGrph
         
      |
46 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . 22
     ..^                                               ..^     |
47 | 46 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . 21
       ..^                                            USGrph
         
   ..^     |
48 | 45, 47 | jca 541 |
. . . . . . . . . . . . . . . . . . . 20
       ..^                                            USGrph
         
        ..^      |
49 | | 2nn 10790 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
50 | | lbfzo0 11983 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^   |
51 | 49, 50 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . . 22
 ..^  |
52 | | 1lt2 10799 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
53 | | elfzo0 11984 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^ 
   |
54 | 9, 49, 52, 53 | mpbir3an 1212 |
. . . . . . . . . . . . . . . . . . . . . 22
 ..^  |
55 | 51, 54 | pm3.2i 462 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^  ..^   |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
       ..^                                            USGrph
         
  ..^  ..^    |
57 | | 0ne1 10699 |
. . . . . . . . . . . . . . . . . . . . 21
 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
       ..^                                            USGrph
         
  |
59 | 48, 56, 58 | 3jca 1210 |
. . . . . . . . . . . . . . . . . . 19
       ..^                                            USGrph
         
         ..^      ..^  ..^     |
60 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
     ..^                                                                                      |
61 | 60 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
       ..^                                            USGrph
         
                                          |
62 | | 2f1fvneq 39158 |
. . . . . . . . . . . . . . . . . . 19
          ..^      ..^
 ..^                                                                     |
63 | 59, 61, 62 | sylc 61 |
. . . . . . . . . . . . . . . . . 18
       ..^                                            USGrph
         
                        |
64 | | necom 2696 |
. . . . . . . . . . . . . . . . . . 19
        
          |
65 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . 21
     |
66 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . 21
     |
67 | 65, 17, 66 | 3pm3.2i 1208 |
. . . . . . . . . . . . . . . . . . . 20
               |
68 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^                                            USGrph        |
69 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                              |
70 | 69 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^                                            USGrph                       |
71 | 16, 68, 70 | jca31 543 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^                                            USGrph    USGrph
                           |
72 | 71 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . 21
       ..^                                            USGrph
         
  USGrph                            |
73 | | usgranloopv 25184 |
. . . . . . . . . . . . . . . . . . . . . 22
  USGrph
                                    |
74 | 73 | imp 436 |
. . . . . . . . . . . . . . . . . . . . 21
   USGrph                                    |
75 | 72, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
       ..^                                            USGrph
         
          |
76 | | pr1nebg 39139 |
. . . . . . . . . . . . . . . . . . . 20
                                                           |
77 | 67, 75, 76 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
       ..^                                            USGrph
         
                                  |
78 | 64, 77 | syl5bb 265 |
. . . . . . . . . . . . . . . . . 18
       ..^                                            USGrph
         
                                  |
79 | 63, 78 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
       ..^                                            USGrph
         
          |
80 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
      ..^                                            USGrph        |
81 | | prcom 4041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
82 | 81 | eqeq2i 2483 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
                     |
83 | 82 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
                                         |
84 | 83 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
                                                              |
85 | 84 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . 20
      ..^                                            USGrph                       |
86 | 16, 80, 85 | jca31 543 |
. . . . . . . . . . . . . . . . . . 19
      ..^                                            USGrph    USGrph
                           |
87 | 86 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
       ..^                                            USGrph
         
  USGrph                            |
88 | | usgranloopv 25184 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
                                    |
89 | 88 | imp 436 |
. . . . . . . . . . . . . . . . . 18
   USGrph                                    |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
       ..^                                            USGrph
         
          |
91 | 79, 90 | nelprd 3981 |
. . . . . . . . . . . . . . . 16
       ..^                                            USGrph
         
                 |
92 | 43, 91 | eldifd 3401 |
. . . . . . . . . . . . . . 15
       ..^                                            USGrph
         
                   |
93 | 92 | ad2antrr 740 |
. . . . . . . . . . . . . 14
         ..^                                            USGrph
                                       |
94 | | preq12 4044 |
. . . . . . . . . . . . . . . . 17
     
                     |
95 | 94 | difeq2d 3540 |
. . . . . . . . . . . . . . . 16
     
                         |
96 | 95 | eleq2d 2534 |
. . . . . . . . . . . . . . 15
     
                                   |
97 | 96 | adantll 728 |
. . . . . . . . . . . . . 14
         ..^                                            USGrph
                                                  |
98 | 93, 97 | mpbird 240 |
. . . . . . . . . . . . 13
         ..^                                            USGrph
                               |
99 | | eqcom 2478 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
100 | | eqcom 2478 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
101 | | eqcom 2478 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
102 | 99, 100, 101 | 3anbi123i 1219 |
. . . . . . . . . . . . . . . . . . . 20
     
   
                     |
103 | 102 | biimpi 199 |
. . . . . . . . . . . . . . . . . . 19
     
   
                     |
104 | 103 | 3expa 1231 |
. . . . . . . . . . . . . . . . . 18
                                 |
105 | 104 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
                                                                   |
106 | 99 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
107 | 106 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
108 | 100 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
109 | 108 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
110 | 107, 109 | preq12d 4050 |
. . . . . . . . . . . . . . . . . . . 20
                                 |
111 | 110 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . 19
                                    
              |
112 | 101 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
113 | 112 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
114 | 109, 113 | preq12d 4050 |
. . . . . . . . . . . . . . . . . . . 20
                                 |
115 | 114 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . 19
                                    
              |
116 | 111, 115 | anbi12d 725 |
. . . . . . . . . . . . . . . . . 18
                                                         
                           |
117 | 116 | biimpa 492 |
. . . . . . . . . . . . . . . . 17
       
                                                                             |
118 | 105, 117 | jca 541 |
. . . . . . . . . . . . . . . 16
       
                                                            
                                |
119 | 118 | exp41 621 |
. . . . . . . . . . . . . . 15
                                                                                                     |
120 | 119 | adantl 473 |
. . . . . . . . . . . . . 14
        ..^                                            USGrph
                                                                                                               |
121 | 120 | imp31 439 |
. . . . . . . . . . . . 13
          ..^                                            USGrph                                                                                                              |
122 | 98, 121 | rspcimedv 3138 |
. . . . . . . . . . . 12
         ..^                                            USGrph
                                                                             
                                 |
123 | 36, 122 | rspcimedv 3138 |
. . . . . . . . . . 11
        ..^                                            USGrph
                                                        
                     
                                 |
124 | 8, 123 | rspcimedv 3138 |
. . . . . . . . . 10
       ..^                                            USGrph
         
                                         

                     
                                 |
125 | 124 | exp41 621 |
. . . . . . . . 9
    ..^                                             USGrph
                                                  

                     
                                    |
126 | 125 | com15 95 |
. . . . . . . 8
                                                                                   USGrph
             ..^    
                     
                                    |
127 | 126 | pm2.43i 48 |
. . . . . . 7
                                          USGrph
             ..^   
                                                          |
128 | 127 | com12 31 |
. . . . . 6
 USGrph                                                  
    ..^   
                                                          |
129 | 128 | adantr 472 |
. . . . 5
  USGrph
                                                      
    ..^   
                                                          |
130 | | oveq2 6316 |
. . . . . . . 8
      ..^      ..^   |
131 | 130 | raleqdv 2979 |
. . . . . . 7
      
 ..^                             ..^                          |
132 | | fzo0to2pr 12027 |
. . . . . . . . 9
 ..^     |
133 | 132 | raleqi 2977 |
. . . . . . . 8
 
 ..^                                                  |
134 | | 2wlklem 25373 |
. . . . . . . 8
 
                                                                  |
135 | 133, 134 | bitri 257 |
. . . . . . 7
 
 ..^                                                                 |
136 | 131, 135 | syl6bb 269 |
. . . . . 6
      
 ..^                                                                      |
137 | 136 | adantl 473 |
. . . . 5
  USGrph
      
 ..^                                                                      |
138 | | oveq2 6316 |
. . . . . . . 8
                   |
139 | 138 | feq2d 5725 |
. . . . . . 7
                 
           |
140 | 139 | adantl 473 |
. . . . . 6
  USGrph
                 
           |
141 | | f1eq2 5788 |
. . . . . . . . 9
  ..^      ..^     ..^          ..^      |
142 | 130, 141 | syl 17 |
. . . . . . . 8
         ..^      
   ..^      |
143 | 142 | imbi1d 324 |
. . . . . . 7
          ..^        
                     
                                   ..^   
                                                         |
144 | 143 | adantl 473 |
. . . . . 6
  USGrph
          ..^        
                     
                                   ..^   
                                                         |
145 | 140, 144 | imbi12d 327 |
. . . . 5
  USGrph
                       ..^        
                     
                               
             ..^    
                     
                                   |
146 | 129, 137,
145 | 3imtr4d 276 |
. . . 4
  USGrph
      
 ..^                          
                 ..^        
                     
                                   |
147 | 146 | com14 90 |
. . 3
    ..^        
 ..^                          
               USGrph       
                     
                                   |
148 | 147 | com23 80 |
. 2
    ..^                       ..^                             USGrph
     

                     
                                   |
149 | 148 | 3imp 1224 |
1
     ..^                     ..^                              USGrph
     

                     
                                 |