Proof of Theorem zeo
Step | Hyp | Ref
| Expression |
1 | | elz 9049 |
. 2
|
2 | | oveq1 5774 |
. . . . . 6
|
3 | | 2cn 8784 |
. . . . . . . 8
|
4 | | 2ap0 8806 |
. . . . . . . 8
# |
5 | 3, 4 | div0api 8499 |
. . . . . . 7
|
6 | | 0z 9058 |
. . . . . . 7
|
7 | 5, 6 | eqeltri 2210 |
. . . . . 6
|
8 | 2, 7 | eqeltrdi 2228 |
. . . . 5
|
9 | 8 | orcd 722 |
. . . 4
|
10 | 9 | adantl 275 |
. . 3
|
11 | | nneoor 9146 |
. . . . 5
|
12 | | nnz 9066 |
. . . . . 6
|
13 | | nnz 9066 |
. . . . . 6
|
14 | 12, 13 | orim12i 748 |
. . . . 5
|
15 | 11, 14 | syl 14 |
. . . 4
|
16 | 15 | adantl 275 |
. . 3
|
17 | | nneoor 9146 |
. . . . 5
|
18 | 17 | adantl 275 |
. . . 4
|
19 | | recn 7746 |
. . . . . . . . . 10
|
20 | | divnegap 8459 |
. . . . . . . . . . 11
# |
21 | 3, 4, 20 | mp3an23 1307 |
. . . . . . . . . 10
|
22 | 19, 21 | syl 14 |
. . . . . . . . 9
|
23 | 22 | eleq1d 2206 |
. . . . . . . 8
|
24 | | nnnegz 9050 |
. . . . . . . 8
|
25 | 23, 24 | syl6bir 163 |
. . . . . . 7
|
26 | 19 | halfcld 8957 |
. . . . . . . . 9
|
27 | 26 | negnegd 8057 |
. . . . . . . 8
|
28 | 27 | eleq1d 2206 |
. . . . . . 7
|
29 | 25, 28 | sylibd 148 |
. . . . . 6
|
30 | | nnz 9066 |
. . . . . . 7
|
31 | | peano2zm 9085 |
. . . . . . . . . 10
|
32 | | ax-1cn 7706 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32, 3 | negsubdi2i 8041 |
. . . . . . . . . . . . . . . . . 18
|
34 | | 2m1e1 8831 |
. . . . . . . . . . . . . . . . . 18
|
35 | 33, 34 | eqtr2i 2159 |
. . . . . . . . . . . . . . . . 17
|
36 | 32, 3 | subcli 8031 |
. . . . . . . . . . . . . . . . . 18
|
37 | 32, 36 | negcon2i 8038 |
. . . . . . . . . . . . . . . . 17
|
38 | 35, 37 | mpbi 144 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | oveq2i 5778 |
. . . . . . . . . . . . . . 15
|
40 | | negcl 7955 |
. . . . . . . . . . . . . . . 16
|
41 | | addsubass 7965 |
. . . . . . . . . . . . . . . . 17
|
42 | 32, 3, 41 | mp3an23 1307 |
. . . . . . . . . . . . . . . 16
|
43 | 40, 42 | syl 14 |
. . . . . . . . . . . . . . 15
|
44 | | negdi 8012 |
. . . . . . . . . . . . . . . 16
|
45 | 32, 44 | mpan2 421 |
. . . . . . . . . . . . . . 15
|
46 | 39, 43, 45 | 3eqtr4a 2196 |
. . . . . . . . . . . . . 14
|
47 | 46 | oveq1d 5782 |
. . . . . . . . . . . . 13
|
48 | | peano2cn 7890 |
. . . . . . . . . . . . . . . 16
|
49 | 40, 48 | syl 14 |
. . . . . . . . . . . . . . 15
|
50 | 3, 4 | pm3.2i 270 |
. . . . . . . . . . . . . . . 16
# |
51 | | divsubdirap 8461 |
. . . . . . . . . . . . . . . 16
#
|
52 | 3, 50, 51 | mp3an23 1307 |
. . . . . . . . . . . . . . 15
|
53 | 49, 52 | syl 14 |
. . . . . . . . . . . . . 14
|
54 | | 2div2e1 8845 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | eqcomi 2141 |
. . . . . . . . . . . . . . 15
|
56 | 55 | oveq2i 5778 |
. . . . . . . . . . . . . 14
|
57 | 53, 56 | syl6reqr 2189 |
. . . . . . . . . . . . 13
|
58 | | peano2cn 7890 |
. . . . . . . . . . . . . 14
|
59 | | divnegap 8459 |
. . . . . . . . . . . . . . 15
#
|
60 | 3, 4, 59 | mp3an23 1307 |
. . . . . . . . . . . . . 14
|
61 | 58, 60 | syl 14 |
. . . . . . . . . . . . 13
|
62 | 47, 57, 61 | 3eqtr4d 2180 |
. . . . . . . . . . . 12
|
63 | 19, 62 | syl 14 |
. . . . . . . . . . 11
|
64 | 63 | eleq1d 2206 |
. . . . . . . . . 10
|
65 | 31, 64 | syl5ib 153 |
. . . . . . . . 9
|
66 | | znegcl 9078 |
. . . . . . . . 9
|
67 | 65, 66 | syl6 33 |
. . . . . . . 8
|
68 | | peano2re 7891 |
. . . . . . . . . . . 12
|
69 | 68 | recnd 7787 |
. . . . . . . . . . 11
|
70 | 69 | halfcld 8957 |
. . . . . . . . . 10
|
71 | 70 | negnegd 8057 |
. . . . . . . . 9
|
72 | 71 | eleq1d 2206 |
. . . . . . . 8
|
73 | 67, 72 | sylibd 148 |
. . . . . . 7
|
74 | 30, 73 | syl5 32 |
. . . . . 6
|
75 | 29, 74 | orim12d 775 |
. . . . 5
|
76 | 75 | adantr 274 |
. . . 4
|
77 | 18, 76 | mpd 13 |
. . 3
|
78 | 10, 16, 77 | 3jaodan 1284 |
. 2
|
79 | 1, 78 | sylbi 120 |
1
|