Theorem oexpreposd

Description: Lemma for dffltz . TODO-SN?: This can be used to show exp11d holds for all integers when the exponent is odd. The more standard -. 2 || M should be used. (Contributed by SN, 4-Mar-2023)

	Ref	Expression
Hypotheses	oexpreposd.n	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
	oexpreposd.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	oexpreposd.1	⊢ ( 𝜑 → ¬ ( 𝑀 / 2 ) ∈ ℕ )
Assertion	oexpreposd	⊢ ( 𝜑 → ( 0 < 𝑁 ↔ 0 < ( 𝑁 ↑ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oexpreposd.n	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
2		oexpreposd.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3		oexpreposd.1	⊢ ( 𝜑 → ¬ ( 𝑀 / 2 ) ∈ ℕ )
4	1	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑁 ∈ ℝ )
5	2	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6	5	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑀 ∈ ℤ )
7		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 < 𝑁 )
8		expgt0	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑁 ) → 0 < ( 𝑁 ↑ 𝑀 ) )
9	4 6 7 8	syl3anc	⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 < ( 𝑁 ↑ 𝑀 ) )
10	9	ex	⊢ ( 𝜑 → ( 0 < 𝑁 → 0 < ( 𝑁 ↑ 𝑀 ) ) )
11		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
12	11 1	lttrid	⊢ ( 𝜑 → ( 0 < 𝑁 ↔ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) ) )
13	12	notbid	⊢ ( 𝜑 → ( ¬ 0 < 𝑁 ↔ ¬ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) ) )
14		notnotr	⊢ ( ¬ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) → ( 0 = 𝑁 ∨ 𝑁 < 0 ) )
15		0re	⊢ 0 ∈ ℝ
16	15	ltnri	⊢ ¬ 0 < 0
17	2	0expd	⊢ ( 𝜑 → ( 0 ↑ 𝑀 ) = 0 )
18	17	breq2d	⊢ ( 𝜑 → ( 0 < ( 0 ↑ 𝑀 ) ↔ 0 < 0 ) )
19	16 18	mtbiri	⊢ ( 𝜑 → ¬ 0 < ( 0 ↑ 𝑀 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ¬ 0 < ( 0 ↑ 𝑀 ) )
21		simpr	⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → 0 = 𝑁 )
22	21	eqcomd	⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → 𝑁 = 0 )
23	22	oveq1d	⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ( 𝑁 ↑ 𝑀 ) = ( 0 ↑ 𝑀 ) )
24	23	breq2d	⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ( 0 < ( 𝑁 ↑ 𝑀 ) ↔ 0 < ( 0 ↑ 𝑀 ) ) )
25	20 24	mtbird	⊢ ( ( 𝜑 ∧ 0 = 𝑁 ) → ¬ 0 < ( 𝑁 ↑ 𝑀 ) )
26	25	ex	⊢ ( 𝜑 → ( 0 = 𝑁 → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
27	1	renegcld	⊢ ( 𝜑 → - 𝑁 ∈ ℝ )
28	27	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → - 𝑁 ∈ ℝ )
29	5	adantr	⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → 𝑀 ∈ ℤ )
30		simpr	⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → 0 < - 𝑁 )
31		expgt0	⊢ ( ( - 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 0 < - 𝑁 ) → 0 < ( - 𝑁 ↑ 𝑀 ) )
32	28 29 30 31	syl3anc	⊢ ( ( 𝜑 ∧ 0 < - 𝑁 ) → 0 < ( - 𝑁 ↑ 𝑀 ) )
33	32	ex	⊢ ( 𝜑 → ( 0 < - 𝑁 → 0 < ( - 𝑁 ↑ 𝑀 ) ) )
34	1	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
35		simpr	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℤ )
36		zq	⊢ ( ( 𝑀 / 2 ) ∈ ℤ → ( 𝑀 / 2 ) ∈ ℚ )
37	36	adantl	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℚ )
38		qden1elz	⊢ ( ( 𝑀 / 2 ) ∈ ℚ → ( ( denom ‘ ( 𝑀 / 2 ) ) = 1 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
39	37 38	syl	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( denom ‘ ( 𝑀 / 2 ) ) = 1 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
40	35 39	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( denom ‘ ( 𝑀 / 2 ) ) = 1 )
41	40	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( 𝑀 / 2 ) · ( denom ‘ ( 𝑀 / 2 ) ) ) = ( ( 𝑀 / 2 ) · 1 ) )
42		qmuldeneqnum	⊢ ( ( 𝑀 / 2 ) ∈ ℚ → ( ( 𝑀 / 2 ) · ( denom ‘ ( 𝑀 / 2 ) ) ) = ( numer ‘ ( 𝑀 / 2 ) ) )
43	37 42	syl	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( 𝑀 / 2 ) · ( denom ‘ ( 𝑀 / 2 ) ) ) = ( numer ‘ ( 𝑀 / 2 ) ) )
44	35	zcnd	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℂ )
45	44	mulid1d	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( ( 𝑀 / 2 ) · 1 ) = ( 𝑀 / 2 ) )
46	41 43 45	3eqtr3rd	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) = ( numer ‘ ( 𝑀 / 2 ) ) )
47	2	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
48		2re	⊢ 2 ∈ ℝ
49	48	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
50	2	nngt0d	⊢ ( 𝜑 → 0 < 𝑀 )
51		2pos	⊢ 0 < 2
52	51	a1i	⊢ ( 𝜑 → 0 < 2 )
53	47 49 50 52	divgt0d	⊢ ( 𝜑 → 0 < ( 𝑀 / 2 ) )
54		qgt0numnn	⊢ ( ( ( 𝑀 / 2 ) ∈ ℚ ∧ 0 < ( 𝑀 / 2 ) ) → ( numer ‘ ( 𝑀 / 2 ) ) ∈ ℕ )
55	36 53 54	syl2anr	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( numer ‘ ( 𝑀 / 2 ) ) ∈ ℕ )
56	46 55	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑀 / 2 ) ∈ ℤ ) → ( 𝑀 / 2 ) ∈ ℕ )
57	3 56	mtand	⊢ ( 𝜑 → ¬ ( 𝑀 / 2 ) ∈ ℤ )
58		evend2	⊢ ( 𝑀 ∈ ℤ → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
59	5 58	syl	⊢ ( 𝜑 → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
60	57 59	mtbird	⊢ ( 𝜑 → ¬ 2 ∥ 𝑀 )
61		oexpneg	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℕ ∧ ¬ 2 ∥ 𝑀 ) → ( - 𝑁 ↑ 𝑀 ) = - ( 𝑁 ↑ 𝑀 ) )
62	34 2 60 61	syl3anc	⊢ ( 𝜑 → ( - 𝑁 ↑ 𝑀 ) = - ( 𝑁 ↑ 𝑀 ) )
63	62	breq2d	⊢ ( 𝜑 → ( 0 < ( - 𝑁 ↑ 𝑀 ) ↔ 0 < - ( 𝑁 ↑ 𝑀 ) ) )
64	63	biimpd	⊢ ( 𝜑 → ( 0 < ( - 𝑁 ↑ 𝑀 ) → 0 < - ( 𝑁 ↑ 𝑀 ) ) )
65	2	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
66	1 65	reexpcld	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑀 ) ∈ ℝ )
67	66	renegcld	⊢ ( 𝜑 → - ( 𝑁 ↑ 𝑀 ) ∈ ℝ )
68	11 67	lttrid	⊢ ( 𝜑 → ( 0 < - ( 𝑁 ↑ 𝑀 ) ↔ ¬ ( 0 = - ( 𝑁 ↑ 𝑀 ) ∨ - ( 𝑁 ↑ 𝑀 ) < 0 ) ) )
69		pm2.46	⊢ ( ¬ ( 0 = - ( 𝑁 ↑ 𝑀 ) ∨ - ( 𝑁 ↑ 𝑀 ) < 0 ) → ¬ - ( 𝑁 ↑ 𝑀 ) < 0 )
70	68 69	syl6bi	⊢ ( 𝜑 → ( 0 < - ( 𝑁 ↑ 𝑀 ) → ¬ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
71	33 64 70	3syld	⊢ ( 𝜑 → ( 0 < - 𝑁 → ¬ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
72	1	lt0neg1d	⊢ ( 𝜑 → ( 𝑁 < 0 ↔ 0 < - 𝑁 ) )
73	66	lt0neg2d	⊢ ( 𝜑 → ( 0 < ( 𝑁 ↑ 𝑀 ) ↔ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
74	73	notbid	⊢ ( 𝜑 → ( ¬ 0 < ( 𝑁 ↑ 𝑀 ) ↔ ¬ - ( 𝑁 ↑ 𝑀 ) < 0 ) )
75	71 72 74	3imtr4d	⊢ ( 𝜑 → ( 𝑁 < 0 → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
76	26 75	jaod	⊢ ( 𝜑 → ( ( 0 = 𝑁 ∨ 𝑁 < 0 ) → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
77	14 76	syl5	⊢ ( 𝜑 → ( ¬ ¬ ( 0 = 𝑁 ∨ 𝑁 < 0 ) → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
78	13 77	sylbid	⊢ ( 𝜑 → ( ¬ 0 < 𝑁 → ¬ 0 < ( 𝑁 ↑ 𝑀 ) ) )
79	10 78	impcon4bid	⊢ ( 𝜑 → ( 0 < 𝑁 ↔ 0 < ( 𝑁 ↑ 𝑀 ) ) )