Description: A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | sqoddm1div8z | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | odd2np1 | |
|
2 | 1 | biimpa | |
3 | eqcom | |
|
4 | sqoddm1div8 | |
|
5 | 4 | adantll | |
6 | mulsucdiv2z | |
|
7 | 6 | ad2antlr | |
8 | 5 7 | eqeltrd | |
9 | 8 | ex | |
10 | 3 9 | syl5bi | |
11 | 10 | rexlimdva | |
12 | 2 11 | mpd | |