Metamath Proof Explorer

Theorem 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∪1…N∖3×0
axlowdimlem13.2 ⊢Q=I+11∪1…N∖I+1×0
Assertion axlowdimlem13 ⊢N∈ℕ∧I∈1…N−1→P≠Q

Proof

Step Hyp Ref Expression
1 axlowdimlem13.1 ⊢P=3−1∪1…N∖3×0
2 axlowdimlem13.2 ⊢Q=I+11∪1…N∖I+1×0
3 2ne0 ⊢2≠0
4 3 neii ⊢¬2=0
5 eqcom ⊢2=0↔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↔1+-1=1+1
10 ax-1cn ⊢1∈ℂ
11 neg1cn ⊢−1∈ℂ
12 10 11 10 addcani ⊢1+-1=1+1↔−1=1
13 5 9 12 3bitri ⊢2=0↔−1=1
14 4 13 mtbi ⊢¬−1=1
15 14 intnanr ⊢¬−1=1∧0=0
16 ax-1ne0 ⊢1≠0
17 16 neii ⊢¬1=0
18 negeq0 ⊢1∈ℂ→1=0↔−1=0
19 10 18 ax-mp ⊢1=0↔−1=0
20 17 19 mtbi ⊢¬−1=0
21 20 intnanr ⊢¬−1=0∧0=1
22 15 21 pm3.2ni ⊢¬−1=1∧0=0∨−1=0∧0=1
23 negex ⊢−1∈V
24 c0ex ⊢0∈V
25 1ex ⊢1∈V
26 23 24 25 24 preq12b ⊢−10=10↔−1=1∧0=0∨−1=0∧0=1
27 22 26 mtbir ⊢¬−10=10
28 3ex ⊢3∈V
29 28 rnsnop ⊢ran⁡3−1=−1
30 29 a1i ⊢N∈ℕ∧I∈1…N−1→ran⁡3−1=−1
31 elnnuz ⊢N∈ℕ↔N∈ℤ≥1
32 eluzfz1 ⊢N∈ℤ≥1→1∈1…N
33 31 32 sylbi ⊢N∈ℕ→1∈1…N
34 df-3 ⊢3=2+1
35 1e0p1 ⊢1=0+1
36 34 35 eqeq12i ⊢3=1↔2+1=0+1
37 2cn ⊢2∈ℂ
38 0cn ⊢0∈ℂ
39 37 38 10 addcan2i ⊢2+1=0+1↔2=0
40 36 39 bitri ⊢3=1↔2=0
41 40 necon3bii ⊢3≠1↔2≠0
42 3 41 mpbir ⊢3≠1
43 42 necomi ⊢1≠3
44 eldifsn ⊢1∈1…N∖3↔1∈1…N∧1≠3
45 33 43 44 sylanblrc ⊢N∈ℕ→1∈1…N∖3
46 45 adantr ⊢N∈ℕ∧I∈1…N−1→1∈1…N∖3
47 ne0i ⊢1∈1…N∖3→1…N∖3≠∅
48 rnxp ⊢1…N∖3≠∅→ran⁡1…N∖3×0=0
49 46 47 48 3syl ⊢N∈ℕ∧I∈1…N−1→ran⁡1…N∖3×0=0
50 30 49 uneq12d ⊢N∈ℕ∧I∈1…N−1→ran⁡3−1∪ran⁡1…N∖3×0=−1∪0
51 rnun ⊢ran⁡3−1∪1…N∖3×0=ran⁡3−1∪ran⁡1…N∖3×0
52 df-pr ⊢−10=−1∪0
53 50 51 52 3eqtr4g ⊢N∈ℕ∧I∈1…N−1→ran⁡3−1∪1…N∖3×0=−10
54 ovex ⊢I+1∈V
55 54 rnsnop ⊢ran⁡I+11=1
56 55 a1i ⊢N∈ℕ∧I∈1…N−1→ran⁡I+11=1
57 nnz ⊢N∈ℕ→N∈ℤ
58 fzssp1 ⊢1…N−1⊆1…N-1+1
59 zcn ⊢N∈ℤ→N∈ℂ
60 npcan1 ⊢N∈ℂ→N-1+1=N
61 60 oveq2d ⊢N∈ℂ→1…N-1+1=1…N
62 59 61 syl ⊢N∈ℤ→1…N-1+1=1…N
63 58 62 sseqtrid ⊢N∈ℤ→1…N−1⊆1…N
64 57 63 syl ⊢N∈ℕ→1…N−1⊆1…N
65 64 sselda ⊢N∈ℕ∧I∈1…N−1→I∈1…N
66 elfzelz ⊢I∈1…N−1→I∈ℤ
67 66 zred ⊢I∈1…N−1→I∈ℝ
68 id ⊢I∈ℝ→I∈ℝ
69 ltp1 ⊢I∈ℝ→I<I+1
70 68 69 ltned ⊢I∈ℝ→I≠I+1
71 67 70 syl ⊢I∈1…N−1→I≠I+1
72 71 adantl ⊢N∈ℕ∧I∈1…N−1→I≠I+1
73 eldifsn ⊢I∈1…N∖I+1↔I∈1…N∧I≠I+1
74 65 72 73 sylanbrc ⊢N∈ℕ∧I∈1…N−1→I∈1…N∖I+1
75 ne0i ⊢I∈1…N∖I+1→1…N∖I+1≠∅
76 rnxp ⊢1…N∖I+1≠∅→ran⁡1…N∖I+1×0=0
77 74 75 76 3syl ⊢N∈ℕ∧I∈1…N−1→ran⁡1…N∖I+1×0=0
78 56 77 uneq12d ⊢N∈ℕ∧I∈1…N−1→ran⁡I+11∪ran⁡1…N∖I+1×0=1∪0
79 rnun ⊢ran⁡I+11∪1…N∖I+1×0=ran⁡I+11∪ran⁡1…N∖I+1×0
80 df-pr ⊢10=1∪0
81 78 79 80 3eqtr4g ⊢N∈ℕ∧I∈1…N−1→ran⁡I+11∪1…N∖I+1×0=10
82 53 81 eqeq12d ⊢N∈ℕ∧I∈1…N−1→ran⁡3−1∪1…N∖3×0=ran⁡I+11∪1…N∖I+1×0↔−10=10
83 27 82 mtbiri ⊢N∈ℕ∧I∈1…N−1→¬ran⁡3−1∪1…N∖3×0=ran⁡I+11∪1…N∖I+1×0
84 rneq ⊢3−1∪1…N∖3×0=I+11∪1…N∖I+1×0→ran⁡3−1∪1…N∖3×0=ran⁡I+11∪1…N∖I+1×0
85 83 84 nsyl ⊢N∈ℕ∧I∈1…N−1→¬3−1∪1…N∖3×0=I+11∪1…N∖I+1×0
86 1 2 eqeq12i ⊢P=Q↔3−1∪1…N∖3×0=I+11∪1…N∖I+1×0
87 86 necon3abii ⊢P≠Q↔¬3−1∪1…N∖3×0=I+11∪1…N∖I+1×0
88 85 87 sylibr ⊢N∈ℕ∧I∈1…N−1→P≠Q