Metamath Proof Explorer

Theorem tgldimor

Description: Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019)

Ref Expression
Hypotheses tgldimor.p ⊢ P = E ⁡ F
tgldimor.a ⊢ φ → A ∈ P
Assertion tgldimor ⊢ φ → P = 1 ∨ 2 ≤ P

Proof

Step Hyp Ref Expression
1 tgldimor.p ⊢ P = E ⁡ F
2 tgldimor.a ⊢ φ → A ∈ P
3 1 fvexi ⊢ P ∈ V
4 hashv01gt1 ⊢ P ∈ V → P = 0 ∨ P = 1 ∨ 1 < P
5 3 4 ax-mp ⊢ P = 0 ∨ P = 1 ∨ 1 < P
6 3orass ⊢ P = 0 ∨ P = 1 ∨ 1 < P ↔ P = 0 ∨ P = 1 ∨ 1 < P
7 5 6 mpbi ⊢ P = 0 ∨ P = 1 ∨ 1 < P
8 1p1e2 ⊢ 1 + 1 = 2
9 1z ⊢ 1 ∈ ℤ
10 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
11 zltp1le ⊢ 1 ∈ ℤ ∧ P ∈ ℤ → 1 < P ↔ 1 + 1 ≤ P
12 9 10 11 sylancr ⊢ P ∈ ℕ 0 → 1 < P ↔ 1 + 1 ≤ P
13 12 biimpac ⊢ 1 < P ∧ P ∈ ℕ 0 → 1 + 1 ≤ P
14 8 13 eqbrtrrid ⊢ 1 < P ∧ P ∈ ℕ 0 → 2 ≤ P
15 2re ⊢ 2 ∈ ℝ
16 15 rexri ⊢ 2 ∈ ℝ *
17 pnfge ⊢ 2 ∈ ℝ * → 2 ≤ +∞
18 16 17 ax-mp ⊢ 2 ≤ +∞
19 breq2 ⊢ P = +∞ → 2 ≤ P ↔ 2 ≤ +∞
20 18 19 mpbiri ⊢ P = +∞ → 2 ≤ P
21 20 adantl ⊢ 1 < P ∧ P = +∞ → 2 ≤ P
22 hashnn0pnf ⊢ P ∈ V → P ∈ ℕ 0 ∨ P = +∞
23 3 22 mp1i ⊢ 1 < P → P ∈ ℕ 0 ∨ P = +∞
24 14 21 23 mpjaodan ⊢ 1 < P → 2 ≤ P
25 24 orim2i ⊢ P = 1 ∨ 1 < P → P = 1 ∨ 2 ≤ P
26 25 orim2i ⊢ P = 0 ∨ P = 1 ∨ 1 < P → P = 0 ∨ P = 1 ∨ 2 ≤ P
27 7 26 mp1i ⊢ φ → P = 0 ∨ P = 1 ∨ 2 ≤ P
28 ne0i ⊢ A ∈ P → P ≠ ∅
29 hasheq0 ⊢ P ∈ V → P = 0 ↔ P = ∅
30 3 29 ax-mp ⊢ P = 0 ↔ P = ∅
31 30 biimpi ⊢ P = 0 → P = ∅
32 31 necon3ai ⊢ P ≠ ∅ → ¬ P = 0
33 biorf ⊢ ¬ P = 0 → P = 1 ∨ 2 ≤ P ↔ P = 0 ∨ P = 1 ∨ 2 ≤ P
34 2 28 32 33 4syl ⊢ φ → P = 1 ∨ 2 ≤ P ↔ P = 0 ∨ P = 1 ∨ 2 ≤ P
35 27 34 mpbird ⊢ φ → P = 1 ∨ 2 ≤ P