Theorem knoppndvlem1

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem1.n	|- ( ph -> N e. NN )
	knoppndvlem1.j	|- ( ph -> J e. ZZ )
	knoppndvlem1.m	|- ( ph -> M e. ZZ )
Assertion	knoppndvlem1	|- ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem1.n	|- ( ph -> N e. NN )
2		knoppndvlem1.j	|- ( ph -> J e. ZZ )
3		knoppndvlem1.m	|- ( ph -> M e. ZZ )
4		2re	|- 2 e. RR
5	4	a1i	|- ( ph -> 2 e. RR )
6		nnz	|- ( N e. NN -> N e. ZZ )
7	1 6	syl	|- ( ph -> N e. ZZ )
8	7	zred	|- ( ph -> N e. RR )
9	5 8	remulcld	|- ( ph -> ( 2 x. N ) e. RR )
10	5	recnd	|- ( ph -> 2 e. CC )
11	8	recnd	|- ( ph -> N e. CC )
12		2ne0	|- 2 =/= 0
13	12	a1i	|- ( ph -> 2 =/= 0 )
14		0red	|- ( ph -> 0 e. RR )
15		1red	|- ( ph -> 1 e. RR )
16		0lt1	|- 0 < 1
17	16	a1i	|- ( ph -> 0 < 1 )
18		nnge1	|- ( N e. NN -> 1 <_ N )
19	1 18	syl	|- ( ph -> 1 <_ N )
20	14 15 8 17 19	ltletrd	|- ( ph -> 0 < N )
21	14 20	ltned	|- ( ph -> 0 =/= N )
22	21	necomd	|- ( ph -> N =/= 0 )
23	10 11 13 22	mulne0d	|- ( ph -> ( 2 x. N ) =/= 0 )
24	2	znegcld	|- ( ph -> -u J e. ZZ )
25	9 23 24	reexpclzd	|- ( ph -> ( ( 2 x. N ) ^ -u J ) e. RR )
26	25 5 13	redivcld	|- ( ph -> ( ( ( 2 x. N ) ^ -u J ) / 2 ) e. RR )
27	3	zred	|- ( ph -> M e. RR )
28	26 27	remulcld	|- ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )