Step | Hyp | Ref
| Expression |
1 | | simpll 495 |
. . . . . 6
|
2 | 1 | recnd 7147 |
. . . . 5
|
3 | | ax-icn 7071 |
. . . . . . 7
|
4 | 3 | a1i 9 |
. . . . . 6
|
5 | | simplr 496 |
. . . . . . 7
|
6 | 5 | recnd 7147 |
. . . . . 6
|
7 | 4, 6 | mulcld 7139 |
. . . . 5
|
8 | 2, 7 | addcld 7138 |
. . . 4
|
9 | | simprl 497 |
. . . . . 6
|
10 | 9 | recnd 7147 |
. . . . 5
|
11 | | simprr 498 |
. . . . . . 7
|
12 | 11 | recnd 7147 |
. . . . . 6
|
13 | 4, 12 | mulcld 7139 |
. . . . 5
|
14 | 10, 13 | addcld 7138 |
. . . 4
|
15 | | eqeq1 2087 |
. . . . . . . . 9
|
16 | 15 | anbi1d 452 |
. . . . . . . 8
|
17 | 16 | anbi1d 452 |
. . . . . . 7
#ℝ #ℝ
#ℝ
#ℝ |
18 | 17 | 2rexbidv 2391 |
. . . . . 6
#ℝ
#ℝ
#ℝ
#ℝ |
19 | 18 | 2rexbidv 2391 |
. . . . 5
#ℝ
#ℝ
#ℝ
#ℝ |
20 | | eqeq1 2087 |
. . . . . . . . 9
|
21 | 20 | anbi2d 451 |
. . . . . . . 8
|
22 | 21 | anbi1d 452 |
. . . . . . 7
#ℝ #ℝ
#ℝ #ℝ |
23 | 22 | 2rexbidv 2391 |
. . . . . 6
#ℝ
#ℝ
#ℝ #ℝ |
24 | 23 | 2rexbidv 2391 |
. . . . 5
#ℝ
#ℝ
#ℝ #ℝ |
25 | | df-ap 7682 |
. . . . 5
#
#ℝ
#ℝ |
26 | 19, 24, 25 | brabg 4024 |
. . . 4
#
#ℝ #ℝ |
27 | 8, 14, 26 | syl2anc 403 |
. . 3
#
#ℝ #ℝ |
28 | | simprr 498 |
. . . . . . 7
#ℝ #ℝ #ℝ #ℝ |
29 | 1 | ad3antrrr 475 |
. . . . . . . . . 10
#ℝ #ℝ |
30 | 9 | ad3antrrr 475 |
. . . . . . . . . 10
#ℝ #ℝ |
31 | | apreap 7687 |
. . . . . . . . . 10
#
#ℝ
|
32 | 29, 30, 31 | syl2anc 403 |
. . . . . . . . 9
#ℝ #ℝ # #ℝ |
33 | 5 | ad3antrrr 475 |
. . . . . . . . . 10
#ℝ #ℝ |
34 | 11 | ad3antrrr 475 |
. . . . . . . . . 10
#ℝ #ℝ |
35 | | apreap 7687 |
. . . . . . . . . 10
#
#ℝ
|
36 | 33, 34, 35 | syl2anc 403 |
. . . . . . . . 9
#ℝ #ℝ # #ℝ |
37 | 32, 36 | orbi12d 739 |
. . . . . . . 8
#ℝ #ℝ # # #ℝ #ℝ |
38 | | simprll 503 |
. . . . . . . . . . . 12
#ℝ #ℝ
|
39 | | simpllr 500 |
. . . . . . . . . . . . 13
#ℝ #ℝ |
40 | | cru 7702 |
. . . . . . . . . . . . 13
|
41 | 29, 33, 39, 40 | syl21anc 1168 |
. . . . . . . . . . . 12
#ℝ #ℝ |
42 | 38, 41 | mpbid 145 |
. . . . . . . . . . 11
#ℝ #ℝ |
43 | 42 | simpld 110 |
. . . . . . . . . 10
#ℝ #ℝ |
44 | | simprlr 504 |
. . . . . . . . . . . 12
#ℝ #ℝ
|
45 | | simplr 496 |
. . . . . . . . . . . . 13
#ℝ #ℝ |
46 | | cru 7702 |
. . . . . . . . . . . . 13
|
47 | 30, 34, 45, 46 | syl21anc 1168 |
. . . . . . . . . . . 12
#ℝ #ℝ |
48 | 44, 47 | mpbid 145 |
. . . . . . . . . . 11
#ℝ #ℝ |
49 | 48 | simpld 110 |
. . . . . . . . . 10
#ℝ #ℝ |
50 | 43, 49 | breq12d 3798 |
. . . . . . . . 9
#ℝ #ℝ #ℝ
#ℝ
|
51 | 42 | simprd 112 |
. . . . . . . . . 10
#ℝ #ℝ |
52 | 48 | simprd 112 |
. . . . . . . . . 10
#ℝ #ℝ |
53 | 51, 52 | breq12d 3798 |
. . . . . . . . 9
#ℝ #ℝ #ℝ
#ℝ
|
54 | 50, 53 | orbi12d 739 |
. . . . . . . 8
#ℝ #ℝ #ℝ
#ℝ
#ℝ
#ℝ |
55 | 37, 54 | bitrd 186 |
. . . . . . 7
#ℝ #ℝ # # #ℝ #ℝ |
56 | 28, 55 | mpbird 165 |
. . . . . 6
#ℝ #ℝ #
# |
57 | 56 | ex 113 |
. . . . 5
#ℝ #ℝ
#
# |
58 | 57 | rexlimdvva 2484 |
. . . 4
#ℝ #ℝ
#
# |
59 | 58 | rexlimdvva 2484 |
. . 3
#ℝ #ℝ
#
# |
60 | 27, 59 | sylbid 148 |
. 2
# # # |
61 | 31 | ad2ant2r 492 |
. . . . . 6
#
#ℝ
|
62 | 35 | ad2ant2l 491 |
. . . . . 6
#
#ℝ
|
63 | 61, 62 | orbi12d 739 |
. . . . 5
#
# #ℝ #ℝ |
64 | 63 | pm5.32i 441 |
. . . 4
#
#
#ℝ
#ℝ |
65 | | eqid 2081 |
. . . . . . . . . . . 12
|
66 | | eqid 2081 |
. . . . . . . . . . . 12
|
67 | 65, 66 | pm3.2i 266 |
. . . . . . . . . . 11
|
68 | 67 | biantrur 297 |
. . . . . . . . . 10
#ℝ #ℝ #ℝ
#ℝ
|
69 | | oveq1 5539 |
. . . . . . . . . . . . . 14
|
70 | 69 | eqeq2d 2092 |
. . . . . . . . . . . . 13
|
71 | 70 | anbi2d 451 |
. . . . . . . . . . . 12
|
72 | | breq2 3789 |
. . . . . . . . . . . . 13
#ℝ #ℝ |
73 | 72 | orbi1d 737 |
. . . . . . . . . . . 12
#ℝ
#ℝ #ℝ #ℝ |
74 | 71, 73 | anbi12d 456 |
. . . . . . . . . . 11
#ℝ
#ℝ
#ℝ
#ℝ
|
75 | | oveq2 5540 |
. . . . . . . . . . . . . . 15
|
76 | 75 | oveq2d 5548 |
. . . . . . . . . . . . . 14
|
77 | 76 | eqeq2d 2092 |
. . . . . . . . . . . . 13
|
78 | 77 | anbi2d 451 |
. . . . . . . . . . . 12
|
79 | | breq2 3789 |
. . . . . . . . . . . . 13
#ℝ #ℝ |
80 | 79 | orbi2d 736 |
. . . . . . . . . . . 12
#ℝ
#ℝ #ℝ #ℝ |
81 | 78, 80 | anbi12d 456 |
. . . . . . . . . . 11
#ℝ
#ℝ
#ℝ
#ℝ
|
82 | 74, 81 | rspc2ev 2715 |
. . . . . . . . . 10
#ℝ
#ℝ
#ℝ
#ℝ |
83 | 68, 82 | syl3an3b 1207 |
. . . . . . . . 9
#ℝ
#ℝ
#ℝ
#ℝ
|
84 | 83 | 3expa 1138 |
. . . . . . . 8
#ℝ #ℝ
#ℝ
#ℝ |
85 | | oveq1 5539 |
. . . . . . . . . . . . 13
|
86 | 85 | eqeq2d 2092 |
. . . . . . . . . . . 12
|
87 | 86 | anbi1d 452 |
. . . . . . . . . . 11
|
88 | | breq1 3788 |
. . . . . . . . . . . 12
#ℝ
#ℝ |
89 | 88 | orbi1d 737 |
. . . . . . . . . . 11
#ℝ
#ℝ #ℝ #ℝ |
90 | 87, 89 | anbi12d 456 |
. . . . . . . . . 10
#ℝ #ℝ
#ℝ
#ℝ
|
91 | 90 | 2rexbidv 2391 |
. . . . . . . . 9
#ℝ
#ℝ
#ℝ
#ℝ
|
92 | | oveq2 5540 |
. . . . . . . . . . . . . 14
|
93 | 92 | oveq2d 5548 |
. . . . . . . . . . . . 13
|
94 | 93 | eqeq2d 2092 |
. . . . . . . . . . . 12
|
95 | 94 | anbi1d 452 |
. . . . . . . . . . 11
|
96 | | breq1 3788 |
. . . . . . . . . . . 12
#ℝ
#ℝ |
97 | 96 | orbi2d 736 |
. . . . . . . . . . 11
#ℝ
#ℝ #ℝ #ℝ |
98 | 95, 97 | anbi12d 456 |
. . . . . . . . . 10
#ℝ
#ℝ
#ℝ
#ℝ
|
99 | 98 | 2rexbidv 2391 |
. . . . . . . . 9
#ℝ
#ℝ
#ℝ
#ℝ
|
100 | 91, 99 | rspc2ev 2715 |
. . . . . . . 8
#ℝ
#ℝ
#ℝ #ℝ |
101 | 84, 100 | syl3an3 1204 |
. . . . . . 7
#ℝ #ℝ
#ℝ #ℝ |
102 | 101 | 3expa 1138 |
. . . . . 6
#ℝ
#ℝ
#ℝ #ℝ |
103 | 102 | anassrs 392 |
. . . . 5
#ℝ
#ℝ
#ℝ #ℝ |
104 | 27 | adantr 270 |
. . . . 5
#ℝ
#ℝ #
#ℝ #ℝ |
105 | 103, 104 | mpbird 165 |
. . . 4
#ℝ
#ℝ
# |
106 | 64, 105 | sylbi 119 |
. . 3
#
# #
|
107 | 106 | ex 113 |
. 2
#
# #
|
108 | 60, 107 | impbid 127 |
1
#
#
# |