Step | Hyp | Ref
| Expression |
1 | | eqeq1 2046 |
. . . . . . . 8
|
2 | 1 | anbi1d 438 |
. . . . . . 7
|
3 | 2 | anbi1d 438 |
. . . . . 6
#ℝ #ℝ
#ℝ
#ℝ |
4 | 3 | 2rexbidv 2349 |
. . . . 5
#ℝ
#ℝ
#ℝ
#ℝ |
5 | 4 | 2rexbidv 2349 |
. . . 4
#ℝ
#ℝ
#ℝ
#ℝ |
6 | | eqeq1 2046 |
. . . . . . . 8
|
7 | 6 | anbi2d 437 |
. . . . . . 7
|
8 | 7 | anbi1d 438 |
. . . . . 6
#ℝ #ℝ
#ℝ
#ℝ |
9 | 8 | 2rexbidv 2349 |
. . . . 5
#ℝ
#ℝ
#ℝ
#ℝ |
10 | 9 | 2rexbidv 2349 |
. . . 4
#ℝ
#ℝ
#ℝ
#ℝ |
11 | | df-ap 7573 |
. . . 4
#
#ℝ
#ℝ |
12 | 5, 10, 11 | brabg 4006 |
. . 3
#
#ℝ
#ℝ |
13 | | simplll 485 |
. . . . . . . . . . . . 13
|
14 | 13 | adantr 261 |
. . . . . . . . . . . 12
#ℝ #ℝ |
15 | | simplrl 487 |
. . . . . . . . . . . . 13
|
16 | 15 | adantr 261 |
. . . . . . . . . . . 12
#ℝ #ℝ |
17 | | simplrr 488 |
. . . . . . . . . . . . 13
|
18 | 17 | adantr 261 |
. . . . . . . . . . . 12
#ℝ #ℝ |
19 | | simprll 489 |
. . . . . . . . . . . 12
#ℝ #ℝ |
20 | | rereim 7577 |
. . . . . . . . . . . 12
|
21 | 14, 16, 18, 19, 20 | syl22anc 1136 |
. . . . . . . . . . 11
#ℝ #ℝ
|
22 | 21 | simprd 107 |
. . . . . . . . . 10
#ℝ #ℝ |
23 | | simpllr 486 |
. . . . . . . . . . . . 13
|
24 | 23 | adantr 261 |
. . . . . . . . . . . 12
#ℝ #ℝ |
25 | | simplrl 487 |
. . . . . . . . . . . 12
#ℝ #ℝ |
26 | | simplrr 488 |
. . . . . . . . . . . 12
#ℝ #ℝ |
27 | | simprlr 490 |
. . . . . . . . . . . 12
#ℝ #ℝ |
28 | | rereim 7577 |
. . . . . . . . . . . 12
|
29 | 24, 25, 26, 27, 28 | syl22anc 1136 |
. . . . . . . . . . 11
#ℝ #ℝ
|
30 | 29 | simprd 107 |
. . . . . . . . . 10
#ℝ #ℝ |
31 | 22, 30 | eqtr4d 2075 |
. . . . . . . . 9
#ℝ #ℝ |
32 | | reapti 7570 |
. . . . . . . . . 10
#ℝ |
33 | 18, 26, 32 | syl2anc 391 |
. . . . . . . . 9
#ℝ #ℝ
#ℝ |
34 | 31, 33 | mpbid 135 |
. . . . . . . 8
#ℝ #ℝ #ℝ |
35 | | simprr 484 |
. . . . . . . 8
#ℝ #ℝ #ℝ #ℝ |
36 | 34, 35 | ecased 1239 |
. . . . . . 7
#ℝ #ℝ #ℝ |
37 | 21 | simpld 105 |
. . . . . . 7
#ℝ #ℝ |
38 | 29 | simpld 105 |
. . . . . . 7
#ℝ #ℝ |
39 | 36, 37, 38 | 3brtr3d 3793 |
. . . . . 6
#ℝ #ℝ #ℝ |
40 | 39 | ex 108 |
. . . . 5
#ℝ
#ℝ #ℝ |
41 | 40 | rexlimdvva 2440 |
. . . 4
#ℝ
#ℝ #ℝ |
42 | 41 | rexlimdvva 2440 |
. . 3
#ℝ
#ℝ #ℝ |
43 | 12, 42 | sylbid 139 |
. 2
# #ℝ |
44 | | ax-icn 6979 |
. . . . . . . 8
|
45 | 44 | mul01i 7388 |
. . . . . . 7
|
46 | 45 | oveq2i 5523 |
. . . . . 6
|
47 | | simp1 904 |
. . . . . . . 8
#ℝ
|
48 | 47 | recnd 7054 |
. . . . . . 7
#ℝ
|
49 | 48 | addid1d 7162 |
. . . . . 6
#ℝ
|
50 | 46, 49 | syl5req 2085 |
. . . . 5
#ℝ
|
51 | 45 | oveq2i 5523 |
. . . . . 6
|
52 | | simp2 905 |
. . . . . . . 8
#ℝ
|
53 | 52 | recnd 7054 |
. . . . . . 7
#ℝ
|
54 | 53 | addid1d 7162 |
. . . . . 6
#ℝ
|
55 | 51, 54 | syl5req 2085 |
. . . . 5
#ℝ
|
56 | | olc 632 |
. . . . . . 7
#ℝ #ℝ #ℝ |
57 | 56 | 3ad2ant3 927 |
. . . . . 6
#ℝ
#ℝ
#ℝ |
58 | 57 | orcomd 648 |
. . . . 5
#ℝ
#ℝ
#ℝ |
59 | 50, 55, 58 | jca31 292 |
. . . 4
#ℝ
#ℝ #ℝ |
60 | | 0red 7028 |
. . . . . . . 8
#ℝ
|
61 | | simpr 103 |
. . . . . . . . . . . . 13
#ℝ
|
62 | 61 | oveq2d 5528 |
. . . . . . . . . . . 12
#ℝ |
63 | 62 | oveq2d 5528 |
. . . . . . . . . . 11
#ℝ |
64 | 63 | eqeq2d 2051 |
. . . . . . . . . 10
#ℝ |
65 | 64 | anbi2d 437 |
. . . . . . . . 9
#ℝ
|
66 | 61 | breq2d 3776 |
. . . . . . . . . 10
#ℝ
#ℝ
#ℝ |
67 | 66 | orbi2d 704 |
. . . . . . . . 9
#ℝ #ℝ #ℝ
#ℝ
#ℝ |
68 | 65, 67 | anbi12d 442 |
. . . . . . . 8
#ℝ
#ℝ
#ℝ
#ℝ #ℝ |
69 | 60, 68 | rspcedv 2660 |
. . . . . . 7
#ℝ
#ℝ
#ℝ #ℝ
#ℝ |
70 | | simpr 103 |
. . . . . . . . . . . . 13
#ℝ |
71 | 70 | oveq1d 5527 |
. . . . . . . . . . . 12
#ℝ
|
72 | 71 | eqeq2d 2051 |
. . . . . . . . . . 11
#ℝ
|
73 | 72 | anbi2d 437 |
. . . . . . . . . 10
#ℝ |
74 | 70 | breq2d 3776 |
. . . . . . . . . . 11
#ℝ #ℝ #ℝ |
75 | 74 | orbi1d 705 |
. . . . . . . . . 10
#ℝ
#ℝ
#ℝ #ℝ #ℝ |
76 | 73, 75 | anbi12d 442 |
. . . . . . . . 9
#ℝ #ℝ
#ℝ
#ℝ
#ℝ |
77 | 76 | rexbidv 2327 |
. . . . . . . 8
#ℝ
#ℝ
#ℝ #ℝ
#ℝ |
78 | 52, 77 | rspcedv 2660 |
. . . . . . 7
#ℝ
#ℝ
#ℝ
#ℝ
#ℝ |
79 | 69, 78 | syld 40 |
. . . . . 6
#ℝ
#ℝ
#ℝ #ℝ
#ℝ |
80 | | simpr 103 |
. . . . . . . . . . . . 13
#ℝ |
81 | 80 | oveq2d 5528 |
. . . . . . . . . . . 12
#ℝ |
82 | 81 | oveq2d 5528 |
. . . . . . . . . . 11
#ℝ |
83 | 82 | eqeq2d 2051 |
. . . . . . . . . 10
#ℝ |
84 | 83 | anbi1d 438 |
. . . . . . . . 9
#ℝ
|
85 | 80 | breq1d 3774 |
. . . . . . . . . 10
#ℝ
#ℝ
#ℝ |
86 | 85 | orbi2d 704 |
. . . . . . . . 9
#ℝ #ℝ #ℝ
#ℝ
#ℝ |
87 | 84, 86 | anbi12d 442 |
. . . . . . . 8
#ℝ
#ℝ
#ℝ
#ℝ #ℝ |
88 | 87 | 2rexbidv 2349 |
. . . . . . 7
#ℝ
#ℝ
#ℝ
#ℝ
#ℝ |
89 | 60, 88 | rspcedv 2660 |
. . . . . 6
#ℝ
#ℝ
#ℝ
#ℝ
#ℝ |
90 | | simpr 103 |
. . . . . . . . . . . . 13
#ℝ |
91 | 90 | oveq1d 5527 |
. . . . . . . . . . . 12
#ℝ
|
92 | 91 | eqeq2d 2051 |
. . . . . . . . . . 11
#ℝ
|
93 | 92 | anbi1d 438 |
. . . . . . . . . 10
#ℝ |
94 | 90 | breq1d 3774 |
. . . . . . . . . . 11
#ℝ #ℝ
#ℝ |
95 | 94 | orbi1d 705 |
. . . . . . . . . 10
#ℝ
#ℝ
#ℝ #ℝ #ℝ |
96 | 93, 95 | anbi12d 442 |
. . . . . . . . 9
#ℝ #ℝ #ℝ
#ℝ
#ℝ |
97 | 96 | rexbidv 2327 |
. . . . . . . 8
#ℝ
#ℝ #ℝ #ℝ
#ℝ
|
98 | 97 | 2rexbidv 2349 |
. . . . . . 7
#ℝ
#ℝ
#ℝ
#ℝ
#ℝ |
99 | 47, 98 | rspcedv 2660 |
. . . . . 6
#ℝ
#ℝ
#ℝ
#ℝ
#ℝ |
100 | 79, 89, 99 | 3syld 51 |
. . . . 5
#ℝ
#ℝ
#ℝ
#ℝ
#ℝ |
101 | 12 | 3adant3 924 |
. . . . 5
#ℝ
#
#ℝ
#ℝ |
102 | 100, 101 | sylibrd 158 |
. . . 4
#ℝ
#ℝ
#ℝ # |
103 | 59, 102 | mpd 13 |
. . 3
#ℝ
# |
104 | 103 | 3expia 1106 |
. 2
#ℝ
# |
105 | 43, 104 | impbid 120 |
1
#
#ℝ
|