Theorem isppw

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	isppw	⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 }
2	1	vmaval	⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) = if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) )
3	2	neeq1d	⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
4		reuen1	⊢ ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o )
5		hash1	⊢ ( ♯ ‘ 1o ) = 1
6	5	eqeq2i	⊢ ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = ( ♯ ‘ 1o ) ↔ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
7		prmdvdsfi	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
8		1onn	⊢ 1o ∈ ω
9		nnfi	⊢ ( 1o ∈ ω → 1o ∈ Fin )
10	8 9	ax-mp	⊢ 1o ∈ Fin
11		hashen	⊢ ( ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin ∧ 1o ∈ Fin ) → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = ( ♯ ‘ 1o ) ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
12	7 10 11	sylancl	⊢ ( 𝐴 ∈ ℕ → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = ( ♯ ‘ 1o ) ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
13	6 12	bitr3id	⊢ ( 𝐴 ∈ ℕ → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
14	13	biimpar	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
15	14	iftrued	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) = ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) )
16		en1b	⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
17	16	bilani	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
18		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ℙ
19	17 18	eqsstrrdi	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ )
20	7	uniexd	⊢ ( 𝐴 ∈ ℕ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
21	20	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
22		snssg	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
23	21 22	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
24	19 23	mpbird	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ )
25		prmuz2	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
26	24 25	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
27		eluzelre	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
28	26 27	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
29		eluz2gt1	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
30	26 29	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
31	28 30	rplogcld	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℝ+ )
32	31	rpne0d	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ≠ 0 )
33	15 32	eqnetrd	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 )
34	33	ex	⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
35		iffalse	⊢ ( ¬ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) = 0 )
36	35	necon1ai	⊢ ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
37	36 13	imbitrid	⊢ ( 𝐴 ∈ ℕ → ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
38	34 37	impbid	⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
39	4 38	bitrid	⊢ ( 𝐴 ∈ ℕ → ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
40	3 39	bitr4d	⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ) )