axlowdimlem13

Description: Lemma for axlowdim . Establish that P and Q are different points. (Contributed by Scott Fenton, 21-Apr-2013)

	Ref	Expression
Hypotheses	axlowdimlem13.1	$⊢ P = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
	axlowdimlem13.2	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
Assertion	axlowdimlem13	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to P \neq Q$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem13.1	$⊢ P = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
2		axlowdimlem13.2	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
3		2ne0	$⊢ 2 \neq 0$
4	3	neii	$⊢ \neg 2 = 0$
5		eqcom	$⊢ 2 = 0 \leftrightarrow 0 = 2$
6		1pneg1e0	$⊢ 1 + -1 = 0$
7	6	eqcomi	$⊢ 0 = 1 + -1$
8		df-2	$⊢ 2 = 1 + 1$
9	7 8	eqeq12i	$⊢ 0 = 2 \leftrightarrow 1 + -1 = 1 + 1$
10		ax-1cn	$⊢ 1 \in ℂ$
11		neg1cn	$⊢ - 1 \in ℂ$
12	10 11 10	addcani	$⊢ 1 + -1 = 1 + 1 \leftrightarrow - 1 = 1$
13	5 9 12	3bitri	$⊢ 2 = 0 \leftrightarrow - 1 = 1$
14	4 13	mtbi	$⊢ \neg - 1 = 1$
15	14	intnanr	$⊢ \neg (- 1 = 1 \land 0 = 0)$
16		ax-1ne0	$⊢ 1 \neq 0$
17	16	neii	$⊢ \neg 1 = 0$
18		negeq0	$⊢ 1 \in ℂ \to (1 = 0 \leftrightarrow - 1 = 0)$
19	10 18	ax-mp	$⊢ 1 = 0 \leftrightarrow - 1 = 0$
20	17 19	mtbi	$⊢ \neg - 1 = 0$
21	20	intnanr	$⊢ \neg (- 1 = 0 \land 0 = 1)$
22	15 21	pm3.2ni	$⊢ \neg ((- 1 = 1 \land 0 = 0) \lor (- 1 = 0 \land 0 = 1))$
23		negex	$⊢ - 1 \in V$
24		c0ex	$⊢ 0 \in V$
25		1ex	$⊢ 1 \in V$
26	23 24 25 24	preq12b	$⊢ \{- 1, 0\} = \{1, 0\} \leftrightarrow ((- 1 = 1 \land 0 = 0) \lor (- 1 = 0 \land 0 = 1))$
27	22 26	mtbir	$⊢ \neg \{- 1, 0\} = \{1, 0\}$
28		3ex	$⊢ 3 \in V$
29	28	rnsnop	$⊢ ran \{⟨3, - 1⟩\} = \{- 1\}$
30	29	a1i	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran \{⟨3, - 1⟩\} = \{- 1\}$
31		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
32		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
33	31 32	sylbi	$⊢ N \in ℕ \to 1 \in (1 \dots N)$
34		df-3	$⊢ 3 = 2 + 1$
35		1e0p1	$⊢ 1 = 0 + 1$
36	34 35	eqeq12i	$⊢ 3 = 1 \leftrightarrow 2 + 1 = 0 + 1$
37		2cn	$⊢ 2 \in ℂ$
38		0cn	$⊢ 0 \in ℂ$
39	37 38 10	addcan2i	$⊢ 2 + 1 = 0 + 1 \leftrightarrow 2 = 0$
40	36 39	bitri	$⊢ 3 = 1 \leftrightarrow 2 = 0$
41	40	necon3bii	$⊢ 3 \neq 1 \leftrightarrow 2 \neq 0$
42	3 41	mpbir	$⊢ 3 \neq 1$
43	42	necomi	$⊢ 1 \neq 3$
44		eldifsn	$⊢ 1 \in ((1 \dots N) ∖ \{3\}) \leftrightarrow (1 \in (1 \dots N) \land 1 \neq 3)$
45	33 43 44	sylanblrc	$⊢ N \in ℕ \to 1 \in ((1 \dots N) ∖ \{3\})$
46	45	adantr	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to 1 \in ((1 \dots N) ∖ \{3\})$
47		ne0i	$⊢ 1 \in ((1 \dots N) ∖ \{3\}) \to (1 \dots N) ∖ \{3\} \neq \emptyset$
48		rnxp	$⊢ (1 \dots N) ∖ \{3\} \neq \emptyset \to ran (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{0\}$
49	46 47 48	3syl	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{0\}$
50	30 49	uneq12d	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran \{⟨3, - 1⟩\} \cup ran (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{- 1\} \cup \{0\}$
51		rnun	$⊢ ran (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})) = ran \{⟨3, - 1⟩\} \cup ran (((1 \dots N) ∖ \{3\}) \times \{0\})$
52		df-pr	$⊢ \{- 1, 0\} = \{- 1\} \cup \{0\}$
53	50 51 52	3eqtr4g	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})) = \{- 1, 0\}$
54		ovex	$⊢ I + 1 \in V$
55	54	rnsnop	$⊢ ran \{⟨I + 1, 1⟩\} = \{1\}$
56	55	a1i	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran \{⟨I + 1, 1⟩\} = \{1\}$
57		nnz	$⊢ N \in ℕ \to N \in ℤ$
58		fzssp1	$⊢ (1 \dots N - 1) \subseteq (1 \dots N - 1 + 1)$
59		zcn	$⊢ N \in ℤ \to N \in ℂ$
60		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
61	60	oveq2d	$⊢ N \in ℂ \to (1 \dots N - 1 + 1) = (1 \dots N)$
62	59 61	syl	$⊢ N \in ℤ \to (1 \dots N - 1 + 1) = (1 \dots N)$
63	58 62	sseqtrid	$⊢ N \in ℤ \to (1 \dots N - 1) \subseteq (1 \dots N)$
64	57 63	syl	$⊢ N \in ℕ \to (1 \dots N - 1) \subseteq (1 \dots N)$
65	64	sselda	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to I \in (1 \dots N)$
66		elfzelz	$⊢ I \in (1 \dots N - 1) \to I \in ℤ$
67	66	zred	$⊢ I \in (1 \dots N - 1) \to I \in ℝ$
68		id	$⊢ I \in ℝ \to I \in ℝ$
69		ltp1	$⊢ I \in ℝ \to I < I + 1$
70	68 69	ltned	$⊢ I \in ℝ \to I \neq I + 1$
71	67 70	syl	$⊢ I \in (1 \dots N - 1) \to I \neq I + 1$
72	71	adantl	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to I \neq I + 1$
73		eldifsn	$⊢ I \in ((1 \dots N) ∖ \{I + 1\}) \leftrightarrow (I \in (1 \dots N) \land I \neq I + 1)$
74	65 72 73	sylanbrc	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to I \in ((1 \dots N) ∖ \{I + 1\})$
75		ne0i	$⊢ I \in ((1 \dots N) ∖ \{I + 1\}) \to (1 \dots N) ∖ \{I + 1\} \neq \emptyset$
76		rnxp	$⊢ (1 \dots N) ∖ \{I + 1\} \neq \emptyset \to ran (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) = \{0\}$
77	74 75 76	3syl	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) = \{0\}$
78	56 77	uneq12d	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran \{⟨I + 1, 1⟩\} \cup ran (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) = \{1\} \cup \{0\}$
79		rnun	$⊢ ran (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) = ran \{⟨I + 1, 1⟩\} \cup ran (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
80		df-pr	$⊢ \{1, 0\} = \{1\} \cup \{0\}$
81	78 79 80	3eqtr4g	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to ran (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) = \{1, 0\}$
82	53 81	eqeq12d	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to (ran (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})) = ran (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})) \leftrightarrow \{- 1, 0\} = \{1, 0\})$
83	27 82	mtbiri	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to \neg ran (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})) = ran (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\}))$
84		rneq	$⊢ \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\}) \to ran (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})) = ran (\{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\}))$
85	83 84	nsyl	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to \neg \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
86	1 2	eqeq12i	$⊢ P = Q \leftrightarrow \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
87	86	necon3abii	$⊢ P \neq Q \leftrightarrow \neg \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
88	85 87	sylibr	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to P \neq Q$

Metamath Proof Explorer

Theorem axlowdimlem13

Proof