Theorem expcnvlem5 7231

Description: Lemma for expcnv 7233. Apply weak deduction theoerem.

Assertion

Ref	Expression
expcnvlem5	|- (((A e. RR /\ 0 < A /\ A < 1) /\ (B e. RR /\ 0 < B)) -> E.x e. NN A.y e. NN (x <_ y -> (A^y) < B))

Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem expcnvlem5

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . 5 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (A^y) = (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y))
2	1	breq1d 2629	. . . 4 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> ((A^y) < B <-> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < B))
3	2	imbi2d 612	. . 3 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> ((x <_ y -> (A^y) < B) <-> (x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < B)))
4	3	rexralbidv 1682	. 2 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (E.x e. NN A.y e. NN (x <_ y -> (A^y) < B) <-> E.x e. NN A.y e. NN (x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < B)))
5		breq2 2623	. . . 4 |- (B = if((B e. RR /\ 0 < B), B, 1) -> ((if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < B <-> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < if((B e. RR /\ 0 < B), B, 1)))
6	5	imbi2d 612	. . 3 |- (B = if((B e. RR /\ 0 < B), B, 1) -> ((x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < B) <-> (x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < if((B e. RR /\ 0 < B), B, 1))))
7	6	rexralbidv 1682	. 2 |- (B = if((B e. RR /\ 0 < B), B, 1) -> (E.x e. NN A.y e. NN (x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < B) <-> E.x e. NN A.y e. NN (x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < if((B e. RR /\ 0 < B), B, 1))))
8		eleq1 1534	. . . . 5 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (A e. RR <-> if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) e. RR))
9		breq2 2623	. . . . 5 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (0 < A <-> 0 < if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))))
10		breq1 2622	. . . . 5 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (A < 1 <-> if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) < 1))
11	8, 9, 10	3anbi123d 893	. . . 4 |- (A = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> ((A e. RR /\ 0 < A /\ A < 1) <-> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) e. RR /\ 0 < if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) /\ if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) < 1)))
12		eleq1 1534	. . . . 5 |- ((1 / 2) = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> ((1 / 2) e. RR <-> if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) e. RR))
13		breq2 2623	. . . . 5 |- ((1 / 2) = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (0 < (1 / 2) <-> 0 < if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))))
14		breq1 2622	. . . . 5 |- ((1 / 2) = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> ((1 / 2) < 1 <-> if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) < 1))
15	12, 13, 14	3anbi123d 893	. . . 4 |- ((1 / 2) = if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) -> (((1 / 2) e. RR /\ 0 < (1 / 2) /\ (1 / 2) < 1) <-> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) e. RR /\ 0 < if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) /\ if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) < 1)))
16		2re 5979	. . . . . 6 |- 2 e. RR
17		2ne0 5990	. . . . . 6 |- 2 =/= 0
18	16, 17	rereccl 5801	. . . . 5 |- (1 / 2) e. RR
19		halfgt0 6029	. . . . 5 |- 0 < (1 / 2)
20		halflt1 6030	. . . . 5 |- (1 / 2) < 1
21	18, 19, 20	3pm3.2i 818	. . . 4 |- ((1 / 2) e. RR /\ 0 < (1 / 2) /\ (1 / 2) < 1)
22	11, 15, 21	elimhyp 2390	. . 3 |- (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) e. RR /\ 0 < if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) /\ if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2)) < 1)
23		eleq1 1534	. . . . 5 |- (B = if((B e. RR /\ 0 < B), B, 1) -> (B e. RR <-> if((B e. RR /\ 0 < B), B, 1) e. RR))
24		breq2 2623	. . . . 5 |- (B = if((B e. RR /\ 0 < B), B, 1) -> (0 < B <-> 0 < if((B e. RR /\ 0 < B), B, 1)))
25	23, 24	anbi12d 628	. . . 4 |- (B = if((B e. RR /\ 0 < B), B, 1) -> ((B e. RR /\ 0 < B) <-> (if((B e. RR /\ 0 < B), B, 1) e. RR /\ 0 < if((B e. RR /\ 0 < B), B, 1))))
26		eleq1 1534	. . . . 5 |- (1 = if((B e. RR /\ 0 < B), B, 1) -> (1 e. RR <-> if((B e. RR /\ 0 < B), B, 1) e. RR))
27		breq2 2623	. . . . 5 |- (1 = if((B e. RR /\ 0 < B), B, 1) -> (0 < 1 <-> 0 < if((B e. RR /\ 0 < B), B, 1)))
28	26, 27	anbi12d 628	. . . 4 |- (1 = if((B e. RR /\ 0 < B), B, 1) -> ((1 e. RR /\ 0 < 1) <-> (if((B e. RR /\ 0 < B), B, 1) e. RR /\ 0 < if((B e. RR /\ 0 < B), B, 1))))
29		1re 5435	. . . . 5 |- 1 e. RR
30		lt01 5680	. . . . 5 |- 0 < 1
31	29, 30	pm3.2i 285	. . . 4 |- (1 e. RR /\ 0 < 1)
32	25, 28, 31	elimhyp 2390	. . 3 |- (if((B e. RR /\ 0 < B), B, 1) e. RR /\ 0 < if((B e. RR /\ 0 < B), B, 1))
33	22, 32	expcnvlem4 7230	. 2 |- E.x e. NN A.y e. NN (x <_ y -> (if((A e. RR /\ 0 < A /\ A < 1), A, (1 / 2))^y) < if((B e. RR /\ 0 < B), B, 1))
34	4, 7, 33	dedth2h 2387	1 |- (((A e. RR /\ 0 < A /\ A < 1) /\ (B e. RR /\ 0 < B)) -> E.x e. NN A.y e. NN (x <_ y -> (A^y) < B))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775   = wceq 956   e. wcel 958  A.wral 1645  E.wrex 1646  ifcif 2361   class class class wbr 2619  (class class class)co 3963  RRcr 5233  0cc0 5234  1c1 5235   / cdiv 5294   <_ cle 5295  NNcn 5296   < clt 5486  2c2 5961  ^cexp 6568

This theorem is referenced by:  expcnvlem6 7232

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-inf2 4625

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an