Proof of Theorem zeo
Step | Hyp | Ref
| Expression |
1 | | elz 9170 |
. 2
|
2 | | oveq1 5832 |
. . . . . 6
|
3 | | 2cn 8905 |
. . . . . . . 8
|
4 | | 2ap0 8927 |
. . . . . . . 8
# |
5 | 3, 4 | div0api 8620 |
. . . . . . 7
|
6 | | 0z 9179 |
. . . . . . 7
|
7 | 5, 6 | eqeltri 2230 |
. . . . . 6
|
8 | 2, 7 | eqeltrdi 2248 |
. . . . 5
|
9 | 8 | orcd 723 |
. . . 4
|
10 | 9 | adantl 275 |
. . 3
|
11 | | nneoor 9267 |
. . . . 5
|
12 | | nnz 9187 |
. . . . . 6
|
13 | | nnz 9187 |
. . . . . 6
|
14 | 12, 13 | orim12i 749 |
. . . . 5
|
15 | 11, 14 | syl 14 |
. . . 4
|
16 | 15 | adantl 275 |
. . 3
|
17 | | nneoor 9267 |
. . . . 5
|
18 | 17 | adantl 275 |
. . . 4
|
19 | | recn 7866 |
. . . . . . . . . 10
|
20 | | divnegap 8580 |
. . . . . . . . . . 11
# |
21 | 3, 4, 20 | mp3an23 1311 |
. . . . . . . . . 10
|
22 | 19, 21 | syl 14 |
. . . . . . . . 9
|
23 | 22 | eleq1d 2226 |
. . . . . . . 8
|
24 | | nnnegz 9171 |
. . . . . . . 8
|
25 | 23, 24 | syl6bir 163 |
. . . . . . 7
|
26 | 19 | halfcld 9078 |
. . . . . . . . 9
|
27 | 26 | negnegd 8178 |
. . . . . . . 8
|
28 | 27 | eleq1d 2226 |
. . . . . . 7
|
29 | 25, 28 | sylibd 148 |
. . . . . 6
|
30 | | nnz 9187 |
. . . . . . 7
|
31 | | peano2zm 9206 |
. . . . . . . . . 10
|
32 | | ax-1cn 7826 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32, 3 | negsubdi2i 8162 |
. . . . . . . . . . . . . . . . . 18
|
34 | | 2m1e1 8952 |
. . . . . . . . . . . . . . . . . 18
|
35 | 33, 34 | eqtr2i 2179 |
. . . . . . . . . . . . . . . . 17
|
36 | 32, 3 | subcli 8152 |
. . . . . . . . . . . . . . . . . 18
|
37 | 32, 36 | negcon2i 8159 |
. . . . . . . . . . . . . . . . 17
|
38 | 35, 37 | mpbi 144 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | oveq2i 5836 |
. . . . . . . . . . . . . . 15
|
40 | | negcl 8076 |
. . . . . . . . . . . . . . . 16
|
41 | | addsubass 8086 |
. . . . . . . . . . . . . . . . 17
|
42 | 32, 3, 41 | mp3an23 1311 |
. . . . . . . . . . . . . . . 16
|
43 | 40, 42 | syl 14 |
. . . . . . . . . . . . . . 15
|
44 | | negdi 8133 |
. . . . . . . . . . . . . . . 16
|
45 | 32, 44 | mpan2 422 |
. . . . . . . . . . . . . . 15
|
46 | 39, 43, 45 | 3eqtr4a 2216 |
. . . . . . . . . . . . . 14
|
47 | 46 | oveq1d 5840 |
. . . . . . . . . . . . 13
|
48 | | 2div2e1 8966 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | eqcomi 2161 |
. . . . . . . . . . . . . . 15
|
50 | 49 | oveq2i 5836 |
. . . . . . . . . . . . . 14
|
51 | | peano2cn 8011 |
. . . . . . . . . . . . . . . 16
|
52 | 40, 51 | syl 14 |
. . . . . . . . . . . . . . 15
|
53 | 3, 4 | pm3.2i 270 |
. . . . . . . . . . . . . . . 16
# |
54 | | divsubdirap 8582 |
. . . . . . . . . . . . . . . 16
#
|
55 | 3, 53, 54 | mp3an23 1311 |
. . . . . . . . . . . . . . 15
|
56 | 52, 55 | syl 14 |
. . . . . . . . . . . . . 14
|
57 | 50, 56 | eqtr4id 2209 |
. . . . . . . . . . . . 13
|
58 | | peano2cn 8011 |
. . . . . . . . . . . . . 14
|
59 | | divnegap 8580 |
. . . . . . . . . . . . . . 15
#
|
60 | 3, 4, 59 | mp3an23 1311 |
. . . . . . . . . . . . . 14
|
61 | 58, 60 | syl 14 |
. . . . . . . . . . . . 13
|
62 | 47, 57, 61 | 3eqtr4d 2200 |
. . . . . . . . . . . 12
|
63 | 19, 62 | syl 14 |
. . . . . . . . . . 11
|
64 | 63 | eleq1d 2226 |
. . . . . . . . . 10
|
65 | 31, 64 | syl5ib 153 |
. . . . . . . . 9
|
66 | | znegcl 9199 |
. . . . . . . . 9
|
67 | 65, 66 | syl6 33 |
. . . . . . . 8
|
68 | | peano2re 8012 |
. . . . . . . . . . . 12
|
69 | 68 | recnd 7907 |
. . . . . . . . . . 11
|
70 | 69 | halfcld 9078 |
. . . . . . . . . 10
|
71 | 70 | negnegd 8178 |
. . . . . . . . 9
|
72 | 71 | eleq1d 2226 |
. . . . . . . 8
|
73 | 67, 72 | sylibd 148 |
. . . . . . 7
|
74 | 30, 73 | syl5 32 |
. . . . . 6
|
75 | 29, 74 | orim12d 776 |
. . . . 5
|
76 | 75 | adantr 274 |
. . . 4
|
77 | 18, 76 | mpd 13 |
. . 3
|
78 | 10, 16, 77 | 3jaodan 1288 |
. 2
|
79 | 1, 78 | sylbi 120 |
1
|