Theorem nnoALTV

Description: An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020) (Revised by AV, 21-Jun-2020)

	Ref	Expression
Assertion	nnoALTV	|- ( ( N e. ( ZZ>= ` 2 ) /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		oddm1div2z	|- ( N e. Odd -> ( ( N - 1 ) / 2 ) e. ZZ )
2	1	adantl	|- ( ( N e. ( ZZ>= ` 2 ) /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. ZZ )
3		eluz2b1	|- ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )
4		1red	|- ( N e. ZZ -> 1 e. RR )
5		zre	|- ( N e. ZZ -> N e. RR )
6	4 5	posdifd	|- ( N e. ZZ -> ( 1 < N <-> 0 < ( N - 1 ) ) )
7	6	biimpa	|- ( ( N e. ZZ /\ 1 < N ) -> 0 < ( N - 1 ) )
8		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
9	8	zred	|- ( N e. ZZ -> ( N - 1 ) e. RR )
10		2re	|- 2 e. RR
11	10	a1i	|- ( N e. ZZ -> 2 e. RR )
12		2pos	|- 0 < 2
13	12	a1i	|- ( N e. ZZ -> 0 < 2 )
14	9 11 13	3jca	|- ( N e. ZZ -> ( ( N - 1 ) e. RR /\ 2 e. RR /\ 0 < 2 ) )
15	14	adantr	|- ( ( N e. ZZ /\ 1 < N ) -> ( ( N - 1 ) e. RR /\ 2 e. RR /\ 0 < 2 ) )
16		gt0div	|- ( ( ( N - 1 ) e. RR /\ 2 e. RR /\ 0 < 2 ) -> ( 0 < ( N - 1 ) <-> 0 < ( ( N - 1 ) / 2 ) ) )
17	15 16	syl	|- ( ( N e. ZZ /\ 1 < N ) -> ( 0 < ( N - 1 ) <-> 0 < ( ( N - 1 ) / 2 ) ) )
18	7 17	mpbid	|- ( ( N e. ZZ /\ 1 < N ) -> 0 < ( ( N - 1 ) / 2 ) )
19	3 18	sylbi	|- ( N e. ( ZZ>= ` 2 ) -> 0 < ( ( N - 1 ) / 2 ) )
20	19	adantr	|- ( ( N e. ( ZZ>= ` 2 ) /\ N e. Odd ) -> 0 < ( ( N - 1 ) / 2 ) )
21		elnnz	|- ( ( ( N - 1 ) / 2 ) e. NN <-> ( ( ( N - 1 ) / 2 ) e. ZZ /\ 0 < ( ( N - 1 ) / 2 ) ) )
22	2 20 21	sylanbrc	|- ( ( N e. ( ZZ>= ` 2 ) /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN )