Step Hyp Ref
Expression 1 supmul.2 . . . . . . 7
2 1 simp2bi 1012 . . . . . 6
3 suprcl 10528 . . . . . 6
4 2 , 3 syl 16 . . . . 5
5 1 simp3bi 1013 . . . . . 6
6 suprcl 10528 . . . . . 6
7 5 , 6 syl 16 . . . . 5
8 recn 9603 . . . . . 6
9 recn 9603 . . . . . 6
10 mulcom 9599 . . . . . 6
11 8 , 9 , 10 syl2an 477 . . . . 5
12 4 , 7 , 11 syl2anc 661 . . . 4
13 5 simp2d 1009 . . . . . . 7
14 n0 3794 . . . . . . 7
15 13 , 14 sylib 196 . . . . . 6
16 0red 9618 . . . . . . 7
17 5 simp1d 1008 . . . . . . . 8
18 17 sselda 3503 . . . . . . 7
19 7 adantr 465 . . . . . . 7
20 simp1r 1021 . . . . . . . . . 10
21 1 , 20 sylbi 195 . . . . . . . . 9
22 breq2 4456 . . . . . . . . . 10
23 22 rspccv 3207 . . . . . . . . 9
24 21 , 23 syl 16 . . . . . . . 8
25 24 imp 429 . . . . . . 7
26 suprub 10529 . . . . . . . 8
27 5 , 26 sylan 471 . . . . . . 7
28 16 , 18 , 19 , 25 , 27 letrd 9760 . . . . . 6
29 15 , 28 exlimddv 1726 . . . . 5
30 simp1l 1020 . . . . . 6
31 1 , 30 sylbi 195 . . . . 5
32 eqid 2457 . . . . . 6
33 biid 236 . . . . . 6
34 32 , 33 supmul1 10533 . . . . 5
35 7 , 29 , 31 , 2 , 34 syl31anc 1231 . . . 4
36 12 , 35 eqtrd 2498 . . 3
37 vex 3112 . . . . . . 7
38 eqeq1 2461 . . . . . . . 8
39 38 rexbidv 2968 . . . . . . 7
40 37 , 39 elab 3246 . . . . . 6
41 7 adantr 465 . . . . . . . . . 10
42 2 simp1d 1008 . . . . . . . . . . 11
43 42 sselda 3503 . . . . . . . . . 10
44 recn 9603 . . . . . . . . . . 11
45 mulcom 9599 . . . . . . . . . . 11
46 9 , 44 , 45 syl2an 477 . . . . . . . . . 10
47 41 , 43 , 46 syl2anc 661 . . . . . . . . 9
48 breq2 4456 . . . . . . . . . . . . . 14
49 48 rspccv 3207 . . . . . . . . . . . . 13
50 31 , 49 syl 16 . . . . . . . . . . . 12
51 50 imp 429 . . . . . . . . . . 11
52 21 adantr 465 . . . . . . . . . . 11
53 5 adantr 465 . . . . . . . . . . 11
54 eqid 2457 . . . . . . . . . . . 12
55 biid 236 . . . . . . . . . . . 12
56 54 , 55 supmul1 10533 . . . . . . . . . . 11
57 43 , 51 , 52 , 53 , 56 syl31anc 1231 . . . . . . . . . 10
58 eqeq1 2461 . . . . . . . . . . . . . . 15
59 58 rexbidv 2968 . . . . . . . . . . . . . 14
60 37 , 59 elab 3246 . . . . . . . . . . . . 13
61 rspe 2915 . . . . . . . . . . . . . . . 16
62 oveq1 6303 . . . . . . . . . . . . . . . . . . . . 21
63 62 eqeq2d 2471 . . . . . . . . . . . . . . . . . . . 20
64 63 rexbidv 2968 . . . . . . . . . . . . . . . . . . 19
65 64 cbvrexv 3085 . . . . . . . . . . . . . . . . . 18
66 58 2rexbidv 2975 . . . . . . . . . . . . . . . . . 18
67 65 , 66 syl5bb 257 . . . . . . . . . . . . . . . . 17
68 supmul.1 . . . . . . . . . . . . . . . . 17
69 37 , 67 , 68 elab2 3249 . . . . . . . . . . . . . . . 16
70 61 , 69 sylibr 212 . . . . . . . . . . . . . . 15
71 70 ex 434 . . . . . . . . . . . . . 14
72 68 , 1 supmullem2 10535 . . . . . . . . . . . . . . 15
73 suprub 10529 . . . . . . . . . . . . . . . 16
74 73 ex 434 . . . . . . . . . . . . . . 15
75 72 , 74 syl 16 . . . . . . . . . . . . . 14
76 71 , 75 sylan9r 658 . . . . . . . . . . . . 13
77 60 , 76 syl5bi 217 . . . . . . . . . . . 12
78 77 ralrimiv 2869 . . . . . . . . . . 11
79 43 adantr 465 . . . . . . . . . . . . . . . 16
80 18 adantlr 714 . . . . . . . . . . . . . . . 16
81 79 , 80 remulcld 9645 . . . . . . . . . . . . . . 15
82 eleq1a 2540 . . . . . . . . . . . . . . 15
83 81 , 82 syl 16 . . . . . . . . . . . . . 14
84 83 rexlimdva 2949 . . . . . . . . . . . . 13
85 84 abssdv 3573 . . . . . . . . . . . 12
86 ovex 6324 . . . . . . . . . . . . . . . . . . 19
87 86 isseti 3115 . . . . . . . . . . . . . . . . . 18
88 87 rgenw 2818 . . . . . . . . . . . . . . . . 17
89 r19.2z 3918 . . . . . . . . . . . . . . . . 17
90 13 , 88 , 89 sylancl 662 . . . . . . . . . . . . . . . 16
91 rexcom4 3129 . . . . . . . . . . . . . . . 16
92 90 , 91 sylib 196 . . . . . . . . . . . . . . 15
93 59 cbvexv 2024 . . . . . . . . . . . . . . 15
94 92 , 93 sylibr 212 . . . . . . . . . . . . . 14
95 abn0 3804 . . . . . . . . . . . . . 14
96 94 , 95 sylibr 212 . . . . . . . . . . . . 13
97 96 adantr 465 . . . . . . . . . . . 12
98 suprcl 10528 . . . . . . . . . . . . . . 15
99 72 , 98 syl 16 . . . . . . . . . . . . . 14
100 99 adantr 465 . . . . . . . . . . . . 13
101 breq2 4456 . . . . . . . . . . . . . . 15
102 101 ralbidv 2896 . . . . . . . . . . . . . 14
103 102 rspcev 3210 . . . . . . . . . . . . 13
104 100 , 78 , 103 syl2anc 661 . . . . . . . . . . . 12
105 suprleub 10532 . . . . . . . . . . . 12
106 85 , 97 , 104 , 100 , 105 syl31anc 1231 . . . . . . . . . . 11
107 78 , 106 mpbird 232 . . . . . . . . . 10
108 57 , 107 eqbrtrd 4472 . . . . . . . . 9
109 47 , 108 eqbrtrd 4472 . . . . . . . 8
110 breq1 4455 . . . . . . . 8
111 109 , 110 syl5ibrcom 222 . . . . . . 7
112 111 rexlimdva 2949 . . . . . 6
113 40 , 112 syl5bi 217 . . . . 5
114 113 ralrimiv 2869 . . . 4
115 41 , 43 remulcld 9645 . . . . . . . 8
116 eleq1a 2540 . . . . . . . 8
117 115 , 116 syl 16 . . . . . . 7
118 117 rexlimdva 2949 . . . . . 6
119 118 abssdv 3573 . . . . 5
120 2 simp2d 1009 . . . . . . . 8
121 ovex 6324 . . . . . . . . . 10
122 121 isseti 3115 . . . . . . . . 9
123 122 rgenw 2818 . . . . . . . 8
124 r19.2z 3918 . . . . . . . 8
125 120 , 123 ,
124 sylancl 662 . . . . . . 7
126 rexcom4 3129 . . . . . . 7
127 125 , 126 sylib 196 . . . . . 6
128 abn0 3804 . . . . . 6
129 127 , 128 sylibr 212 . . . . 5
130 101 ralbidv 2896 . . . . . . 7
131 130 rspcev 3210 . . . . . 6
132 99 , 114 , 131 syl2anc 661 . . . . 5
133 suprleub 10532 . . . . 5
134 119 , 129 ,
132 , 99 , 133 syl31anc 1231 . . . 4
135 114 , 134 mpbird 232 . . 3
136 36 , 135 eqbrtrd 4472 . 2
137 68 , 1 supmullem1 10534 . . 3
138 4 , 7 remulcld 9645 . . . 4
139 suprleub 10532 . . . 4
140 72 , 138 , 139 syl2anc 661 . . 3
141 137 , 140 mpbird 232 . 2
142 138 , 99 letri3d 9748 . 2
143 136 , 141 ,
142 mpbir2and 922 1
