Step | Hyp | Ref
| Expression |
1 | | bfp.2 |
. . 3
|
2 | | cmetmet 23084 |
. . . . 5
|
3 | 1, 2 | syl 17 |
. . . 4
|
4 | | nnuz 11723 |
. . . . 5
|
5 | | bfp.10 |
. . . . 5
|
6 | | 1zzd 11408 |
. . . . 5
|
7 | | bfp.9 |
. . . . 5
|
8 | | bfp.6 |
. . . . 5
|
9 | 4, 5, 6, 7, 8 | algrf 15286 |
. . . 4
|
10 | 8, 7 | ffvelrnd 6360 |
. . . . . 6
|
11 | | metcl 22137 |
. . . . . 6
|
12 | 3, 7, 10, 11 | syl3anc 1326 |
. . . . 5
|
13 | | bfp.4 |
. . . . 5
|
14 | 12, 13 | rerpdivcld 11903 |
. . . 4
|
15 | | bfp.5 |
. . . 4
|
16 | | fveq2 6191 |
. . . . . . . . 9
|
17 | | oveq1 6657 |
. . . . . . . . . 10
|
18 | 17 | fveq2d 6195 |
. . . . . . . . 9
|
19 | 16, 18 | oveq12d 6668 |
. . . . . . . 8
|
20 | | oveq2 6658 |
. . . . . . . . 9
|
21 | 20 | oveq2d 6666 |
. . . . . . . 8
|
22 | 19, 21 | breq12d 4666 |
. . . . . . 7
|
23 | 22 | imbi2d 330 |
. . . . . 6
|
24 | | fveq2 6191 |
. . . . . . . . 9
|
25 | | oveq1 6657 |
. . . . . . . . . 10
|
26 | 25 | fveq2d 6195 |
. . . . . . . . 9
|
27 | 24, 26 | oveq12d 6668 |
. . . . . . . 8
|
28 | | oveq2 6658 |
. . . . . . . . 9
|
29 | 28 | oveq2d 6666 |
. . . . . . . 8
|
30 | 27, 29 | breq12d 4666 |
. . . . . . 7
|
31 | 30 | imbi2d 330 |
. . . . . 6
|
32 | | fveq2 6191 |
. . . . . . . . 9
|
33 | | oveq1 6657 |
. . . . . . . . . 10
|
34 | 33 | fveq2d 6195 |
. . . . . . . . 9
|
35 | 32, 34 | oveq12d 6668 |
. . . . . . . 8
|
36 | | oveq2 6658 |
. . . . . . . . 9
|
37 | 36 | oveq2d 6666 |
. . . . . . . 8
|
38 | 35, 37 | breq12d 4666 |
. . . . . . 7
|
39 | 38 | imbi2d 330 |
. . . . . 6
|
40 | 12 | leidd 10594 |
. . . . . . 7
|
41 | 4, 5, 6, 7 | algr0 15285 |
. . . . . . . 8
|
42 | | 1nn 11031 |
. . . . . . . . . 10
|
43 | 4, 5, 6, 7, 8 | algrp1 15287 |
. . . . . . . . . 10
|
44 | 42, 43 | mpan2 707 |
. . . . . . . . 9
|
45 | 41 | fveq2d 6195 |
. . . . . . . . 9
|
46 | 44, 45 | eqtrd 2656 |
. . . . . . . 8
|
47 | 41, 46 | oveq12d 6668 |
. . . . . . 7
|
48 | 13 | rpred 11872 |
. . . . . . . . . . 11
|
49 | 48 | recnd 10068 |
. . . . . . . . . 10
|
50 | 49 | exp1d 13003 |
. . . . . . . . 9
|
51 | 50 | oveq2d 6666 |
. . . . . . . 8
|
52 | 12 | recnd 10068 |
. . . . . . . . 9
|
53 | 13 | rpne0d 11877 |
. . . . . . . . 9
|
54 | 52, 49, 53 | divcan1d 10802 |
. . . . . . . 8
|
55 | 51, 54 | eqtrd 2656 |
. . . . . . 7
|
56 | 40, 47, 55 | 3brtr4d 4685 |
. . . . . 6
|
57 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
58 | | peano2nn 11032 |
. . . . . . . . . . . . 13
|
59 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
60 | 9, 58, 59 | syl2an 494 |
. . . . . . . . . . . 12
|
61 | 57, 60 | jca 554 |
. . . . . . . . . . 11
|
62 | | bfp.7 |
. . . . . . . . . . . . 13
|
63 | 62 | ralrimivva 2971 |
. . . . . . . . . . . 12
|
64 | 63 | adantr 481 |
. . . . . . . . . . 11
|
65 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
67 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
68 | 67 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
69 | 66, 68 | breq12d 4666 |
. . . . . . . . . . . 12
|
70 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
71 | 70 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
72 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
73 | 72 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
74 | 71, 73 | breq12d 4666 |
. . . . . . . . . . . 12
|
75 | 69, 74 | rspc2v 3322 |
. . . . . . . . . . 11
|
76 | 61, 64, 75 | sylc 65 |
. . . . . . . . . 10
|
77 | 3 | adantr 481 |
. . . . . . . . . . . 12
|
78 | 8 | adantr 481 |
. . . . . . . . . . . . 13
|
79 | 78, 57 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
80 | 78, 60 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
81 | | metcl 22137 |
. . . . . . . . . . . 12
|
82 | 77, 79, 80, 81 | syl3anc 1326 |
. . . . . . . . . . 11
|
83 | 48 | adantr 481 |
. . . . . . . . . . . 12
|
84 | | metcl 22137 |
. . . . . . . . . . . . 13
|
85 | 77, 57, 60, 84 | syl3anc 1326 |
. . . . . . . . . . . 12
|
86 | 83, 85 | remulcld 10070 |
. . . . . . . . . . 11
|
87 | 14 | adantr 481 |
. . . . . . . . . . . 12
|
88 | 58 | adantl 482 |
. . . . . . . . . . . . . 14
|
89 | 88 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
90 | 83, 89 | reexpcld 13025 |
. . . . . . . . . . . 12
|
91 | 87, 90 | remulcld 10070 |
. . . . . . . . . . 11
|
92 | | letr 10131 |
. . . . . . . . . . 11
|
93 | 82, 86, 91, 92 | syl3anc 1326 |
. . . . . . . . . 10
|
94 | 76, 93 | mpand 711 |
. . . . . . . . 9
|
95 | | nnnn0 11299 |
. . . . . . . . . . . . 13
|
96 | | reexpcl 12877 |
. . . . . . . . . . . . 13
|
97 | 48, 95, 96 | syl2an 494 |
. . . . . . . . . . . 12
|
98 | 87, 97 | remulcld 10070 |
. . . . . . . . . . 11
|
99 | 13 | rpgt0d 11875 |
. . . . . . . . . . . 12
|
100 | 99 | adantr 481 |
. . . . . . . . . . 11
|
101 | | lemul1 10875 |
. . . . . . . . . . 11
|
102 | 85, 98, 83, 100, 101 | syl112anc 1330 |
. . . . . . . . . 10
|
103 | 85 | recnd 10068 |
. . . . . . . . . . . 12
|
104 | 49 | adantr 481 |
. . . . . . . . . . . 12
|
105 | 103, 104 | mulcomd 10061 |
. . . . . . . . . . 11
|
106 | 87 | recnd 10068 |
. . . . . . . . . . . . 13
|
107 | 97 | recnd 10068 |
. . . . . . . . . . . . 13
|
108 | 106, 107,
104 | mulassd 10063 |
. . . . . . . . . . . 12
|
109 | | expp1 12867 |
. . . . . . . . . . . . . 14
|
110 | 49, 95, 109 | syl2an 494 |
. . . . . . . . . . . . 13
|
111 | 110 | oveq2d 6666 |
. . . . . . . . . . . 12
|
112 | 108, 111 | eqtr4d 2659 |
. . . . . . . . . . 11
|
113 | 105, 112 | breq12d 4666 |
. . . . . . . . . 10
|
114 | 102, 113 | bitrd 268 |
. . . . . . . . 9
|
115 | 4, 5, 6, 7, 8 | algrp1 15287 |
. . . . . . . . . . 11
|
116 | 4, 5, 6, 7, 8 | algrp1 15287 |
. . . . . . . . . . . 12
|
117 | 58, 116 | sylan2 491 |
. . . . . . . . . . 11
|
118 | 115, 117 | oveq12d 6668 |
. . . . . . . . . 10
|
119 | 118 | breq1d 4663 |
. . . . . . . . 9
|
120 | 94, 114, 119 | 3imtr4d 283 |
. . . . . . . 8
|
121 | 120 | expcom 451 |
. . . . . . 7
|
122 | 121 | a2d 29 |
. . . . . 6
|
123 | 23, 31, 39, 31, 56, 122 | nnind 11038 |
. . . . 5
|
124 | 123 | impcom 446 |
. . . 4
|
125 | 3, 9, 14, 13, 15, 124 | geomcau 33555 |
. . 3
|
126 | | bfp.8 |
. . . 4
|
127 | 126 | cmetcau 23087 |
. . 3
|
128 | 1, 125, 127 | syl2anc 693 |
. 2
|
129 | | metxmet 22139 |
. . . 4
|
130 | 126 | methaus 22325 |
. . . 4
|
131 | 3, 129, 130 | 3syl 18 |
. . 3
|
132 | | lmfun 21185 |
. . 3
|
133 | | funfvbrb 6330 |
. . 3
|
134 | 131, 132,
133 | 3syl 18 |
. 2
|
135 | 128, 134 | mpbid 222 |
1
|