Step Hyp Ref
Expression 1 vex 3112 . . . . . . . 8
2 oveq2 6304 . . . . . . . . . . 11
3 2 eqeq2d 2471 . . . . . . . . . 10
4 3 cbvrexv 3085 . . . . . . . . 9
5 eqeq1 2461 . . . . . . . . . 10
6 5 rexbidv 2968 . . . . . . . . 9
7 4 , 6 syl5bb 257 . . . . . . . 8
8 supmul1.1 . . . . . . . 8
9 1 , 7 , 8 elab2 3249 . . . . . . 7
10 supmul1.2 . . . . . . . . . . . . 13
11 simpr 461 . . . . . . . . . . . . 13
12 10 , 11 sylbi 195 . . . . . . . . . . . 12
13 12 simp1d 1008 . . . . . . . . . . 11
14 13 sselda 3503 . . . . . . . . . 10
15 suprcl 10528 . . . . . . . . . . . 12
16 12 , 15 syl 16 . . . . . . . . . . 11
17 16 adantr 465 . . . . . . . . . 10
18 simpl1 999 . . . . . . . . . . . . 13
19 10 , 18 sylbi 195 . . . . . . . . . . . 12
20 simpl2 1000 . . . . . . . . . . . . 13
21 10 , 20 sylbi 195 . . . . . . . . . . . 12
22 19 , 21 jca 532 . . . . . . . . . . 11
23 22 adantr 465 . . . . . . . . . 10
24 suprub 10529 . . . . . . . . . . 11
25 12 , 24 sylan 471 . . . . . . . . . 10
26 lemul2a 10422 . . . . . . . . . 10
27 14 , 17 , 23 , 25 , 26 syl31anc 1231 . . . . . . . . 9
28 breq1 4455 . . . . . . . . 9
29 27 , 28 syl5ibrcom 222 . . . . . . . 8
30 29 rexlimdva 2949 . . . . . . 7
31 9 , 30 syl5bi 217 . . . . . 6
32 31 ralrimiv 2869 . . . . 5
33 19 adantr 465 . . . . . . . . . . . 12
34 33 , 14 remulcld 9645 . . . . . . . . . . 11
35 eleq1a 2540 . . . . . . . . . . 11
36 34 , 35 syl 16 . . . . . . . . . 10
37 36 rexlimdva 2949 . . . . . . . . 9
38 9 , 37 syl5bi 217 . . . . . . . 8
39 38 ssrdv 3509 . . . . . . 7
40 simpr2 1003 . . . . . . . . . 10
41 10 , 40 sylbi 195 . . . . . . . . 9
42 ovex 6324 . . . . . . . . . . 11
43 42 isseti 3115 . . . . . . . . . 10
44 43 rgenw 2818 . . . . . . . . 9
45 r19.2z 3918 . . . . . . . . 9
46 41 , 44 , 45 sylancl 662 . . . . . . . 8
47 9 exbii 1667 . . . . . . . . 9
48 n0 3794 . . . . . . . . 9
49 rexcom4 3129 . . . . . . . . 9
50 47 , 48 , 49 3bitr4i 277 . . . . . . . 8
51 46 , 50 sylibr 212 . . . . . . 7
52 19 , 16 remulcld 9645 . . . . . . . 8
53 breq2 4456 . . . . . . . . . 10
54 53 ralbidv 2896 . . . . . . . . 9
55 54 rspcev 3210 . . . . . . . 8
56 52 , 32 , 55 syl2anc 661 . . . . . . 7
57 39 , 51 , 56 3jca 1176 . . . . . 6
58 suprleub 10532 . . . . . 6
59 57 , 52 , 58 syl2anc 661 . . . . 5
60 32 , 59 mpbird 232 . . . 4
61 simpr 461 . . . . . . 7
62 suprcl 10528 . . . . . . . . . 10
63 57 , 62 syl 16 . . . . . . . . 9
64 63 adantr 465 . . . . . . . 8
65 16 adantr 465 . . . . . . . 8
66 19 adantr 465 . . . . . . . 8
67 n0 3794 . . . . . . . . . . . 12
68 0red 9618 . . . . . . . . . . . . . . 15
69 simpl3 1001 . . . . . . . . . . . . . . . . 17
70 10 , 69 sylbi 195 . . . . . . . . . . . . . . . 16
71 breq2 4456 . . . . . . . . . . . . . . . . 17
72 71 rspccva 3209 . . . . . . . . . . . . . . . 16
73 70 , 72 sylan 471 . . . . . . . . . . . . . . 15
74 68 , 14 , 17 , 73 , 25 letrd 9760 . . . . . . . . . . . . . 14
75 74 ex 434 . . . . . . . . . . . . 13
76 75 exlimdv 1724 . . . . . . . . . . . 12
77 67 , 76 syl5bi 217 . . . . . . . . . . 11
78 41 , 77 mpd 15 . . . . . . . . . 10
79 78 adantr 465 . . . . . . . . 9
80 0red 9618 . . . . . . . . . . . . . . . 16
81 38 imp 429 . . . . . . . . . . . . . . . 16
82 63 adantr 465 . . . . . . . . . . . . . . . 16
83 21 adantr 465 . . . . . . . . . . . . . . . . . . . . 21
84 33 , 14 , 83 , 73 mulge0d 10154 . . . . . . . . . . . . . . . . . . . 20
85 breq2 4456 . . . . . . . . . . . . . . . . . . . 20
86 84 , 85 syl5ibrcom 222 . . . . . . . . . . . . . . . . . . 19
87 86 rexlimdva 2949 . . . . . . . . . . . . . . . . . 18
88 9 , 87 syl5bi 217 . . . . . . . . . . . . . . . . 17
89 88 imp 429 . . . . . . . . . . . . . . . 16
90 suprub 10529 . . . . . . . . . . . . . . . . 17
91 57 , 90 sylan 471 . . . . . . . . . . . . . . . 16
92 80 , 81 , 82 , 89 , 91 letrd 9760 . . . . . . . . . . . . . . 15
93 92 ex 434 . . . . . . . . . . . . . 14
94 93 exlimdv 1724 . . . . . . . . . . . . 13
95 48 , 94 syl5bi 217 . . . . . . . . . . . 12
96 51 , 95 mpd 15 . . . . . . . . . . 11
97 96 anim1i 568 . . . . . . . . . 10
98 0red 9618 . . . . . . . . . . . 12
99 lelttr 9696 . . . . . . . . . . . 12
100 98 , 63 , 52 , 99 syl3anc 1228 . . . . . . . . . . 11
101 100 adantr 465 . . . . . . . . . 10
102 97 , 101 mpd 15 . . . . . . . . 9
103 prodgt02 10413 . . . . . . . . 9
104 66 , 65 , 79 , 102 , 103 syl22anc 1229 . . . . . . . 8
105 ltdivmul 10442 . . . . . . . 8
106 64 , 65 , 66 , 104 , 105 syl112anc 1232 . . . . . . 7
107 61 , 106 mpbird 232 . . . . . 6
108 12 adantr 465 . . . . . . 7
109 104 gt0ne0d 10142 . . . . . . . 8
110 64 , 66 , 109 redivcld 10397 . . . . . . 7
111 suprlub 10530 . . . . . . 7
112 108 , 110 ,
111 syl2anc 661 . . . . . 6
113 107 , 112 mpbid 210 . . . . 5
114 rspe 2915 . . . . . . . . . . . . . . 15
115 114 , 9 sylibr 212 . . . . . . . . . . . . . 14
116 115 adantl 466 . . . . . . . . . . . . 13
117 simplrr 762 . . . . . . . . . . . . . 14
118 91 adantlr 714 . . . . . . . . . . . . . 14
119 117 , 118 eqbrtrrd 4474 . . . . . . . . . . . . 13
120 116 , 119 mpdan 668 . . . . . . . . . . . 12
121 120 expr 615 . . . . . . . . . . 11
122 121 exlimdv 1724 . . . . . . . . . 10
123 43 , 122 mpi 17 . . . . . . . . 9
124 123 adantlr 714 . . . . . . . 8
125 34 adantlr 714 . . . . . . . . 9
126 63 ad2antrr 725 . . . . . . . . 9
127 125 , 126 lenltd 9752 . . . . . . . 8
128 124 , 127 mpbid 210 . . . . . . 7
129 14 adantlr 714 . . . . . . . 8
130 19 ad2antrr 725 . . . . . . . 8
131 104 adantr 465 . . . . . . . 8
132 ltdivmul 10442 . . . . . . . 8
133 126 , 129 ,
130 , 131 , 132 syl112anc 1232 . . . . . . 7
134 128 , 133 mtbird 301 . . . . . 6
135 134 nrexdv 2913 . . . . 5
136 113 , 135 pm2.65da 576 . . . 4
137 60 , 136 jca 532 . . 3
138 63 , 52 eqleltd 9750 . . 3
139 137 , 138 mpbird 232 . 2
140 139 eqcomd 2465 1
