Step | Hyp | Ref
| Expression |
1 | | tru 1487 |
. . . 4
|
2 | | eqeq12 2635 |
. . . . . 6
|
3 | | csbeq1 3536 |
. . . . . . . 8
..^ ..^ |
4 | | csbeq1 3536 |
. . . . . . . 8
..^ ..^ |
5 | 3, 4 | ineqan12d 3816 |
. . . . . . 7
..^ ..^
..^
..^ |
6 | 5 | eqeq1d 2624 |
. . . . . 6
..^ ..^
..^
..^ |
7 | 2, 6 | orbi12d 746 |
. . . . 5
..^ ..^ ..^ ..^ |
8 | | eqeq12 2635 |
. . . . . . 7
|
9 | | equcom 1945 |
. . . . . . 7
|
10 | 8, 9 | syl6bb 276 |
. . . . . 6
|
11 | | csbeq1 3536 |
. . . . . . . . 9
..^ ..^ |
12 | | csbeq1 3536 |
. . . . . . . . 9
..^ ..^ |
13 | 11, 12 | ineqan12d 3816 |
. . . . . . . 8
..^ ..^
..^
..^ |
14 | | incom 3805 |
. . . . . . . 8
..^ ..^
..^
..^ |
15 | 13, 14 | syl6eq 2672 |
. . . . . . 7
..^ ..^
..^
..^ |
16 | 15 | eqeq1d 2624 |
. . . . . 6
..^ ..^
..^
..^ |
17 | 10, 16 | orbi12d 746 |
. . . . 5
..^ ..^ ..^ ..^ |
18 | | fzossnn 12516 |
. . . . . . 7
..^ |
19 | | nnssre 11024 |
. . . . . . 7
|
20 | 18, 19 | sstri 3612 |
. . . . . 6
..^ |
21 | 20 | a1i 11 |
. . . . 5
..^ |
22 | | biidd 252 |
. . . . 5
..^ ..^ ..^ ..^ ..^ ..^ |
23 | | nesym 2850 |
. . . . . . . 8
|
24 | 20 | sseli 3599 |
. . . . . . . . . 10
..^
|
25 | 20 | sseli 3599 |
. . . . . . . . . 10
..^
|
26 | | id 22 |
. . . . . . . . . 10
|
27 | | leltne 10127 |
. . . . . . . . . 10
|
28 | 24, 25, 26, 27 | syl3an 1368 |
. . . . . . . . 9
..^ ..^
|
29 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
30 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
31 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
..^ |
32 | | iundisj2fi.0 |
. . . . . . . . . . . . . . . . 17
|
33 | 31, 32 | nfiun 4548 |
. . . . . . . . . . . . . . . 16
..^ |
34 | 30, 33 | nfdif 3731 |
. . . . . . . . . . . . . . 15
..^ |
35 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
36 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
37 | 36 | iuneq1d 4545 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
38 | 35, 37 | difeq12d 3729 |
. . . . . . . . . . . . . . 15
..^
..^ |
39 | 29, 34, 38 | csbief 3558 |
. . . . . . . . . . . . . 14
..^ ..^ |
40 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
41 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
42 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
..^ |
43 | 42, 32 | nfiun 4548 |
. . . . . . . . . . . . . . . 16
..^ |
44 | 41, 43 | nfdif 3731 |
. . . . . . . . . . . . . . 15
..^ |
45 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
46 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
47 | 46 | iuneq1d 4545 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
48 | 45, 47 | difeq12d 3729 |
. . . . . . . . . . . . . . 15
..^
..^ |
49 | 40, 44, 48 | csbief 3558 |
. . . . . . . . . . . . . 14
..^ ..^ |
50 | 39, 49 | ineq12i 3812 |
. . . . . . . . . . . . 13
..^ ..^
..^
..^ |
51 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
..^ |
52 | 18, 51 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
53 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . 18
|
54 | 52, 53 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
55 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
..^ |
56 | 18, 55 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
57 | 56 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
58 | | simp3 1063 |
. . . . . . . . . . . . . . . . 17
..^ ..^
|
59 | | elfzo2 12473 |
. . . . . . . . . . . . . . . . 17
..^
|
60 | 54, 57, 58, 59 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . 16
..^ ..^
..^ |
61 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | | iundisj2fi.1 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 61, 32, 62 | csbhypf 3552 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63 | equcoms 1947 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
66 | 65 | ssiun2s 4564 |
. . . . . . . . . . . . . . . 16
..^
..^ |
67 | 60, 66 | syl 17 |
. . . . . . . . . . . . . . 15
..^ ..^
..^ |
68 | 67 | ssdifssd 3748 |
. . . . . . . . . . . . . 14
..^ ..^
..^
..^ |
69 | | ssrin 3838 |
. . . . . . . . . . . . . 14
..^ ..^
..^
..^ ..^
..^ |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
..^ ..^
..^
..^ ..^
..^ |
71 | 50, 70 | syl5eqss 3649 |
. . . . . . . . . . . 12
..^ ..^
..^ ..^
..^
..^ |
72 | | disjdif 4040 |
. . . . . . . . . . . 12
..^
..^ |
73 | | sseq0 3975 |
. . . . . . . . . . . 12
..^ ..^
..^
..^
..^
..^ ..^ ..^ |
74 | 71, 72, 73 | sylancl 694 |
. . . . . . . . . . 11
..^ ..^
..^ ..^ |
75 | 74 | 3expia 1267 |
. . . . . . . . . 10
..^ ..^
..^ ..^ |
76 | 75 | 3adant3 1081 |
. . . . . . . . 9
..^ ..^
..^ ..^ |
77 | 28, 76 | sylbird 250 |
. . . . . . . 8
..^ ..^
..^ ..^ |
78 | 23, 77 | syl5bir 233 |
. . . . . . 7
..^ ..^
..^
..^ |
79 | 78 | orrd 393 |
. . . . . 6
..^ ..^
..^
..^ |
80 | 79 | adantl 482 |
. . . . 5
..^ ..^
..^ ..^ |
81 | 7, 17, 21, 22, 80 | wlogle 10561 |
. . . 4
..^ ..^
..^ ..^ |
82 | 1, 81 | mpan 706 |
. . 3
..^ ..^
..^
..^ |
83 | 82 | rgen2a 2977 |
. 2
..^ ..^
..^ ..^ |
84 | | disjors 4635 |
. 2
Disj ..^
..^
..^
..^
..^
..^ |
85 | 83, 84 | mpbir 221 |
1
Disj ..^
..^ |