Theorem 2sqreulem4

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

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

Proof

Step	Hyp	Ref	Expression
1		2sqreulem4.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
2		2sqreulem3	⊢ ( ( 𝑎 ∈ ℕ0 ∧ ( 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ) → ( ( ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ( [ 𝑐 / 𝑏 ] 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 ) ) → 𝑏 = 𝑐 ) )
3	2	ralrimivva	⊢ ( 𝑎 ∈ ℕ0 → ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ( ( ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ( [ 𝑐 / 𝑏 ] 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 ) ) → 𝑏 = 𝑐 ) )
4	1	rmobii	⊢ ( ∃* 𝑏 ∈ ℕ0 𝜑 ↔ ∃* 𝑏 ∈ ℕ0 ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) )
5		nfcv	⊢ Ⅎ 𝑏 ℕ0
6		nfcv	⊢ Ⅎ 𝑐 ℕ0
7		nfsbc1v	⊢ Ⅎ 𝑏 [ 𝑐 / 𝑏 ] 𝜓
8		nfv	⊢ Ⅎ 𝑏 ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃
9	7 8	nfan	⊢ Ⅎ 𝑏 ( [ 𝑐 / 𝑏 ] 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 )
10		sbceq1a	⊢ ( 𝑏 = 𝑐 → ( 𝜓 ↔ [ 𝑐 / 𝑏 ] 𝜓 ) )
11		oveq1	⊢ ( 𝑏 = 𝑐 → ( 𝑏 ↑ 2 ) = ( 𝑐 ↑ 2 ) )
12	11	oveq2d	⊢ ( 𝑏 = 𝑐 → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) )
13	12	eqeq1d	⊢ ( 𝑏 = 𝑐 → ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ↔ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 ) )
14	10 13	anbi12d	⊢ ( 𝑏 = 𝑐 → ( ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( [ 𝑐 / 𝑏 ] 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 ) ) )
15	5 6 9 14	rmo4f	⊢ ( ∃* 𝑏 ∈ ℕ0 ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ( ( ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ( [ 𝑐 / 𝑏 ] 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 ) ) → 𝑏 = 𝑐 ) )
16	4 15	bitri	⊢ ( ∃* 𝑏 ∈ ℕ0 𝜑 ↔ ∀ 𝑏 ∈ ℕ0 ∀ 𝑐 ∈ ℕ0 ( ( ( 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ( [ 𝑐 / 𝑏 ] 𝜓 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑐 ↑ 2 ) ) = 𝑃 ) ) → 𝑏 = 𝑐 ) )
17	3 16	sylibr	⊢ ( 𝑎 ∈ ℕ0 → ∃* 𝑏 ∈ ℕ0 𝜑 )
18	17	rgen	⊢ ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑