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	$⊢ φ \to N \in ℝ$
	oexpreposd.m	$⊢ φ \to M \in ℕ$
	oexpreposd.1	$⊢ φ \to \neg \frac{M}{2} \in ℕ$
Assertion	oexpreposd	$⊢ φ \to (0 < N \leftrightarrow 0 < N^{M})$

Proof

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

Metamath Proof Explorer

Theorem oexpreposd

Proof