Proof of Theorem nn01to3
Step | Hyp | Ref
| Expression |
1 | | 3mix3 1232 |
. . 3
|
2 | 1 | a1d 25 |
. 2
|
3 | | nn0re 11301 |
. . . . . . . . . 10
|
4 | 3 | 3ad2ant1 1082 |
. . . . . . . . 9
|
5 | | 3re 11094 |
. . . . . . . . . 10
|
6 | 5 | a1i 11 |
. . . . . . . . 9
|
7 | | simp3 1063 |
. . . . . . . . 9
|
8 | 4, 6, 7 | leltned 10190 |
. . . . . . . 8
|
9 | | nesym 2850 |
. . . . . . . 8
|
10 | 8, 9 | syl6rbb 277 |
. . . . . . 7
|
11 | | elnnnn0c 11338 |
. . . . . . . . 9
|
12 | | orc 400 |
. . . . . . . . . . . 12
|
13 | 12 | a1d 25 |
. . . . . . . . . . 11
|
14 | 13 | a1d 25 |
. . . . . . . . . 10
|
15 | | eluz2b3 11762 |
. . . . . . . . . . . 12
|
16 | | eluz2 11693 |
. . . . . . . . . . . . . . . 16
|
17 | | 2a1 28 |
. . . . . . . . . . . . . . . . 17
|
18 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . 20
|
19 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . 20
|
20 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
|
21 | | leltne 10127 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 18, 19, 20, 21 | syl3an 1368 |
. . . . . . . . . . . . . . . . . . 19
|
23 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
25 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
26 | | df-3 11080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
28 | 27 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
29 | 28 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
31 | | btwnnz 11453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
32 | 24, 25, 30, 31 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
33 | 32 | pm2.21d 118 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
34 | 33 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 34 | com24 95 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | pm2.43i 52 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 22, 37 | sylbird 250 |
. . . . . . . . . . . . . . . . . 18
|
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . 17
|
40 | 17, 39 | pm2.61ine 2877 |
. . . . . . . . . . . . . . . 16
|
41 | 16, 40 | sylbi 207 |
. . . . . . . . . . . . . . 15
|
42 | 41 | imp 445 |
. . . . . . . . . . . . . 14
|
43 | 42 | olcd 408 |
. . . . . . . . . . . . 13
|
44 | 43 | ex 450 |
. . . . . . . . . . . 12
|
45 | 15, 44 | sylbir 225 |
. . . . . . . . . . 11
|
46 | 45 | expcom 451 |
. . . . . . . . . 10
|
47 | 14, 46 | pm2.61ine 2877 |
. . . . . . . . 9
|
48 | 11, 47 | sylbir 225 |
. . . . . . . 8
|
49 | 48 | 3adant3 1081 |
. . . . . . 7
|
50 | 10, 49 | sylbid 230 |
. . . . . 6
|
51 | 50 | impcom 446 |
. . . . 5
|
52 | 51 | orcd 407 |
. . . 4
|
53 | | df-3or 1038 |
. . . 4
|
54 | 52, 53 | sylibr 224 |
. . 3
|
55 | 54 | ex 450 |
. 2
|
56 | 2, 55 | pm2.61i 176 |
1
|