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	sseldi	$⊢ ((φ \land k \in (M \dots N)) \land (k < K \land x = F (k))) \to k \in (M \dots N + 1)$
31	27 30	ffvelrnd	$⊢ ((φ \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	ffvelrnd	$⊢ φ \to F^{-1} (N + 1) \in (M \dots N + 1)$
73	9 72	eqeltrid	$⊢ φ \to K \in (M \dots N + 1)$
74		elfzelz	$⊢ K \in (M \dots N + 1) \to K \in ℤ$
75	73 74	syl	$⊢ φ \to K \in ℤ$
76	75	zred	$⊢ φ \to K \in ℝ$
77	76	ad2antrr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K \in ℝ$
78	21	ad2antlr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k \in ℝ$
79		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
80	78 79	syl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k + 1 \in ℝ$
81		simprl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to \neg k < K$
82	77 78 81	nltled	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K \leq k$
83	78	ltp1d	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k < k + 1$
84	77 78 80 82 83	lelttrd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K < k + 1$
85	77 84	ltned	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to K \neq k + 1$
86	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)$
87		fzp1elp1	$⊢ k \in (M \dots N) \to k + 1 \in (M \dots N + 1)$
88	87	ad2antlr	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k + 1 \in (M \dots N + 1)$
89	86 88	ffvelrnd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F (k + 1) \in (M \dots N + 1)$
90		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))$
91	4 90	syl	$⊢ φ \to (F (k + 1) \in (M \dots N + 1) \leftrightarrow (F (k + 1) \in (M \dots N) \lor F (k + 1) = N + 1))$
92	91	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))$
93	89 92	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)$
94	93	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)$
95	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)$
96		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)$
97	95 88 96	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)$
98	9	eqeq1i	$⊢ K = k + 1 \leftrightarrow F^{-1} (N + 1) = k + 1$
99	97 98	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)$
100	94 99	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)$
101	100	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))$
102	85 101	mpd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F (k + 1) \in (M \dots N)$
103	61 102	eqeltrd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to x \in (M \dots N)$
104	61	eqcomd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F (k + 1) = x$
105		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)$
106	95 88 105	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)$
107	104 106	mpd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F^{-1} (x) = k + 1$
108	107	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)$
109		lttr	$⊢ (k \in ℝ \land k + 1 \in ℝ \land K \in ℝ) \to ((k < k + 1 \land k + 1 < K) \to k < K)$
110	78 80 77 109	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)$
111	83 110	mpand	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (k + 1 < K \to k < K)$
112	108 111	sylbid	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to (F^{-1} (x) < K \to k < K)$
113	81 112	mtod	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to \neg F^{-1} (x) < K$
114		iffalse	$⊢ \neg F^{-1} (x) < K \to if (F^{-1} (x) < K, F^{-1} (x), F^{-1} (x) - 1) = F^{-1} (x) - 1$
115	113 114	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$
116	107	oveq1d	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to F^{-1} (x) - 1 = k + 1 - 1$
117	78	recnd	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k \in ℂ$
118		ax-1cn	$⊢ 1 \in ℂ$
119		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
120	117 118 119	sylancl	$⊢ ((φ \land k \in (M \dots N)) \land (\neg k < K \land x = F (k + 1))) \to k + 1 - 1 = k$
121	115 116 120	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)$
122	103 121	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))$
123	122	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)))$
124	60 123	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)))$
125	56 124	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)))$
126	125	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)))$
127	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))$
128	127	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))$
129		simprr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k = F^{-1} (x)$
130	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)$
131		simplr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to x \in (M \dots N)$
132	28 131	sseldi	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to x \in (M \dots N + 1)$
133	130 132	ffvelrnd	$⊢ ((φ \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)$
134	129 133	eqeltrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in (M \dots N + 1)$
135		elfzle1	$⊢ k \in (M \dots N + 1) \to M \leq k$
136	134 135	syl	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to M \leq k$
137		elfzelz	$⊢ k \in (M \dots N + 1) \to k \in ℤ$
138	134 137	syl	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in ℤ$
139	138	zred	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in ℝ$
140	76	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to K \in ℝ$
141		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
142	4 141	syl	$⊢ φ \to N \in ℤ$
143	142	peano2zd	$⊢ φ \to N + 1 \in ℤ$
144	143	zred	$⊢ φ \to N + 1 \in ℝ$
145	144	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to N + 1 \in ℝ$
146		simprl	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F^{-1} (x) < K$
147	129 146	eqbrtrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k < K$
148		elfzle2	$⊢ K \in (M \dots N + 1) \to K \leq N + 1$
149	73 148	syl	$⊢ φ \to K \leq N + 1$
150	149	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to K \leq N + 1$
151	139 140 145 147 150	ltletrd	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k < N + 1$
152	142	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to N \in ℤ$
153		zleltp1	$⊢ (k \in ℤ \land N \in ℤ) \to (k \leq N \leftrightarrow k < N + 1)$
154	138 152 153	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)$
155	151 154	mpbird	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \leq N$
156		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
157	4 156	syl	$⊢ φ \to M \in ℤ$
158	157	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to M \in ℤ$
159		elfz	$⊢ (k \in ℤ \land M \in ℤ \land N \in ℤ) \to (k \in (M \dots N) \leftrightarrow (M \leq k \land k \leq N))$
160	138 158 152 159	syl3anc	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to (k \in (M \dots N) \leftrightarrow (M \leq k \land k \leq N))$
161	136 155 160	mpbir2and	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to k \in (M \dots N)$
162	147 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)$
163	129	fveq2d	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F (k) = F (F^{-1} (x))$
164	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)$
165		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$
166	164 132 165	syl2anc	$⊢ ((φ \land x \in (M \dots N)) \land (F^{-1} (x) < K \land k = F^{-1} (x))) \to F (F^{-1} (x)) = x$
167	162 163 166	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))$
168	161 167	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)))$
169	168	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))))$
170	128 169	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))))$
171	114	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)$
172	171	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)$
173	157	zred	$⊢ φ \to M \in ℝ$
174	173	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \in ℝ$
175	76	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \in ℝ$
176		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$
177	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)$
178		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)$
179	28 178	sseldi	$⊢ ((φ \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)$
180	177 179	ffvelrnd	$⊢ ((φ \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)$
181		elfzelz	$⊢ F^{-1} (x) \in (M \dots N + 1) \to F^{-1} (x) \in ℤ$
182	180 181	syl	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in ℤ$
183		peano2zm	$⊢ F^{-1} (x) \in ℤ \to F^{-1} (x) - 1 \in ℤ$
184	182 183	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 ℤ$
185	176 184	eqeltrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \in ℤ$
186	185	zred	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \in ℝ$
187		elfzle1	$⊢ K \in (M \dots N + 1) \to M \leq K$
188	73 187	syl	$⊢ φ \to M \leq K$
189	188	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \leq K$
190	182	zred	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in ℝ$
191		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$
192	175 190 191	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)$
193		elfzelz	$⊢ x \in (M \dots N) \to x \in ℤ$
194	193	adantl	$⊢ (φ \land x \in (M \dots N)) \to x \in ℤ$
195	194	zred	$⊢ (φ \land x \in (M \dots N)) \to x \in ℝ$
196	142	zred	$⊢ φ \to N \in ℝ$
197	196	adantr	$⊢ (φ \land x \in (M \dots N)) \to N \in ℝ$
198	144	adantr	$⊢ (φ \land x \in (M \dots N)) \to N + 1 \in ℝ$
199		elfzle2	$⊢ x \in (M \dots N) \to x \leq N$
200	199	adantl	$⊢ (φ \land x \in (M \dots N)) \to x \leq N$
201	197	ltp1d	$⊢ (φ \land x \in (M \dots N)) \to N < N + 1$
202	195 197 198 200 201	lelttrd	$⊢ (φ \land x \in (M \dots N)) \to x < N + 1$
203	195 202	gtned	$⊢ (φ \land x \in (M \dots N)) \to N + 1 \neq x$
204	203	adantr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N + 1 \neq x$
205	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)$
206	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)$
207		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)$
208	205 206 179 207	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)$
209	208	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)$
210	204 209	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)$
211	9	neeq1i	$⊢ K \neq F^{-1} (x) \leftrightarrow F^{-1} (N + 1) \neq F^{-1} (x)$
212	210 211	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)$
213	212	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$
214	175 190 192 213	leneltd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K < F^{-1} (x)$
215	75	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \in ℤ$
216		zltlem1	$⊢ (K \in ℤ \land F^{-1} (x) \in ℤ) \to (K < F^{-1} (x) \leftrightarrow K \leq F^{-1} (x) - 1)$
217	215 182 216	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)$
218	214 217	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$
219	218 176	breqtrrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to K \leq k$
220	174 175 186 189 219	letrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \leq k$
221		elfzle2	$⊢ F^{-1} (x) \in (M \dots N + 1) \to F^{-1} (x) \leq N + 1$
222	180 221	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$
223	196	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N \in ℝ$
224		1re	$⊢ 1 \in ℝ$
225		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)$
226	224 225	mp3an2	$⊢ (F^{-1} (x) \in ℝ \land N \in ℝ) \to (F^{-1} (x) - 1 \leq N \leftrightarrow F^{-1} (x) \leq N + 1)$
227	190 223 226	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)$
228	222 227	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$
229	176 228	eqbrtrd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \leq N$
230	157	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to M \in ℤ$
231	142	ad2antrr	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to N \in ℤ$
232	185 230 231 159	syl3anc	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to (k \in (M \dots N) \leftrightarrow (M \leq k \land k \leq N))$
233	220 229 232	mpbir2and	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to k \in (M \dots N)$
234	175 186 219	lensymd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to \neg k < K$
235	234 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)$
236	176	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$
237	182	zcnd	$⊢ ((φ \land x \in (M \dots N)) \land (\neg F^{-1} (x) < K \land k = F^{-1} (x) - 1)) \to F^{-1} (x) \in ℂ$
238		npcan	$⊢ (F^{-1} (x) \in ℂ \land 1 \in ℂ) \to F^{-1} (x) - 1 + 1 = F^{-1} (x)$
239	237 118 238	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)$
240	236 239	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)$
241	240	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))$
242	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)$
243	242 179 165	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$
244	235 241 243	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))$
245	233 244	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)))$
246	245	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))))$
247	172 246	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))))$
248	170 247	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))))$
249	248	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))))$
250	126 249	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)))$
251	8 10 14 250	f1od	$⊢ φ \to J : (M \dots N) \underset{1-1 onto}{⟶} (M \dots N)$

Metamath Proof Explorer

Theorem seqf1olem1

Proof