Theorem 2sqreunnlem2

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

	Ref	Expression
Hypothesis	2sqreulem4.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
Assertion	2sqreunnlem2	⊢ ∀ 𝑎 ∈ ℕ ∃* 𝑏 ∈ ℕ 𝜑

Proof

Step	Hyp	Ref	Expression
1		2sqreulem4.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2		nnssnn0	⊢ ℕ ⊆ ℕ0
3	1	2sqreulem4	⊢ ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑
4		nfcv	⊢ Ⅎ 𝑏 ℕ
5		nfcv	⊢ Ⅎ 𝑏 ℕ0
6	4 5	ssrmof	⊢ ( ℕ ⊆ ℕ0 → ( ∃* 𝑏 ∈ ℕ0 𝜑 → ∃* 𝑏 ∈ ℕ 𝜑 ) )
7	6	ralimdv	⊢ ( ℕ ⊆ ℕ0 → ( ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑 → ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ 𝜑 ) )
8	2 3 7	mp2	⊢ ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ 𝜑
9		ssralv	⊢ ( ℕ ⊆ ℕ0 → ( ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ 𝜑 → ∀ 𝑎 ∈ ℕ ∃* 𝑏 ∈ ℕ 𝜑 ) )
10	2 8 9	mp2	⊢ ∀ 𝑎 ∈ ℕ ∃* 𝑏 ∈ ℕ 𝜑