Metamath Proof Explorer


Theorem subfacp1lem1

Description: Lemma for subfacp1 . The set K together with { 1 , M } partitions the set 1 ... ( N + 1 ) . (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Hypotheses derang.d D = x Fin f | f : x 1-1 onto x y x f y y
subfac.n S = n 0 D 1 n
subfacp1lem.a A = f | f : 1 N + 1 1-1 onto 1 N + 1 y 1 N + 1 f y y
subfacp1lem1.n φ N
subfacp1lem1.m φ M 2 N + 1
subfacp1lem1.x M V
subfacp1lem1.k K = 2 N + 1 M
Assertion subfacp1lem1 φ K 1 M = K 1 M = 1 N + 1 K = N 1

Proof

Step Hyp Ref Expression
1 derang.d D = x Fin f | f : x 1-1 onto x y x f y y
2 subfac.n S = n 0 D 1 n
3 subfacp1lem.a A = f | f : 1 N + 1 1-1 onto 1 N + 1 y 1 N + 1 f y y
4 subfacp1lem1.n φ N
5 subfacp1lem1.m φ M 2 N + 1
6 subfacp1lem1.x M V
7 subfacp1lem1.k K = 2 N + 1 M
8 disj K 1 M = x K ¬ x 1 M
9 eldifi x 2 N + 1 M x 2 N + 1
10 elfzle1 x 2 N + 1 2 x
11 1lt2 1 < 2
12 1re 1
13 2re 2
14 12 13 ltnlei 1 < 2 ¬ 2 1
15 11 14 mpbi ¬ 2 1
16 breq2 x = 1 2 x 2 1
17 15 16 mtbiri x = 1 ¬ 2 x
18 17 necon2ai 2 x x 1
19 9 10 18 3syl x 2 N + 1 M x 1
20 eldifsni x 2 N + 1 M x M
21 19 20 jca x 2 N + 1 M x 1 x M
22 21 7 eleq2s x K x 1 x M
23 neanior x 1 x M ¬ x = 1 x = M
24 22 23 sylib x K ¬ x = 1 x = M
25 vex x V
26 25 elpr x 1 M x = 1 x = M
27 24 26 sylnibr x K ¬ x 1 M
28 8 27 mprgbir K 1 M =
29 28 a1i φ K 1 M =
30 uncom 1 K M = K M 1
31 1z 1
32 fzsn 1 1 1 = 1
33 31 32 ax-mp 1 1 = 1
34 7 uneq1i K M = 2 N + 1 M M
35 undif1 2 N + 1 M M = 2 N + 1 M
36 34 35 eqtr2i 2 N + 1 M = K M
37 33 36 uneq12i 1 1 2 N + 1 M = 1 K M
38 df-pr 1 M = 1 M
39 38 equncomi 1 M = M 1
40 39 uneq2i K 1 M = K M 1
41 unass K M 1 = K M 1
42 40 41 eqtr4i K 1 M = K M 1
43 30 37 42 3eqtr4i 1 1 2 N + 1 M = K 1 M
44 5 snssd φ M 2 N + 1
45 ssequn2 M 2 N + 1 2 N + 1 M = 2 N + 1
46 44 45 sylib φ 2 N + 1 M = 2 N + 1
47 df-2 2 = 1 + 1
48 47 oveq1i 2 N + 1 = 1 + 1 N + 1
49 46 48 syl6eq φ 2 N + 1 M = 1 + 1 N + 1
50 49 uneq2d φ 1 1 2 N + 1 M = 1 1 1 + 1 N + 1
51 4 peano2nnd φ N + 1
52 nnuz = 1
53 51 52 eleqtrdi φ N + 1 1
54 eluzfz1 N + 1 1 1 1 N + 1
55 fzsplit 1 1 N + 1 1 N + 1 = 1 1 1 + 1 N + 1
56 53 54 55 3syl φ 1 N + 1 = 1 1 1 + 1 N + 1
57 50 56 eqtr4d φ 1 1 2 N + 1 M = 1 N + 1
58 43 57 syl5eqr φ K 1 M = 1 N + 1
59 47 oveq2i N + 1 - 2 = N + 1 - 1 + 1
60 fzfi 2 N + 1 Fin
61 diffi 2 N + 1 Fin 2 N + 1 M Fin
62 60 61 ax-mp 2 N + 1 M Fin
63 7 62 eqeltri K Fin
64 prfi 1 M Fin
65 hashun K Fin 1 M Fin K 1 M = K 1 M = K + 1 M
66 63 64 28 65 mp3an K 1 M = K + 1 M
67 58 fveq2d φ K 1 M = 1 N + 1
68 neeq1 x = M x 1 M 1
69 10 18 syl x 2 N + 1 x 1
70 68 69 vtoclga M 2 N + 1 M 1
71 5 70 syl φ M 1
72 71 necomd φ 1 M
73 1ex 1 V
74 hashprg 1 V M V 1 M 1 M = 2
75 73 6 74 mp2an 1 M 1 M = 2
76 72 75 sylib φ 1 M = 2
77 76 oveq2d φ K + 1 M = K + 2
78 66 67 77 3eqtr3a φ 1 N + 1 = K + 2
79 51 nnnn0d φ N + 1 0
80 hashfz1 N + 1 0 1 N + 1 = N + 1
81 79 80 syl φ 1 N + 1 = N + 1
82 78 81 eqtr3d φ K + 2 = N + 1
83 51 nncnd φ N + 1
84 2cnd φ 2
85 hashcl K Fin K 0
86 63 85 ax-mp K 0
87 86 nn0cni K
88 87 a1i φ K
89 83 84 88 subadd2d φ N + 1 - 2 = K K + 2 = N + 1
90 82 89 mpbird φ N + 1 - 2 = K
91 4 nncnd φ N
92 1cnd φ 1
93 91 92 92 pnpcan2d φ N + 1 - 1 + 1 = N 1
94 59 90 93 3eqtr3a φ K = N 1
95 29 58 94 3jca φ K 1 M = K 1 M = 1 N + 1 K = N 1