Step | Hyp | Ref
| Expression |
1 | | fmul01.6 |
. 2
|
2 | | fveq2 6191 |
. . . . . 6
|
3 | 2 | breq2d 4665 |
. . . . 5
|
4 | 2 | breq1d 4663 |
. . . . 5
|
5 | 3, 4 | anbi12d 747 |
. . . 4
|
6 | 5 | imbi2d 330 |
. . 3
|
7 | | fveq2 6191 |
. . . . . 6
|
8 | 7 | breq2d 4665 |
. . . . 5
|
9 | 7 | breq1d 4663 |
. . . . 5
|
10 | 8, 9 | anbi12d 747 |
. . . 4
|
11 | 10 | imbi2d 330 |
. . 3
|
12 | | fveq2 6191 |
. . . . . 6
|
13 | 12 | breq2d 4665 |
. . . . 5
|
14 | 12 | breq1d 4663 |
. . . . 5
|
15 | 13, 14 | anbi12d 747 |
. . . 4
|
16 | 15 | imbi2d 330 |
. . 3
|
17 | | fveq2 6191 |
. . . . . 6
|
18 | 17 | breq2d 4665 |
. . . . 5
|
19 | 17 | breq1d 4663 |
. . . . 5
|
20 | 18, 19 | anbi12d 747 |
. . . 4
|
21 | 20 | imbi2d 330 |
. . 3
|
22 | | fmul01.4 |
. . . . . . . . . 10
|
23 | 22 | zred 11482 |
. . . . . . . . 9
|
24 | 23 | leidd 10594 |
. . . . . . . 8
|
25 | | fmul01.5 |
. . . . . . . . 9
|
26 | | eluzelz 11697 |
. . . . . . . . . . 11
|
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
|
28 | | eluz 11701 |
. . . . . . . . . 10
|
29 | 22, 27, 28 | syl2anc 693 |
. . . . . . . . 9
|
30 | 25, 29 | mpbid 222 |
. . . . . . . 8
|
31 | | elfz 12332 |
. . . . . . . . 9
|
32 | 22, 22, 27, 31 | syl3anc 1326 |
. . . . . . . 8
|
33 | 24, 30, 32 | mpbir2and 957 |
. . . . . . 7
|
34 | 33 | ancli 574 |
. . . . . . 7
|
35 | | fmul01.2 |
. . . . . . . . . 10
|
36 | | nfv 1843 |
. . . . . . . . . 10
|
37 | 35, 36 | nfan 1828 |
. . . . . . . . 9
|
38 | | nfcv 2764 |
. . . . . . . . . 10
|
39 | | nfcv 2764 |
. . . . . . . . . 10
|
40 | | fmul01.1 |
. . . . . . . . . . 11
|
41 | | nfcv 2764 |
. . . . . . . . . . 11
|
42 | 40, 41 | nffv 6198 |
. . . . . . . . . 10
|
43 | 38, 39, 42 | nfbr 4699 |
. . . . . . . . 9
|
44 | 37, 43 | nfim 1825 |
. . . . . . . 8
|
45 | | eleq1 2689 |
. . . . . . . . . 10
|
46 | 45 | anbi2d 740 |
. . . . . . . . 9
|
47 | | fveq2 6191 |
. . . . . . . . . 10
|
48 | 47 | breq2d 4665 |
. . . . . . . . 9
|
49 | 46, 48 | imbi12d 334 |
. . . . . . . 8
|
50 | | fmul01.8 |
. . . . . . . 8
|
51 | 44, 49, 50 | vtoclg1f 3265 |
. . . . . . 7
|
52 | 33, 34, 51 | sylc 65 |
. . . . . 6
|
53 | | fmul01.3 |
. . . . . . . 8
|
54 | 53 | fveq1i 6192 |
. . . . . . 7
|
55 | | seq1 12814 |
. . . . . . . 8
|
56 | 22, 55 | syl 17 |
. . . . . . 7
|
57 | 54, 56 | syl5eq 2668 |
. . . . . 6
|
58 | 52, 57 | breqtrrd 4681 |
. . . . 5
|
59 | | nfcv 2764 |
. . . . . . . . . 10
|
60 | 42, 39, 59 | nfbr 4699 |
. . . . . . . . 9
|
61 | 37, 60 | nfim 1825 |
. . . . . . . 8
|
62 | 47 | breq1d 4663 |
. . . . . . . . 9
|
63 | 46, 62 | imbi12d 334 |
. . . . . . . 8
|
64 | | fmul01.9 |
. . . . . . . 8
|
65 | 61, 63, 64 | vtoclg1f 3265 |
. . . . . . 7
|
66 | 33, 34, 65 | sylc 65 |
. . . . . 6
|
67 | 57, 66 | eqbrtrd 4675 |
. . . . 5
|
68 | 58, 67 | jca 554 |
. . . 4
|
69 | 68 | a1i 11 |
. . 3
|
70 | | elfzouz 12474 |
. . . . . . . . . 10
..^
|
71 | 70 | 3ad2ant1 1082 |
. . . . . . . . 9
..^
|
72 | | simpl3 1066 |
. . . . . . . . . 10
..^
|
73 | | elfzouz2 12484 |
. . . . . . . . . . . . 13
..^
|
74 | | fzss2 12381 |
. . . . . . . . . . . . 13
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
..^
|
76 | 75 | 3ad2ant1 1082 |
. . . . . . . . . . 11
..^
|
77 | 76 | sselda 3603 |
. . . . . . . . . 10
..^
|
78 | | nfv 1843 |
. . . . . . . . . . . . 13
|
79 | 35, 78 | nfan 1828 |
. . . . . . . . . . . 12
|
80 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
81 | 40, 80 | nffv 6198 |
. . . . . . . . . . . . 13
|
82 | 81 | nfel1 2779 |
. . . . . . . . . . . 12
|
83 | 79, 82 | nfim 1825 |
. . . . . . . . . . 11
|
84 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
85 | 84 | anbi2d 740 |
. . . . . . . . . . . 12
|
86 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
87 | 86 | eleq1d 2686 |
. . . . . . . . . . . 12
|
88 | 85, 87 | imbi12d 334 |
. . . . . . . . . . 11
|
89 | | fmul01.7 |
. . . . . . . . . . 11
|
90 | 83, 88, 89 | chvar 2262 |
. . . . . . . . . 10
|
91 | 72, 77, 90 | syl2anc 693 |
. . . . . . . . 9
..^
|
92 | | remulcl 10021 |
. . . . . . . . . 10
|
93 | 92 | adantl 482 |
. . . . . . . . 9
..^
|
94 | 71, 91, 93 | seqcl 12821 |
. . . . . . . 8
..^
|
95 | | simp3 1063 |
. . . . . . . . 9
..^
|
96 | | fzofzp1 12565 |
. . . . . . . . . 10
..^
|
97 | 96 | 3ad2ant1 1082 |
. . . . . . . . 9
..^
|
98 | | nfv 1843 |
. . . . . . . . . . . . 13
|
99 | 35, 98 | nfan 1828 |
. . . . . . . . . . . 12
|
100 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
101 | 40, 100 | nffv 6198 |
. . . . . . . . . . . . 13
|
102 | 101 | nfel1 2779 |
. . . . . . . . . . . 12
|
103 | 99, 102 | nfim 1825 |
. . . . . . . . . . 11
|
104 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
105 | 104 | anbi2d 740 |
. . . . . . . . . . . 12
|
106 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
107 | 106 | eleq1d 2686 |
. . . . . . . . . . . 12
|
108 | 105, 107 | imbi12d 334 |
. . . . . . . . . . 11
|
109 | 103, 108,
89 | vtoclg1f 3265 |
. . . . . . . . . 10
|
110 | 109 | anabsi7 860 |
. . . . . . . . 9
|
111 | 95, 97, 110 | syl2anc 693 |
. . . . . . . 8
..^
|
112 | | pm3.35 611 |
. . . . . . . . . . . 12
|
113 | 112 | ancoms 469 |
. . . . . . . . . . 11
|
114 | | simpl 473 |
. . . . . . . . . . 11
|
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
|
116 | 115 | 3adant1 1079 |
. . . . . . . . 9
..^
|
117 | 53 | fveq1i 6192 |
. . . . . . . . 9
|
118 | 116, 117 | syl6breq 4694 |
. . . . . . . 8
..^
|
119 | | simp1 1061 |
. . . . . . . . 9
..^
..^ |
120 | 96 | adantl 482 |
. . . . . . . . . 10
..^ |
121 | | simpl 473 |
. . . . . . . . . . 11
..^ |
122 | 121, 120 | jca 554 |
. . . . . . . . . 10
..^ |
123 | 38, 39, 101 | nfbr 4699 |
. . . . . . . . . . . 12
|
124 | 99, 123 | nfim 1825 |
. . . . . . . . . . 11
|
125 | 106 | breq2d 4665 |
. . . . . . . . . . . 12
|
126 | 105, 125 | imbi12d 334 |
. . . . . . . . . . 11
|
127 | 124, 126,
50 | vtoclg1f 3265 |
. . . . . . . . . 10
|
128 | 120, 122,
127 | sylc 65 |
. . . . . . . . 9
..^ |
129 | 95, 119, 128 | syl2anc 693 |
. . . . . . . 8
..^
|
130 | 94, 111, 118, 129 | mulge0d 10604 |
. . . . . . 7
..^
|
131 | | seqp1 12816 |
. . . . . . . 8
|
132 | 71, 131 | syl 17 |
. . . . . . 7
..^
|
133 | 130, 132 | breqtrrd 4681 |
. . . . . 6
..^
|
134 | 53 | fveq1i 6192 |
. . . . . 6
|
135 | 133, 134 | syl6breqr 4695 |
. . . . 5
..^
|
136 | 94, 111 | remulcld 10070 |
. . . . . . . 8
..^
|
137 | | 1red 10055 |
. . . . . . . 8
..^
|
138 | 95, 97 | jca 554 |
. . . . . . . . . . 11
..^
|
139 | 101, 39, 59 | nfbr 4699 |
. . . . . . . . . . . . 13
|
140 | 99, 139 | nfim 1825 |
. . . . . . . . . . . 12
|
141 | 106 | breq1d 4663 |
. . . . . . . . . . . . 13
|
142 | 105, 141 | imbi12d 334 |
. . . . . . . . . . . 12
|
143 | 140, 142,
64 | vtoclg1f 3265 |
. . . . . . . . . . 11
|
144 | 97, 138, 143 | sylc 65 |
. . . . . . . . . 10
..^
|
145 | 111, 137,
94, 118, 144 | lemul2ad 10964 |
. . . . . . . . 9
..^
|
146 | 94 | recnd 10068 |
. . . . . . . . . 10
..^
|
147 | 146 | mulid1d 10057 |
. . . . . . . . 9
..^
|
148 | 145, 147 | breqtrd 4679 |
. . . . . . . 8
..^
|
149 | | simp2 1062 |
. . . . . . . . . 10
..^
|
150 | 112 | simprd 479 |
. . . . . . . . . 10
|
151 | 95, 149, 150 | syl2anc 693 |
. . . . . . . . 9
..^
|
152 | 117, 151 | syl5eqbrr 4689 |
. . . . . . . 8
..^
|
153 | 136, 94, 137, 148, 152 | letrd 10194 |
. . . . . . 7
..^
|
154 | 132, 153 | eqbrtrd 4675 |
. . . . . 6
..^
|
155 | 134, 154 | syl5eqbr 4688 |
. . . . 5
..^
|
156 | 135, 155 | jca 554 |
. . . 4
..^
|
157 | 156 | 3exp 1264 |
. . 3
..^
|
158 | 6, 11, 16, 21, 69, 157 | fzind2 12586 |
. 2
|
159 | 1, 158 | mpcom 38 |
1
|