Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  coe1mul2lem1 Structured version   Unicode version

Theorem coe1mul2lem1 18095
 Description: An equivalence for coe1mul2 18097. (Contributed by Stefan O'Rear, 25-Mar-2015.)
Assertion
Ref Expression
coe1mul2lem1

Proof of Theorem coe1mul2lem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 1on 7137 . . . 4
21a1i 11 . . 3
3 fvex 5875 . . . 4
43a1i 11 . . 3
5 simpll 753 . . 3
6 df1o2 7142 . . . . . 6
7 nn0ex 10800 . . . . . 6
8 0ex 4577 . . . . . 6
96, 7, 8mapsnconst 7464 . . . . 5
109adantl 466 . . . 4
11 fconstmpt 5042 . . . 4
1210, 11syl6eq 2524 . . 3
13 fconstmpt 5042 . . . 4
1413a1i 11 . . 3
152, 4, 5, 12, 14ofrfval2 6540 . 2
16 1n0 7145 . . 3
17 r19.3rzv 3921 . . 3
1816, 17mp1i 12 . 2
19 elmapi 7440 . . . . . 6
20 0lt1o 7154 . . . . . 6
21 ffvelrn 6018 . . . . . 6
2219, 20, 21sylancl 662 . . . . 5
2322adantl 466 . . . 4
2423biantrurd 508 . . 3
25 fznn0 11768 . . . 4