Proof of Theorem nn01to3
Step | Hyp | Ref
| Expression |
1 | | 3mix3 1180 |
. . 3
 
   |
2 | 1 | a1d 26 |
. 2
  
      |
3 | | nn0re 10885 |
. . . . . . . . . 10

  |
4 | 3 | 3ad2ant1 1030 |
. . . . . . . . 9
     |
5 | | 3re 10690 |
. . . . . . . . . 10
 |
6 | 5 | a1i 11 |
. . . . . . . . 9
     |
7 | | simp3 1011 |
. . . . . . . . 9
     |
8 | 4, 6, 7 | leltned 9793 |
. . . . . . . 8
   
   |
9 | | nesym 2682 |
. . . . . . . 8

  |
10 | 8, 9 | syl6rbb 266 |
. . . . . . 7
   
   |
11 | | elnnnn0c 10922 |
. . . . . . . . 9

    |
12 | | orc 387 |
. . . . . . . . . . . 12
 
   |
13 | 12 | a1d 26 |
. . . . . . . . . . 11
  
    |
14 | 13 | a1d 26 |
. . . . . . . . . 10
 
       |
15 | | eluz2b3 11239 |
. . . . . . . . . . . 12
         |
16 | | eluz2 11172 |
. . . . . . . . . . . . . . . 16
         |
17 | | 2a1 28 |
. . . . . . . . . . . . . . . . 17
         |
18 | | zre 10948 |
. . . . . . . . . . . . . . . . . . . 20
   |
19 | | zre 10948 |
. . . . . . . . . . . . . . . . . . . 20
   |
20 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
   |
21 | | leltne 9728 |
. . . . . . . . . . . . . . . . . . . 20
 
 
   |
22 | 18, 19, 20, 21 | syl3an 1311 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
23 | | 2z 10976 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
25 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
26 | | df-3 10676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
28 | 27 | breq2d 4417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
     |
29 | 28 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
30 | 29 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
    |
31 | | btwnnz 11019 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
32 | 24, 25, 30, 31 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
  |
33 | 32 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . . . . . . 23
    

   |
34 | 33 | exp31 609 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      |
35 | 34 | com24 90 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
36 | 35 | pm2.43i 49 |
. . . . . . . . . . . . . . . . . . . 20
 

    |
37 | 36 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . 19
 
 

    |
38 | 22, 37 | sylbird 239 |
. . . . . . . . . . . . . . . . . 18
 
       |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . 17
         |
40 | 17, 39 | pm2.61ine 2709 |
. . . . . . . . . . . . . . . 16
 
     |
41 | 16, 40 | sylbi 199 |
. . . . . . . . . . . . . . 15
    

   |
42 | 41 | imp 431 |
. . . . . . . . . . . . . 14
         |
43 | 42 | olcd 395 |
. . . . . . . . . . . . 13
       
   |
44 | 43 | ex 436 |
. . . . . . . . . . . 12
    

     |
45 | 15, 44 | sylbir 217 |
. . . . . . . . . . 11
         |
46 | 45 | expcom 437 |
. . . . . . . . . 10
 
       |
47 | 14, 46 | pm2.61ine 2709 |
. . . . . . . . 9
  
    |
48 | 11, 47 | sylbir 217 |
. . . . . . . 8
         |
49 | 48 | 3adant3 1029 |
. . . . . . 7
    
    |
50 | 10, 49 | sylbid 219 |
. . . . . 6
   
     |
51 | 50 | impcom 432 |
. . . . 5
  
  
   |
52 | 51 | orcd 394 |
. . . 4
  
        |
53 | | df-3or 987 |
. . . 4
         |
54 | 52, 53 | sylibr 216 |
. . 3
  
  
   |
55 | 54 | ex 436 |
. 2
  

     |
56 | 2, 55 | pm2.61i 168 |
1
   
   |