Description: Lemma 1 for lmodfopne . (Contributed by AV, 2-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lmodfopne.t | |
|
lmodfopne.a | |
||
lmodfopne.v | |
||
lmodfopne.s | |
||
lmodfopne.k | |
||
Assertion | lmodfopnelem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodfopne.t | |
|
2 | lmodfopne.a | |
|
3 | lmodfopne.v | |
|
4 | lmodfopne.s | |
|
5 | lmodfopne.k | |
|
6 | 3 4 5 1 | lmodscaf | |
7 | 6 | ffnd | |
8 | 3 2 | plusffn | |
9 | fneq1 | |
|
10 | fndmu | |
|
11 | 10 | ex | |
12 | 9 11 | syl6bi | |
13 | 12 | com13 | |
14 | 13 | impcom | |
15 | 3 | lmodbn0 | |
16 | xp11 | |
|
17 | 15 15 16 | syl2anc | |
18 | 17 | simprbda | |
19 | 18 | expcom | |
20 | 14 19 | syl6 | |
21 | 20 | com23 | |
22 | 21 | ex | |
23 | 22 | com23 | |
24 | 8 23 | ax-mp | |
25 | 7 24 | mpd | |
26 | 25 | imp | |