Metamath Proof Explorer

Theorem fzass4

Description: Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzass4 ( ( 𝐵 ∈ ( 𝐴 ... 𝐷 ) ∧ 𝐶 ∈ ( 𝐵 ... 𝐷 ) ) ↔ ( 𝐵 ∈ ( 𝐴 ... 𝐶 ) ∧ 𝐶 ∈ ( 𝐴 ... 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
2 simprl ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) )
3 1 2 jca ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
4 uztrn ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) )
5 4 ancoms ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) )
6 5 ad2ant2r ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) )
7 simprr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) )
8 3 6 7 jca32 ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) )
9 simpll ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) )
10 uztrn ⊢ ( ( 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) → 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) )
11 10 ancoms ⊢ ( ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) → 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) )
12 11 ad2ant2l ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) )
13 9 12 jca ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
14 simplr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) )
15 simprr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) )
16 13 14 15 jca32 ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) → ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) )
17 8 16 impbii ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) ↔ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) )
18 elfzuzb ⊢ ( 𝐵 ∈ ( 𝐴 ... 𝐷 ) ↔ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
19 elfzuzb ⊢ ( 𝐶 ∈ ( 𝐵 ... 𝐷 ) ↔ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) )
20 18 19 anbi12i ⊢ ( ( 𝐵 ∈ ( 𝐴 ... 𝐷 ) ∧ 𝐶 ∈ ( 𝐵 ... 𝐷 ) ) ↔ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) )
21 elfzuzb ⊢ ( 𝐵 ∈ ( 𝐴 ... 𝐶 ) ↔ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
22 elfzuzb ⊢ ( 𝐶 ∈ ( 𝐴 ... 𝐷 ) ↔ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) )
23 21 22 anbi12i ⊢ ( ( 𝐵 ∈ ( 𝐴 ... 𝐶 ) ∧ 𝐶 ∈ ( 𝐴 ... 𝐷 ) ) ↔ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) ∧ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐷 ∈ ( ℤ≥ ‘ 𝐶 ) ) ) )
24 17 20 23 3bitr4i ⊢ ( ( 𝐵 ∈ ( 𝐴 ... 𝐷 ) ∧ 𝐶 ∈ ( 𝐵 ... 𝐷 ) ) ↔ ( 𝐵 ∈ ( 𝐴 ... 𝐶 ) ∧ 𝐶 ∈ ( 𝐴 ... 𝐷 ) ) )