seqf1olem1

	Ref	Expression
Hypotheses	seqf1o.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqf1o.2	$⊢ (φ \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
	seqf1o.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	seqf1o.4	$⊢ φ \to N \in ℤ_{\geq M}$
	seqf1o.5	$⊢ φ \to C \subseteq S$
	seqf1olem.5	$⊢ φ \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
	seqf1olem.6	$⊢ φ \to G : (M \dots N + 1) ⟶ C$
	seqf1olem.7	$⊢ J = (k \in (M \dots N) ⟼ F (if (k < K, k, k + 1)))$
	seqf1olem.8	$⊢ K = F^{-1} (N + 1)$
Assertion	seqf1olem1	$⊢ φ \to J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$

Proof

Step	Hyp	Ref	Expression
1		seqf1o.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqf1o.2	$⊢ (φ \land (x \in C \land y \in C)) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
3		seqf1o.3	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
4		seqf1o.4	$⊢ φ \to N \in ℤ_{\geq M}$
5		seqf1o.5	$⊢ φ \to C \subseteq S$
6		seqf1olem.5	$⊢ φ \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
7		seqf1olem.6	$⊢ φ \to G : (M \dots N + 1) ⟶ C$
8		seqf1olem.7	$⊢ J = (k \in (M \dots N) ⟼ F (if (k < K, k, k + 1)))$
9		seqf1olem.8	$⊢ K = F^{-1} (N + 1)$
10		fvexd	$⊢ (φ \land k \in (M \dots N)) \to F (if (k < K, k, k + 1)) \in V$
11		fvex	$⊢ F^{-1} (x) \in V$
12		ovex	$⊢ F^{-1} (x) - 1 \in V$
13	11 12	ifex	$⊢ if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \in V$
14	13	a1i	$⊢ (φ \land x \in (M \dots N)) \to if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \in V$
15		iftrue	$⊢ k < K \to if (k < K, k, k + 1) = k$
16	15	fveq2d	$⊢ k < K \to F (if (k < K, k, k + 1)) = F (k)$
17	16	eqeq2d	$⊢ k < K \to (x = F (if (k < K, k, k + 1)) \leftrightarrow x = F (k))$
18	17	adantl	$⊢ ((φ \land k \in (M \dots N)) \land k < K) \to (x = F (if (k < K, k, k + 1)) \leftrightarrow x = F (k))$
19		simprr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to x = F (k)$
20		elfzelz	$⊢ k \in (M \dots N) \to k \in ℤ$
21	20	zred	$⊢ k \in (M \dots N) \to k \in ℝ$
22	21	ad2antlr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to k \in ℝ$
23		simprl	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to k < K$
24	22 23	gtned	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to K \neq k$
25		f1of	$⊢ F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
26	6 25	syl	$⊢ φ \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
27	26	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
28		fzssp1	$⊢ (M \dots N) \subseteq (M \dots N + 1)$
29		simplr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to k \in (M \dots N)$
30	28 29	sselid	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to k \in (M \dots N + 1)$
31	27 30	ffvelcdmd	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F (k) \in (M \dots N + 1)$
32		elfzp1	$⊢ N \in ℤ_{\geq M} \to (F (k) \in (M \dots N + 1) \leftrightarrow (F (k) \in (M \dots N) \lor F (k) = N + 1))$
33	4 32	syl	$⊢ φ \to (F (k) \in (M \dots N + 1) \leftrightarrow (F (k) \in (M \dots N) \lor F (k) = N + 1))$
34	33	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (F (k) \in (M \dots N + 1) \leftrightarrow (F (k) \in (M \dots N) \lor F (k) = N + 1))$
35	31 34	mpbid	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (F (k) \in (M \dots N) \lor F (k) = N + 1)$
36	35	ord	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (\neg F (k) \in (M \dots N) \to F (k) = N + 1)$
37	6	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
38		f1ocnvfv	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land k \in (M \dots N + 1)) \to (F (k) = N + 1 \to F^{-1} (N + 1) = k)$
39	37 30 38	syl2anc	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (F (k) = N + 1 \to F^{-1} (N + 1) = k)$
40	9	eqeq1i	$⊢ K = k \leftrightarrow F^{-1} (N + 1) = k$
41	39 40	syl6ibr	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (F (k) = N + 1 \to K = k)$
42	36 41	syld	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (\neg F (k) \in (M \dots N) \to K = k)$
43	42	necon1ad	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (K \neq k \to F (k) \in (M \dots N))$
44	24 43	mpd	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F (k) \in (M \dots N)$
45	19 44	eqeltrd	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to x \in (M \dots N)$
46	19	eqcomd	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F (k) = x$
47		f1ocnvfv	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land k \in (M \dots N + 1)) \to (F (k) = x \to F^{-1} (x) = k)$
48	37 30 47	syl2anc	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (F (k) = x \to F^{-1} (x) = k)$
49	46 48	mpd	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F^{-1} (x) = k$
50	49 23	eqbrtrd	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to F^{-1} (x) < K$
51		iftrue	$⊢ F^{-1} (x) < K \to if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) = F^{-1} (x)$
52	50 51	syl	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) = F^{-1} (x)$
53	52 49	eqtr2d	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)$
54	45 53	jca	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1))$
55	54	expr	$⊢ ((φ \land k \in (M \dots N)) \land k < K) \to (x = F (k) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
56	18 55	sylbid	$⊢ ((φ \land k \in (M \dots N)) \land k < K) \to (x = F (if (k < K, k, k + 1)) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
57		iffalse	$⊢ \neg k < K \to if (k < K, k, k + 1) = k + 1$
58	57	fveq2d	$⊢ \neg k < K \to F (if (k < K, k, k + 1)) = F (k + 1)$
59	58	eqeq2d	$⊢ \neg k < K \to (x = F (if (k < K, k, k + 1)) \leftrightarrow x = F (k + 1))$
60	59	adantl	$⊢ ((φ \land k \in (M \dots N)) \land \neg k < K) \to (x = F (if (k < K, k, k + 1)) \leftrightarrow x = F (k + 1))$
61		simprr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to x = F (k + 1)$
62		f1ocnv	$⊢ F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \to F^{-1} : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
63	6 62	syl	$⊢ φ \to F^{-1} : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
64		f1of1	$⊢ F^{-1} : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \to F^{-1} : (M \dots N + 1) \underset{1-1}{⟶} (M \dots N + 1)$
65	63 64	syl	$⊢ φ \to F^{-1} : (M \dots N + 1) \underset{1-1}{⟶} (M \dots N + 1)$
66		f1f	$⊢ F^{-1} : (M \dots N + 1) \underset{1-1}{⟶} (M \dots N + 1) \to F^{-1} : (M \dots N + 1) ⟶ (M \dots N + 1)$
67	65 66	syl	$⊢ φ \to F^{-1} : (M \dots N + 1) ⟶ (M \dots N + 1)$
68		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
69	4 68	syl	$⊢ φ \to N + 1 \in ℤ_{\geq M}$
70		eluzfz2	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 \in (M \dots N + 1)$
71	69 70	syl	$⊢ φ \to N + 1 \in (M \dots N + 1)$
72	67 71	ffvelcdmd	$⊢ φ \to F^{-1} (N + 1) \in (M \dots N + 1)$
73	9 72	eqeltrid	$⊢ φ \to K \in (M \dots N + 1)$
74	73	elfzelzd	$⊢ φ \to K \in ℤ$
75	74	zred	$⊢ φ \to K \in ℝ$
76	75	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K \in ℝ$
77	21	ad2antlr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k \in ℝ$
78		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
79	77 78	syl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k + 1 \in ℝ$
80		simprl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to \neg k < K$
81	76 77 80	nltled	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K \leq k$
82	77	ltp1d	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k < k + 1$
83	76 77 79 81 82	lelttrd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K < k + 1$
84	76 83	ltned	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K \neq k + 1$
85	26	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F : (M \dots N + 1) ⟶ (M \dots N + 1)$
86		fzp1elp1	$⊢ k \in (M \dots N) \to k + 1 \in (M \dots N + 1)$
87	86	ad2antlr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k + 1 \in (M \dots N + 1)$
88	85 87	ffvelcdmd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F (k + 1) \in (M \dots N + 1)$
89		elfzp1	$⊢ N \in ℤ_{\geq M} \to (F (k + 1) \in (M \dots N + 1) \leftrightarrow (F (k + 1) \in (M \dots N) \lor F (k + 1) = N + 1))$
90	4 89	syl	$⊢ φ \to (F (k + 1) \in (M \dots N + 1) \leftrightarrow (F (k + 1) \in (M \dots N) \lor F (k + 1) = N + 1))$
91	90	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F (k + 1) \in (M \dots N + 1) \leftrightarrow (F (k + 1) \in (M \dots N) \lor F (k + 1) = N + 1))$
92	88 91	mpbid	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F (k + 1) \in (M \dots N) \lor F (k + 1) = N + 1)$
93	92	ord	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (\neg F (k + 1) \in (M \dots N) \to F (k + 1) = N + 1)$
94	6	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
95		f1ocnvfv	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land k + 1 \in (M \dots N + 1)) \to (F (k + 1) = N + 1 \to F^{-1} (N + 1) = k + 1)$
96	94 87 95	syl2anc	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F (k + 1) = N + 1 \to F^{-1} (N + 1) = k + 1)$
97	9	eqeq1i	$⊢ K = k + 1 \leftrightarrow F^{-1} (N + 1) = k + 1$
98	96 97	syl6ibr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F (k + 1) = N + 1 \to K = k + 1)$
99	93 98	syld	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (\neg F (k + 1) \in (M \dots N) \to K = k + 1)$
100	99	necon1ad	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (K \neq k + 1 \to F (k + 1) \in (M \dots N))$
101	84 100	mpd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F (k + 1) \in (M \dots N)$
102	61 101	eqeltrd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to x \in (M \dots N)$
103	61	eqcomd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F (k + 1) = x$
104		f1ocnvfv	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land k + 1 \in (M \dots N + 1)) \to (F (k + 1) = x \to F^{-1} (x) = k + 1)$
105	94 87 104	syl2anc	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F (k + 1) = x \to F^{-1} (x) = k + 1)$
106	103 105	mpd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F^{-1} (x) = k + 1$
107	106	breq1d	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F^{-1} (x) < K \leftrightarrow k + 1 < K)$
108		lttr	$⊢ (k \in ℝ \land k + 1 \in ℝ \land K \in ℝ) \to ((k < k + 1 \land k + 1 < K) \to k < K)$
109	77 79 76 108	syl3anc	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to ((k < k + 1 \land k + 1 < K) \to k < K)$
110	82 109	mpand	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (k + 1 < K \to k < K)$
111	107 110	sylbid	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F^{-1} (x) < K \to k < K)$
112	80 111	mtod	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to \neg F^{-1} (x) < K$
113		iffalse	$⊢ \neg F^{-1} (x) < K \to if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) = F^{-1} (x) - 1$
114	112 113	syl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) = F^{-1} (x) - 1$
115	106	oveq1d	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F^{-1} (x) - 1 = k + 1 - 1$
116	77	recnd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k \in ℂ$
117		ax-1cn	$⊢ 1 \in ℂ$
118		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
119	116 117 118	sylancl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k + 1 - 1 = k$
120	114 115 119	3eqtrrd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)$
121	102 120	jca	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1))$
122	121	expr	$⊢ ((φ \land k \in (M \dots N)) \land \neg k < K) \to (x = F (k + 1) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
123	60 122	sylbid	$⊢ ((φ \land k \in (M \dots N)) \land \neg k < K) \to (x = F (if (k < K, k, k + 1)) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
124	56 123	pm2.61dan	$⊢ (φ \land k \in (M \dots N)) \to (x = F (if (k < K, k, k + 1)) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
125	124	expimpd	$⊢ φ \to ((k \in (M \dots N) \land x = F (if (k < K, k, k + 1))) \to (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
126	51	eqeq2d	$⊢ F^{-1} (x) < K \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \leftrightarrow k = F^{-1} (x))$
127	126	adantl	$⊢ ((φ \land x \in (M \dots N)) \land F^{-1} (x) < K) \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \leftrightarrow k = F^{-1} (x))$
128		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
129	4 128	syl	$⊢ φ \to M \in ℤ$
130	129	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to M \in ℤ$
131		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
132	4 131	syl	$⊢ φ \to N \in ℤ$
133	132	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to N \in ℤ$
134		simprr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k = F^{-1} (x)$
135	67	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F^{-1} : (M \dots N + 1) ⟶ (M \dots N + 1)$
136		simplr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to x \in (M \dots N)$
137	28 136	sselid	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to x \in (M \dots N + 1)$
138	135 137	ffvelcdmd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F^{-1} (x) \in (M \dots N + 1)$
139	134 138	eqeltrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in (M \dots N + 1)$
140	139	elfzelzd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in ℤ$
141		elfzle1	$⊢ k \in (M \dots N + 1) \to M \leq k$
142	139 141	syl	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to M \leq k$
143	140	zred	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in ℝ$
144	75	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to K \in ℝ$
145	132	peano2zd	$⊢ φ \to N + 1 \in ℤ$
146	145	zred	$⊢ φ \to N + 1 \in ℝ$
147	146	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to N + 1 \in ℝ$
148		simprl	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F^{-1} (x) < K$
149	134 148	eqbrtrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k < K$
150		elfzle2	$⊢ K \in (M \dots N + 1) \to K \leq N + 1$
151	73 150	syl	$⊢ φ \to K \leq N + 1$
152	151	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to K \leq N + 1$
153	143 144 147 149 152	ltletrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k < N + 1$
154		zleltp1	$⊢ (k \in ℤ \land N \in ℤ) \to (k \leq N \leftrightarrow k < N + 1)$
155	140 133 154	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to (k \leq N \leftrightarrow k < N + 1)$
156	153 155	mpbird	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \leq N$
157	130 133 140 142 156	elfzd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in (M \dots N)$
158	149 16	syl	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F (if (k < K, k, k + 1)) = F (k)$
159	134	fveq2d	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F (k) = F (F^{-1} (x))$
160	6	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
161		f1ocnvfv2	$⊢ (F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1) \land x \in (M \dots N + 1)) \to F (F^{-1} (x)) = x$
162	160 137 161	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F (F^{-1} (x)) = x$
163	158 159 162	3eqtrrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to x = F (if (k < K, k, k + 1))$
164	157 163	jca	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1)))$
165	164	expr	$⊢ ((φ \land x \in (M \dots N)) \land F^{-1} (x) < K) \to (k = F^{-1} (x) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1))))$
166	127 165	sylbid	$⊢ ((φ \land x \in (M \dots N)) \land F^{-1} (x) < K) \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1))))$
167	113	eqeq2d	$⊢ \neg F^{-1} (x) < K \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \leftrightarrow k = F^{-1} (x) - 1)$
168	167	adantl	$⊢ ((φ \land x \in (M \dots N)) \land \neg F^{-1} (x) < K) \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \leftrightarrow k = F^{-1} (x) - 1)$
169	129	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \in ℤ$
170	132	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N \in ℤ$
171		simprr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k = F^{-1} (x) - 1$
172	67	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} : (M \dots N + 1) ⟶ (M \dots N + 1)$
173		simplr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to x \in (M \dots N)$
174	28 173	sselid	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to x \in (M \dots N + 1)$
175	172 174	ffvelcdmd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in (M \dots N + 1)$
176	175	elfzelzd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in ℤ$
177		peano2zm	$⊢ F^{-1} (x) \in ℤ \to F^{-1} (x) - 1 \in ℤ$
178	176 177	syl	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) - 1 \in ℤ$
179	171 178	eqeltrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \in ℤ$
180	129	zred	$⊢ φ \to M \in ℝ$
181	180	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \in ℝ$
182	75	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \in ℝ$
183	179	zred	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \in ℝ$
184		elfzle1	$⊢ K \in (M \dots N + 1) \to M \leq K$
185	73 184	syl	$⊢ φ \to M \leq K$
186	185	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \leq K$
187	176	zred	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in ℝ$
188		simprl	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to \neg F^{-1} (x) < K$
189	182 187 188	nltled	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \leq F^{-1} (x)$
190		elfzelz	$⊢ x \in (M \dots N) \to x \in ℤ$
191	190	adantl	$⊢ (φ \land x \in (M \dots N)) \to x \in ℤ$
192	191	zred	$⊢ (φ \land x \in (M \dots N)) \to x \in ℝ$
193	132	zred	$⊢ φ \to N \in ℝ$
194	193	adantr	$⊢ (φ \land x \in (M \dots N)) \to N \in ℝ$
195	146	adantr	$⊢ (φ \land x \in (M \dots N)) \to N + 1 \in ℝ$
196		elfzle2	$⊢ x \in (M \dots N) \to x \leq N$
197	196	adantl	$⊢ (φ \land x \in (M \dots N)) \to x \leq N$
198	194	ltp1d	$⊢ (φ \land x \in (M \dots N)) \to N < N + 1$
199	192 194 195 197 198	lelttrd	$⊢ (φ \land x \in (M \dots N)) \to x < N + 1$
200	192 199	gtned	$⊢ (φ \land x \in (M \dots N)) \to N + 1 \neq x$
201	200	adantr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N + 1 \neq x$
202	65	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} : (M \dots N + 1) \underset{1-1}{⟶} (M \dots N + 1)$
203	71	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N + 1 \in (M \dots N + 1)$
204		f1fveq	$⊢ (F^{-1} : (M \dots N + 1) \underset{1-1}{⟶} (M \dots N + 1) \land (N + 1 \in (M \dots N + 1) \land x \in (M \dots N + 1))) \to (F^{-1} (N + 1) = F^{-1} (x) \leftrightarrow N + 1 = x)$
205	202 203 174 204	syl12anc	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to (F^{-1} (N + 1) = F^{-1} (x) \leftrightarrow N + 1 = x)$
206	205	necon3bid	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to (F^{-1} (N + 1) \neq F^{-1} (x) \leftrightarrow N + 1 \neq x)$
207	201 206	mpbird	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (N + 1) \neq F^{-1} (x)$
208	9	neeq1i	$⊢ K \neq F^{-1} (x) \leftrightarrow F^{-1} (N + 1) \neq F^{-1} (x)$
209	207 208	sylibr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \neq F^{-1} (x)$
210	209	necomd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \neq K$
211	182 187 189 210	leneltd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K < F^{-1} (x)$
212	74	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \in ℤ$
213		zltlem1	$⊢ (K \in ℤ \land F^{-1} (x) \in ℤ) \to (K < F^{-1} (x) \leftrightarrow K \leq F^{-1} (x) - 1)$
214	212 176 213	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to (K < F^{-1} (x) \leftrightarrow K \leq F^{-1} (x) - 1)$
215	211 214	mpbid	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \leq F^{-1} (x) - 1$
216	215 171	breqtrrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \leq k$
217	181 182 183 186 216	letrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \leq k$
218		elfzle2	$⊢ F^{-1} (x) \in (M \dots N + 1) \to F^{-1} (x) \leq N + 1$
219	175 218	syl	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \leq N + 1$
220	193	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N \in ℝ$
221		1re	$⊢ 1 \in ℝ$
222		lesubadd	$⊢ (F^{-1} (x) \in ℝ \land 1 \in ℝ \land N \in ℝ) \to (F^{-1} (x) - 1 \leq N \leftrightarrow F^{-1} (x) \leq N + 1)$
223	221 222	mp3an2	$⊢ (F^{-1} (x) \in ℝ \land N \in ℝ) \to (F^{-1} (x) - 1 \leq N \leftrightarrow F^{-1} (x) \leq N + 1)$
224	187 220 223	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to (F^{-1} (x) - 1 \leq N \leftrightarrow F^{-1} (x) \leq N + 1)$
225	219 224	mpbird	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) - 1 \leq N$
226	171 225	eqbrtrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \leq N$
227	169 170 179 217 226	elfzd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \in (M \dots N)$
228	182 183 216	lensymd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to \neg k < K$
229	228 58	syl	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F (if (k < K, k, k + 1)) = F (k + 1)$
230	171	oveq1d	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k + 1 = F^{-1} (x) - 1 + 1$
231	176	zcnd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in ℂ$
232		npcan	$⊢ (F^{-1} (x) \in ℂ \land 1 \in ℂ) \to F^{-1} (x) - 1 + 1 = F^{-1} (x)$
233	231 117 232	sylancl	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) - 1 + 1 = F^{-1} (x)$
234	230 233	eqtrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k + 1 = F^{-1} (x)$
235	234	fveq2d	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F (k + 1) = F (F^{-1} (x))$
236	6	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F : (M \dots N + 1) \underset{1-1 onto}{⟶} (M \dots N + 1)$
237	236 174 161	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F (F^{-1} (x)) = x$
238	229 235 237	3eqtrrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to x = F (if (k < K, k, k + 1))$
239	227 238	jca	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1)))$
240	239	expr	$⊢ ((φ \land x \in (M \dots N)) \land \neg F^{-1} (x) < K) \to (k = F^{-1} (x) - 1 \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1))))$
241	168 240	sylbid	$⊢ ((φ \land x \in (M \dots N)) \land \neg F^{-1} (x) < K) \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1))))$
242	166 241	pm2.61dan	$⊢ (φ \land x \in (M \dots N)) \to (k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1))))$
243	242	expimpd	$⊢ φ \to ((x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)) \to (k \in (M \dots N) \land x = F (if (k < K, k, k + 1))))$
244	125 243	impbid	$⊢ φ \to ((k \in (M \dots N) \land x = F (if (k < K, k, k + 1))) \leftrightarrow (x \in (M \dots N) \land k = if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1)))$
245	8 10 14 244	f1od	$⊢ φ \to J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$

Metamath Proof Explorer

Theorem seqf1olem1

Proof