Proof of Theorem subfzo0
Step | Hyp | Ref
| Expression |
1 | | elfzo0 10165 |
. . 3
  ..^ 
   |
2 | | elfzo0 10165 |
. . . . 5
  ..^ 
   |
3 | | nn0re 9171 |
. . . . . . . . . . . 12

  |
4 | 3 | adantr 276 |
. . . . . . . . . . 11
  
  |
5 | | nnre 8912 |
. . . . . . . . . . . . . 14
   |
6 | | nn0re 9171 |
. . . . . . . . . . . . . 14

  |
7 | | resubcl 8208 |
. . . . . . . . . . . . . 14
 
     |
8 | 5, 6, 7 | syl2an 289 |
. . . . . . . . . . . . 13
 
     |
9 | 8 | ancoms 268 |
. . . . . . . . . . . 12
 
     |
10 | 9 | 3adant3 1017 |
. . . . . . . . . . 11
 
 
   |
11 | 4, 10 | anim12i 338 |
. . . . . . . . . 10
    
   
    |
12 | | nn0ge0 9187 |
. . . . . . . . . . . 12

  |
13 | 12 | adantr 276 |
. . . . . . . . . . 11
  
  |
14 | | posdif 8399 |
. . . . . . . . . . . . 13
 
       |
15 | 6, 5, 14 | syl2an 289 |
. . . . . . . . . . . 12
 
       |
16 | 15 | biimp3a 1345 |
. . . . . . . . . . 11
 
     |
17 | 13, 16 | anim12i 338 |
. . . . . . . . . 10
    
  
     |
18 | | addgegt0 8393 |
. . . . . . . . . 10
       
         |
19 | 11, 17, 18 | syl2anc 411 |
. . . . . . . . 9
    
        |
20 | | nn0cn 9172 |
. . . . . . . . . . . 12

  |
21 | 20 | adantr 276 |
. . . . . . . . . . 11
  
  |
22 | 21 | adantr 276 |
. . . . . . . . . 10
    
    |
23 | | nn0cn 9172 |
. . . . . . . . . . . 12

  |
24 | 23 | 3ad2ant1 1018 |
. . . . . . . . . . 11
 
   |
25 | 24 | adantl 277 |
. . . . . . . . . 10
    
    |
26 | | nncn 8913 |
. . . . . . . . . . . 12
   |
27 | 26 | 3ad2ant2 1019 |
. . . . . . . . . . 11
 
   |
28 | 27 | adantl 277 |
. . . . . . . . . 10
    
    |
29 | 22, 25, 28 | subadd23d 8277 |
. . . . . . . . 9
    
       
    |
30 | 19, 29 | breqtrrd 4028 |
. . . . . . . 8
    
        |
31 | 6 | 3ad2ant1 1018 |
. . . . . . . . . 10
 
   |
32 | | resubcl 8208 |
. . . . . . . . . 10
 
     |
33 | 4, 31, 32 | syl2an 289 |
. . . . . . . . 9
    
      |
34 | 5 | 3ad2ant2 1019 |
. . . . . . . . . 10
 
   |
35 | 34 | adantl 277 |
. . . . . . . . 9
    
    |
36 | 33, 35 | possumd 8513 |
. . . . . . . 8
    
  
   
      |
37 | 30, 36 | mpbid 147 |
. . . . . . 7
    
       |
38 | 3 | adantr 276 |
. . . . . . . . . . . 12
  
    |
39 | 34 | adantl 277 |
. . . . . . . . . . . 12
  
    |
40 | | readdcl 7925 |
. . . . . . . . . . . . . . 15
 
     |
41 | 6, 5, 40 | syl2an 289 |
. . . . . . . . . . . . . 14
 
     |
42 | 41 | 3adant3 1017 |
. . . . . . . . . . . . 13
 
 
   |
43 | 42 | adantl 277 |
. . . . . . . . . . . 12
  
      |
44 | 38, 39, 43 | 3jca 1177 |
. . . . . . . . . . 11
  
        |
45 | | nn0ge0 9187 |
. . . . . . . . . . . . . 14

  |
46 | 45 | 3ad2ant1 1018 |
. . . . . . . . . . . . 13
 
   |
47 | 46 | adantl 277 |
. . . . . . . . . . . 12
  
    |
48 | 5, 6 | anim12i 338 |
. . . . . . . . . . . . . . . 16
 
     |
49 | 48 | ancoms 268 |
. . . . . . . . . . . . . . 15
 
     |
50 | 49 | 3adant3 1017 |
. . . . . . . . . . . . . 14
 
 
   |
51 | 50 | adantl 277 |
. . . . . . . . . . . . 13
  
      |
52 | | addge02 8417 |
. . . . . . . . . . . . 13
 
       |
53 | 51, 52 | syl 14 |
. . . . . . . . . . . 12
  
  
     |
54 | 47, 53 | mpbid 147 |
. . . . . . . . . . 11
  
  
   |
55 | 44, 54 | lelttrdi 8370 |
. . . . . . . . . 10
  
  
     |
56 | 55 | impancom 260 |
. . . . . . . . 9
    

     |
57 | 56 | imp 124 |
. . . . . . . 8
    
      |
58 | 4 | adantr 276 |
. . . . . . . . 9
    
    |
59 | 31 | adantl 277 |
. . . . . . . . 9
    
    |
60 | 58, 59, 35 | ltsubadd2d 8487 |
. . . . . . . 8
    
    
     |
61 | 57, 60 | mpbird 167 |
. . . . . . 7
    
      |
62 | 37, 61 | jca 306 |
. . . . . 6
    
      

   |
63 | 62 | ex 115 |
. . . . 5
    

   
      |
64 | 2, 63 | biimtrid 152 |
. . . 4
     ..^           |
65 | 64 | 3adant2 1016 |
. . 3
 
 
 ..^     

    |
66 | 1, 65 | sylbi 121 |
. 2
  ..^
  ..^    
      |
67 | 66 | imp 124 |
1
   ..^  ..^ 
   
     |