Metamath Proof Explorer

Theorem 2sqreulem4

Description: Lemma 4 for 2sqreu et. (Contributed by AV, 25-Jun-2023)

Ref Expression
Hypothesis 2sqreulem4.1 ⊢ φ ↔ ψ ∧ a 2 + b 2 = P
Assertion 2sqreulem4 ⊢ ∀ a ∈ ℕ 0 ∃* b ∈ ℕ 0 φ

Proof

Step Hyp Ref Expression
1 2sqreulem4.1 ⊢ φ ↔ ψ ∧ a 2 + b 2 = P
2 2sqreulem3 ⊢ a ∈ ℕ 0 ∧ b ∈ ℕ 0 ∧ c ∈ ℕ 0 → ψ ∧ a 2 + b 2 = P ∧ [˙c / b]˙ ψ ∧ a 2 + c 2 = P → b = c
3 2 ralrimivva ⊢ a ∈ ℕ 0 → ∀ b ∈ ℕ 0 ∀ c ∈ ℕ 0 ψ ∧ a 2 + b 2 = P ∧ [˙c / b]˙ ψ ∧ a 2 + c 2 = P → b = c
4 1 rmobii ⊢ ∃* b ∈ ℕ 0 φ ↔ ∃* b ∈ ℕ 0 ψ ∧ a 2 + b 2 = P
5 nfcv ⊢ Ⅎ _ b ℕ 0
6 nfcv ⊢ Ⅎ _ c ℕ 0
7 nfsbc1v ⊢ Ⅎ b [˙c / b]˙ ψ
8 nfv ⊢ Ⅎ b a 2 + c 2 = P
9 7 8 nfan ⊢ Ⅎ b [˙c / b]˙ ψ ∧ a 2 + c 2 = P
10 sbceq1a ⊢ b = c → ψ ↔ [˙c / b]˙ ψ
11 oveq1 ⊢ b = c → b 2 = c 2
12 11 oveq2d ⊢ b = c → a 2 + b 2 = a 2 + c 2
13 12 eqeq1d ⊢ b = c → a 2 + b 2 = P ↔ a 2 + c 2 = P
14 10 13 anbi12d ⊢ b = c → ψ ∧ a 2 + b 2 = P ↔ [˙c / b]˙ ψ ∧ a 2 + c 2 = P
15 5 6 9 14 rmo4f ⊢ ∃* b ∈ ℕ 0 ψ ∧ a 2 + b 2 = P ↔ ∀ b ∈ ℕ 0 ∀ c ∈ ℕ 0 ψ ∧ a 2 + b 2 = P ∧ [˙c / b]˙ ψ ∧ a 2 + c 2 = P → b = c
16 4 15 bitri ⊢ ∃* b ∈ ℕ 0 φ ↔ ∀ b ∈ ℕ 0 ∀ c ∈ ℕ 0 ψ ∧ a 2 + b 2 = P ∧ [˙c / b]˙ ψ ∧ a 2 + c 2 = P → b = c
17 3 16 sylibr ⊢ a ∈ ℕ 0 → ∃* b ∈ ℕ 0 φ
18 17 rgen ⊢ ∀ a ∈ ℕ 0 ∃* b ∈ ℕ 0 φ