Theorem submateqlem2

Description: Lemma for submateq . (Contributed by Thierry Arnoux, 26-Aug-2020)

	Ref	Expression
Hypotheses	submateqlem2.n	|- ( ph -> N e. NN )
	submateqlem2.k	|- ( ph -> K e. ( 1 ... N ) )
	submateqlem2.m	|- ( ph -> M e. ( 1 ... ( N - 1 ) ) )
	submateqlem2.1	|- ( ph -> M < K )
Assertion	submateqlem2	|- ( ph -> ( M e. ( 1 ..^ K ) /\ M e. ( ( 1 ... N ) \ { K } ) ) )

Proof

Step	Hyp	Ref	Expression
1		submateqlem2.n	|- ( ph -> N e. NN )
2		submateqlem2.k	|- ( ph -> K e. ( 1 ... N ) )
3		submateqlem2.m	|- ( ph -> M e. ( 1 ... ( N - 1 ) ) )
4		submateqlem2.1	|- ( ph -> M < K )
5		fz1ssnn	|- ( 1 ... ( N - 1 ) ) C_ NN
6	5 3	sselid	|- ( ph -> M e. NN )
7	6	nnge1d	|- ( ph -> 1 <_ M )
8	7 4	jca	|- ( ph -> ( 1 <_ M /\ M < K ) )
9	3	elfzelzd	|- ( ph -> M e. ZZ )
10		1zzd	|- ( ph -> 1 e. ZZ )
11	2	elfzelzd	|- ( ph -> K e. ZZ )
12		elfzo	|- ( ( M e. ZZ /\ 1 e. ZZ /\ K e. ZZ ) -> ( M e. ( 1 ..^ K ) <-> ( 1 <_ M /\ M < K ) ) )
13	9 10 11 12	syl3anc	|- ( ph -> ( M e. ( 1 ..^ K ) <-> ( 1 <_ M /\ M < K ) ) )
14	8 13	mpbird	|- ( ph -> M e. ( 1 ..^ K ) )
15	3	orcd	|- ( ph -> ( M e. ( 1 ... ( N - 1 ) ) \/ M = N ) )
16		nnuz	|- NN = ( ZZ>= ` 1 )
17	1 16	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 1 ) )
18		fzm1	|- ( N e. ( ZZ>= ` 1 ) -> ( M e. ( 1 ... N ) <-> ( M e. ( 1 ... ( N - 1 ) ) \/ M = N ) ) )
19	17 18	syl	|- ( ph -> ( M e. ( 1 ... N ) <-> ( M e. ( 1 ... ( N - 1 ) ) \/ M = N ) ) )
20	15 19	mpbird	|- ( ph -> M e. ( 1 ... N ) )
21	6	nnred	|- ( ph -> M e. RR )
22	21 4	ltned	|- ( ph -> M =/= K )
23		nelsn	|- ( M =/= K -> -. M e. { K } )
24	22 23	syl	|- ( ph -> -. M e. { K } )
25	20 24	eldifd	|- ( ph -> M e. ( ( 1 ... N ) \ { K } ) )
26	14 25	jca	|- ( ph -> ( M e. ( 1 ..^ K ) /\ M e. ( ( 1 ... N ) \ { K } ) ) )