Description: Lemma 2 for 2sqreunn . (Contributed by AV, 25-Jun-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 2sqreulem4.1 | |
|
Assertion | 2sqreunnlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2sqreulem4.1 | |
|
2 | nnssnn0 | |
|
3 | 1 | 2sqreulem4 | |
4 | nfcv | |
|
5 | nfcv | |
|
6 | 4 5 | ssrmof | |
7 | 6 | ralimdv | |
8 | 2 3 7 | mp2 | |
9 | ssralv | |
|
10 | 2 8 9 | mp2 | |