Step | Hyp | Ref
| Expression |
1 | | necom 2994 |
. . . . 5
β’ (π΄ β π΅ β π΅ β π΄) |
2 | | xrleltne 13073 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β (π΄ < π΅ β π΅ β π΄)) |
3 | | mnfxr 11220 |
. . . . . . . . . . . 12
β’ -β
β β* |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -β β β*) |
5 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΄
β β*) |
6 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΅
β β*) |
7 | | pnfnre 11204 |
. . . . . . . . . . . . . 14
β’ +β
β β |
8 | 7 | neli 3048 |
. . . . . . . . . . . . 13
β’ Β¬
+β β β |
9 | | mnfle 13063 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β*
β -β β€ π΄) |
10 | 5, 9 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -β β€ π΄) |
11 | | simpl3 1194 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΄
< π΅) |
12 | 4, 5, 6, 10, 11 | xrlelttrd 13088 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -β < π΅) |
13 | | xrltne 13091 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ π΅ β β* β§ -β
< π΅) β π΅ β -β) |
14 | 4, 6, 12, 13 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΅
β -β) |
15 | | xaddpnf1 13154 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β β*
β§ π΅ β -β)
β (π΅
+π +β) = +β) |
16 | 6, 14, 15 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΅
+π +β) = +β) |
17 | 16 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β ((π΅
+π +β) β β β +β β
β)) |
18 | 8, 17 | mtbiri 327 |
. . . . . . . . . . . 12
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β Β¬ (π΅ +π +β) β
β) |
19 | | ngtmnft 13094 |
. . . . . . . . . . . . . 14
β’ (π΄ β β*
β (π΄ = -β β
Β¬ -β < π΄)) |
20 | 5, 19 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΄ =
-β β Β¬ -β < π΄)) |
21 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΅
+π -ππ΄) β β) |
22 | | xnegeq 13135 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ = -β β
-ππ΄ =
-π-β) |
23 | | xnegmnf 13138 |
. . . . . . . . . . . . . . . . 17
β’
-π-β = +β |
24 | 22, 23 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
β’ (π΄ = -β β
-ππ΄ =
+β) |
25 | 24 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ (π΄ = -β β (π΅ +π
-ππ΄) =
(π΅ +π
+β)) |
26 | 25 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π΄ = -β β ((π΅ +π
-ππ΄)
β β β (π΅
+π +β) β β)) |
27 | 21, 26 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΄ =
-β β (π΅
+π +β) β β)) |
28 | 20, 27 | sylbird 260 |
. . . . . . . . . . . 12
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (Β¬ -β < π΄ β (π΅ +π +β) β
β)) |
29 | 18, 28 | mt3d 148 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -β < π΄) |
30 | | xrre2 13098 |
. . . . . . . . . . 11
β’
(((-β β β* β§ π΄ β β* β§ π΅ β β*)
β§ (-β < π΄
β§ π΄ < π΅)) β π΄ β β) |
31 | 4, 5, 6, 29, 11, 30 | syl32anc 1379 |
. . . . . . . . . 10
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΄
β β) |
32 | | pnfxr 11217 |
. . . . . . . . . . . 12
β’ +β
β β* |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β +β β β*) |
34 | 5 | xnegcld 13228 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -ππ΄ β
β*) |
35 | | xnegpnf 13137 |
. . . . . . . . . . . . . . . . 17
β’
-π+β = -β |
36 | | pnfge 13059 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΅ β β*
β π΅ β€
+β) |
37 | 6, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΅
β€ +β) |
38 | 5, 6, 33, 11, 37 | xrltletrd 13089 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΄
< +β) |
39 | | xltnegi 13144 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β β*
β§ +β β β* β§ π΄ < +β) β
-π+β < -ππ΄) |
40 | 5, 33, 38, 39 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -π+β <
-ππ΄) |
41 | 35, 40 | eqbrtrrid 5145 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -β < -ππ΄) |
42 | | xrltne 13091 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ -ππ΄ β β*
β§ -β < -ππ΄) β -ππ΄ β -β) |
43 | 4, 34, 41, 42 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β -ππ΄ β -β) |
44 | | xaddpnf2 13155 |
. . . . . . . . . . . . . . 15
β’
((-ππ΄ β β* β§
-ππ΄ β
-β) β (+β +π -ππ΄) = +β) |
45 | 34, 43, 44 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (+β +π
-ππ΄) =
+β) |
46 | 45 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β ((+β +π
-ππ΄)
β β β +β β β)) |
47 | 8, 46 | mtbiri 327 |
. . . . . . . . . . . 12
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β Β¬ (+β +π
-ππ΄)
β β) |
48 | | nltpnft 13092 |
. . . . . . . . . . . . . 14
β’ (π΅ β β*
β (π΅ = +β β
Β¬ π΅ <
+β)) |
49 | 6, 48 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΅ =
+β β Β¬ π΅
< +β)) |
50 | | oveq1 7368 |
. . . . . . . . . . . . . . 15
β’ (π΅ = +β β (π΅ +π
-ππ΄) =
(+β +π -ππ΄)) |
51 | 50 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π΅ = +β β ((π΅ +π
-ππ΄)
β β β (+β +π
-ππ΄)
β β)) |
52 | 21, 51 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΅ =
+β β (+β +π -ππ΄) β
β)) |
53 | 49, 52 | sylbird 260 |
. . . . . . . . . . . 12
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (Β¬ π΅ < +β β (+β
+π -ππ΄) β β)) |
54 | 47, 53 | mt3d 148 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΅
< +β) |
55 | | xrre2 13098 |
. . . . . . . . . . 11
β’ (((π΄ β β*
β§ π΅ β
β* β§ +β β β*) β§ (π΄ < π΅ β§ π΅ < +β)) β π΅ β β) |
56 | 5, 6, 33, 11, 54, 55 | syl32anc 1379 |
. . . . . . . . . 10
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β π΅
β β) |
57 | 31, 56 | jca 513 |
. . . . . . . . 9
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β§ (π΅ +π
-ππ΄)
β β) β (π΄
β β β§ π΅
β β)) |
58 | 57 | ex 414 |
. . . . . . . 8
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
< π΅) β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β))) |
59 | 58 | 3expia 1122 |
. . . . . . 7
β’ ((π΄ β β*
β§ π΅ β
β*) β (π΄ < π΅ β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β)))) |
60 | 59 | 3adant3 1133 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β (π΄ < π΅ β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β)))) |
61 | 2, 60 | sylbird 260 |
. . . . 5
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β (π΅ β π΄ β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β)))) |
62 | 1, 61 | biimtrid 241 |
. . . 4
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β (π΄ β π΅ β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β)))) |
63 | 62 | 3exp 1120 |
. . 3
β’ (π΄ β β*
β (π΅ β
β* β (π΄ β€ π΅ β (π΄ β π΅ β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β)))))) |
64 | 63 | com34 91 |
. 2
β’ (π΄ β β*
β (π΅ β
β* β (π΄ β π΅ β (π΄ β€ π΅ β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β)))))) |
65 | 64 | 3imp1 1348 |
1
β’ (((π΄ β β*
β§ π΅ β
β* β§ π΄
β π΅) β§ π΄ β€ π΅) β ((π΅ +π
-ππ΄)
β β β (π΄
β β β§ π΅
β β))) |