Step Hyp Ref
Expression 1 ltrelsr 9466 . . . 4
2 1 brel 5053 . . 3
3 2 simprd 463 . 2
4 df-nr 9455 . . 3
5 breq2 4456 . . . 4
6 oveq1 6303 . . . . . 6
7 6 eqeq1d 2459 . . . . 5
8 7 rexbidv 2968 . . . 4
9 5 , 8 imbi12d 320 . . 3
10 gt0srpr 9476 . . . . 5
11 ltexpri 9442 . . . . 5
12 10 , 11 sylbi 195 . . . 4
13 recexpr 9450 . . . . . 6
14 1pr 9414 . . . . . . . . . . . 12
15 addclpr 9417 . . . . . . . . . . . 12
16 14 , 15 mpan2 671 . . . . . . . . . . 11
17 enrex 9465 . . . . . . . . . . . 12
18 17 , 4 ecopqsi 7387 . . . . . . . . . . 11
19 16 , 14 , 18 sylancl 662 . . . . . . . . . 10
20 19 ad2antlr 726 . . . . . . . . 9
21 16 , 14 jctir 538 . . . . . . . . . . . . . 14
22 21 anim2i 569 . . . . . . . . . . . . 13
23 22 adantr 465 . . . . . . . . . . . 12
24 mulsrpr 9474 . . . . . . . . . . . 12
25 23 , 24 syl 16 . . . . . . . . . . 11
26 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
27 26 eqcomd 2465 . . . . . . . . . . . . . . . . . . 19
28 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
29 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
30 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
31 mulcompr 9422 . . . . . . . . . . . . . . . . . . . . 21
32 distrpr 9427 . . . . . . . . . . . . . . . . . . . . 21
33 28 , 29 , 30 , 31 , 32 caovdir 6509 . . . . . . . . . . . . . . . . . . . 20
34 oveq2 6304 . . . . . . . . . . . . . . . . . . . 20
35 33 , 34 syl5eq 2510 . . . . . . . . . . . . . . . . . . 19
36 27 , 35 sylan9eqr 2520 . . . . . . . . . . . . . . . . . 18
37 36 oveq1d 6311 . . . . . . . . . . . . . . . . 17
38 ovex 6324 . . . . . . . . . . . . . . . . . 18
39 14 elexi 3119 . . . . . . . . . . . . . . . . . 18
40 ovex 6324 . . . . . . . . . . . . . . . . . 18
41 addcompr 9420 . . . . . . . . . . . . . . . . . 18
42 addasspr 9421 . . . . . . . . . . . . . . . . . 18
43 38 , 39 , 40 , 41 , 42 caov32 6502 . . . . . . . . . . . . . . . . 17
44 37 , 43 syl6eq 2514 . . . . . . . . . . . . . . . 16
45 44 oveq1d 6311 . . . . . . . . . . . . . . 15
46 addasspr 9421 . . . . . . . . . . . . . . 15
47 45 , 46 syl6eq 2514 . . . . . . . . . . . . . 14
48 distrpr 9427 . . . . . . . . . . . . . . . . 17
49 48 oveq1i 6306 . . . . . . . . . . . . . . . 16
50 addasspr 9421 . . . . . . . . . . . . . . . 16
51 49 , 50 eqtri 2486 . . . . . . . . . . . . . . 15
52 51 oveq1i 6306 . . . . . . . . . . . . . 14
53 distrpr 9427 . . . . . . . . . . . . . . . . 17
54 53 oveq2i 6307 . . . . . . . . . . . . . . . 16
55 ovex 6324 . . . . . . . . . . . . . . . . 17
56 ovex 6324 . . . . . . . . . . . . . . . . 17
57 55 , 38 , 56 , 41 , 42 caov12 6503 . . . . . . . . . . . . . . . 16
58 54 , 57 eqtri 2486 . . . . . . . . . . . . . . 15
59 58 oveq1i 6306 . . . . . . . . . . . . . 14
60 47 , 52 , 59 3eqtr4g 2523 . . . . . . . . . . . . 13
61 mulclpr 9419 . . . . . . . . . . . . . . . . . 18
62 16 , 61 sylan2 474 . . . . . . . . . . . . . . . . 17
63 mulclpr 9419 . . . . . . . . . . . . . . . . . 18
64 14 , 63 mpan2 671 . . . . . . . . . . . . . . . . 17
65 addclpr 9417 . . . . . . . . . . . . . . . . 17
66 62 , 64 , 65 syl2an 477 . . . . . . . . . . . . . . . 16
67 66 an32s 804 . . . . . . . . . . . . . . 15
68 mulclpr 9419 . . . . . . . . . . . . . . . . . 18
69 14 , 68 mpan2 671 . . . . . . . . . . . . . . . . 17
70 mulclpr 9419 . . . . . . . . . . . . . . . . . 18
71 16 , 70 sylan2 474 . . . . . . . . . . . . . . . . 17
72 addclpr 9417 . . . . . . . . . . . . . . . . 17
73 69 , 71 , 72 syl2an 477 . . . . . . . . . . . . . . . 16
74 73 anassrs 648 . . . . . . . . . . . . . . 15
75 67 , 74 jca 532 . . . . . . . . . . . . . 14
76 addclpr 9417 . . . . . . . . . . . . . . . 16
77 14 , 14 , 76 mp2an 672 . . . . . . . . . . . . . . 15
78 77 , 14 pm3.2i 455 . . . . . . . . . . . . . 14
79 enreceq 9464 . . . . . . . . . . . . . 14
80 75 , 78 , 79 sylancl 662 . . . . . . . . . . . . 13
81 60 , 80 syl5ibr 221 . . . . . . . . . . . 12
82 81 imp 429 . . . . . . . . . . 11
83 25 , 82 eqtrd 2498 . . . . . . . . . 10
84 df-1r 9460 . . . . . . . . . 10
85 83 , 84 syl6eqr 2516 . . . . . . . . 9
86 oveq2 6304 . . . . . . . . . . 11
87 86 eqeq1d 2459 . . . . . . . . . 10
88 87 rspcev 3210 . . . . . . . . 9
89 20 , 85 , 88 syl2anc 661 . . . . . . . 8
90 89 exp43 612 . . . . . . 7
91 90 rexlimdv 2947 . . . . . 6
92 13 , 91 syl5 32 . . . . 5
93 92 rexlimdv 2947 . . . 4
94 12 , 93 syl5 32 . . 3
95 4 , 9 , 94 ecoptocl 7420 . 2
96 3 , 95 mpcom 36 1
