Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmuldfeqlem1 Structured version   Unicode version

Theorem fmuldfeqlem1 31160
 Description: induction step for the proof of fmuldfeq 31161. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
fmuldfeqlem1.1
fmuldfeqlem1.2
fmuldfeqlem1.3
fmuldfeqlem1.5
fmuldfeqlem1.6
fmuldfeqlem1.7
fmuldfeqlem1.8
fmuldfeqlem1.9
fmuldfeqlem1.10
fmuldfeqlem1.11
fmuldfeqlem1.12
fmuldfeqlem1.13
Assertion
Ref Expression
fmuldfeqlem1
Distinct variable groups:   ,,,   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   (,,,)   (,,,)   ()   ()   (,,,)   (,,)   (,)   (,)

Proof of Theorem fmuldfeqlem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6309 . . . . . . . 8
21mptex 6131 . . . . . . 7
3 fmuldfeqlem1.6 . . . . . . . 8
43fvmpt2 5957 . . . . . . 7
52, 4mpan2 671 . . . . . 6
6 fveq2 5866 . . . . . . . 8
76fveq1d 5868 . . . . . . 7
87cbvmptv 4538 . . . . . 6
95, 8syl6eq 2524 . . . . 5
109adantl 466 . . . 4
11 fveq2 5866 . . . . . 6
1211fveq1d 5868 . . . . 5
1312adantl 466 . . . 4
14 fmuldfeqlem1.11 . . . . 5
1514adantr 465 . . . 4
16 fmuldfeqlem1.8 . . . . . . 7
1716, 14ffvelrnd 6022 . . . . . 6
1817ancli 551 . . . . . 6
19 nfcv 2629 . . . . . . 7
20 fmuldfeqlem1.1 . . . . . . . . 9
21 nfv 1683 . . . . . . . . 9
2220, 21nfan 1875 . . . . . . . 8
23 nfv 1683 . . . . . . . 8
2422, 23nfim 1867 . . . . . . 7
25 eleq1 2539 . . . . . . . . 9
2625anbi2d 703 . . . . . . . 8
27 feq1 5713 . . . . . . . 8
2826, 27imbi12d 320 . . . . . . 7
29 fmuldfeqlem1.13 . . . . . . 7
3019, 24, 28, 29vtoclgf 3169 . . . . . 6
3117, 18, 30sylc 60 . . . . 5
3231fnvinran 30995 . . . 4
3310, 13, 15, 32fvmptd 5955 . . 3
3433oveq2d 6300 . 2
35 fmuldfeqlem1.10 . . . . 5
36 elfzuz 11684 . . . . 5
3735, 36syl 16 . . . 4
38 seqp1 12090 . . . 4
3937, 38syl 16 . . 3
41 seqp1 12090 . . . . . . . 8
4237, 41syl 16 . . . . . . 7
43 fmuldfeqlem1.5 . . . . . . . . . 10
44 nfcv 2629 . . . . . . . . . . 11
45 nfcv 2629 . . . . . . . . . . 11
46 nfcv 2629 . . . . . . . . . . 11
47 nfcv 2629 . . . . . . . . . . 11
48 fveq1 5865 . . . . . . . . . . . . 13
49 fveq1 5865 . . . . . . . . . . . . 13
5048, 49oveqan12d 6303 . . . . . . . . . . . 12
5150mpteq2dv 4534 . . . . . . . . . . 11
5244, 45, 46, 47, 51cbvmpt2 6360 . . . . . . . . . 10
5343, 52eqtri 2496 . . . . . . . . 9
5453a1i 11 . . . . . . . 8
55 nfcv 2629 . . . . . . . . . . . . . 14
56 fmuldfeqlem1.3 . . . . . . . . . . . . . . . 16
57 nfmpt1 4536 . . . . . . . . . . . . . . . 16
5856, 56, 57nfmpt2 6350 . . . . . . . . . . . . . . 15
5943, 58nfcxfr 2627 . . . . . . . . . . . . . 14
60 nfcv 2629 . . . . . . . . . . . . . 14
6155, 59, 60nfseq 12085 . . . . . . . . . . . . 13
62 nfcv 2629 . . . . . . . . . . . . 13
6361, 62nffv 5873 . . . . . . . . . . . 12
6463nfeq2 2646 . . . . . . . . . . 11
65 nfv 1683 . . . . . . . . . . 11
6664, 65nfan 1875 . . . . . . . . . 10
67 fveq1 5865 . . . . . . . . . . . 12
6867ad2antrr 725 . . . . . . . . . . 11
69 fveq1 5865 . . . . . . . . . . . 12
7069ad2antlr 726 . . . . . . . . . . 11
7168, 70oveq12d 6302 . . . . . . . . . 10
7266, 71mpteq2da 4532 . . . . . . . . 9
7372adantl 466 . . . . . . . 8
74 eqid 2467 . . . . . . . . 9
75 3simpc 995 . . . . . . . . . 10
76 nfcv 2629 . . . . . . . . . . 11
77 nfcv 2629 . . . . . . . . . . 11
78 nfcv 2629 . . . . . . . . . . 11
79 nfv 1683 . . . . . . . . . . . . 13
80 nfv 1683 . . . . . . . . . . . . 13
8120, 79, 80nf3an 1877 . . . . . . . . . . . 12
82 nfv 1683 . . . . . . . . . . . 12
8381, 82nfim 1867 . . . . . . . . . . 11
84 fmuldfeqlem1.2 . . . . . . . . . . . . 13
85 nfv 1683 . . . . . . . . . . . . 13
86 nfv 1683 . . . . . . . . . . . . 13
8784, 85, 86nf3an 1877 . . . . . . . . . . . 12
88 nfv 1683 . . . . . . . . . . . 12
8987, 88nfim 1867 . . . . . . . . . . 11
90 eleq1 2539 . . . . . . . . . . . . 13
91903anbi2d 1304 . . . . . . . . . . . 12
9248oveq1d 6299 . . . . . . . . . . . . . 14
9392mpteq2dv 4534 . . . . . . . . . . . . 13
9493eleq1d 2536 . . . . . . . . . . . 12
9591, 94imbi12d 320 . . . . . . . . . . 11
96 eleq1 2539 . . . . . . . . . . . . 13
97963anbi3d 1305 . . . . . . . . . . . 12
9849oveq2d 6300 . . . . . . . . . . . . . 14
9998mpteq2dv 4534 . . . . . . . . . . . . 13
10099eleq1d 2536 . . . . . . . . . . . 12
10197, 100imbi12d 320 . . . . . . . . . . 11
102 fmuldfeqlem1.9 . . . . . . . . . . 11
10376, 77, 78, 83, 89, 95, 101, 102vtocl2gf 3173 . . . . . . . . . 10
10475, 103mpcom 36 . . . . . . . . 9
105 fmuldfeqlem1.7 . . . . . . . . 9
10653, 74, 35, 16, 104, 105fmulcl 31159 . . . . . . . 8
107 mptexg 6130 . . . . . . . . 9
108105, 107syl 16 . . . . . . . 8
10954, 73, 106, 17, 108ovmpt2d 6414 . . . . . . 7
11042, 109eqtrd 2508 . . . . . 6
111110fveq1d 5868 . . . . 5
112111adantr 465 . . . 4
113 simpr 461 . . . . 5
114106ancli 551 . . . . . . . 8
115 nfcv 2629 . . . . . . . . . . 11
116 nfmpt21 6348 . . . . . . . . . . . 12
11743, 116nfcxfr 2627 . . . . . . . . . . 11
118 nfcv 2629 . . . . . . . . . . 11
119115, 117, 118nfseq 12085 . . . . . . . . . 10
120 nfcv 2629 . . . . . . . . . 10
121119, 120nffv 5873 . . . . . . . . 9
122121nfel1 2645 . . . . . . . . . . 11
12320, 122nfan 1875 . . . . . . . . . 10
124 nfcv 2629 . . . . . . . . . . 11
125 nfcv 2629 . . . . . . . . . . 11
126121, 124, 125nff 5727 . . . . . . . . . 10
127123, 126nfim 1867 . . . . . . . . 9
128 eleq1 2539 . . . . . . . . . . 11
129128anbi2d 703 . . . . . . . . . 10
130 feq1 5713 . . . . . . . . . 10
131129, 130imbi12d 320 . . . . . . . . 9
132121, 127, 131, 29vtoclgf 3169 . . . . . . . 8
133106, 114, 132sylc 60 . . . . . . 7
134133fnvinran 30995 . . . . . 6
135134, 32remulcld 9624 . . . . 5
136 eqid 2467 . . . . . 6
137136fvmpt2 5957 . . . . 5
138113, 135, 137syl2anc 661 . . . 4
139112, 138eqtrd 2508 . . 3
140 fmuldfeqlem1.12 . . . . 5
141140oveq1d 6299 . . . 4