Theorem iseqf1olemqk 10925

Description: Lemma for seq3f1o 10935. Q is constant for one more position than J is. (Contributed by Jim Kingdon, 21-Aug-2022.)

Hypotheses

Ref	Expression
iseqf1olemqf.k	|- ( ph -> K e. ( M ... N ) )
iseqf1olemqf.j	|- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
iseqf1olemqf.q	|- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )
iseqf1olemqk.const	|- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )

Assertion

Ref	Expression
iseqf1olemqk	|- ( ph -> A. x e. ( M ... K ) ( Q ` x ) = x )

Distinct variable groups:   u, J, x   u, K, x   u, M, x   u, N   x, Q   ph, x

Allowed substitution hints:   ph( u)   Q( u)   N( x)

Proof of Theorem iseqf1olemqk

Step	Hyp	Ref	Expression
1		elfzole1 10544	. . . . . . . 8 |- ( x e. ( M..^ K ) -> M <_ x )
2	1	adantl 277	. . . . . . 7 |- ( ( ph /\ x e. ( M..^ K ) ) -> M <_ x )
3		iseqf1olemqf.k	. . . . . . . . . 10 |- ( ph -> K e. ( M ... N ) )
4		elfzle2 10414	. . . . . . . . . 10 |- ( K e. ( M ... N ) -> K <_ N )
5	3, 4	syl 14	. . . . . . . . 9 |- ( ph -> K <_ N )
6		elfzolt2 10545	. . . . . . . . 9 |- ( x e. ( M..^ K ) -> x < K )
7	5, 6	anim12ci 339	. . . . . . . 8 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( x < K /\ K <_ N ) )
8		elfzoelz 10535	. . . . . . . . . . 11 |- ( x e. ( M..^ K ) -> x e. ZZ )
9	8	adantl 277	. . . . . . . . . 10 |- ( ( ph /\ x e. ( M..^ K ) ) -> x e. ZZ )
10	9	zred 9750	. . . . . . . . 9 |- ( ( ph /\ x e. ( M..^ K ) ) -> x e. RR )
11		elfzoel2 10534	. . . . . . . . . . 11 |- ( x e. ( M..^ K ) -> K e. ZZ )
12	11	adantl 277	. . . . . . . . . 10 |- ( ( ph /\ x e. ( M..^ K ) ) -> K e. ZZ )
13	12	zred 9750	. . . . . . . . 9 |- ( ( ph /\ x e. ( M..^ K ) ) -> K e. RR )
14		elfzel2 10408	. . . . . . . . . . . 12 |- ( K e. ( M ... N ) -> N e. ZZ )
15	3, 14	syl 14	. . . . . . . . . . 11 |- ( ph -> N e. ZZ )
16	15	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ x e. ( M..^ K ) ) -> N e. ZZ )
17	16	zred 9750	. . . . . . . . 9 |- ( ( ph /\ x e. ( M..^ K ) ) -> N e. RR )
18		ltleletr 8400	. . . . . . . . 9 |- ( ( x e. RR /\ K e. RR /\ N e. RR ) -> ( ( x < K /\ K <_ N ) -> x <_ N ) )
19	10, 13, 17, 18	syl3anc 1278	. . . . . . . 8 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( ( x < K /\ K <_ N ) -> x <_ N ) )
20	7, 19	mpd 13	. . . . . . 7 |- ( ( ph /\ x e. ( M..^ K ) ) -> x <_ N )
21		elfzel1 10409	. . . . . . . . . 10 |- ( K e. ( M ... N ) -> M e. ZZ )
22	3, 21	syl 14	. . . . . . . . 9 |- ( ph -> M e. ZZ )
23	22	adantr 276	. . . . . . . 8 |- ( ( ph /\ x e. ( M..^ K ) ) -> M e. ZZ )
24		elfz 10399	. . . . . . . 8 |- ( ( x e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( x e. ( M ... N ) <-> ( M <_ x /\ x <_ N ) ) )
25	9, 23, 16, 24	syl3anc 1278	. . . . . . 7 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( x e. ( M ... N ) <-> ( M <_ x /\ x <_ N ) ) )
26	2, 20, 25	mpbir2and 957	. . . . . 6 |- ( ( ph /\ x e. ( M..^ K ) ) -> x e. ( M ... N ) )
27	6	adantl 277	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M..^ K ) ) -> x < K )
28		zltnle 9672	. . . . . . . . . . . . 13 |- ( ( x e. ZZ /\ K e. ZZ ) -> ( x < K <-> -. K <_ x ) )
29	9, 12, 28	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( x < K <-> -. K <_ x ) )
30	27, 29	mpbid 147	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( M..^ K ) ) -> -. K <_ x )
31	30	intnanrd 944	. . . . . . . . . 10 |- ( ( ph /\ x e. ( M..^ K ) ) -> -. ( K <_ x /\ x <_ ( `' J ` K ) ) )
32		iseqf1olemqf.j	. . . . . . . . . . . . . . 15 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
33		f1ocnv 5650	. . . . . . . . . . . . . . 15 |- ( J : ( M ... N ) -1-1-onto-> ( M ... N ) -> `' J : ( M ... N ) -1-1-onto-> ( M ... N ) )
34		f1of 5637	. . . . . . . . . . . . . . 15 |- ( `' J : ( M ... N ) -1-1-onto-> ( M ... N ) -> `' J : ( M ... N ) --> ( M ... N ) )
35	32, 33, 34	3syl 17	. . . . . . . . . . . . . 14 |- ( ph -> `' J : ( M ... N ) --> ( M ... N ) )
36	35, 3	ffvelcdmd 5838	. . . . . . . . . . . . 13 |- ( ph -> ( `' J ` K ) e. ( M ... N ) )
37		elfzelz 10410	. . . . . . . . . . . . 13 |- ( ( `' J ` K ) e. ( M ... N ) -> ( `' J ` K ) e. ZZ )
38	36, 37	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( `' J ` K ) e. ZZ )
39	38	adantr 276	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( `' J ` K ) e. ZZ )
40		elfz 10399	. . . . . . . . . . 11 |- ( ( x e. ZZ /\ K e. ZZ /\ ( `' J ` K ) e. ZZ ) -> ( x e. ( K ... ( `' J ` K ) ) <-> ( K <_ x /\ x <_ ( `' J ` K ) ) ) )
41	9, 12, 39, 40	syl3anc 1278	. . . . . . . . . 10 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( x e. ( K ... ( `' J ` K ) ) <-> ( K <_ x /\ x <_ ( `' J ` K ) ) ) )
42	31, 41	mtbird 684	. . . . . . . . 9 |- ( ( ph /\ x e. ( M..^ K ) ) -> -. x e. ( K ... ( `' J ` K ) ) )
43	42	iffalsed 3650	. . . . . . . 8 |- ( ( ph /\ x e. ( M..^ K ) ) -> if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) = ( J ` x ) )
44		iseqf1olemqk.const	. . . . . . . . 9 |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )
45	44	r19.21bi 2638	. . . . . . . 8 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( J ` x ) = x )
46	43, 45	eqtrd 2271	. . . . . . 7 |- ( ( ph /\ x e. ( M..^ K ) ) -> if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) = x )
47		simpr 110	. . . . . . 7 |- ( ( ph /\ x e. ( M..^ K ) ) -> x e. ( M..^ K ) )
48	46, 47	eqeltrd 2315	. . . . . 6 |- ( ( ph /\ x e. ( M..^ K ) ) -> if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) e. ( M..^ K ) )
49		eleq1w 2299	. . . . . . . 8 |- ( u = x -> ( u e. ( K ... ( `' J ` K ) ) <-> x e. ( K ... ( `' J ` K ) ) ) )
50		eqeq1 2245	. . . . . . . . 9 |- ( u = x -> ( u = K <-> x = K ) )
51		oveq1 6085	. . . . . . . . . 10 |- ( u = x -> ( u - 1 ) = ( x - 1 ) )
52	51	fveq2d 5697	. . . . . . . . 9 |- ( u = x -> ( J ` ( u - 1 ) ) = ( J ` ( x - 1 ) ) )
53	50, 52	ifbieq2d 3665	. . . . . . . 8 |- ( u = x -> if ( u = K , K , ( J ` ( u - 1 ) ) ) = if ( x = K , K , ( J ` ( x - 1 ) ) ) )
54		fveq2 5693	. . . . . . . 8 |- ( u = x -> ( J ` u ) = ( J ` x ) )
55	49, 53, 54	ifbieq12d 3667	. . . . . . 7 |- ( u = x -> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) = if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) )
56		iseqf1olemqf.q	. . . . . . 7 |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )
57	55, 56	fvmptg 5778	. . . . . 6 |- ( ( x e. ( M ... N ) /\ if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) e. ( M..^ K ) ) -> ( Q ` x ) = if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) )
58	26, 48, 57	syl2anc 415	. . . . 5 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( Q ` x ) = if ( x e. ( K ... ( `' J ` K ) ) , if ( x = K , K , ( J ` ( x - 1 ) ) ) , ( J ` x ) ) )
59	58, 46	eqtrd 2271	. . . 4 |- ( ( ph /\ x e. ( M..^ K ) ) -> ( Q ` x ) = x )
60	59	ralrimiva 2623	. . 3 |- ( ph -> A. x e. ( M..^ K ) ( Q ` x ) = x )
61	3, 32, 3, 56	iseqf1olemqval 10918	. . . . 5 |- ( ph -> ( Q ` K ) = if ( K e. ( K ... ( `' J ` K ) ) , if ( K = K , K , ( J ` ( K - 1 ) ) ) , ( J ` K ) ) )
62		elfzelz 10410	. . . . . . . . . 10 |- ( K e. ( M ... N ) -> K e. ZZ )
63	3, 62	syl 14	. . . . . . . . 9 |- ( ph -> K e. ZZ )
64		elfzuz2 10415	. . . . . . . . . . 11 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
65	3, 64	syl 14	. . . . . . . . . 10 |- ( ph -> N e. ( ZZ>= ` M ) )
66	65, 3, 32, 44	iseqf1olemkle 10915	. . . . . . . . 9 |- ( ph -> K <_ ( `' J ` K ) )
67		eluz2 9909	. . . . . . . . 9 |- ( ( `' J ` K ) e. ( ZZ>= ` K ) <-> ( K e. ZZ /\ ( `' J ` K ) e. ZZ /\ K <_ ( `' J ` K ) ) )
68	63, 38, 66, 67	syl3anbrc 1212	. . . . . . . 8 |- ( ph -> ( `' J ` K ) e. ( ZZ>= ` K ) )
69		eluzfz1 10417	. . . . . . . 8 |- ( ( `' J ` K ) e. ( ZZ>= ` K ) -> K e. ( K ... ( `' J ` K ) ) )
70	68, 69	syl 14	. . . . . . 7 |- ( ph -> K e. ( K ... ( `' J ` K ) ) )
71	70	iftrued 3647	. . . . . 6 |- ( ph -> if ( K e. ( K ... ( `' J ` K ) ) , if ( K = K , K , ( J ` ( K - 1 ) ) ) , ( J ` K ) ) = if ( K = K , K , ( J ` ( K - 1 ) ) ) )
72		eqid 2238	. . . . . . 7 |- K = K
73	72	iftruei 3646	. . . . . 6 |- if ( K = K , K , ( J ` ( K - 1 ) ) ) = K
74	71, 73	eqtrdi 2287	. . . . 5 |- ( ph -> if ( K e. ( K ... ( `' J ` K ) ) , if ( K = K , K , ( J ` ( K - 1 ) ) ) , ( J ` K ) ) = K )
75	61, 74	eqtrd 2271	. . . 4 |- ( ph -> ( Q ` K ) = K )
76		fveq2 5693	. . . . . . 7 |- ( x = K -> ( Q ` x ) = ( Q ` K ) )
77		id 19	. . . . . . 7 |- ( x = K -> x = K )
78	76, 77	eqeq12d 2253	. . . . . 6 |- ( x = K -> ( ( Q ` x ) = x <-> ( Q ` K ) = K ) )
79	78	ralsng 3748	. . . . 5 |- ( K e. ZZ -> ( A. x e. { K } ( Q ` x ) = x <-> ( Q ` K ) = K ) )
80	3, 62, 79	3syl 17	. . . 4 |- ( ph -> ( A. x e. { K } ( Q ` x ) = x <-> ( Q ` K ) = K ) )
81	75, 80	mpbird 167	. . 3 |- ( ph -> A. x e. { K } ( Q ` x ) = x )
82		ralun 3411	. . 3 |- ( ( A. x e. ( M..^ K ) ( Q ` x ) = x /\ A. x e. { K } ( Q ` x ) = x ) -> A. x e. ( ( M..^ K ) u. { K } ) ( Q ` x ) = x )
83	60, 81, 82	syl2anc 415	. 2 |- ( ph -> A. x e. ( ( M..^ K ) u. { K } ) ( Q ` x ) = x )
84		elfzuz 10406	. . . 4 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
85		fzisfzounsn 10636	. . . 4 |- ( K e. ( ZZ>= ` M ) -> ( M ... K ) = ( ( M..^ K ) u. { K } ) )
86	3, 84, 85	3syl 17	. . 3 |- ( ph -> ( M ... K ) = ( ( M..^ K ) u. { K } ) )
87	86	raleqdv 2755	. 2 |- ( ph -> ( A. x e. ( M ... K ) ( Q ` x ) = x <-> A. x e. ( ( M..^ K ) u. { K } ) ( Q ` x ) = x ) )
88	83, 87	mpbird 167	1 |- ( ph -> A. x e. ( M ... K ) ( Q ` x ) = x )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   A.wral 2528   u. cun 3218   ifcif 3638   {csn 3708   class class class wbr 4128   |-> cmpt 4190   `'ccnv 4771   -->wf 5371   -1-1-onto->wf1o 5374   ` cfv 5375  (class class class)co 6078   RRcr 8171   1c1 8173   < clt 8353   <_ cle 8354   - cmin 8490   ZZcz 9626   ZZ>=cuz 9903   ...cfz 10393  ..^cfzo 10530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8263  ax-resscn 8264  ax-1cn 8265  ax-1re 8266  ax-icn 8267  ax-addcl 8268  ax-addrcl 8269  ax-mulcl 8270  ax-addcom 8272  ax-addass 8274  ax-distr 8276  ax-i2m1 8277  ax-0lt1 8278  ax-0id 8280  ax-rnegex 8281  ax-cnre 8283  ax-pre-ltirr 8284  ax-pre-ltwlin 8285  ax-pre-lttrn 8286  ax-pre-apti 8287  ax-pre-ltadd 8288

This theorem depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-if 3639  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-iun 4012  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-riota 6031  df-ov 6081  df-oprab 6082  df-mpo 6083  df-1st 6367  df-2nd 6368  df-pnf 8355  df-mnf 8356  df-xr 8357  df-ltxr 8358  df-le 8359  df-sub 8492  df-neg 8493  df-inn 9287  df-n0 9546  df-z 9627  df-uz 9904  df-fz 10394  df-fzo 10531

This theorem is referenced by:  seq3f1olemstep  10932