Metamath Proof Explorer

Theorem axcontlem5

Description: Lemma for axcont . Compute the value of F . (Contributed by Scott Fenton, 18-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 axcontlem5 $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P = T ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ 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 1 2 axcontlem2 $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U → F : D ⟶ 1-1 onto 0 +∞$
4 f1of $⊢ F : D ⟶ 1-1 onto 0 +∞ → F : D ⟶ 0 +∞$
5 3 4 syl $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U → F : D ⟶ 0 +∞$
6 5 ffvelrnda $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P ∈ 0 +∞$
7 eleq1 $⊢ F ⁡ P = T → F ⁡ P ∈ 0 +∞ ↔ T ∈ 0 +∞$
8 6 7 syl5ibcom $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P = T → T ∈ 0 +∞$
9 simpl $⊢ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i → T ∈ 0 +∞$
10 9 a1i $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i → T ∈ 0 +∞$
11 f1ofn $⊢ F : D ⟶ 1-1 onto 0 +∞ → F Fn D$
12 3 11 syl $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U → F Fn D$
13 fnbrfvb $⊢ F Fn D ∧ P ∈ D → F ⁡ P = T ↔ P F T$
14 12 13 sylan $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P = T ↔ P F T$
15 14 3adant3 $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D ∧ T ∈ 0 +∞ → F ⁡ P = T ↔ P F T$
16 eleq1 $⊢ x = P → x ∈ D ↔ P ∈ D$
17 fveq1 $⊢ x = P → x ⁡ i = P ⁡ i$
18 17 eqeq1d $⊢ x = P → x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i$
19 18 ralbidv $⊢ x = P → ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i$
20 19 anbi2d $⊢ x = P → t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i$
21 16 20 anbi12d $⊢ x = P → x ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N x ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ P ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i$
22 eleq1 $⊢ t = T → t ∈ 0 +∞ ↔ T ∈ 0 +∞$
23 oveq2 $⊢ t = T → 1 − t = 1 − T$
24 23 oveq1d $⊢ t = T → 1 − t ⁢ Z ⁡ i = 1 − T ⁢ Z ⁡ i$
25 oveq1 $⊢ t = T → t ⁢ U ⁡ i = T ⁢ U ⁡ i$
26 24 25 oveq12d $⊢ t = T → 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
27 26 eqeq2d $⊢ t = T → P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
28 27 ralbidv $⊢ t = T → ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
29 22 28 anbi12d $⊢ t = T → t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
30 29 anbi2d $⊢ t = T → P ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
31 anass $⊢ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞$
32 anidm $⊢ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ↔ T ∈ 0 +∞$
33 32 anbi2i $⊢ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ↔ P ∈ D ∧ T ∈ 0 +∞$
34 31 33 bitr2i $⊢ P ∈ D ∧ T ∈ 0 +∞ ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞$
35 34 anbi1i $⊢ P ∈ D ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
36 anass $⊢ P ∈ D ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
37 anass $⊢ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
38 35 36 37 3bitr3i $⊢ P ∈ D ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
39 30 38 bitrdi $⊢ t = T → P ∈ D ∧ t ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − t ⁢ Z ⁡ i + t ⁢ U ⁡ i ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
40 21 39 2 brabg $⊢ P ∈ D ∧ T ∈ 0 +∞ → P F T ↔ P ∈ D ∧ T ∈ 0 +∞ ∧ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
41 40 bianabs $⊢ P ∈ D ∧ T ∈ 0 +∞ → P F T ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
42 41 3adant1 $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D ∧ T ∈ 0 +∞ → P F T ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
43 15 42 bitrd $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D ∧ T ∈ 0 +∞ → F ⁡ P = T ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
44 43 3expia $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → T ∈ 0 +∞ → F ⁡ P = T ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$
45 8 10 44 pm5.21ndd $⊢ N ∈ ℕ ∧ Z ∈ 𝔼 ⁡ N ∧ U ∈ 𝔼 ⁡ N ∧ Z ≠ U ∧ P ∈ D → F ⁡ P = T ↔ T ∈ 0 +∞ ∧ ∀ i ∈ 1 … N P ⁡ i = 1 − T ⁢ Z ⁡ i + T ⁢ U ⁡ i$