This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzprval

Description: Two ways of defining the first two values of a sequence on NN . (Contributed by NM, 5-Sep-2011)

Ref Expression
Assertion fzprval ⊢ ∀ x ∈ 1 … 2 F ⁡ x = if x = 1 A B ↔ F ⁡ 1 = A ∧ F ⁡ 2 = B

Proof

Step Hyp Ref Expression
1 fz12pr ⊢ 1 … 2 = 1 2
2 1 raleqi ⊢ ∀ x ∈ 1 … 2 F ⁡ x = if x = 1 A B ↔ ∀ x ∈ 1 2 F ⁡ x = if x = 1 A B
3 1ex ⊢ 1 ∈ V
4 2ex ⊢ 2 ∈ V
5 fveq2 ⊢ x = 1 → F ⁡ x = F ⁡ 1
6 iftrue ⊢ x = 1 → if x = 1 A B = A
7 5 6 eqeq12d ⊢ x = 1 → F ⁡ x = if x = 1 A B ↔ F ⁡ 1 = A
8 fveq2 ⊢ x = 2 → F ⁡ x = F ⁡ 2
9 1ne2 ⊢ 1 ≠ 2
10 9 necomi ⊢ 2 ≠ 1
11 pm13.181 ⊢ x = 2 ∧ 2 ≠ 1 → x ≠ 1
12 10 11 mpan2 ⊢ x = 2 → x ≠ 1
13 12 neneqd ⊢ x = 2 → ¬ x = 1
14 13 iffalsed ⊢ x = 2 → if x = 1 A B = B
15 8 14 eqeq12d ⊢ x = 2 → F ⁡ x = if x = 1 A B ↔ F ⁡ 2 = B
16 3 4 7 15 ralpr ⊢ ∀ x ∈ 1 2 F ⁡ x = if x = 1 A B ↔ F ⁡ 1 = A ∧ F ⁡ 2 = B
17 2 16 bitri ⊢ ∀ x ∈ 1 … 2 F ⁡ x = if x = 1 A B ↔ F ⁡ 1 = A ∧ F ⁡ 2 = B