Step | Hyp | Ref
| Expression |
1 | | nnex 11026 |
. . . . . . . . . . . . 13
|
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
|
3 | | reprinfz1.a |
. . . . . . . . . . . 12
|
4 | 2, 3 | ssexd 4805 |
. . . . . . . . . . 11
|
5 | | ovex 6678 |
. . . . . . . . . . 11
..^ |
6 | | elmapg 7870 |
. . . . . . . . . . 11
..^ ..^
..^ |
7 | 4, 5, 6 | sylancl 694 |
. . . . . . . . . 10
..^
..^ |
8 | 7 | biimpa 501 |
. . . . . . . . 9
..^
..^ |
9 | 8 | adantr 481 |
. . . . . . . 8
..^ ..^ ..^ |
10 | | elmapfn 7880 |
. . . . . . . . . . 11
..^ ..^ |
11 | 10 | ad2antlr 763 |
. . . . . . . . . 10
..^ ..^ ..^ |
12 | | simplr 792 |
. . . . . . . . . . . . 13
..^
..^
..^ ..^ |
13 | | reprinfz1.n |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 13 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 14 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
16 | 3 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
17 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ ..^ |
18 | 7 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ ..^
..^ |
19 | 17, 18 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ ..^ |
20 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ ..^ |
21 | 19, 20 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
22 | 16, 21 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
23 | 22 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
24 | | fzofi 12773 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ ..^ |
26 | 3 | ad4antr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ ..^ |
27 | 19 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ ..^ |
28 | 26, 27 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ ..^ |
29 | 28 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ ..^ |
30 | 25, 29 | fsumrecl 14465 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^ |
31 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
32 | 13 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
33 | 32 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^ |
34 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^
|
36 | 22 | biantrurd 529 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^
|
37 | 35, 36 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^
|
38 | 37 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
|
39 | 31, 38 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
|
40 | 15, 23 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^
|
41 | 39, 40 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
42 | 23 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
43 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
44 | 43 | sumsn 14475 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
45 | 20, 42, 44 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
46 | 28 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ ..^ |
47 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . . . . 22
|
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ ..^ |
49 | | snssi 4339 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ |
50 | 49 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^
..^ |
51 | 25, 29, 48, 50 | fsumless 14528 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ ..^ |
52 | 45, 51 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^ |
53 | 15, 23, 30, 41, 52 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ ..^ |
54 | 15, 53 | ltned 10173 |
. . . . . . . . . . . . . . . . 17
..^ ..^ ..^ |
55 | 54 | necomd 2849 |
. . . . . . . . . . . . . . . 16
..^ ..^ ..^ |
56 | 55 | r19.29an 3077 |
. . . . . . . . . . . . . . 15
..^ ..^
..^ |
57 | 56 | neneqd 2799 |
. . . . . . . . . . . . . 14
..^ ..^
..^ |
58 | 57 | adantlr 751 |
. . . . . . . . . . . . 13
..^
..^
..^ ..^ |
59 | 12, 58 | pm2.65da 600 |
. . . . . . . . . . . 12
..^ ..^
..^ |
60 | | dfral2 2994 |
. . . . . . . . . . . 12
..^
..^ |
61 | 59, 60 | sylibr 224 |
. . . . . . . . . . 11
..^ ..^ ..^ |
62 | 43 | eleq1d 2686 |
. . . . . . . . . . . 12
|
63 | 62 | cbvralv 3171 |
. . . . . . . . . . 11
..^ ..^ |
64 | 61, 63 | sylibr 224 |
. . . . . . . . . 10
..^ ..^ ..^ |
65 | 11, 64 | jca 554 |
. . . . . . . . 9
..^ ..^ ..^ ..^ |
66 | | ffnfv 6388 |
. . . . . . . . 9
..^
..^ ..^ |
67 | 65, 66 | sylibr 224 |
. . . . . . . 8
..^ ..^ ..^ |
68 | 9, 67 | jca 554 |
. . . . . . 7
..^ ..^ ..^ ..^ |
69 | | fin 6085 |
. . . . . . 7
..^
..^ ..^ |
70 | 68, 69 | sylibr 224 |
. . . . . 6
..^ ..^ ..^ |
71 | | ovex 6678 |
. . . . . . . 8
|
72 | 71 | inex2 4800 |
. . . . . . 7
|
73 | 72, 5 | elmap 7886 |
. . . . . 6
..^ ..^ |
74 | 70, 73 | sylibr 224 |
. . . . 5
..^ ..^ ..^ |
75 | 74 | anasss 679 |
. . . 4
..^ ..^ ..^ |
76 | 75 | rabss3d 29351 |
. . 3
..^ ..^ ..^
..^ |
77 | | reprinfz1.s |
. . . 4
|
78 | 3, 32, 77 | reprval 30688 |
. . 3
repr ..^ ..^ |
79 | | inss1 3833 |
. . . . . 6
|
80 | 79 | a1i 11 |
. . . . 5
|
81 | 80, 3 | sstrd 3613 |
. . . 4
|
82 | 81, 32, 77 | reprval 30688 |
. . 3
repr ..^ ..^ |
83 | 76, 78, 82 | 3sstr4d 3648 |
. 2
repr repr |
84 | 3, 32, 77, 80 | reprss 30695 |
. 2
repr repr |
85 | 83, 84 | eqssd 3620 |
1
repr repr |