NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sfinltfin Unicode version

Theorem sfinltfin 4535
Description: Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
sfinltfin Sfin Sfin <fin <fin

Proof of Theorem sfinltfin
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sfin 4446 . . 3 Sfin Nn Nn 1
2 df-sfin 4446 . . 3 Sfin Nn Nn 1
3 3an6 1262 . . . 4 Nn Nn Nn Nn 1 1 Nn Nn 1 Nn Nn 1
4 eeanv 1913 . . . . . 6 1 1 1 1
5 simp1l 979 . . . . . . . . . 10 Nn Nn Nn Nn 1 1 Nn
6 simp3ll 1026 . . . . . . . . . 10 Nn Nn Nn Nn 1 1 1
7 ncfinlower 4483 . . . . . . . . . 10 Nn 1 1 Nn
85, 6, 6, 7syl3anc 1182 . . . . . . . . 9 Nn Nn Nn Nn 1 1 Nn
9 simp1r 980 . . . . . . . . . 10 Nn Nn Nn Nn 1 1 Nn
10 simp3rl 1028 . . . . . . . . . 10 Nn Nn Nn Nn 1 1 1
11 ncfinlower 4483 . . . . . . . . . 10 Nn 1 1 Nn
129, 10, 10, 11syl3anc 1182 . . . . . . . . 9 Nn Nn Nn Nn 1 1 Nn
13 reeanv 2778 . . . . . . . . . 10 Nn Nn Nn Nn
14 simpl 443 . . . . . . . . . . . . 13
15 simpl 443 . . . . . . . . . . . . 13
1614, 15anim12i 549 . . . . . . . . . . . 12
176adantr 451 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn 1
18 simprll 738 . . . . . . . . . . . . . . . . . 18 Nn Nn Nn Nn 1 1 Nn Nn Nn
19 simprrl 740 . . . . . . . . . . . . . . . . . 18 Nn Nn Nn Nn 1 1 Nn Nn
20 tfinpw1 4494 . . . . . . . . . . . . . . . . . 18 Nn 1 Tfin
2118, 19, 20syl2anc 642 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn 1 Tfin
22 elin 3219 . . . . . . . . . . . . . . . . 17 1 Tfin 1 1 Tfin
2317, 21, 22sylanbrc 645 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn 1 Tfin
24 n0i 3555 . . . . . . . . . . . . . . . 16 1 Tfin Tfin
2523, 24syl 15 . . . . . . . . . . . . . . 15 Nn Nn Nn Nn 1 1 Nn Nn Tfin
26 simpl1l 1006 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn Nn
27 ne0i 3556 . . . . . . . . . . . . . . . . . 18
2819, 27syl 15 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn
29 tfinprop 4489 . . . . . . . . . . . . . . . . . 18 Nn Tfin Nn 1 Tfin
3029simpld 445 . . . . . . . . . . . . . . . . 17 Nn Tfin Nn
3118, 28, 30syl2anc 642 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn Tfin Nn
32 nndisjeq 4429 . . . . . . . . . . . . . . . 16 Nn Tfin Nn Tfin Tfin
3326, 31, 32syl2anc 642 . . . . . . . . . . . . . . 15 Nn Nn Nn Nn 1 1 Nn Nn Tfin Tfin
34 orel1 371 . . . . . . . . . . . . . . 15 Tfin Tfin Tfin Tfin
3525, 33, 34sylc 56 . . . . . . . . . . . . . 14 Nn Nn Nn Nn 1 1 Nn Nn Tfin
3610adantr 451 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn 1
37 simprlr 739 . . . . . . . . . . . . . . . . . 18 Nn Nn Nn Nn 1 1 Nn Nn Nn
38 simprrr 741 . . . . . . . . . . . . . . . . . 18 Nn Nn Nn Nn 1 1 Nn Nn
39 tfinpw1 4494 . . . . . . . . . . . . . . . . . 18 Nn 1 Tfin
4037, 38, 39syl2anc 642 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn 1 Tfin
41 elin 3219 . . . . . . . . . . . . . . . . 17 1 Tfin 1 1 Tfin
4236, 40, 41sylanbrc 645 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn 1 Tfin
43 n0i 3555 . . . . . . . . . . . . . . . 16 1 Tfin Tfin
4442, 43syl 15 . . . . . . . . . . . . . . 15 Nn Nn Nn Nn 1 1 Nn Nn Tfin
45 simpl1r 1007 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn Nn
46 ne0i 3556 . . . . . . . . . . . . . . . . . 18
4738, 46syl 15 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn
48 tfinprop 4489 . . . . . . . . . . . . . . . . . 18 Nn Tfin Nn 1 Tfin
4948simpld 445 . . . . . . . . . . . . . . . . 17 Nn Tfin Nn
5037, 47, 49syl2anc 642 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn Tfin Nn
51 nndisjeq 4429 . . . . . . . . . . . . . . . 16 Nn Tfin Nn Tfin Tfin
5245, 50, 51syl2anc 642 . . . . . . . . . . . . . . 15 Nn Nn Nn Nn 1 1 Nn Nn Tfin Tfin
53 orel1 371 . . . . . . . . . . . . . . 15 Tfin Tfin Tfin Tfin
5444, 52, 53sylc 56 . . . . . . . . . . . . . 14 Nn Nn Nn Nn 1 1 Nn Nn Tfin
55 tfinltfin 4501 . . . . . . . . . . . . . . . . 17 Nn Nn <fin Tfin Tfin <fin
5655ad2antrl 708 . . . . . . . . . . . . . . . 16 Nn Nn Nn Nn 1 1 Nn Nn <fin Tfin Tfin <fin
57 opkltfing 4449 . . . . . . . . . . . . . . . . . 18 Nn Nn <fin Nn 1c
5857ad2antrl 708 . . . . . . . . . . . . . . . . 17 Nn Nn Nn Nn 1 1 Nn Nn <fin Nn 1c
59 simp2rr 1025 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c
60 simp3r 984 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
6159, 60eleqtrd 2429 . . . . . . . . . . . . . . . . . . . . . . 23 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
62 addcass 4415 . . . . . . . . . . . . . . . . . . . . . . 23 1c 1c
6361, 62syl6eleq 2443 . . . . . . . . . . . . . . . . . . . . . 22 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
64 eladdc 4398 . . . . . . . . . . . . . . . . . . . . . . 23 1c 1c
65 0nelsuc 4400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1c
66 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c 1c
67 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1c 1c
6866, 67syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c 1c
6965, 68mtoi 169 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
70 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7169, 70sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
72 n0 3559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
73 ssun2 3427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
74 sseq2 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7573, 74mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7675sseld 3272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
77 disjr 3592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78 rsp 2674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7977, 78sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8076, 79anim12ii 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8180ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8281ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
83 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8483snelpw 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8583snelpw 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8685notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8784, 86anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
88 ssun1 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
89 sseq2 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9088, 89mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91 sspwb 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9290, 91sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9392adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9493ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
95 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9695biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9796con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9897imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9998anim2i 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100 dfpss2 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
10199, 100sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102 simp2ll 1022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c Nn
103102adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
104 simp2rl 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c
105104adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
106 simprll 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
107 nnpweq 4523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Nn
108103, 105, 106, 107syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
109 simpr2l 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
110 simp3lr 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nn Nn Nn Nn 1 1
1111103ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c
112111ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
113 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
114109, 112, 113sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
115 n0i 3555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
116114, 115syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
117 simpr1 961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
118 simp12l 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c Nn
119118ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
120 nndisjeq 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Nn Nn
121117, 119, 120syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
122 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
123116, 121, 122sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
124 simp3rr 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Nn Nn Nn Nn 1 1
1251243ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c
126125ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
127 simp12r 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c Nn
128127ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
129 elunii 3896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nn Nn
130126, 128, 129syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
131 df-fin 4380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Fin Nn
132130, 131syl6eleqr 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Fin
133 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
134133pwex 4329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
135 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
136135pwex 4329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
137134, 136difex 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
138 difss 3393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
139 ssfin 4470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Fin Fin
140137, 138, 139mp3an13 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Fin Fin
141132, 140syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Fin
142 elfin 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Fin Nn
143125adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c
1441433ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
145 undif1 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
146 uncom 3408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
147145, 146eqtr3i 2375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
148 simp23 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
149148pssssd 3366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
150 ssequn2 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
151149, 150sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
152147, 151syl5eqr 2399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
153 simp22r 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
154 simp3r 984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
155 disjdif 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
156155a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
157 eladdci 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
158153, 154, 156, 157syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
159152, 158eqeltrrd 2428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
160 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
161144, 159, 160sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
162 n0i 3555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
163161, 162syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
164127adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn
1651643ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn Nn
166 simp21 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn Nn
167 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn Nn
168 nncaddccl 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn
169166, 167, 168syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn Nn
170 nndisjeq 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nn Nn
171165, 169, 170syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
172 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
173163, 171, 172sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
174 ne0i 3556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
175153, 174syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
176 df-pss 3261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
177 ssdif0 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
178 eqss 3287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
179178simplbi2 608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
180177, 179syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
181180necon3d 2554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
182181imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
183176, 182sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
184148, 183syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn
185 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 0c 0c
186185biimpcd 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 0c 0c
187 el0c 4421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 0c
188186, 187syl6ib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 0c
189188necon3ad 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 0c
190154, 184, 189sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn 0c
191 nnc0suc 4412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Nn 0c Nn 1c
192167, 191sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn 0c Nn 1c
193 orel1 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 0c 0c Nn 1c Nn 1c
194190, 192, 193sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn Nn 1c
195 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1c 1c
196 addcass 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 1c 1c
197195, 196syl6eqr 2403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1c 1c
198197reximi 2721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Nn 1c Nn 1c
199194, 198syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn Nn 1c
200 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
201 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
202200, 201addcex 4394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
203 opkltfing 4449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 <fin Nn 1c
204200, 202, 203mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 <fin Nn 1c
205175, 199, 204sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn <fin
206 opkeq2 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
207206eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 <fin <fin
208205, 207syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn <fin
209173, 208mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn <fin
2102093expa 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn <fin
211210exp32 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn <fin
212211rexlimdv 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Nn <fin
213142, 212syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn Fin <fin
214141, 213mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn <fin
215 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
216215eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 <fin <fin
217214, 216syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn <fin
218123, 217mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn <fin
2192183exp2 1169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn <fin
220219rexlimdv 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c Nn <fin
221108, 220mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c <fin
222101, 221syl5 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c <fin
22394, 222mpand 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Nn Nn Nn Nn 1 1 Nn Nn Nn 1c 1c <fin
22487, 223syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn Nn Nn Nn 1 1