Step Hyp Ref
Expression 1 ltexprlem.1 . . . . . . . 8
2 1 ltexprlem5 9439 . . . . . . 7
3 ltaddpr 9433 . . . . . . . . . . . . . . 15
4 addclpr 9417 . . . . . . . . . . . . . . . 16
5 ltprord 9429 . . . . . . . . . . . . . . . 16
6 4 , 5 syldan 470 . . . . . . . . . . . . . . 15
7 3 , 6 mpbid 210 . . . . . . . . . . . . . 14
8 7 pssssd 3600 . . . . . . . . . . . . 13
9 8 sseld 3502 . . . . . . . . . . . 12
10 9 a1d 25 . . . . . . . . . . 11
11 10 a1d 25 . . . . . . . . . 10
12 11 com4r 86 . . . . . . . . 9
13 12 expd 436 . . . . . . . 8
14 prnmadd 9396 . . . . . . . . . . . 12
15 14 ex 434 . . . . . . . . . . 11
16 elprnq 9390 . . . . . . . . . . . . . . . 16
17 addnqf 9347 . . . . . . . . . . . . . . . . . 18
18 17 fdmi 5741 . . . . . . . . . . . . . . . . 17
19 0nnq 9323 . . . . . . . . . . . . . . . . 17
20 18 , 19 ndmovrcl 6461 . . . . . . . . . . . . . . . 16
21 16 , 20 syl 16 . . . . . . . . . . . . . . 15
22 21 simpld 459 . . . . . . . . . . . . . 14
23 vex 3112 . . . . . . . . . . . . . . . . . . 19
24 23 prlem934 9432 . . . . . . . . . . . . . . . . . 18
25 24 adantr 465 . . . . . . . . . . . . . . . . 17
26 prub 9393 . . . . . . . . . . . . . . . . . . . . 21
27 ltexnq 9374 . . . . . . . . . . . . . . . . . . . . . 22
28 27 adantl 466 . . . . . . . . . . . . . . . . . . . . 21
29 26 , 28 sylibd 214 . . . . . . . . . . . . . . . . . . . 20
30 29 ex 434 . . . . . . . . . . . . . . . . . . 19
31 30 ad2ant2r 746 . . . . . . . . . . . . . . . . . 18
32 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
33 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
34 addcomnq 9350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
35 addassnq 9357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
36 32 , 23 , 33 , 34 , 35 caov32 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
37 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
38 36 , 37 syl5eq 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
39 38 eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . 26
40 39 biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 ovex 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
42 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
43 42 notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
44 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
45 44 eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
46 43 , 45 anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
47 41 , 46 spcev 3201 . . . . . . . . . . . . . . . . . . . . . . . . . 26
48 1 abeq2i 2584 . . . . . . . . . . . . . . . . . . . . . . . . . 26
49 47 , 48 sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . 25
50 40 , 49 sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . 24
51 df-plp 9382 . . . . . . . . . . . . . . . . . . . . . . . . 25
52 addclnq 9344 . . . . . . . . . . . . . . . . . . . . . . . . 25
53 51 , 52 genpprecl 9400 . . . . . . . . . . . . . . . . . . . . . . . 24
54 50 , 53 sylan2i 655 . . . . . . . . . . . . . . . . . . . . . . 23
55 54 exp4d 609 . . . . . . . . . . . . . . . . . . . . . 22
56 55 imp42 594 . . . . . . . . . . . . . . . . . . . . 21
57 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . 22
58 57 ad2antrl 727 . . . . . . . . . . . . . . . . . . . . 21
59 56 , 58 mpbid 210 . . . . . . . . . . . . . . . . . . . 20
60 59 exp32 605 . . . . . . . . . . . . . . . . . . 19
61 60 exlimdv 1724 . . . . . . . . . . . . . . . . . 18
62 31 , 61 syl6d 69 . . . . . . . . . . . . . . . . 17
63 25 , 62 rexlimddv 2953 . . . . . . . . . . . . . . . 16
64 63 com14 88 . . . . . . . . . . . . . . 15
65 64 adantl 466 . . . . . . . . . . . . . 14
66 22 , 65 mpd 15 . . . . . . . . . . . . 13
67 66 ex 434 . . . . . . . . . . . 12
68 67 exlimdv 1724 . . . . . . . . . . 11
69 15 , 68 syld 44 . . . . . . . . . 10
70 69 com4t 85 . . . . . . . . 9
71 70 expd 436 . . . . . . . 8
72 13 , 71 pm2.61i 164 . . . . . . 7
73 2 , 72 syl5 32 . . . . . 6
74 73 expd 436 . . . . 5
75 74 com34 83 . . . 4
76 75 pm2.43d 48 . . 3
77 76 imp31 432 . 2
78 77 ssrdv 3509 1
