Theorem expcnvlem5 7174

Description: Lemma for expcnv 7176. 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 3959	. . . . 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 2624	. . . 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 611	. . 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 1679	. 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 2618	. . . 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 611	. . 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 1679	. 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 1531	. . . . 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 2618	. . . . 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 2617	. . . . 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 891	. . . 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 1531	. . . . 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 2618	. . . . 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 2617	. . . . 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 891	. . . 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 5934	. . . . . 6 |- 2 e. RR
17		2ne0 5945	. . . . . 6 |- 2 =/= 0
18	16, 17	rereccl 5765	. . . . 5 |- (1 / 2) e. RR
19		halfgt0 5984	. . . . 5 |- 0 < (1 / 2)
20		halflt1 5985	. . . . 5 |- (1 / 2) < 1
21	18, 19, 20	3pm3.2i 817	. . . 4 |- ((1 / 2) e. RR /\ 0 < (1 / 2) /\ (1 / 2) < 1)
22	11, 15, 21	elimhyp 2386	. . 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 1531	. . . . 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 2618	. . . . 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 627	. . . 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 1531	. . . . 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 2618	. . . . 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 627	. . . 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 5415	. . . . 5 |- 1 e. RR
30		lt01 5661	. . . . 5 |- 0 < 1
31	29, 30	pm3.2i 285	. . . 4 |- (1 e. RR /\ 0 < 1)
32	25, 28, 31	elimhyp 2386	. . 3 |- (if((B e. RR /\ 0 < B), B, 1) e. RR /\ 0 < if((B e. RR /\ 0 < B), B, 1))
33	22, 32	expcnvlem4 7173	. 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 2383	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 774   = wceq 954   e. wcel 956  A.wral 1642  E.wrex 1643  ifcif 2357   class class class wbr 2614  (class class class)co 3954  RRcr 5213  0cc0 5214  1c1 5215   / cdiv 5274   <_ cle 5275  NNcn 5276   < clt 5466  2c2 5916  ^cexp 6508

This theorem is referenced by:  expcnvlem6 7175

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

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