Theorem expcnvlem5 7166

Description: Lemma for expcnv 7168. 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 3953	. . . . 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 2619	. . . 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 610	. . 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 1674	. 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 2613	. . . 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 610	. . 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 1674	. 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 1526	. . . . 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 2613	. . . . 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 2612	. . . . 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 890	. . . 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 1526	. . . . 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 2613	. . . . 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 2612	. . . . 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 890	. . . 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 5926	. . . . . 6 |- 2 e. RR
17		2ne0 5937	. . . . . 6 |- 2 =/= 0
18	16, 17	rereccl 5757	. . . . 5 |- (1 / 2) e. RR
19		halfgt0 5976	. . . . 5 |- 0 < (1 / 2)
20		halflt1 5977	. . . . 5 |- (1 / 2) < 1
21	18, 19, 20	3pm3.2i 816	. . . 4 |- ((1 / 2) e. RR /\ 0 < (1 / 2) /\ (1 / 2) < 1)
22	11, 15, 21	elimhyp 2380	. . 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 1526	. . . . 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 2613	. . . . 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 626	. . . 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 1526	. . . . 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 2613	. . . . 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 626	. . . 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 5407	. . . . 5 |- 1 e. RR
30		lt01 5653	. . . . 5 |- 0 < 1
31	29, 30	pm3.2i 285	. . . 4 |- (1 e. RR /\ 0 < 1)
32	25, 28, 31	elimhyp 2380	. . 3 |- (if((B e. RR /\ 0 < B), B, 1) e. RR /\ 0 < if((B e. RR /\ 0 < B), B, 1))
33	22, 32	expcnvlem4 7165	. 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 2377	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 773   = wceq 953   e. wcel 955  A.wral 1637  E.wrex 1638  ifcif 2351   class class class wbr 2609  (class class class)co 3948  RRcr 5205  0cc0 5206  1c1 5207   / cdiv 5266   <_ cle 5267  NNcn 5268   < clt 5458  2c2 5908  ^cexp 6500

This theorem is referenced by:  expcnvlem6 7167

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

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