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

Metamath Proof Explorer

Theorem zriotaneg

Description: The negative of the unique integer such that ph . (Contributed by AV, 1-Dec-2018)

Ref Expression
Hypothesis zriotaneg.1 ⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion zriotaneg ( ∃! 𝑥 ∈ ℤ 𝜑 → ( ℩ 𝑥 ∈ ℤ 𝜑 ) = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 zriotaneg.1 ⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 tru ⊢ ⊤
3 nfriota1 ⊢ Ⅎ 𝑦 ( ℩ 𝑦 ∈ ℤ 𝜓 )
4 3 nfneg ⊢ Ⅎ 𝑦 - ( ℩ 𝑦 ∈ ℤ 𝜓 )
5 znegcl ⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
6 5 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ℤ ) → - 𝑦 ∈ ℤ )
7 simpr ⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ ) → ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ )
8 7 znegcld ⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ ) → - ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ )
9 negeq ⊢ ( 𝑦 = ( ℩ 𝑦 ∈ ℤ 𝜓 ) → - 𝑦 = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )
10 znegcl ⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
11 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
12 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
13 negcon2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
14 11 12 13 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
15 10 14 reuhyp ⊢ ( 𝑥 ∈ ℤ → ∃! 𝑦 ∈ ℤ 𝑥 = - 𝑦 )
16 15 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℤ ) → ∃! 𝑦 ∈ ℤ 𝑥 = - 𝑦 )
17 4 6 8 1 9 16 riotaxfrd ⊢ ( ( ⊤ ∧ ∃! 𝑥 ∈ ℤ 𝜑 ) → ( ℩ 𝑥 ∈ ℤ 𝜑 ) = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )
18 2 17 mpan ⊢ ( ∃! 𝑥 ∈ ℤ 𝜑 → ( ℩ 𝑥 ∈ ℤ 𝜑 ) = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )