Metamath Proof Explorer

Theorem axcontlem6

Description: Lemma for axcont . State the defining properties of the value of F . (Contributed by Scott Fenton, 19-Jun-2013)

Ref Expression
Hypotheses axcontlem5.1 ⊢ D = p ∈ 𝔼 ⁡ N | U Btwn Z p ∨ p Btwn Z U
axcontlem5.2 ⊢ F = x t | x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i
Assertion axcontlem6 ⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − F ⁡ P ⁢ Z ⁡ i + F ⁡ P ⁢ U ⁡ i

Proof

Step Hyp Ref Expression
1 axcontlem5.1 ⊢ D = p ∈ 𝔼 ⁡ N | U Btwn Z p ∨ p Btwn Z U
2 axcontlem5.2 ⊢ F = x t | x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i
3 eqid ⊢ F ⁡ P = F ⁡ P
4 2 axcontlem1 ⊢ F = y s | y ∈ D ∧ s ∈ 0 +∞ ∧ ∀ j ∈ 1 … N y ⁡ j = 1 − s ⁢ Z ⁡ j + s ⁢ U ⁡ j
5 1 4 axcontlem5 ⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P = F ⁡ P ↔ F ⁡ P ∈ 0 +∞ ∧ ∀ j ∈ 1 … N P ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ j + F ⁡ P ⁢ U ⁡ j
6 3 5 mpbii ⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P ∈ 0 +∞ ∧ ∀ j ∈ 1 … N P ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ j + F ⁡ P ⁢ U ⁡ j
7 fveq2 ⊢ j = i → P ⁡ j = P ⁡ i
8 fveq2 ⊢ j = i → Z ⁡ j = Z ⁡ i
9 8 oveq2d ⊢ j = i → 1 − F ⁡ P ⁢ Z ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ i
10 fveq2 ⊢ j = i → U ⁡ j = U ⁡ i
11 10 oveq2d ⊢ j = i → F ⁡ P ⁢ U ⁡ j = F ⁡ P ⁢ U ⁡ i
12 9 11 oveq12d ⊢ j = i → 1 − F ⁡ P ⁢ Z ⁡ j + F ⁡ P ⁢ U ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ i + F ⁡ P ⁢ U ⁡ i
13 7 12 eqeq12d ⊢ j = i → P ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ j + F ⁡ P ⁢ U ⁡ j ↔ P ⁡ i = 1 − F ⁡ P ⁢ Z ⁡ i + F ⁡ P ⁢ U ⁡ i
14 13 cbvralvw ⊢ ∀ j ∈ 1 … N P ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ j + F ⁡ P ⁢ U ⁡ j ↔ ∀ i ∈ 1 … N P ⁡ i = 1 − F ⁡ P ⁢ Z ⁡ i + F ⁡ P ⁢ U ⁡ i
15 14 anbi2i ⊢ F ⁡ P ∈ 0 +∞ ∧ ∀ j ∈ 1 … N P ⁡ j = 1 − F ⁡ P ⁢ Z ⁡ j + F ⁡ P ⁢ U ⁡ j ↔ F ⁡ P ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − F ⁡ P ⁢ Z ⁡ i + F ⁡ P ⁢ U ⁡ i
16 6 15 sylib ⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − F ⁡ P ⁢ Z ⁡ i + F ⁡ P ⁢ U ⁡ i