Theorem expgt0b

Description: A real number A raised to an odd integer power is positive iff it is positive. (Contributed by SN, 4-Mar-2023) Use the more standard -. 2 || N (Revised by Thierry Arnoux, 14-Jun-2025)

	Ref	Expression
Hypotheses	expgt0b.n	$$⊢\phi \to A\in ℝ$$
	expgt0b.m	$$⊢\phi \to N\in \mathbb{N}$$
	expgt0b.1	$$⊢\phi \to \neg 2\parallel N$$
Assertion	expgt0b	$$⊢\phi \to \left(0<A\leftrightarrow 0<A^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		expgt0b.n	$$⊢\phi \to A\in ℝ$$
2		expgt0b.m	$$⊢\phi \to N\in \mathbb{N}$$
3		expgt0b.1	$$⊢\phi \to \neg 2\parallel N$$
4	1	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A\in ℝ$$
5	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
6	5	adantr	$$⊢\left(\phi \wedge 0<A\right)\to N\in \mathbb{Z}$$
7		simpr	$$⊢\left(\phi \wedge 0<A\right)\to 0<A$$
8		expgt0	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\wedge 0<A\right)\to 0<A^N$$
9	4 6 7 8	syl3anc	$$⊢\left(\phi \wedge 0<A\right)\to 0<A^N$$
10	9	ex	$$⊢\phi \to \left(0<A\to 0<A^N\right)$$
11		0red	$$⊢\phi \to 0\in ℝ$$
12	11 1	lttrid	$$⊢\phi \to \left(0<A\leftrightarrow \neg \left(0=A\vee A<0\right)\right)$$
13	12	notbid	$$⊢\phi \to \left(\neg 0<A\leftrightarrow \neg \neg \left(0=A\vee A<0\right)\right)$$
14		notnotr	$$⊢\neg \neg \left(0=A\vee A<0\right)\to \left(0=A\vee A<0\right)$$
15		0re	$$⊢0\in ℝ$$
16	15	ltnri	$$⊢\neg 0<0$$
17	2	0expd	$$⊢\phi \to 0^N=0$$
18	17	breq2d	$$⊢\phi \to \left(0<0^N\leftrightarrow 0<0\right)$$
19	16 18	mtbiri	$$⊢\phi \to \neg 0<0^N$$
20	19	adantr	$$⊢\left(\phi \wedge 0=A\right)\to \neg 0<0^N$$
21		simpr	$$⊢\left(\phi \wedge 0=A\right)\to 0=A$$
22	21	eqcomd	$$⊢\left(\phi \wedge 0=A\right)\to A=0$$
23	22	oveq1d	$$⊢\left(\phi \wedge 0=A\right)\to A^N=0^N$$
24	23	breq2d	$$⊢\left(\phi \wedge 0=A\right)\to \left(0<A^N\leftrightarrow 0<0^N\right)$$
25	20 24	mtbird	$$⊢\left(\phi \wedge 0=A\right)\to \neg 0<A^N$$
26	25	ex	$$⊢\phi \to \left(0=A\to \neg 0<A^N\right)$$
27	1	renegcld	$$⊢\phi \to -A\in ℝ$$
28	27	adantr	$$⊢\left(\phi \wedge 0<-A\right)\to -A\in ℝ$$
29	5	adantr	$$⊢\left(\phi \wedge 0<-A\right)\to N\in \mathbb{Z}$$
30		simpr	$$⊢\left(\phi \wedge 0<-A\right)\to 0<-A$$
31		expgt0	$$⊢\left(-A\in ℝ\wedge N\in \mathbb{Z}\wedge 0<-A\right)\to 0<{\left(-A\right)}^N$$
32	28 29 30 31	syl3anc	$$⊢\left(\phi \wedge 0<-A\right)\to 0<{\left(-A\right)}^N$$
33	32	ex	$$⊢\phi \to \left(0<-A\to 0<{\left(-A\right)}^N\right)$$
34	1	recnd	$$⊢\phi \to A\in ℂ$$
35		oexpneg	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\wedge \neg 2\parallel N\right)\to {\left(-A\right)}^N=-A^N$$
36	34 2 3 35	syl3anc	$$⊢\phi \to {\left(-A\right)}^N=-A^N$$
37	36	breq2d	$$⊢\phi \to \left(0<{\left(-A\right)}^N\leftrightarrow 0<-A^N\right)$$
38	37	biimpd	$$⊢\phi \to \left(0<{\left(-A\right)}^N\to 0<-A^N\right)$$
39	2	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
40	1 39	reexpcld	$$⊢\phi \to A^N\in ℝ$$
41	40	renegcld	$$⊢\phi \to -A^N\in ℝ$$
42	11 41	lttrid	$$⊢\phi \to \left(0<-A^N\leftrightarrow \neg \left(0=-A^N\vee -A^N<0\right)\right)$$
43		pm2.46	$$⊢\neg \left(0=-A^N\vee -A^N<0\right)\to \neg -A^N<0$$
44	42 43	biimtrdi	$$⊢\phi \to \left(0<-A^N\to \neg -A^N<0\right)$$
45	33 38 44	3syld	$$⊢\phi \to \left(0<-A\to \neg -A^N<0\right)$$
46	1	lt0neg1d	$$⊢\phi \to \left(A<0\leftrightarrow 0<-A\right)$$
47	40	lt0neg2d	$$⊢\phi \to \left(0<A^N\leftrightarrow -A^N<0\right)$$
48	47	notbid	$$⊢\phi \to \left(\neg 0<A^N\leftrightarrow \neg -A^N<0\right)$$
49	45 46 48	3imtr4d	$$⊢\phi \to \left(A<0\to \neg 0<A^N\right)$$
50	26 49	jaod	$$⊢\phi \to \left(\left(0=A\vee A<0\right)\to \neg 0<A^N\right)$$
51	14 50	syl5	$$⊢\phi \to \left(\neg \neg \left(0=A\vee A<0\right)\to \neg 0<A^N\right)$$
52	13 51	sylbid	$$⊢\phi \to \left(\neg 0<A\to \neg 0<A^N\right)$$
53	10 52	impcon4bid	$$⊢\phi \to \left(0<A\leftrightarrow 0<A^N\right)$$