Step | Hyp | Ref
| Expression |
1 | | 1zzd 12208 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℤ) |
2 | | eluzelz 12448 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
3 | | 2nn 11903 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
4 | | uznnssnn 12491 |
. . . . . . . . . . 11
⊢ (2 ∈
ℕ → (ℤ≥‘2) ⊆
ℕ) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℤ≥‘2) ⊆ ℕ |
6 | | nnuz 12477 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
7 | 5, 6 | sseqtri 3937 |
. . . . . . . . 9
⊢
(ℤ≥‘2) ⊆
(ℤ≥‘1) |
8 | 7 | sseli 3896 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
(ℤ≥‘1)) |
9 | | eluzle 12451 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ≤ 𝑁) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ 𝑁) |
11 | | 1re 10833 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
12 | 11 | leidi 11366 |
. . . . . . 7
⊢ 1 ≤
1 |
13 | 10, 12 | jctil 523 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 ≤ 1 ∧ 1 ≤ 𝑁)) |
14 | | elfz4 13105 |
. . . . . 6
⊢ (((1
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ≤ 1 ∧ 1 ≤ 𝑁)) → 1 ∈ (1...𝑁)) |
15 | 1, 2, 1, 13, 14 | syl31anc 1375 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ (1...𝑁)) |
16 | | eluzel2 12443 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℤ) |
17 | | eluzle 12451 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) |
18 | | 1le2 12039 |
. . . . . . 7
⊢ 1 ≤
2 |
19 | 17, 18 | jctil 523 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 ≤ 2 ∧ 2 ≤ 𝑁)) |
20 | | elfz4 13105 |
. . . . . 6
⊢ (((1
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 ≤ 2 ∧ 2 ≤ 𝑁)) → 2 ∈ (1...𝑁)) |
21 | 1, 2, 16, 19, 20 | syl31anc 1375 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ (1...𝑁)) |
22 | | ax-1ne0 10798 |
. . . . . . 7
⊢ 1 ≠
0 |
23 | | 1t1e1 11992 |
. . . . . . . 8
⊢ (1
· 1) = 1 |
24 | | 0cn 10825 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
25 | 24 | mul01i 11022 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
26 | 23, 25 | neeq12i 3007 |
. . . . . . 7
⊢ ((1
· 1) ≠ (0 · 0) ↔ 1 ≠ 0) |
27 | 22, 26 | mpbir 234 |
. . . . . 6
⊢ (1
· 1) ≠ (0 · 0) |
28 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘1)) |
29 | | 0re 10835 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
30 | 11, 29 | axlowdimlem4 27036 |
. . . . . . . . . . . . . . 15
⊢ {〈1,
1〉, 〈2, 0〉}:(1...2)⟶ℝ |
31 | | ffn 6545 |
. . . . . . . . . . . . . . 15
⊢
({〈1, 1〉, 〈2, 0〉}:(1...2)⟶ℝ →
{〈1, 1〉, 〈2, 0〉} Fn (1...2)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ {〈1,
1〉, 〈2, 0〉} Fn (1...2) |
33 | | axlowdimlem1 27033 |
. . . . . . . . . . . . . . 15
⊢
((3...𝑁) ×
{0}):(3...𝑁)⟶ℝ |
34 | | ffn 6545 |
. . . . . . . . . . . . . . 15
⊢
(((3...𝑁) ×
{0}):(3...𝑁)⟶ℝ
→ ((3...𝑁) ×
{0}) Fn (3...𝑁)) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((3...𝑁) ×
{0}) Fn (3...𝑁) |
36 | | axlowdimlem2 27034 |
. . . . . . . . . . . . . . 15
⊢ ((1...2)
∩ (3...𝑁)) =
∅ |
37 | | 1z 12207 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
38 | | 2z 12209 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
39 | 37, 38, 37 | 3pm3.2i 1341 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ) |
40 | 12, 18 | pm3.2i 474 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≤ 1
∧ 1 ≤ 2) |
41 | | elfz4 13105 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ≤ 1
∧ 1 ≤ 2)) → 1 ∈ (1...2)) |
42 | 39, 40, 41 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
(1...2) |
43 | 36, 42 | pm3.2i 474 |
. . . . . . . . . . . . . 14
⊢ (((1...2)
∩ (3...𝑁)) = ∅
∧ 1 ∈ (1...2)) |
44 | | fvun1 6802 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 1〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 1
∈ (1...2))) → (({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘1) = ({〈1, 1〉, 〈2,
0〉}‘1)) |
45 | 32, 35, 43, 44 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) = ({〈1,
1〉, 〈2, 0〉}‘1) |
46 | | 1ne2 12038 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
2 |
47 | | 1ex 10829 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
48 | 47, 47 | fvpr1 7005 |
. . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 1〉, 〈2, 0〉}‘1) = 1) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈1, 1〉, 〈2, 0〉}‘1) = 1 |
50 | 45, 49 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) =
1 |
51 | 28, 50 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑖 = 1 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = 1) |
52 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘1)) |
53 | 29, 29 | axlowdimlem4 27036 |
. . . . . . . . . . . . . . 15
⊢ {〈1,
0〉, 〈2, 0〉}:(1...2)⟶ℝ |
54 | | ffn 6545 |
. . . . . . . . . . . . . . 15
⊢
({〈1, 0〉, 〈2, 0〉}:(1...2)⟶ℝ →
{〈1, 0〉, 〈2, 0〉} Fn (1...2)) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ {〈1,
0〉, 〈2, 0〉} Fn (1...2) |
56 | | fvun1 6802 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 1
∈ (1...2))) → (({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘1) = ({〈1, 0〉, 〈2,
0〉}‘1)) |
57 | 55, 35, 43, 56 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) = ({〈1,
0〉, 〈2, 0〉}‘1) |
58 | 29 | elexi 3427 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
59 | 47, 58 | fvpr1 7005 |
. . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 0〉}‘1) = 0) |
60 | 46, 59 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 0〉}‘1) = 0 |
61 | 57, 60 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) =
0 |
62 | 52, 61 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = 0) |
63 | 51, 62 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
(1 − 0)) |
64 | | 1m0e1 11951 |
. . . . . . . . . 10
⊢ (1
− 0) = 1 |
65 | 63, 64 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑖 = 1 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
1) |
66 | 65 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑖 = 1 → (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(1 · ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)))) |
67 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0}))‘1)) |
68 | 29, 11 | axlowdimlem4 27036 |
. . . . . . . . . . . . . . 15
⊢ {〈1,
0〉, 〈2, 1〉}:(1...2)⟶ℝ |
69 | | ffn 6545 |
. . . . . . . . . . . . . . 15
⊢
({〈1, 0〉, 〈2, 1〉}:(1...2)⟶ℝ →
{〈1, 0〉, 〈2, 1〉} Fn (1...2)) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ {〈1,
0〉, 〈2, 1〉} Fn (1...2) |
71 | | fvun1 6802 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 1〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 1
∈ (1...2))) → (({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) ×
{0}))‘1) = ({〈1, 0〉, 〈2,
1〉}‘1)) |
72 | 70, 35, 43, 71 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘1) = ({〈1,
0〉, 〈2, 1〉}‘1) |
73 | 47, 58 | fvpr1 7005 |
. . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 1〉}‘1) = 0) |
74 | 46, 73 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 1〉}‘1) = 0 |
75 | 72, 74 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘1) =
0 |
76 | 67, 75 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) = 0) |
77 | 76, 62 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
(0 − 0)) |
78 | | 0m0e0 11950 |
. . . . . . . . . 10
⊢ (0
− 0) = 0 |
79 | 77, 78 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑖 = 1 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
0) |
80 | 79 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝑖 = 1 → (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· 0)) |
81 | 66, 80 | neeq12d 3002 |
. . . . . . 7
⊢ (𝑖 = 1 → ((((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ (1 · ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · 0))) |
82 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) = (({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0}))‘2)) |
83 | 37, 38, 38 | 3pm3.2i 1341 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ) |
84 | | 2re 11904 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
85 | 84 | leidi 11366 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ≤
2 |
86 | 18, 85 | pm3.2i 474 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≤ 2
∧ 2 ≤ 2) |
87 | | elfz4 13105 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 ≤ 2
∧ 2 ≤ 2)) → 2 ∈ (1...2)) |
88 | 83, 86, 87 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
(1...2) |
89 | 36, 88 | pm3.2i 474 |
. . . . . . . . . . . . . 14
⊢ (((1...2)
∩ (3...𝑁)) = ∅
∧ 2 ∈ (1...2)) |
90 | | fvun1 6802 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 1〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 2
∈ (1...2))) → (({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) ×
{0}))‘2) = ({〈1, 0〉, 〈2,
1〉}‘2)) |
91 | 70, 35, 89, 90 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘2) = ({〈1,
0〉, 〈2, 1〉}‘2) |
92 | 38 | elexi 3427 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
V |
93 | 92, 47 | fvpr2 7006 |
. . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 1〉}‘2) = 1) |
94 | 46, 93 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 1〉}‘2) = 1 |
95 | 91, 94 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘2) =
1 |
96 | 82, 95 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) = 1) |
97 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = (({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘2)) |
98 | | fvun1 6802 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 2
∈ (1...2))) → (({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘2) = ({〈1, 0〉, 〈2,
0〉}‘2)) |
99 | 55, 35, 89, 98 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) = ({〈1,
0〉, 〈2, 0〉}‘2) |
100 | 92, 58 | fvpr2 7006 |
. . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 0〉}‘2) = 0) |
101 | 46, 100 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 0〉}‘2) = 0 |
102 | 99, 101 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) =
0 |
103 | 97, 102 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = 0) |
104 | 96, 103 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑗 = 2 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
(1 − 0)) |
105 | 104, 64 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑗 = 2 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
1) |
106 | 105 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝑗 = 2 → (1 ·
((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(1 · 1)) |
107 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑗 = 2 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = (({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘2)) |
108 | | fvun1 6802 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 1〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 2
∈ (1...2))) → (({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘2) = ({〈1, 1〉, 〈2,
0〉}‘2)) |
109 | 32, 35, 89, 108 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) = ({〈1,
1〉, 〈2, 0〉}‘2) |
110 | 92, 58 | fvpr2 7006 |
. . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 1〉, 〈2, 0〉}‘2) = 0) |
111 | 46, 110 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
({〈1, 1〉, 〈2, 0〉}‘2) = 0 |
112 | 109, 111 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) =
0 |
113 | 107, 112 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑗 = 2 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = 0) |
114 | 113, 103 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑗 = 2 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
(0 − 0)) |
115 | 114, 78 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑗 = 2 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
0) |
116 | 115 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑗 = 2 → (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· 0) = (0 · 0)) |
117 | 106, 116 | neeq12d 3002 |
. . . . . . 7
⊢ (𝑗 = 2 → ((1 ·
((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· 0) ↔ (1 · 1) ≠ (0 · 0))) |
118 | 81, 117 | rspc2ev 3549 |
. . . . . 6
⊢ ((1
∈ (1...𝑁) ∧ 2
∈ (1...𝑁) ∧ (1
· 1) ≠ (0 · 0)) → ∃𝑖 ∈ (1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
119 | 27, 118 | mp3an3 1452 |
. . . . 5
⊢ ((1
∈ (1...𝑁) ∧ 2
∈ (1...𝑁)) →
∃𝑖 ∈ (1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
120 | 15, 21, 119 | syl2anc 587 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑖 ∈ (1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
121 | | df-ne 2941 |
. . . . . . . 8
⊢
((((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ¬ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
122 | 121 | rexbii 3170 |
. . . . . . 7
⊢
(∃𝑗 ∈
(1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ∃𝑗 ∈
(1...𝑁) ¬ (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))) |
123 | | rexnal 3160 |
. . . . . . 7
⊢
(∃𝑗 ∈
(1...𝑁) ¬ (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ¬ ∀𝑗
∈ (1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))) |
124 | 122, 123 | bitri 278 |
. . . . . 6
⊢
(∃𝑗 ∈
(1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ¬ ∀𝑗
∈ (1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))) |
125 | 124 | rexbii 3170 |
. . . . 5
⊢
(∃𝑖 ∈
(1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑁) ¬ ∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
126 | | rexnal 3160 |
. . . . 5
⊢
(∃𝑖 ∈
(1...𝑁) ¬ ∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))) ↔ ¬ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
127 | 125, 126 | bitri 278 |
. . . 4
⊢
(∃𝑖 ∈
(1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))) ↔ ¬ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
128 | 120, 127 | sylib 221 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) |
129 | 29, 29 | axlowdimlem5 27037 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
130 | 11, 29 | axlowdimlem5 27037 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
131 | 29, 11 | axlowdimlem5 27037 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
132 | | colinearalg 27001 |
. . . 4
⊢
((({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁)) → ((({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))))) |
133 | 129, 130,
131, 132 | syl3anc 1373 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))))) |
134 | 128, 133 | mtbird 328 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
135 | | axlowdimlem6.1 |
. . . 4
⊢ 𝐴 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) |
136 | | axlowdimlem6.2 |
. . . . 5
⊢ 𝐵 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) |
137 | | axlowdimlem6.3 |
. . . . 5
⊢ 𝐶 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) |
138 | 136, 137 | opeq12i 4789 |
. . . 4
⊢
〈𝐵, 𝐶〉 = 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 |
139 | 135, 138 | breq12i 5062 |
. . 3
⊢ (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
140 | 137, 135 | opeq12i 4789 |
. . . 4
⊢
〈𝐶, 𝐴〉 = 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 |
141 | 136, 140 | breq12i 5062 |
. . 3
⊢ (𝐵 Btwn 〈𝐶, 𝐴〉 ↔ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
142 | 135, 136 | opeq12i 4789 |
. . . 4
⊢
〈𝐴, 𝐵〉 = 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 |
143 | 137, 142 | breq12i 5062 |
. . 3
⊢ (𝐶 Btwn 〈𝐴, 𝐵〉 ↔ ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
144 | 139, 141,
143 | 3orbi123i 1158 |
. 2
⊢ ((𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉) ↔ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
145 | 134, 144 | sylnibr 332 |
1
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉)) |