Step | Hyp | Ref
| Expression |
1 | | zsupssdc.ub |
. . 3
âĒ (ð â âðĨ â âĪ âðĶ â ðī ðĶ âĪ ðĨ) |
2 | | breq1 4007 |
. . . . . 6
âĒ (ðĶ = ð â (ðĶ âĪ ðĨ â ð âĪ ðĨ)) |
3 | 2 | cbvralvw 2708 |
. . . . 5
âĒ
(âðĶ â
ðī ðĶ âĪ ðĨ â âð â ðī ð âĪ ðĨ) |
4 | | breq2 4008 |
. . . . . 6
âĒ (ðĨ = ð â (ð âĪ ðĨ â ð âĪ ð)) |
5 | 4 | ralbidv 2477 |
. . . . 5
âĒ (ðĨ = ð â (âð â ðī ð âĪ ðĨ â âð â ðī ð âĪ ð)) |
6 | 3, 5 | bitrid 192 |
. . . 4
âĒ (ðĨ = ð â (âðĶ â ðī ðĶ âĪ ðĨ â âð â ðī ð âĪ ð)) |
7 | 6 | cbvrexvw 2709 |
. . 3
âĒ
(âðĨ â
âĪ âðĶ â
ðī ðĶ âĪ ðĨ â âð â âĪ âð â ðī ð âĪ ð) |
8 | 1, 7 | sylib 122 |
. 2
âĒ (ð â âð â âĪ âð â ðī ð âĪ ð) |
9 | | zsupssdc.m |
. . . . . . 7
âĒ (ð â âðĨ ðĨ â ðī) |
10 | | eleq1w 2238 |
. . . . . . . 8
âĒ (ðĨ = ð â (ðĨ â ðī â ð â ðī)) |
11 | 10 | cbvexv 1918 |
. . . . . . 7
âĒ
(âðĨ ðĨ â ðī â âð ð â ðī) |
12 | 9, 11 | sylib 122 |
. . . . . 6
âĒ (ð â âð ð â ðī) |
13 | 12 | adantr 276 |
. . . . 5
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â âð ð â ðī) |
14 | | uzssz 9547 |
. . . . . . 7
âĒ
(âĪâĨâ-ð) â âĪ |
15 | | rabss2 3239 |
. . . . . . 7
âĒ
((âĪâĨâ-ð) â âĪ â {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī} â {ðĪ â âĪ âĢ -ðĪ â ðī}) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
âĒ {ðĪ â
(âĪâĨâ-ð) âĢ -ðĪ â ðī} â {ðĪ â âĪ âĢ -ðĪ â ðī} |
17 | | negeq 8150 |
. . . . . . . . . . . . . 14
âĒ (ð = ðĪ â -ð = -ðĪ) |
18 | 17 | eleq1d 2246 |
. . . . . . . . . . . . 13
âĒ (ð = ðĪ â (-ð â ðī â -ðĪ â ðī)) |
19 | | simp1rl 1062 |
. . . . . . . . . . . . . . 15
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â ð â âĪ) |
20 | 19 | znegcld 9377 |
. . . . . . . . . . . . . 14
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â -ð â âĪ) |
21 | | simp2 998 |
. . . . . . . . . . . . . 14
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â ðĪ â âĪ) |
22 | 21 | zred 9375 |
. . . . . . . . . . . . . . 15
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â ðĪ â â) |
23 | 19 | zred 9375 |
. . . . . . . . . . . . . . 15
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â ð â â) |
24 | | breq1 4007 |
. . . . . . . . . . . . . . . 16
âĒ (ð = -ðĪ â (ð âĪ ð â -ðĪ âĪ ð)) |
25 | | simp1rr 1063 |
. . . . . . . . . . . . . . . 16
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â âð â ðī ð âĪ ð) |
26 | | simp3 999 |
. . . . . . . . . . . . . . . 16
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â -ðĪ â ðī) |
27 | 24, 25, 26 | rspcdva 2847 |
. . . . . . . . . . . . . . 15
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â -ðĪ âĪ ð) |
28 | 22, 23, 27 | lenegcon1d 8484 |
. . . . . . . . . . . . . 14
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â -ð âĪ ðĪ) |
29 | | eluz2 9534 |
. . . . . . . . . . . . . 14
âĒ (ðĪ â
(âĪâĨâ-ð) â (-ð â âĪ ⧠ðĪ â âĪ ⧠-ð âĪ ðĪ)) |
30 | 20, 21, 28, 29 | syl3anbrc 1181 |
. . . . . . . . . . . . 13
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â ðĪ â (âĪâĨâ-ð)) |
31 | 18, 30, 26 | elrabd 2896 |
. . . . . . . . . . . 12
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â âĪ ⧠-ðĪ â ðī) â ðĪ â {ð â (âĪâĨâ-ð) âĢ -ð â ðī}) |
32 | 31 | rabssdv 3236 |
. . . . . . . . . . 11
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â {ðĪ â âĪ âĢ -ðĪ â ðī} â {ð â (âĪâĨâ-ð) âĢ -ð â ðī}) |
33 | 18 | cbvrabv 2737 |
. . . . . . . . . . 11
âĒ {ð â
(âĪâĨâ-ð) âĢ -ð â ðī} = {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī} |
34 | 32, 33 | sseqtrdi 3204 |
. . . . . . . . . 10
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â {ðĪ â âĪ âĢ -ðĪ â ðī} â {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}) |
35 | 16 | a1i 9 |
. . . . . . . . . 10
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī} â {ðĪ â âĪ âĢ -ðĪ â ðī}) |
36 | 34, 35 | eqssd 3173 |
. . . . . . . . 9
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â {ðĪ â âĪ âĢ -ðĪ â ðī} = {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}) |
37 | 36 | infeq1d 7011 |
. . . . . . . 8
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) = inf({ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}, â, < )) |
38 | 37 | adantr 276 |
. . . . . . 7
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) = inf({ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}, â, < )) |
39 | | simprl 529 |
. . . . . . . . . 10
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â ð â âĪ) |
40 | 39 | znegcld 9377 |
. . . . . . . . 9
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â -ð â âĪ) |
41 | 40 | adantr 276 |
. . . . . . . 8
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â -ð â âĪ) |
42 | | eqid 2177 |
. . . . . . . 8
âĒ {ðĪ â
(âĪâĨâ-ð) âĢ -ðĪ â ðī} = {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī} |
43 | | negeq 8150 |
. . . . . . . . . 10
âĒ (ðĪ = -ð â -ðĪ = --ð) |
44 | 43 | eleq1d 2246 |
. . . . . . . . 9
âĒ (ðĪ = -ð â (-ðĪ â ðī â --ð â ðī)) |
45 | | zsupssdc.a |
. . . . . . . . . . . . 13
âĒ (ð â ðī â âĪ) |
46 | 45 | ad2antrr 488 |
. . . . . . . . . . . 12
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ðī â âĪ) |
47 | | simpr 110 |
. . . . . . . . . . . 12
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð â ðī) |
48 | 46, 47 | sseldd 3157 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð â âĪ) |
49 | 48 | znegcld 9377 |
. . . . . . . . . 10
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â -ð â âĪ) |
50 | | breq1 4007 |
. . . . . . . . . . . 12
âĒ (ð = ð â (ð âĪ ð â ð âĪ ð)) |
51 | | simplrr 536 |
. . . . . . . . . . . 12
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â âð â ðī ð âĪ ð) |
52 | 50, 51, 47 | rspcdva 2847 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð âĪ ð) |
53 | 48 | zred 9375 |
. . . . . . . . . . . 12
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð â â) |
54 | 39 | adantr 276 |
. . . . . . . . . . . . 13
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð â âĪ) |
55 | 54 | zred 9375 |
. . . . . . . . . . . 12
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð â â) |
56 | 53, 55 | lenegd 8481 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â (ð âĪ ð â -ð âĪ -ð)) |
57 | 52, 56 | mpbid 147 |
. . . . . . . . . 10
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â -ð âĪ -ð) |
58 | | eluz2 9534 |
. . . . . . . . . 10
âĒ (-ð â
(âĪâĨâ-ð) â (-ð â âĪ ⧠-ð â âĪ ⧠-ð âĪ -ð)) |
59 | 41, 49, 57, 58 | syl3anbrc 1181 |
. . . . . . . . 9
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â -ð â (âĪâĨâ-ð)) |
60 | 48 | zcnd 9376 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð â â) |
61 | 60 | negnegd 8259 |
. . . . . . . . . 10
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â --ð = ð) |
62 | 61, 47 | eqeltrd 2254 |
. . . . . . . . 9
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â --ð â ðī) |
63 | 44, 59, 62 | elrabd 2896 |
. . . . . . . 8
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â -ð â {ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}) |
64 | | eleq1 2240 |
. . . . . . . . . . 11
âĒ (ðĨ = -ðĪ â (ðĨ â ðī â -ðĪ â ðī)) |
65 | 64 | dcbid 838 |
. . . . . . . . . 10
âĒ (ðĨ = -ðĪ â (DECID ðĨ â ðī â DECID -ðĪ â ðī)) |
66 | | zsupssdc.dc |
. . . . . . . . . . 11
âĒ (ð â âðĨ â âĪ DECID ðĨ â ðī) |
67 | 66 | ad2antrr 488 |
. . . . . . . . . 10
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â (-ð...-ð)) â âðĨ â âĪ DECID ðĨ â ðī) |
68 | | elfzelz 10025 |
. . . . . . . . . . . 12
âĒ (ðĪ â (-ð...-ð) â ðĪ â âĪ) |
69 | 68 | adantl 277 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â (-ð...-ð)) â ðĪ â âĪ) |
70 | 69 | znegcld 9377 |
. . . . . . . . . 10
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â (-ð...-ð)) â -ðĪ â âĪ) |
71 | 65, 67, 70 | rspcdva 2847 |
. . . . . . . . 9
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ðĪ â (-ð...-ð)) â DECID -ðĪ â ðī) |
72 | 71 | adantlr 477 |
. . . . . . . 8
âĒ ((((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) ⧠ðĪ â (-ð...-ð)) â DECID -ðĪ â ðī) |
73 | 41, 42, 63, 72 | infssuzcldc 11952 |
. . . . . . 7
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}, â, < ) â {ðĪ â
(âĪâĨâ-ð) âĢ -ðĪ â ðī}) |
74 | 38, 73 | eqeltrd 2254 |
. . . . . 6
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â {ðĪ â
(âĪâĨâ-ð) âĢ -ðĪ â ðī}) |
75 | 16, 74 | sselid 3154 |
. . . . 5
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â {ðĪ â âĪ âĢ -ðĪ â ðī}) |
76 | 13, 75 | exlimddv 1898 |
. . . 4
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â {ðĪ â âĪ âĢ -ðĪ â ðī}) |
77 | | negeq 8150 |
. . . . . . 7
âĒ (ð = inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â -ð = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < )) |
78 | 77 | eleq1d 2246 |
. . . . . 6
âĒ (ð = inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (-ð â ðī â -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â ðī)) |
79 | | negeq 8150 |
. . . . . . . 8
âĒ (ðĪ = ð â -ðĪ = -ð) |
80 | 79 | eleq1d 2246 |
. . . . . . 7
âĒ (ðĪ = ð â (-ðĪ â ðī â -ð â ðī)) |
81 | 80 | cbvrabv 2737 |
. . . . . 6
âĒ {ðĪ â âĪ âĢ -ðĪ â ðī} = {ð â âĪ âĢ -ð â ðī} |
82 | 78, 81 | elrab2 2897 |
. . . . 5
âĒ
(inf({ðĪ â
âĪ âĢ -ðĪ â
ðī}, â, < ) â
{ðĪ â âĪ âĢ
-ðĪ â ðī} â (inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âĪ â§
-inf({ðĪ â âĪ
âĢ -ðĪ â ðī}, â, < ) â ðī)) |
83 | 82 | simprbi 275 |
. . . 4
âĒ
(inf({ðĪ â
âĪ âĢ -ðĪ â
ðī}, â, < ) â
{ðĪ â âĪ âĢ
-ðĪ â ðī} â -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â ðī) |
84 | 76, 83 | syl 14 |
. . 3
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â ðī) |
85 | | ssrab2 3241 |
. . . . . . . . 9
âĒ {ðĪ â âĪ âĢ -ðĪ â ðī} â âĪ |
86 | 85, 75 | sselid 3154 |
. . . . . . . 8
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â
âĪ) |
87 | 86 | zred 9375 |
. . . . . . 7
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â
â) |
88 | 87 | renegcld 8337 |
. . . . . 6
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â
â) |
89 | 41, 42, 63, 72 | infssuzledc 11951 |
. . . . . . . 8
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â (âĪâĨâ-ð) âĢ -ðĪ â ðī}, â, < ) âĪ -ð) |
90 | 38, 89 | eqbrtrd 4026 |
. . . . . . 7
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) âĪ -ð) |
91 | 87, 53, 90 | lenegcon2d 8485 |
. . . . . 6
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ð âĪ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < )) |
92 | 53, 88, 91 | lensymd 8079 |
. . . . 5
âĒ (((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) ⧠ð â ðī) â ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ð) |
93 | 92 | ralrimiva 2550 |
. . . 4
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â âð â ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ð) |
94 | | breq2 4008 |
. . . . . 6
âĒ (ð = ðĶ â (-inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ð â -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ)) |
95 | 94 | notbid 667 |
. . . . 5
âĒ (ð = ðĶ â (ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ð â ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ)) |
96 | 95 | cbvralv 2704 |
. . . 4
âĒ
(âð â
ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ð â âðĶ â ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ) |
97 | 93, 96 | sylib 122 |
. . 3
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â âðĶ â ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ) |
98 | | breq2 4008 |
. . . . . . 7
âĒ (ð§ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (ðĶ < ð§ â ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ))) |
99 | 98 | rspcev 2842 |
. . . . . 6
âĒ
((-inf({ðĪ â
âĪ âĢ -ðĪ â
ðī}, â, < ) â
ðī ⧠ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < )) â âð§ â ðī ðĶ < ð§) |
100 | 99 | ex 115 |
. . . . 5
âĒ
(-inf({ðĪ â
âĪ âĢ -ðĪ â
ðī}, â, < ) â
ðī â (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§)) |
101 | 84, 100 | syl 14 |
. . . 4
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§)) |
102 | 101 | ralrimivw 2551 |
. . 3
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â âðĶ â ðĩ (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§)) |
103 | | breq1 4007 |
. . . . . . 7
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (ðĨ < ðĶ â -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ)) |
104 | 103 | notbid 667 |
. . . . . 6
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (ÂŽ ðĨ < ðĶ â ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ)) |
105 | 104 | ralbidv 2477 |
. . . . 5
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (âðĶ â ðī ÂŽ ðĨ < ðĶ â âðĶ â ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ)) |
106 | | breq2 4008 |
. . . . . . 7
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (ðĶ < ðĨ â ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ))) |
107 | 106 | imbi1d 231 |
. . . . . 6
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â ((ðĶ < ðĨ â âð§ â ðī ðĶ < ð§) â (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§))) |
108 | 107 | ralbidv 2477 |
. . . . 5
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â (âðĶ â ðĩ (ðĶ < ðĨ â âð§ â ðī ðĶ < ð§) â âðĶ â ðĩ (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§))) |
109 | 105, 108 | anbi12d 473 |
. . . 4
âĒ (ðĨ = -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â ((âðĶ â ðī ÂŽ ðĨ < ðĶ ⧠âðĶ â ðĩ (ðĶ < ðĨ â âð§ â ðī ðĶ < ð§)) â (âðĶ â ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ ⧠âðĶ â ðĩ (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§)))) |
110 | 109 | rspcev 2842 |
. . 3
âĒ
((-inf({ðĪ â
âĪ âĢ -ðĪ â
ðī}, â, < ) â
ðī ⧠(âðĶ â ðī ÂŽ -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) < ðĶ ⧠âðĶ â ðĩ (ðĶ < -inf({ðĪ â âĪ âĢ -ðĪ â ðī}, â, < ) â âð§ â ðī ðĶ < ð§))) â âðĨ â ðī (âðĶ â ðī ÂŽ ðĨ < ðĶ ⧠âðĶ â ðĩ (ðĶ < ðĨ â âð§ â ðī ðĶ < ð§))) |
111 | 84, 97, 102, 110 | syl12anc 1236 |
. 2
âĒ ((ð ⧠(ð â âĪ ⧠âð â ðī ð âĪ ð)) â âðĨ â ðī (âðĶ â ðī ÂŽ ðĨ < ðĶ ⧠âðĶ â ðĩ (ðĶ < ðĨ â âð§ â ðī ðĶ < ð§))) |
112 | 8, 111 | rexlimddv 2599 |
1
âĒ (ð â âðĨ â ðī (âðĶ â ðī ÂŽ ðĨ < ðĶ ⧠âðĶ â ðĩ (ðĶ < ðĨ â âð§ â ðī ðĶ < ð§))) |