Step | Hyp | Ref
| Expression |
1 | | breq2 4644 |
. . . . . 6
  c c    |
2 | | breq1 4643 |
. . . . . 6
  c c    |
3 | 1, 2 | orbi12d 690 |
. . . . 5
  
c c   c c     |
4 | 3 | imbi2d 307 |
. . . 4
  
Nn  c
c    Nn  c c      |
5 | | elun 3221 |
. . . . . . . . . . . 12
   c    
c        c     c        |
6 | | eliniseg 5021 |
. . . . . . . . . . . . 13
  c     c   |
7 | | elimasn 5020 |
. . . . . . . . . . . . . 14
 c        c  |
8 | | df-br 4641 |
. . . . . . . . . . . . . 14
 c
   c  |
9 | 7, 8 | bitr4i 243 |
. . . . . . . . . . . . 13
 c     c   |
10 | 6, 9 | orbi12i 507 |
. . . . . . . . . . . 12
   c    
c       c c    |
11 | 5, 10 | bitri 240 |
. . . . . . . . . . 11
   c    
c       c c    |
12 | 11 | eqabi 2465 |
. . . . . . . . . 10
  c     c      
 c c    |
13 | 12 | uneq2i 3416 |
. . . . . . . . 9
 
Nn   c     c        
Nn   c c     |
14 | | unab 3522 |
. . . . . . . . 9
 
Nn   c c    

Nn  c c     |
15 | 13, 14 | eqtri 2373 |
. . . . . . . 8
 
Nn   c     c       

Nn  c c     |
16 | | imor 401 |
. . . . . . . . 9
  Nn  c c    Nn 
c c     |
17 | 16 | abbii 2466 |
. . . . . . . 8
  Nn  c c    

Nn  c c     |
18 | 15, 17 | eqtr4i 2376 |
. . . . . . 7
 
Nn   c     c       
 Nn 
c c     |
19 | | abexv 4325 |
. . . . . . . 8
 Nn  |
20 | | lecex 6116 |
. . . . . . . . . . 11
c  |
21 | 20 | cnvex 5103 |
. . . . . . . . . 10
c  |
22 | | snex 4112 |
. . . . . . . . . 10
 
 |
23 | 21, 22 | imaex 4748 |
. . . . . . . . 9
 c      |
24 | 20, 22 | imaex 4748 |
. . . . . . . . 9
c      |
25 | 23, 24 | unex 4107 |
. . . . . . . 8
  c     c       |
26 | 19, 25 | unex 4107 |
. . . . . . 7
 
Nn   c     c        |
27 | 18, 26 | eqeltrri 2424 |
. . . . . 6
  Nn  c c     |
28 | | breq1 4643 |
. . . . . . . 8
 0c  c
0c c    |
29 | | breq2 4644 |
. . . . . . . 8
 0c  c c 0c  |
30 | 28, 29 | orbi12d 690 |
. . . . . . 7
 0c   c c  0c c c 0c   |
31 | 30 | imbi2d 307 |
. . . . . 6
 0c   Nn  c c    Nn 0c c c 0c    |
32 | | breq1 4643 |
. . . . . . . 8
  c c    |
33 | | breq2 4644 |
. . . . . . . 8
  c
c    |
34 | 32, 33 | orbi12d 690 |
. . . . . . 7
  
c c   c c     |
35 | 34 | imbi2d 307 |
. . . . . 6
  
Nn  c c    Nn  c c      |
36 | | breq1 4643 |
. . . . . . . 8
  1c  c  1c c    |
37 | | breq2 4644 |
. . . . . . . 8
  1c  c c 
1c   |
38 | 36, 37 | orbi12d 690 |
. . . . . . 7
  1c   c c    1c c c  1c    |
39 | 38 | imbi2d 307 |
. . . . . 6
  1c   Nn  c c    Nn   1c c c  1c     |
40 | | breq1 4643 |
. . . . . . . 8
  c c    |
41 | | breq2 4644 |
. . . . . . . 8
  c
c    |
42 | 40, 41 | orbi12d 690 |
. . . . . . 7
  
c c   c c     |
43 | 42 | imbi2d 307 |
. . . . . 6
  
Nn  c c    Nn  c c      |
44 | | nnnc 6147 |
. . . . . . . 8
 Nn NC  |
45 | | le0nc 6201 |
. . . . . . . 8
 NC 0c c   |
46 | 44, 45 | syl 15 |
. . . . . . 7
 Nn 0c c   |
47 | | orc 374 |
. . . . . . 7
0c c 0c c c
0c  |
48 | 46, 47 | syl 15 |
. . . . . 6
 Nn 0c c c 0c  |
49 | | nnnc 6147 |
. . . . . . . . 9
 Nn NC  |
50 | | dflec2 6211 |
. . . . . . . . . . 11
  NC NC  c  NC      |
51 | | nc0le1 6217 |
. . . . . . . . . . . . . . . . . 18
 NC  0c 1c
c    |
52 | | 1cnc 6140 |
. . . . . . . . . . . . . . . . . . . . . 22
1c
NC |
53 | | le0nc 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
1c NC 0c c 1c |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
0c c 1c |
55 | | breq1 4643 |
. . . . . . . . . . . . . . . . . . . . 21
 0c  c
1c 0c c 1c  |
56 | 54, 55 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . 20
 0c c 1c |
57 | 56 | orim1i 503 |
. . . . . . . . . . . . . . . . . . 19
 
0c 1c c 
 c 1c 1c c    |
58 | 57 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
 NC   0c 1c c   c 1c 1c c     |
59 | 51, 58 | mpd 14 |
. . . . . . . . . . . . . . . . 17
 NC  c
1c 1c c    |
60 | 59 | orcomd 377 |
. . . . . . . . . . . . . . . 16
 NC 1c c c 1c  |
61 | 60 | adantl 452 |
. . . . . . . . . . . . . . 15
  NC NC 1c c c 1c  |
62 | | simpll 730 |
. . . . . . . . . . . . . . . . . 18
   NC NC
1c c  NC  |
63 | 52 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
   NC NC
1c c  1c
NC  |
64 | | simplr 731 |
. . . . . . . . . . . . . . . . . 18
   NC NC
1c c  NC  |
65 | | simpr 447 |
. . . . . . . . . . . . . . . . . 18
   NC NC
1c c  1c
c   |
66 | | leaddc2 6216 |
. . . . . . . . . . . . . . . . . 18
   NC 1c NC NC
1c c   1c c     |
67 | 62, 63, 64, 65, 66 | syl31anc 1185 |
. . . . . . . . . . . . . . . . 17
   NC NC
1c c   1c c     |
68 | 67 | ex 423 |
. . . . . . . . . . . . . . . 16
  NC NC 1c c 
1c
c      |
69 | | simpll 730 |
. . . . . . . . . . . . . . . . . 18
   NC NC c 1c
NC  |
70 | | simplr 731 |
. . . . . . . . . . . . . . . . . 18
   NC NC c 1c
NC  |
71 | 52 | a1i 10 |
. . . . . . . . . . . . . . . . . 18
   NC NC c 1c 1c NC  |
72 | | simpr 447 |
. . . . . . . . . . . . . . . . . 18
   NC NC c 1c c 1c |
73 | | leaddc2 6216 |
. . . . . . . . . . . . . . . . . 18
   NC NC 1c NC c
1c
  c 
1c  |
74 | 69, 70, 71, 72, 73 | syl31anc 1185 |
. . . . . . . . . . . . . . . . 17
   NC NC c 1c 
 c 
1c  |
75 | 74 | ex 423 |
. . . . . . . . . . . . . . . 16
  NC NC  c 1c 
 c 
1c   |
76 | 68, 75 | orim12d 811 |
. . . . . . . . . . . . . . 15
  NC NC  1c c c
1c
 
1c
c     c 
1c    |
77 | 61, 76 | mpd 14 |
. . . . . . . . . . . . . 14
  NC NC  
1c
c     c 
1c   |
78 | | breq2 4644 |
. . . . . . . . . . . . . . . . 17
  
 
1c
c  1c c      |
79 | | breq1 4643 |
. . . . . . . . . . . . . . . . 17
  
 c 
1c
  c  1c   |
80 | 78, 79 | orbi12d 690 |
. . . . . . . . . . . . . . . 16
  
  
1c
c c 
1c  
1c
c     c 
1c    |
81 | 80 | biimprd 214 |
. . . . . . . . . . . . . . 15
  
  
1c
c     c 
1c  
1c
c c 
1c    |
82 | 81 | com12 27 |
. . . . . . . . . . . . . 14
  
1c
c     c 
1c 
   
1c
c c 
1c    |
83 | 77, 82 | syl 15 |
. . . . . . . . . . . . 13
  NC NC   
 
1c
c c 
1c    |
84 | 83 | rexlimdva 2739 |
. . . . . . . . . . . 12
 NC   NC     1c c c 
1c    |
85 | 84 | adantr 451 |
. . . . . . . . . . 11
  NC NC  
NC    
1c
c c 
1c    |
86 | 50, 85 | sylbid 206 |
. . . . . . . . . 10
  NC NC  c  
1c
c c 
1c    |
87 | | addlecncs 6210 |
. . . . . . . . . . . . . . 15
  NC 1c NC c  1c  |
88 | 52, 87 | mpan2 652 |
. . . . . . . . . . . . . 14
 NC c 
1c  |
89 | 88 | adantl 452 |
. . . . . . . . . . . . 13
  NC NC c 
1c  |
90 | | peano2nc 6146 |
. . . . . . . . . . . . . . 15
 NC 
1c
NC  |
91 | 90 | adantl 452 |
. . . . . . . . . . . . . 14
  NC NC  1c
NC  |
92 | | lectr 6212 |
. . . . . . . . . . . . . 14
  NC NC  1c NC   c
c  1c
c 
1c   |
93 | 91, 92 | mpd3an3 1278 |
. . . . . . . . . . . . 13
  NC NC   c c 
1c c 
1c   |
94 | 89, 93 | mpan2d 655 |
. . . . . . . . . . . 12
  NC NC  c c 
1c   |
95 | 94 | ancoms 439 |
. . . . . . . . . . 11
  NC NC  c c 
1c   |
96 | | olc 373 |
. . . . . . . . . . 11
 c 
1c
 
1c
c c 
1c   |
97 | 95, 96 | syl6 29 |
. . . . . . . . . 10
  NC NC  c  
1c
c c 
1c    |
98 | 86, 97 | jaod 369 |
. . . . . . . . 9
  NC NC   c c   
1c
c c 
1c    |
99 | 49, 44, 98 | syl2an 463 |
. . . . . . . 8
  Nn Nn   c c   
1c
c c 
1c    |
100 | 99 | ex 423 |
. . . . . . 7
 Nn  Nn   c c   
1c
c c 
1c     |
101 | 100 | a2d 23 |
. . . . . 6
 Nn   Nn  c c   
Nn   1c c c  1c     |
102 | 27, 31, 35, 39, 43, 48, 101 | finds 4412 |
. . . . 5
 Nn  Nn  c
c     |
103 | 102 | com12 27 |
. . . 4
 Nn  Nn  c
c     |
104 | 4, 103 | vtoclga 2921 |
. . 3
 Nn  Nn  c c     |
105 | 104 | com12 27 |
. 2
 Nn  Nn  c c     |
106 | 105 | imp 418 |
1
  Nn Nn  c c    |