Proof of Theorem zeo
Step | Hyp | Ref
| Expression |
1 | | elz 8023 |
. 2
  
     |
2 | | oveq1 5462 |
. . . . . 6
       |
3 | | 2cn 7766 |
. . . . . . . 8
 |
4 | | 2ap0 7789 |
. . . . . . . 8
#  |
5 | 3, 4 | div0api 7504 |
. . . . . . 7
   |
6 | | 0z 8032 |
. . . . . . 7
 |
7 | 5, 6 | eqeltri 2107 |
. . . . . 6
   |
8 | 2, 7 | syl6eqel 2125 |
. . . . 5
     |
9 | 8 | orcd 651 |
. . . 4
  

       |
10 | 9 | adantl 262 |
. . 3
 
       
   |
11 | | nneoor 8116 |
. . . . 5
  

       |
12 | | nnz 8040 |
. . . . . 6
       |
13 | | nnz 8040 |
. . . . . 6
      
    |
14 | 12, 13 | orim12i 675 |
. . . . 5
   
       
       |
15 | 11, 14 | syl 14 |
. . . 4
  

       |
16 | 15 | adantl 262 |
. . 3
 
       
   |
17 | | nneoor 8116 |
. . . . 5
 
            |
18 | 17 | adantl 262 |
. . . 4
                |
19 | | recn 6812 |
. . . . . . . . . 10
   |
20 | | divnegap 7465 |
. . . . . . . . . . 11
 
# 
        |
21 | 3, 4, 20 | mp3an23 1223 |
. . . . . . . . . 10
         |
22 | 19, 21 | syl 14 |
. . . . . . . . 9
         |
23 | 22 | eleq1d 2103 |
. . . . . . . 8
    
      |
24 | | nnnegz 8024 |
. . . . . . . 8
  

   
  |
25 | 23, 24 | syl6bir 153 |
. . . . . . 7
    
   
   |
26 | 19 | halfcld 7946 |
. . . . . . . . 9
     |
27 | 26 | negnegd 7109 |
. . . . . . . 8
         |
28 | 27 | eleq1d 2103 |
. . . . . . 7
     
     |
29 | 25, 28 | sylibd 138 |
. . . . . 6
    


   |
30 | | nnz 8040 |
. . . . . . 7
     
    
  |
31 | | peano2zm 8059 |
. . . . . . . . . 10
     
         |
32 | | ax-1cn 6776 |
. . . . . . . . . . . . . . . . . . 19
 |
33 | 32, 3 | negsubdi2i 7093 |
. . . . . . . . . . . . . . . . . 18
      |
34 | | 2m1e1 7812 |
. . . . . . . . . . . . . . . . . 18
   |
35 | 33, 34 | eqtr2i 2058 |
. . . . . . . . . . . . . . . . 17
    |
36 | 32, 3 | subcli 7083 |
. . . . . . . . . . . . . . . . . 18
   |
37 | 32, 36 | negcon2i 7090 |
. . . . . . . . . . . . . . . . 17
         |
38 | 35, 37 | mpbi 133 |
. . . . . . . . . . . . . . . 16
    |
39 | 38 | oveq2i 5466 |
. . . . . . . . . . . . . . 15
 
        |
40 | | negcl 7008 |
. . . . . . . . . . . . . . . 16
    |
41 | | addsubass 7018 |
. . . . . . . . . . . . . . . . 17
  
             |
42 | 32, 3, 41 | mp3an23 1223 |
. . . . . . . . . . . . . . . 16
 
      
     |
43 | 40, 42 | syl 14 |
. . . . . . . . . . . . . . 15
             |
44 | | negdi 7064 |
. . . . . . . . . . . . . . . 16
 
          |
45 | 32, 44 | mpan2 401 |
. . . . . . . . . . . . . . 15
  
       |
46 | 39, 43, 45 | 3eqtr4a 2095 |
. . . . . . . . . . . . . 14
           |
47 | 46 | oveq1d 5470 |
. . . . . . . . . . . . 13
          
    |
48 | | peano2cn 6945 |
. . . . . . . . . . . . . . . 16
 
     |
49 | 40, 48 | syl 14 |
. . . . . . . . . . . . . . 15
      |
50 | 3, 4 | pm3.2i 257 |
. . . . . . . . . . . . . . . 16
 #   |
51 | | divsubdirap 7466 |
. . . . . . . . . . . . . . . 16
      #      
         
    |
52 | 3, 50, 51 | mp3an23 1223 |
. . . . . . . . . . . . . . 15
          
           |
53 | 49, 52 | syl 14 |
. . . . . . . . . . . . . 14
                   |
54 | | 2div2e1 7820 |
. . . . . . . . . . . . . . . 16
   |
55 | 54 | eqcomi 2041 |
. . . . . . . . . . . . . . 15
   |
56 | 55 | oveq2i 5466 |
. . . . . . . . . . . . . 14
          
      |
57 | 53, 56 | syl6reqr 2088 |
. . . . . . . . . . . . 13
           
     |
58 | | peano2cn 6945 |
. . . . . . . . . . . . . 14
 
   |
59 | | divnegap 7465 |
. . . . . . . . . . . . . . 15
   
# 
  
         |
60 | 3, 4, 59 | mp3an23 1223 |
. . . . . . . . . . . . . 14
     
         |
61 | 58, 60 | syl 14 |
. . . . . . . . . . . . 13
   
         |
62 | 47, 57, 61 | 3eqtr4d 2079 |
. . . . . . . . . . . 12
               |
63 | 19, 62 | syl 14 |
. . . . . . . . . . 11
               |
64 | 63 | eleq1d 2103 |
. . . . . . . . . 10
           
     |
65 | 31, 64 | syl5ib 143 |
. . . . . . . . 9
      
    
   |
66 | | znegcl 8052 |
. . . . . . . . 9
         
    |
67 | 65, 66 | syl6 29 |
. . . . . . . 8
      
     
   |
68 | | peano2re 6946 |
. . . . . . . . . . . 12
 
   |
69 | 68 | recnd 6851 |
. . . . . . . . . . 11
 
   |
70 | 69 | halfcld 7946 |
. . . . . . . . . 10
  
    |
71 | 70 | negnegd 7109 |
. . . . . . . . 9
    
        |
72 | 71 | eleq1d 2103 |
. . . . . . . 8
       
       |
73 | 67, 72 | sylibd 138 |
. . . . . . 7
      
       |
74 | 30, 73 | syl5 28 |
. . . . . 6
      
       |
75 | 29, 74 | orim12d 699 |
. . . . 5
                       |
76 | 75 | adantr 261 |
. . . 4
                 
        |
77 | 18, 76 | mpd 13 |
. . 3
          
   |
78 | 10, 16, 77 | 3jaodan 1200 |
. 2
  
  
 

       |
79 | 1, 78 | sylbi 114 |
1
  

       |