Theorem nn0opthi

Description: An ordered pair theorem for nonnegative integers. Theorem 17.3 of Quine p. 124. We can represent an ordered pair of nonnegative integers A and B by ( ( ( A + B ) x. ( A + B ) ) + B ) . If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op that works for any set. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by Scott Fenton, 8-Sep-2010)

	Ref	Expression
Hypotheses	nn0opth.1	$$⊢A\in {\mathbb{N}}_0$$
	nn0opth.2	$$⊢B\in {\mathbb{N}}_0$$
	nn0opth.3	$$⊢C\in {\mathbb{N}}_0$$
	nn0opth.4	$$⊢D\in {\mathbb{N}}_0$$
Assertion	nn0opthi	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\leftrightarrow \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0opth.1	$$⊢A\in {\mathbb{N}}_0$$
2		nn0opth.2	$$⊢B\in {\mathbb{N}}_0$$
3		nn0opth.3	$$⊢C\in {\mathbb{N}}_0$$
4		nn0opth.4	$$⊢D\in {\mathbb{N}}_0$$
5	1 2	nn0addcli	$$⊢A+B\in {\mathbb{N}}_0$$
6	5	nn0rei	$$⊢A+B\in ℝ$$
7	3 4	nn0addcli	$$⊢C+D\in {\mathbb{N}}_0$$
8	7	nn0rei	$$⊢C+D\in ℝ$$
9	6 8	lttri2i	$$⊢A+B\ne C+D\leftrightarrow \left(A+B<C+D\vee C+D<A+B\right)$$
10	1 2 7 4	nn0opthlem2	$$⊢A+B<C+D\to \left(C+D\right)\left(C+D\right)+D\ne \left(A+B\right)\left(A+B\right)+B$$
11	10	necomd	$$⊢A+B<C+D\to \left(A+B\right)\left(A+B\right)+B\ne \left(C+D\right)\left(C+D\right)+D$$
12	3 4 5 2	nn0opthlem2	$$⊢C+D<A+B\to \left(A+B\right)\left(A+B\right)+B\ne \left(C+D\right)\left(C+D\right)+D$$
13	11 12	jaoi	$$⊢\left(A+B<C+D\vee C+D<A+B\right)\to \left(A+B\right)\left(A+B\right)+B\ne \left(C+D\right)\left(C+D\right)+D$$
14	9 13	sylbi	$$⊢A+B\ne C+D\to \left(A+B\right)\left(A+B\right)+B\ne \left(C+D\right)\left(C+D\right)+D$$
15	14	necon4i	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to A+B=C+D$$
16		id	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to \left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D$$
17	15 15	oveq12d	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to \left(A+B\right)\left(A+B\right)=\left(C+D\right)\left(C+D\right)$$
18	17	oveq1d	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to \left(A+B\right)\left(A+B\right)+D=\left(C+D\right)\left(C+D\right)+D$$
19	16 18	eqtr4d	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to \left(A+B\right)\left(A+B\right)+B=\left(A+B\right)\left(A+B\right)+D$$
20	5	nn0cni	$$⊢A+B\in ℂ$$
21	20 20	mulcli	$$⊢\left(A+B\right)\left(A+B\right)\in ℂ$$
22	2	nn0cni	$$⊢B\in ℂ$$
23	4	nn0cni	$$⊢D\in ℂ$$
24	21 22 23	addcani	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(A+B\right)\left(A+B\right)+D\leftrightarrow B=D$$
25	19 24	sylib	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to B=D$$
26	25	oveq2d	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to C+B=C+D$$
27	15 26	eqtr4d	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to A+B=C+B$$
28	1	nn0cni	$$⊢A\in ℂ$$
29	3	nn0cni	$$⊢C\in ℂ$$
30	28 29 22	addcan2i	$$⊢A+B=C+B\leftrightarrow A=C$$
31	27 30	sylib	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to A=C$$
32	31 25	jca	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\to \left(A=C\wedge B=D\right)$$
33		oveq12	$$⊢\left(A=C\wedge B=D\right)\to A+B=C+D$$
34	33 33	oveq12d	$$⊢\left(A=C\wedge B=D\right)\to \left(A+B\right)\left(A+B\right)=\left(C+D\right)\left(C+D\right)$$
35		simpr	$$⊢\left(A=C\wedge B=D\right)\to B=D$$
36	34 35	oveq12d	$$⊢\left(A=C\wedge B=D\right)\to \left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D$$
37	32 36	impbii	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\leftrightarrow \left(A=C\wedge B=D\right)$$