Theorem nnneo

Description: If a natural number is even, its successor is odd. (Contributed by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	nnneo	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ¬ suc 𝐶 = ( 2o ·o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		onnbtwn	⊢ ( 𝐴 ∈ On → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ω → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
5		suceq	⊢ ( 𝐶 = ( 2o ·o 𝐴 ) → suc 𝐶 = suc ( 2o ·o 𝐴 ) )
6	5	eqeq1d	⊢ ( 𝐶 = ( 2o ·o 𝐴 ) → ( suc 𝐶 = ( 2o ·o 𝐵 ) ↔ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) )
7	6	3ad2ant3	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ( suc 𝐶 = ( 2o ·o 𝐵 ) ↔ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) )
8		ovex	⊢ ( 2o ·o 𝐴 ) ∈ V
9	8	sucid	⊢ ( 2o ·o 𝐴 ) ∈ suc ( 2o ·o 𝐴 )
10		eleq2	⊢ ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( ( 2o ·o 𝐴 ) ∈ suc ( 2o ·o 𝐴 ) ↔ ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) ) )
11	9 10	mpbii	⊢ ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) )
12		2onn	⊢ 2o ∈ ω
13		nnmord	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 2o ∈ ω ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) ) )
14	12 13	mp3an3	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) ) )
15		simpl	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 2o ) → 𝐴 ∈ 𝐵 )
16	14 15	biimtrrdi	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) → 𝐴 ∈ 𝐵 ) )
17	11 16	syl5	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → 𝐴 ∈ 𝐵 ) )
18		simpr	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) )
19		nnmcl	⊢ ( ( 2o ∈ ω ∧ 𝐴 ∈ ω ) → ( 2o ·o 𝐴 ) ∈ ω )
20	12 19	mpan	⊢ ( 𝐴 ∈ ω → ( 2o ·o 𝐴 ) ∈ ω )
21		nnon	⊢ ( ( 2o ·o 𝐴 ) ∈ ω → ( 2o ·o 𝐴 ) ∈ On )
22		oa1suc	⊢ ( ( 2o ·o 𝐴 ) ∈ On → ( ( 2o ·o 𝐴 ) +o 1o ) = suc ( 2o ·o 𝐴 ) )
23	20 21 22	3syl	⊢ ( 𝐴 ∈ ω → ( ( 2o ·o 𝐴 ) +o 1o ) = suc ( 2o ·o 𝐴 ) )
24		1oex	⊢ 1o ∈ V
25	24	sucid	⊢ 1o ∈ suc 1o
26		df-2o	⊢ 2o = suc 1o
27	25 26	eleqtrri	⊢ 1o ∈ 2o
28		1onn	⊢ 1o ∈ ω
29		nnaord	⊢ ( ( 1o ∈ ω ∧ 2o ∈ ω ∧ ( 2o ·o 𝐴 ) ∈ ω ) → ( 1o ∈ 2o ↔ ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( ( 2o ·o 𝐴 ) +o 2o ) ) )
30	28 12 20 29	mp3an12i	⊢ ( 𝐴 ∈ ω → ( 1o ∈ 2o ↔ ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( ( 2o ·o 𝐴 ) +o 2o ) ) )
31	27 30	mpbii	⊢ ( 𝐴 ∈ ω → ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( ( 2o ·o 𝐴 ) +o 2o ) )
32		nnmsuc	⊢ ( ( 2o ∈ ω ∧ 𝐴 ∈ ω ) → ( 2o ·o suc 𝐴 ) = ( ( 2o ·o 𝐴 ) +o 2o ) )
33	12 32	mpan	⊢ ( 𝐴 ∈ ω → ( 2o ·o suc 𝐴 ) = ( ( 2o ·o 𝐴 ) +o 2o ) )
34	31 33	eleqtrrd	⊢ ( 𝐴 ∈ ω → ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( 2o ·o suc 𝐴 ) )
35	23 34	eqeltrrd	⊢ ( 𝐴 ∈ ω → suc ( 2o ·o 𝐴 ) ∈ ( 2o ·o suc 𝐴 ) )
36	35	ad2antrr	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → suc ( 2o ·o 𝐴 ) ∈ ( 2o ·o suc 𝐴 ) )
37	18 36	eqeltrrd	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) )
38		peano2	⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
39		nnmord	⊢ ( ( 𝐵 ∈ ω ∧ suc 𝐴 ∈ ω ∧ 2o ∈ ω ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
40	12 39	mp3an3	⊢ ( ( 𝐵 ∈ ω ∧ suc 𝐴 ∈ ω ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
41	38 40	sylan2	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
42	41	ancoms	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
43	42	adantr	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
44	37 43	mpbird	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) )
45	44	simpld	⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → 𝐵 ∈ suc 𝐴 )
46	45	ex	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → 𝐵 ∈ suc 𝐴 ) )
47	17 46	jcad	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) ) )
48	47	3adant3	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) ) )
49	7 48	sylbid	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ( suc 𝐶 = ( 2o ·o 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) ) )
50	4 49	mtod	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ¬ suc 𝐶 = ( 2o ·o 𝐵 ) )