poimirlem7

Description: Lemma for poimir , similar to poimirlem6 , but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem9.1	$⊢ φ \to T \in S$
	poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
	poimirlem7.3	$⊢ φ \to M \in (2^{nd} (T) + 1 + 1 \dots N)$
Assertion	poimirlem7	$⊢ φ \to (ι n \in (1 \dots N) \| F (M - 2) (n) \neq F (M - 1) (n)) = 2^{nd} (1^{st} (T)) (M)$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem9.1	$⊢ φ \to T \in S$
4		poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
5		poimirlem7.3	$⊢ φ \to M \in (2^{nd} (T) + 1 + 1 \dots N)$
6		elrabi	$⊢ T \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
7	6 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
8	3 7	syl	$⊢ φ \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
9		xp1st	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
10	8 9	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
11		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
12	10 11	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
13		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
14		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
15	13 14	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
16	12 15	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
17		f1of	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
18	16 17	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
19		elfznn	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℕ$
20	4 19	syl	$⊢ φ \to 2^{nd} (T) \in ℕ$
21	20	peano2nnd	$⊢ φ \to 2^{nd} (T) + 1 \in ℕ$
22	21	peano2nnd	$⊢ φ \to 2^{nd} (T) + 1 + 1 \in ℕ$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24	22 23	eleqtrdi	$⊢ φ \to 2^{nd} (T) + 1 + 1 \in ℤ_{\geq 1}$
25		fzss1	$⊢ 2^{nd} (T) + 1 + 1 \in ℤ_{\geq 1} \to (2^{nd} (T) + 1 + 1 \dots N) \subseteq (1 \dots N)$
26	24 25	syl	$⊢ φ \to (2^{nd} (T) + 1 + 1 \dots N) \subseteq (1 \dots N)$
27	26 5	sseldd	$⊢ φ \to M \in (1 \dots N)$
28	18 27	ffvelrnd	$⊢ φ \to 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)$
29		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
30	10 29	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
31		elmapfn	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
32	30 31	syl	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
33	32	adantr	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
34		1ex	$⊢ 1 \in V$
35		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)]$
36	34 35	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)]$
37		c0ex	$⊢ 0 \in V$
38		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)]$
39	37 38	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)]$
40	36 39	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)])$
41		dff1o3	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (1^{st} (T))}^{-1})$
42	41	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
43	16 42	syl	$⊢ φ \to Fun {2^{nd} (1^{st} (T))}^{-1}$
44		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)]$
45	43 44	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)]$
46	5	elfzelzd	$⊢ φ \to M \in ℤ$
47	46	zred	$⊢ φ \to M \in ℝ$
48	47	ltm1d	$⊢ φ \to M - 1 < M$
49		fzdisj	$⊢ M - 1 < M \to (1 \dots M - 1) \cap (M \dots N) = \emptyset$
50	48 49	syl	$⊢ φ \to (1 \dots M - 1) \cap (M \dots N) = \emptyset$
51	50	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
52		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
53	51 52	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = \emptyset$
54	45 53	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset$
55		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)])$
56	40 54 55	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)])$
57	46	zcnd	$⊢ φ \to M \in ℂ$
58		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
59	57 58	syl	$⊢ φ \to M - 1 + 1 = M$
60		1red	$⊢ φ \to 1 \in ℝ$
61	22	nnred	$⊢ φ \to 2^{nd} (T) + 1 + 1 \in ℝ$
62	21	nnred	$⊢ φ \to 2^{nd} (T) + 1 \in ℝ$
63	21	nnge1d	$⊢ φ \to 1 \leq 2^{nd} (T) + 1$
64	62	ltp1d	$⊢ φ \to 2^{nd} (T) + 1 < 2^{nd} (T) + 1 + 1$
65	60 62 61 63 64	lelttrd	$⊢ φ \to 1 < 2^{nd} (T) + 1 + 1$
66		elfzle1	$⊢ M \in (2^{nd} (T) + 1 + 1 \dots N) \to 2^{nd} (T) + 1 + 1 \leq M$
67	5 66	syl	$⊢ φ \to 2^{nd} (T) + 1 + 1 \leq M$
68	60 61 47 65 67	ltletrd	$⊢ φ \to 1 < M$
69	60 47 68	ltled	$⊢ φ \to 1 \leq M$
70		elnnz1	$⊢ M \in ℕ \leftrightarrow (M \in ℤ \land 1 \leq M)$
71	46 69 70	sylanbrc	$⊢ φ \to M \in ℕ$
72	71 23	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
73	59 72	eqeltrd	$⊢ φ \to M - 1 + 1 \in ℤ_{\geq 1}$
74		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
75	46 74	syl	$⊢ φ \to M - 1 \in ℤ$
76		uzid	$⊢ M - 1 \in ℤ \to M - 1 \in ℤ_{\geq (M - 1)}$
77		peano2uz	$⊢ M - 1 \in ℤ_{\geq (M - 1)} \to M - 1 + 1 \in ℤ_{\geq (M - 1)}$
78	75 76 77	3syl	$⊢ φ \to M - 1 + 1 \in ℤ_{\geq (M - 1)}$
79	59 78	eqeltrrd	$⊢ φ \to M \in ℤ_{\geq (M - 1)}$
80		uzss	$⊢ M \in ℤ_{\geq (M - 1)} \to ℤ_{\geq M} \subseteq ℤ_{\geq (M - 1)}$
81	79 80	syl	$⊢ φ \to ℤ_{\geq M} \subseteq ℤ_{\geq (M - 1)}$
82		elfzuz3	$⊢ M \in (2^{nd} (T) + 1 + 1 \dots N) \to N \in ℤ_{\geq M}$
83	5 82	syl	$⊢ φ \to N \in ℤ_{\geq M}$
84	81 83	sseldd	$⊢ φ \to N \in ℤ_{\geq (M - 1)}$
85		fzsplit2	$⊢ (M - 1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq (M - 1)}) \to (1 \dots N) = (1 \dots M - 1) \cup (M - 1 + 1 \dots N)$
86	73 84 85	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots M - 1) \cup (M - 1 + 1 \dots N)$
87	59	oveq1d	$⊢ φ \to (M - 1 + 1 \dots N) = (M \dots N)$
88	87	uneq2d	$⊢ φ \to (1 \dots M - 1) \cup (M - 1 + 1 \dots N) = (1 \dots M - 1) \cup (M \dots N)$
89	86 88	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots M - 1) \cup (M \dots N)$
90	89	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M \dots N)]$
91		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)]$
92	90 91	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)]$
93		f1ofo	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
94	16 93	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
95		foima	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
96	94 95	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
97	92 96	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)] = (1 \dots N)$
98	97	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (1 \dots N))$
99	56 98	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (1 \dots N)$
100	99	adantr	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (1 \dots N)$
101		ovexd	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to (1 \dots N) \in V$
102		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
103		eqidd	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) = 1^{st} (1^{st} (T)) (n)$
104		imaundi	$⊢ 2^{nd} (1^{st} (T)) [\{M\} \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\{M\}] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
105		fzpred	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
106	83 105	syl	$⊢ φ \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
107	106	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] = 2^{nd} (1^{st} (T)) [\{M\} \cup (M + 1 \dots N)]$
108		f1ofn	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
109	16 108	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
110		fnsnfv	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land M \in (1 \dots N)) \to \{2^{nd} (1^{st} (T)) (M)\} = 2^{nd} (1^{st} (T)) [\{M\}]$
111	109 27 110	syl2anc	$⊢ φ \to \{2^{nd} (1^{st} (T)) (M)\} = 2^{nd} (1^{st} (T)) [\{M\}]$
112	111	uneq1d	$⊢ φ \to \{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\{M\}] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
113	104 107 112	3eqtr4a	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] = \{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
114	113	xpeq1d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\} = (\{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \times \{0\}$
115		xpundir	$⊢ (\{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \times \{0\} = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
116	114 115	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\} = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
117	116	uneq2d	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
118		un12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
119	117 118	eqtrdi	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
120	119	fveq1d	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
121	120	ad2antrr	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
122		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
123	37 122	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
124	36 123	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
125		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
126	43 125	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
127	75	zred	$⊢ φ \to M - 1 \in ℝ$
128		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
129	47 128	syl	$⊢ φ \to M + 1 \in ℝ$
130	47	ltp1d	$⊢ φ \to M < M + 1$
131	127 47 129 48 130	lttrd	$⊢ φ \to M - 1 < M + 1$
132		fzdisj	$⊢ M - 1 < M + 1 \to (1 \dots M - 1) \cap (M + 1 \dots N) = \emptyset$
133	131 132	syl	$⊢ φ \to (1 \dots M - 1) \cap (M + 1 \dots N) = \emptyset$
134	133	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
135	134 52	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = \emptyset$
136	126 135	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset$
137		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
138	124 136 137	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
139		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
140		imadif	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{M\}]$
141	43 140	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{M\}]$
142		fzsplit	$⊢ M \in (1 \dots N) \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
143	27 142	syl	$⊢ φ \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
144	143	difeq1d	$⊢ φ \to (1 \dots N) ∖ \{M\} = ((1 \dots M) \cup (M + 1 \dots N)) ∖ \{M\}$
145		difundir	$⊢ ((1 \dots M) \cup (M + 1 \dots N)) ∖ \{M\} = ((1 \dots M) ∖ \{M\}) \cup ((M + 1 \dots N) ∖ \{M\})$
146		fzsplit2	$⊢ (M - 1 + 1 \in ℤ_{\geq 1} \land M \in ℤ_{\geq (M - 1)}) \to (1 \dots M) = (1 \dots M - 1) \cup (M - 1 + 1 \dots M)$
147	73 79 146	syl2anc	$⊢ φ \to (1 \dots M) = (1 \dots M - 1) \cup (M - 1 + 1 \dots M)$
148	59	oveq1d	$⊢ φ \to (M - 1 + 1 \dots M) = (M \dots M)$
149		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
150	46 149	syl	$⊢ φ \to (M \dots M) = \{M\}$
151	148 150	eqtrd	$⊢ φ \to (M - 1 + 1 \dots M) = \{M\}$
152	151	uneq2d	$⊢ φ \to (1 \dots M - 1) \cup (M - 1 + 1 \dots M) = (1 \dots M - 1) \cup \{M\}$
153	147 152	eqtrd	$⊢ φ \to (1 \dots M) = (1 \dots M - 1) \cup \{M\}$
154	153	difeq1d	$⊢ φ \to (1 \dots M) ∖ \{M\} = ((1 \dots M - 1) \cup \{M\}) ∖ \{M\}$
155		difun2	$⊢ ((1 \dots M - 1) \cup \{M\}) ∖ \{M\} = (1 \dots M - 1) ∖ \{M\}$
156	127 47	ltnled	$⊢ φ \to (M - 1 < M \leftrightarrow \neg M \leq M - 1)$
157	48 156	mpbid	$⊢ φ \to \neg M \leq M - 1$
158		elfzle2	$⊢ M \in (1 \dots M - 1) \to M \leq M - 1$
159	157 158	nsyl	$⊢ φ \to \neg M \in (1 \dots M - 1)$
160		difsn	$⊢ \neg M \in (1 \dots M - 1) \to (1 \dots M - 1) ∖ \{M\} = (1 \dots M - 1)$
161	159 160	syl	$⊢ φ \to (1 \dots M - 1) ∖ \{M\} = (1 \dots M - 1)$
162	155 161	eqtrid	$⊢ φ \to ((1 \dots M - 1) \cup \{M\}) ∖ \{M\} = (1 \dots M - 1)$
163	154 162	eqtrd	$⊢ φ \to (1 \dots M) ∖ \{M\} = (1 \dots M - 1)$
164	47 129	ltnled	$⊢ φ \to (M < M + 1 \leftrightarrow \neg M + 1 \leq M)$
165	130 164	mpbid	$⊢ φ \to \neg M + 1 \leq M$
166		elfzle1	$⊢ M \in (M + 1 \dots N) \to M + 1 \leq M$
167	165 166	nsyl	$⊢ φ \to \neg M \in (M + 1 \dots N)$
168		difsn	$⊢ \neg M \in (M + 1 \dots N) \to (M + 1 \dots N) ∖ \{M\} = (M + 1 \dots N)$
169	167 168	syl	$⊢ φ \to (M + 1 \dots N) ∖ \{M\} = (M + 1 \dots N)$
170	163 169	uneq12d	$⊢ φ \to ((1 \dots M) ∖ \{M\}) \cup ((M + 1 \dots N) ∖ \{M\}) = (1 \dots M - 1) \cup (M + 1 \dots N)$
171	145 170	eqtrid	$⊢ φ \to ((1 \dots M) \cup (M + 1 \dots N)) ∖ \{M\} = (1 \dots M - 1) \cup (M + 1 \dots N)$
172	144 171	eqtrd	$⊢ φ \to (1 \dots N) ∖ \{M\} = (1 \dots M - 1) \cup (M + 1 \dots N)$
173	172	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M + 1 \dots N)]$
174	111	eqcomd	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{M\}] = \{2^{nd} (1^{st} (T)) (M)\}$
175	96 174	difeq12d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{M\}] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}$
176	141 173 175	3eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M + 1 \dots N)] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}$
177	139 176	eqtr3id	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}$
178	177	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))$
179	138 178	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})$
180		eldifsn	$⊢ n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \leftrightarrow (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))$
181	180	biimpri	$⊢ (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M)) \to n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})$
182	181	ancoms	$⊢ (n \neq 2^{nd} (1^{st} (T)) (M) \land n \in (1 \dots N)) \to n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})$
183		disjdif	$⊢ \{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset$
184		fnconstg	$⊢ 0 \in V \to (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
185	37 184	ax-mp	$⊢ (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
186		fvun2	$⊢ ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (M)\} \land ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
187	185 186	mp3an1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
188	183 187	mpanr1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
189	179 182 188	syl2an	$⊢ (φ \land (n \neq 2^{nd} (1^{st} (T)) (M) \land n \in (1 \dots N))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
190	189	anassrs	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
191	121 190	eqtrd	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
192	33 100 101 101 102 103 191	ofval	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
193		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
194	34 193	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
195	194 123	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
196		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
197	43 196	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
198		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
199	130 198	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
200	199	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
201	200 52	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = \emptyset$
202	197 201	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset$
203		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
204	195 202 203	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
205	143	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)]$
206		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
207	205 206	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
208	207 96	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = (1 \dots N)$
209	208	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
210	204 209	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
211	210	adantr	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
212		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [\{M\}]$
213	153	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup \{M\}]$
214	111	uneq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\} = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [\{M\}]$
215	212 213 214	3eqtr4a	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\}$
216	215	xpeq1d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\} = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\}) \times \{1\}$
217		xpundir	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\}) \times \{1\} = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})$
218	216 217	eqtrdi	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\} = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})$
219	218	uneq1d	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
220		un23	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})$
221	220	equncomi	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
222	219 221	eqtrdi	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
223	222	fveq1d	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
224	223	ad2antrr	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
225		fnconstg	$⊢ 1 \in V \to (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
226	34 225	ax-mp	$⊢ (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
227		fvun2	$⊢ ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (M)\} \land ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
228	226 227	mp3an1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
229	183 228	mpanr1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
230	179 182 229	syl2an	$⊢ (φ \land (n \neq 2^{nd} (1^{st} (T)) (M) \land n \in (1 \dots N))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
231	230	anassrs	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
232	224 231	eqtrd	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
233	33 211 101 101 102 103 232	ofval	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
234	192 233	eqtr4d	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
235	234	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land n \neq 2^{nd} (1^{st} (T)) (M)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
236	235	anasss	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
237		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
238	237	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
239	238	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
240	239	csbeq1d	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))$
241		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
242		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
243	242	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
244	243	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
245	242	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
246	245	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
247	244 246	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
248	241 247	oveq12d	$⊢ t = T \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))$
249	248	csbeq2dv	$⊢ t = T \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
250	240 249	eqtrd	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
251	250	mpteq2dv	$⊢ t = T \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
252	251	eqeq2d	$⊢ t = T \to (F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
253	252 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
254	253	simprbi	$⊢ T \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
255	3 254	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
256		breq1	$⊢ y = M - 2 \to (y < 2^{nd} (T) \leftrightarrow M - 2 < 2^{nd} (T))$
257	256	adantl	$⊢ (φ \land y = M - 2) \to (y < 2^{nd} (T) \leftrightarrow M - 2 < 2^{nd} (T))$
258		oveq1	$⊢ y = M - 2 \to y + 1 = M - 2 + 1$
259		sub1m1	$⊢ M \in ℂ \to M - 1 - 1 = M - 2$
260	57 259	syl	$⊢ φ \to M - 1 - 1 = M - 2$
261	260	oveq1d	$⊢ φ \to (M - 1) - 1 + 1 = M - 2 + 1$
262	75	zcnd	$⊢ φ \to M - 1 \in ℂ$
263		npcan1	$⊢ M - 1 \in ℂ \to (M - 1) - 1 + 1 = M - 1$
264	262 263	syl	$⊢ φ \to (M - 1) - 1 + 1 = M - 1$
265	261 264	eqtr3d	$⊢ φ \to M - 2 + 1 = M - 1$
266	258 265	sylan9eqr	$⊢ (φ \land y = M - 2) \to y + 1 = M - 1$
267	257 266	ifbieq2d	$⊢ (φ \land y = M - 2) \to if (y < 2^{nd} (T), y, y + 1) = if (M - 2 < 2^{nd} (T), y, M - 1)$
268	20	nncnd	$⊢ φ \to 2^{nd} (T) \in ℂ$
269		add1p1	$⊢ 2^{nd} (T) \in ℂ \to 2^{nd} (T) + 1 + 1 = 2^{nd} (T) + 2$
270	268 269	syl	$⊢ φ \to 2^{nd} (T) + 1 + 1 = 2^{nd} (T) + 2$
271	270 67	eqbrtrrd	$⊢ φ \to 2^{nd} (T) + 2 \leq M$
272	20	nnred	$⊢ φ \to 2^{nd} (T) \in ℝ$
273		2re	$⊢ 2 \in ℝ$
274		leaddsub	$⊢ (2^{nd} (T) \in ℝ \land 2 \in ℝ \land M \in ℝ) \to (2^{nd} (T) + 2 \leq M \leftrightarrow 2^{nd} (T) \leq M - 2)$
275	273 274	mp3an2	$⊢ (2^{nd} (T) \in ℝ \land M \in ℝ) \to (2^{nd} (T) + 2 \leq M \leftrightarrow 2^{nd} (T) \leq M - 2)$
276	272 47 275	syl2anc	$⊢ φ \to (2^{nd} (T) + 2 \leq M \leftrightarrow 2^{nd} (T) \leq M - 2)$
277	60 47	posdifd	$⊢ φ \to (1 < M \leftrightarrow 0 < M - 1)$
278	68 277	mpbid	$⊢ φ \to 0 < M - 1$
279		elnnz	$⊢ M - 1 \in ℕ \leftrightarrow (M - 1 \in ℤ \land 0 < M - 1)$
280	75 278 279	sylanbrc	$⊢ φ \to M - 1 \in ℕ$
281		nnm1nn0	$⊢ M - 1 \in ℕ \to M - 1 - 1 \in ℕ_{0}$
282	280 281	syl	$⊢ φ \to M - 1 - 1 \in ℕ_{0}$
283	260 282	eqeltrrd	$⊢ φ \to M - 2 \in ℕ_{0}$
284	283	nn0red	$⊢ φ \to M - 2 \in ℝ$
285	272 284	lenltd	$⊢ φ \to (2^{nd} (T) \leq M - 2 \leftrightarrow \neg M - 2 < 2^{nd} (T))$
286	276 285	bitrd	$⊢ φ \to (2^{nd} (T) + 2 \leq M \leftrightarrow \neg M - 2 < 2^{nd} (T))$
287	271 286	mpbid	$⊢ φ \to \neg M - 2 < 2^{nd} (T)$
288	287	iffalsed	$⊢ φ \to if (M - 2 < 2^{nd} (T), y, M - 1) = M - 1$
289	288	adantr	$⊢ (φ \land y = M - 2) \to if (M - 2 < 2^{nd} (T), y, M - 1) = M - 1$
290	267 289	eqtrd	$⊢ (φ \land y = M - 2) \to if (y < 2^{nd} (T), y, y + 1) = M - 1$
291	290	csbeq1d	$⊢ (φ \land y = M - 2) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ (M - 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
292		oveq2	$⊢ j = M - 1 \to (1 \dots j) = (1 \dots M - 1)$
293	292	imaeq2d	$⊢ j = M - 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)]$
294	293	xpeq1d	$⊢ j = M - 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}$
295	294	adantl	$⊢ (φ \land j = M - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}$
296		oveq1	$⊢ j = M - 1 \to j + 1 = M - 1 + 1$
297	296 59	sylan9eqr	$⊢ (φ \land j = M - 1) \to j + 1 = M$
298	297	oveq1d	$⊢ (φ \land j = M - 1) \to (j + 1 \dots N) = (M \dots N)$
299	298	imaeq2d	$⊢ (φ \land j = M - 1) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(M \dots N)]$
300	299	xpeq1d	$⊢ (φ \land j = M - 1) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}$
301	295 300	uneq12d	$⊢ (φ \land j = M - 1) \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})$
302	301	oveq2d	$⊢ (φ \land j = M - 1) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
303	75 302	csbied	$⊢ φ \to ⦋ (M - 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
304	303	adantr	$⊢ (φ \land y = M - 2) \to ⦋ (M - 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
305	291 304	eqtrd	$⊢ (φ \land y = M - 2) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
306		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
307	1 306	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
308	1	nnred	$⊢ φ \to N \in ℝ$
309	47	lem1d	$⊢ φ \to M - 1 \leq M$
310		elfzle2	$⊢ M \in (2^{nd} (T) + 1 + 1 \dots N) \to M \leq N$
311	5 310	syl	$⊢ φ \to M \leq N$
312	127 47 308 309 311	letrd	$⊢ φ \to M - 1 \leq N$
313	127 308 60 312	lesub1dd	$⊢ φ \to M - 1 - 1 \leq N - 1$
314	260 313	eqbrtrrd	$⊢ φ \to M - 2 \leq N - 1$
315		elfz2nn0	$⊢ M - 2 \in (0 \dots N - 1) \leftrightarrow (M - 2 \in ℕ_{0} \land N - 1 \in ℕ_{0} \land M - 2 \leq N - 1)$
316	283 307 314 315	syl3anbrc	$⊢ φ \to M - 2 \in (0 \dots N - 1)$
317		ovexd	$⊢ φ \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) \in V$
318	255 305 316 317	fvmptd	$⊢ φ \to F (M - 2) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
319	318	fveq1d	$⊢ φ \to F (M - 2) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n)$
320	319	adantr	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to F (M - 2) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n)$
321		breq1	$⊢ y = M - 1 \to (y < 2^{nd} (T) \leftrightarrow M - 1 < 2^{nd} (T))$
322	321	adantl	$⊢ (φ \land y = M - 1) \to (y < 2^{nd} (T) \leftrightarrow M - 1 < 2^{nd} (T))$
323		oveq1	$⊢ y = M - 1 \to y + 1 = M - 1 + 1$
324	323 59	sylan9eqr	$⊢ (φ \land y = M - 1) \to y + 1 = M$
325	322 324	ifbieq2d	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (T), y, y + 1) = if (M - 1 < 2^{nd} (T), y, M)$
326	62	lep1d	$⊢ φ \to 2^{nd} (T) + 1 \leq 2^{nd} (T) + 1 + 1$
327	62 61 47 326 67	letrd	$⊢ φ \to 2^{nd} (T) + 1 \leq M$
328		1re	$⊢ 1 \in ℝ$
329		leaddsub	$⊢ (2^{nd} (T) \in ℝ \land 1 \in ℝ \land M \in ℝ) \to (2^{nd} (T) + 1 \leq M \leftrightarrow 2^{nd} (T) \leq M - 1)$
330	328 329	mp3an2	$⊢ (2^{nd} (T) \in ℝ \land M \in ℝ) \to (2^{nd} (T) + 1 \leq M \leftrightarrow 2^{nd} (T) \leq M - 1)$
331	272 47 330	syl2anc	$⊢ φ \to (2^{nd} (T) + 1 \leq M \leftrightarrow 2^{nd} (T) \leq M - 1)$
332	272 127	lenltd	$⊢ φ \to (2^{nd} (T) \leq M - 1 \leftrightarrow \neg M - 1 < 2^{nd} (T))$
333	331 332	bitrd	$⊢ φ \to (2^{nd} (T) + 1 \leq M \leftrightarrow \neg M - 1 < 2^{nd} (T))$
334	327 333	mpbid	$⊢ φ \to \neg M - 1 < 2^{nd} (T)$
335	334	iffalsed	$⊢ φ \to if (M - 1 < 2^{nd} (T), y, M) = M$
336	335	adantr	$⊢ (φ \land y = M - 1) \to if (M - 1 < 2^{nd} (T), y, M) = M$
337	325 336	eqtrd	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (T), y, y + 1) = M$
338	337	csbeq1d	$⊢ (φ \land y = M - 1) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ M / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
339		oveq2	$⊢ j = M \to (1 \dots j) = (1 \dots M)$
340	339	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots M)]$
341	340	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}$
342		oveq1	$⊢ j = M \to j + 1 = M + 1$
343	342	oveq1d	$⊢ j = M \to (j + 1 \dots N) = (M + 1 \dots N)$
344	343	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
345	344	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}$
346	341 345	uneq12d	$⊢ j = M \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
347	346	oveq2d	$⊢ j = M \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
348	347	adantl	$⊢ (φ \land j = M) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
349	5 348	csbied	$⊢ φ \to ⦋ M / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
350	349	adantr	$⊢ (φ \land y = M - 1) \to ⦋ M / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
351	338 350	eqtrd	$⊢ (φ \land y = M - 1) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
352	280	nnnn0d	$⊢ φ \to M - 1 \in ℕ_{0}$
353	47 308 60 311	lesub1dd	$⊢ φ \to M - 1 \leq N - 1$
354		elfz2nn0	$⊢ M - 1 \in (0 \dots N - 1) \leftrightarrow (M - 1 \in ℕ_{0} \land N - 1 \in ℕ_{0} \land M - 1 \leq N - 1)$
355	352 307 353 354	syl3anbrc	$⊢ φ \to M - 1 \in (0 \dots N - 1)$
356		ovexd	$⊢ φ \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) \in V$
357	255 351 355 356	fvmptd	$⊢ φ \to F (M - 1) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
358	357	fveq1d	$⊢ φ \to F (M - 1) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
359	358	adantr	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to F (M - 1) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
360	236 320 359	3eqtr4d	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to F (M - 2) (n) = F (M - 1) (n)$
361	360	expr	$⊢ (φ \land n \in (1 \dots N)) \to (n \neq 2^{nd} (1^{st} (T)) (M) \to F (M - 2) (n) = F (M - 1) (n))$
362	361	necon1d	$⊢ (φ \land n \in (1 \dots N)) \to (F (M - 2) (n) \neq F (M - 1) (n) \to n = 2^{nd} (1^{st} (T)) (M))$
363		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
364	30 363	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
365	364 28	ffvelrnd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in (0 ..^K)$
366		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℕ_{0}$
367	365 366	syl	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℕ_{0}$
368	367	nn0red	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℝ$
369	368	ltp1d	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) < 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
370	368 369	ltned	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \neq 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
371	318	fveq1d	$⊢ φ \to F (M - 2) (2^{nd} (1^{st} (T)) (M)) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M))$
372		ovexd	$⊢ φ \to (1 \dots N) \in V$
373		eqidd	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M))$
374		fzss1	$⊢ M \in ℤ_{\geq 1} \to (M \dots N) \subseteq (1 \dots N)$
375	72 374	syl	$⊢ φ \to (M \dots N) \subseteq (1 \dots N)$
376		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
377	83 376	syl	$⊢ φ \to M \in (M \dots N)$
378		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (M \dots N) \subseteq (1 \dots N) \land M \in (M \dots N)) \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)]$
379	109 375 377 378	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)]$
380		fvun2	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M))$
381	36 39 380	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M))$
382	54 379 381	syl2anc	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M))$
383	37	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)] \to (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M)) = 0$
384	379 383	syl	$⊢ φ \to (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M)) = 0$
385	382 384	eqtrd	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 0$
386	385	adantr	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 0$
387	32 99 372 372 102 373 386	ofval	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 0$
388	28 387	mpdan	$⊢ φ \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 0$
389	367	nn0cnd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℂ$
390	389	addid1d	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 0 = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M))$
391	371 388 390	3eqtrd	$⊢ φ \to F (M - 2) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M))$
392	357	fveq1d	$⊢ φ \to F (M - 1) (2^{nd} (1^{st} (T)) (M)) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M))$
393		fzss2	$⊢ N \in ℤ_{\geq M} \to (1 \dots M) \subseteq (1 \dots N)$
394	83 393	syl	$⊢ φ \to (1 \dots M) \subseteq (1 \dots N)$
395		elfz1end	$⊢ M \in ℕ \leftrightarrow M \in (1 \dots M)$
396	71 395	sylib	$⊢ φ \to M \in (1 \dots M)$
397		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (1 \dots M) \subseteq (1 \dots N) \land M \in (1 \dots M)) \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)]$
398	109 394 396 397	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)]$
399		fvun1	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M))$
400	194 123 399	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M))$
401	202 398 400	syl2anc	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M))$
402	34	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M)) = 1$
403	398 402	syl	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M)) = 1$
404	401 403	eqtrd	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 1$
405	404	adantr	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 1$
406	32 210 372 372 102 373 405	ofval	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
407	28 406	mpdan	$⊢ φ \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
408	392 407	eqtrd	$⊢ φ \to F (M - 1) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
409	370 391 408	3netr4d	$⊢ φ \to F (M - 2) (2^{nd} (1^{st} (T)) (M)) \neq F (M - 1) (2^{nd} (1^{st} (T)) (M))$
410		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (M) \to F (M - 2) (n) = F (M - 2) (2^{nd} (1^{st} (T)) (M))$
411		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (M) \to F (M - 1) (n) = F (M - 1) (2^{nd} (1^{st} (T)) (M))$
412	410 411	neeq12d	$⊢ n = 2^{nd} (1^{st} (T)) (M) \to (F (M - 2) (n) \neq F (M - 1) (n) \leftrightarrow F (M - 2) (2^{nd} (1^{st} (T)) (M)) \neq F (M - 1) (2^{nd} (1^{st} (T)) (M)))$
413	409 412	syl5ibrcom	$⊢ φ \to (n = 2^{nd} (1^{st} (T)) (M) \to F (M - 2) (n) \neq F (M - 1) (n))$
414	413	adantr	$⊢ (φ \land n \in (1 \dots N)) \to (n = 2^{nd} (1^{st} (T)) (M) \to F (M - 2) (n) \neq F (M - 1) (n))$
415	362 414	impbid	$⊢ (φ \land n \in (1 \dots N)) \to (F (M - 2) (n) \neq F (M - 1) (n) \leftrightarrow n = 2^{nd} (1^{st} (T)) (M))$
416	28 415	riota5	$⊢ φ \to (ι n \in (1 \dots N) \| F (M - 2) (n) \neq F (M - 1) (n)) = 2^{nd} (1^{st} (T)) (M)$

Metamath Proof Explorer

Theorem poimirlem7

Proof