Metamath Proof Explorer


Theorem irrapxlem4

Description: Lemma for irrapx1 . Eliminate ranges, use positivity of the input to force positivity of the output by increasing B as needed. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem4 A+BxyAxy<1ifxBBx

Proof

Step Hyp Ref Expression
1 elfznn a1ifB1A+11A+1Ba
2 1 ad3antlr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1Ba
3 nn0z b0b
4 3 ad2antlr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1Bb
5 simpl A+BA+
6 5 ad3antrrr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BA+
7 6 rpred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BA
8 2 nnred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1Ba
9 7 8 remulcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAa
10 nn0re b0b
11 10 ad2antlr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1Bb
12 9 11 resubcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab
13 12 recnd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab
14 13 abscld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab
15 5 rpreccld A+B1A+
16 15 rprege0d A+B1A01A
17 flge0nn0 1A01A1A0
18 nn0p1nn 1A01A+1
19 16 17 18 3syl A+B1A+1
20 19 ad3antrrr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A+1
21 simpr A+BB
22 21 ad3antrrr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BB
23 20 22 ifcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifB1A+11A+1B
24 23 nnrecred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1ifB1A+11A+1B
25 0red A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0
26 9 25 resubcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAa0
27 simpr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab<1ifB1A+11A+1B
28 20 nnrecred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B11A+1
29 22 nnred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BB
30 6 rprecred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A
31 30 flcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A
32 31 zred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A
33 peano2re 1A1A+1
34 32 33 syl A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A+1
35 max2 B1A+11A+1ifB1A+11A+1B
36 29 34 35 syl2anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A+1ifB1A+11A+1B
37 20 nngt0d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<1A+1
38 23 nnred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifB1A+11A+1B
39 23 nngt0d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<ifB1A+11A+1B
40 lerec 1A+10<1A+1ifB1A+11A+1B0<ifB1A+11A+1B1A+1ifB1A+11A+1B1ifB1A+11A+1B11A+1
41 34 37 38 39 40 syl22anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A+1ifB1A+11A+1B1ifB1A+11A+1B11A+1
42 36 41 mpbid A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1ifB1A+11A+1B11A+1
43 fllep1 1A1A1A+1
44 30 43 syl A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A1A+1
45 20 nncnd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A+1
46 20 nnne0d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A+10
47 45 46 recrecd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B111A+1=1A+1
48 44 47 breqtrrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1A111A+1
49 34 37 recgt0d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<11A+1
50 6 rpgt0d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<A
51 lerec 11A+10<11A+1A0<A11A+1A1A111A+1
52 28 49 7 50 51 syl22anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B11A+1A1A111A+1
53 48 52 mpbird A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B11A+1A
54 24 28 7 42 53 letrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1ifB1A+11A+1BA
55 7 recnd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BA
56 55 mulid1d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BA1=A
57 2 nnge1d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1a
58 1red A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1
59 58 8 6 lemul2d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1aA1Aa
60 57 59 mpbid A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BA1Aa
61 56 60 eqbrtrrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAAa
62 9 recnd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAa
63 62 subid1d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAa0=Aa
64 61 63 breqtrrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAAa0
65 24 7 26 54 64 letrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1ifB1A+11A+1BAa0
66 14 24 26 27 65 ltletrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab<Aa0
67 12 26 absltd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab<Aa0Aa0<AabAab<Aa0
68 66 67 mpbid A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAa0<AabAab<Aa0
69 68 simprd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab<Aa0
70 25 11 9 ltsub2d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<bAab<Aa0
71 69 70 mpbird A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<b
72 elnnz bb0<b
73 4 71 72 sylanbrc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1Bb
74 22 2 ifcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifaBBa
75 74 nnrecred A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1ifaBBa
76 elfzle2 a1ifB1A+11A+1BaifB1A+11A+1B
77 76 ad3antlr A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BaifB1A+11A+1B
78 max1 B1A+1BifB1A+11A+1B
79 29 34 78 syl2anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BBifB1A+11A+1B
80 maxle aBifB1A+11A+1BifaBBaifB1A+11A+1BaifB1A+11A+1BBifB1A+11A+1B
81 8 29 38 80 syl3anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifaBBaifB1A+11A+1BaifB1A+11A+1BBifB1A+11A+1B
82 77 79 81 mpbir2and A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifaBBaifB1A+11A+1B
83 29 8 ifcld A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifaBBa
84 22 nngt0d A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<B
85 max2 aBBifaBBa
86 8 29 85 syl2anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BBifaBBa
87 25 29 83 84 86 ltletrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B0<ifaBBa
88 lerec ifaBBa0<ifaBBaifB1A+11A+1B0<ifB1A+11A+1BifaBBaifB1A+11A+1B1ifB1A+11A+1B1ifaBBa
89 83 87 38 39 88 syl22anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BifaBBaifB1A+11A+1B1ifB1A+11A+1B1ifaBBa
90 82 89 mpbid A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B1ifB1A+11A+1B1ifaBBa
91 14 24 75 27 90 ltletrd A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BAab<1ifaBBa
92 oveq2 x=aAx=Aa
93 92 fvoveq1d x=aAxy=Aay
94 breq1 x=axBaB
95 id x=ax=a
96 94 95 ifbieq2d x=aifxBBx=ifaBBa
97 96 oveq2d x=a1ifxBBx=1ifaBBa
98 93 97 breq12d x=aAxy<1ifxBBxAay<1ifaBBa
99 oveq2 y=bAay=Aab
100 99 fveq2d y=bAay=Aab
101 100 breq1d y=bAay<1ifaBBaAab<1ifaBBa
102 98 101 rspc2ev abAab<1ifaBBaxyAxy<1ifxBBx
103 2 73 91 102 syl3anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1BxyAxy<1ifxBBx
104 19 21 ifcld A+BifB1A+11A+1B
105 irrapxlem3 A+ifB1A+11A+1Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B
106 5 104 105 syl2anc A+Ba1ifB1A+11A+1Bb0Aab<1ifB1A+11A+1B
107 103 106 r19.29vva A+BxyAxy<1ifxBBx