Theorem submateqlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		submateqlem1.n	|- ( ph -> N e. NN )
2		submateqlem1.k	|- ( ph -> K e. ( 1 ... N ) )
3		submateqlem1.m	|- ( ph -> M e. ( 1 ... ( N - 1 ) ) )
4		submateqlem1.1	|- ( ph -> K <_ M )
5		fz1ssnn	|- ( 1 ... N ) C_ NN
6	5 2	sselid	|- ( ph -> K e. NN )
7	6	nnzd	|- ( ph -> K e. ZZ )
8	1	nnzd	|- ( ph -> N e. ZZ )
9		fz1ssnn	|- ( 1 ... ( N - 1 ) ) C_ NN
10	9 3	sselid	|- ( ph -> M e. NN )
11	10	nnzd	|- ( ph -> M e. ZZ )
12	10	nnred	|- ( ph -> M e. RR )
13	1	nnred	|- ( ph -> N e. RR )
14		1red	|- ( ph -> 1 e. RR )
15	13 14	resubcld	|- ( ph -> ( N - 1 ) e. RR )
16		elfzle2	|- ( M e. ( 1 ... ( N - 1 ) ) -> M <_ ( N - 1 ) )
17	3 16	syl	|- ( ph -> M <_ ( N - 1 ) )
18	13	lem1d	|- ( ph -> ( N - 1 ) <_ N )
19	12 15 13 17 18	letrd	|- ( ph -> M <_ N )
20	7 8 11 4 19	elfzd	|- ( ph -> M e. ( K ... N ) )
21		1zzd	|- ( ph -> 1 e. ZZ )
22	11	peano2zd	|- ( ph -> ( M + 1 ) e. ZZ )
23	10	nnnn0d	|- ( ph -> M e. NN0 )
24	23	nn0ge0d	|- ( ph -> 0 <_ M )
25		1re	|- 1 e. RR
26		addge02	|- ( ( 1 e. RR /\ M e. RR ) -> ( 0 <_ M <-> 1 <_ ( M + 1 ) ) )
27	25 12 26	sylancr	|- ( ph -> ( 0 <_ M <-> 1 <_ ( M + 1 ) ) )
28	24 27	mpbid	|- ( ph -> 1 <_ ( M + 1 ) )
29	1	nnnn0d	|- ( ph -> N e. NN0 )
30		nn0ltlem1	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M < N <-> M <_ ( N - 1 ) ) )
31	23 29 30	syl2anc	|- ( ph -> ( M < N <-> M <_ ( N - 1 ) ) )
32	17 31	mpbird	|- ( ph -> M < N )
33		nnltp1le	|- ( ( M e. NN /\ N e. NN ) -> ( M < N <-> ( M + 1 ) <_ N ) )
34	10 1 33	syl2anc	|- ( ph -> ( M < N <-> ( M + 1 ) <_ N ) )
35	32 34	mpbid	|- ( ph -> ( M + 1 ) <_ N )
36	21 8 22 28 35	elfzd	|- ( ph -> ( M + 1 ) e. ( 1 ... N ) )
37	6	nnred	|- ( ph -> K e. RR )
38		nnleltp1	|- ( ( K e. NN /\ M e. NN ) -> ( K <_ M <-> K < ( M + 1 ) ) )
39	6 10 38	syl2anc	|- ( ph -> ( K <_ M <-> K < ( M + 1 ) ) )
40	4 39	mpbid	|- ( ph -> K < ( M + 1 ) )
41	37 40	ltned	|- ( ph -> K =/= ( M + 1 ) )
42	41	necomd	|- ( ph -> ( M + 1 ) =/= K )
43		nelsn	|- ( ( M + 1 ) =/= K -> -. ( M + 1 ) e. { K } )
44	42 43	syl	|- ( ph -> -. ( M + 1 ) e. { K } )
45	36 44	eldifd	|- ( ph -> ( M + 1 ) e. ( ( 1 ... N ) \ { K } ) )
46	20 45	jca	|- ( ph -> ( M e. ( K ... N ) /\ ( M + 1 ) e. ( ( 1 ... N ) \ { K } ) ) )