| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | axlowdimlem14.1 | . . . . . . 7
⊢ 𝑄 = ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) | 
| 2 | 1 | axlowdimlem10 28966 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 ∈ (𝔼‘𝑁)) | 
| 3 |  | elee 28909 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑄 ∈ (𝔼‘𝑁) ↔ 𝑄:(1...𝑁)⟶ℝ)) | 
| 4 | 3 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝑄 ∈ (𝔼‘𝑁) ↔ 𝑄:(1...𝑁)⟶ℝ)) | 
| 5 | 2, 4 | mpbid 232 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄:(1...𝑁)⟶ℝ) | 
| 6 | 5 | ffnd 6737 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑄 Fn (1...𝑁)) | 
| 7 |  | axlowdimlem14.2 | . . . . . . 7
⊢ 𝑅 = ({〈(𝐽 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐽 + 1)}) × {0})) | 
| 8 | 7 | axlowdimlem10 28966 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → 𝑅 ∈ (𝔼‘𝑁)) | 
| 9 |  | elee 28909 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑅 ∈ (𝔼‘𝑁) ↔ 𝑅:(1...𝑁)⟶ℝ)) | 
| 10 | 9 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝑅 ∈ (𝔼‘𝑁) ↔ 𝑅:(1...𝑁)⟶ℝ)) | 
| 11 | 8, 10 | mpbid 232 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → 𝑅:(1...𝑁)⟶ℝ) | 
| 12 | 11 | ffnd 6737 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1))) → 𝑅 Fn (1...𝑁)) | 
| 13 |  | eqfnfv 7051 | . . . 4
⊢ ((𝑄 Fn (1...𝑁) ∧ 𝑅 Fn (1...𝑁)) → (𝑄 = 𝑅 ↔ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) | 
| 14 | 6, 12, 13 | syl2an 596 | . . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) ∧ (𝑁 ∈ ℕ ∧ 𝐽 ∈ (1...(𝑁 − 1)))) → (𝑄 = 𝑅 ↔ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) | 
| 15 | 14 | 3impdi 1351 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝑄 = 𝑅 ↔ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) | 
| 16 |  | fznatpl1 13618 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | 
| 17 | 16 | 3adant3 1133 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | 
| 18 |  | ax-1ne0 11224 | . . . . . . . 8
⊢ 1 ≠
0 | 
| 19 | 18 | a1i 11 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → 1 ≠ 0) | 
| 20 | 1 | axlowdimlem11 28967 | . . . . . . . 8
⊢ (𝑄‘(𝐼 + 1)) = 1 | 
| 21 | 20 | a1i 11 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝑄‘(𝐼 + 1)) = 1) | 
| 22 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ∈ ℤ) | 
| 23 | 22 | zcnd 12723 | . . . . . . . . . . . 12
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ∈ ℂ) | 
| 24 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝐽 ∈ (1...(𝑁 − 1)) → 𝐽 ∈ ℤ) | 
| 25 | 24 | zcnd 12723 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ (1...(𝑁 − 1)) → 𝐽 ∈ ℂ) | 
| 26 |  | ax-1cn 11213 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℂ | 
| 27 |  | addcan2 11446 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐼 + 1) =
(𝐽 + 1) ↔ 𝐼 = 𝐽)) | 
| 28 | 26, 27 | mp3an3 1452 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ) → ((𝐼 + 1) = (𝐽 + 1) ↔ 𝐼 = 𝐽)) | 
| 29 | 23, 25, 28 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → ((𝐼 + 1) = (𝐽 + 1) ↔ 𝐼 = 𝐽)) | 
| 30 | 29 | 3adant1 1131 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → ((𝐼 + 1) = (𝐽 + 1) ↔ 𝐼 = 𝐽)) | 
| 31 | 30 | necon3bid 2985 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → ((𝐼 + 1) ≠ (𝐽 + 1) ↔ 𝐼 ≠ 𝐽)) | 
| 32 | 31 | biimpar 477 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝐼 + 1) ≠ (𝐽 + 1)) | 
| 33 | 7 | axlowdimlem12 28968 | . . . . . . . 8
⊢ (((𝐼 + 1) ∈ (1...𝑁) ∧ (𝐼 + 1) ≠ (𝐽 + 1)) → (𝑅‘(𝐼 + 1)) = 0) | 
| 34 | 17, 32, 33 | syl2an2r 685 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝑅‘(𝐼 + 1)) = 0) | 
| 35 | 19, 21, 34 | 3netr4d 3018 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1))) | 
| 36 |  | df-ne 2941 | . . . . . . . 8
⊢ ((𝑄‘𝑖) ≠ (𝑅‘𝑖) ↔ ¬ (𝑄‘𝑖) = (𝑅‘𝑖)) | 
| 37 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑖 = (𝐼 + 1) → (𝑄‘𝑖) = (𝑄‘(𝐼 + 1))) | 
| 38 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑖 = (𝐼 + 1) → (𝑅‘𝑖) = (𝑅‘(𝐼 + 1))) | 
| 39 | 37, 38 | neeq12d 3002 | . . . . . . . 8
⊢ (𝑖 = (𝐼 + 1) → ((𝑄‘𝑖) ≠ (𝑅‘𝑖) ↔ (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1)))) | 
| 40 | 36, 39 | bitr3id 285 | . . . . . . 7
⊢ (𝑖 = (𝐼 + 1) → (¬ (𝑄‘𝑖) = (𝑅‘𝑖) ↔ (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1)))) | 
| 41 | 40 | rspcev 3622 | . . . . . 6
⊢ (((𝐼 + 1) ∈ (1...𝑁) ∧ (𝑄‘(𝐼 + 1)) ≠ (𝑅‘(𝐼 + 1))) → ∃𝑖 ∈ (1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖)) | 
| 42 | 17, 35, 41 | syl2an2r 685 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) ∧ 𝐼 ≠ 𝐽) → ∃𝑖 ∈ (1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖)) | 
| 43 | 42 | ex 412 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝐼 ≠ 𝐽 → ∃𝑖 ∈ (1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖))) | 
| 44 |  | df-ne 2941 | . . . 4
⊢ (𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽) | 
| 45 |  | rexnal 3100 | . . . 4
⊢
(∃𝑖 ∈
(1...𝑁) ¬ (𝑄‘𝑖) = (𝑅‘𝑖) ↔ ¬ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖)) | 
| 46 | 43, 44, 45 | 3imtr3g 295 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (¬ 𝐼 = 𝐽 → ¬ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖))) | 
| 47 | 46 | con4d 115 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (𝑅‘𝑖) → 𝐼 = 𝐽)) | 
| 48 | 15, 47 | sylbid 240 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1)) ∧ 𝐽 ∈ (1...(𝑁 − 1))) → (𝑄 = 𝑅 → 𝐼 = 𝐽)) |