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		simpr	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o )
17		en1b	⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
18	16 17	sylib	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
19		ssrab2	⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ℙ
20	18 19	eqsstrrdi	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ )
21	7	uniexd	⊢ ( 𝐴 ∈ ℕ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
22	21	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
23		snssg	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
24	22 23	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
25	20 24	mpbird	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ )
26		prmuz2	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
27	25 26	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
28		eluzelre	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
29	27 28	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
30		eluz2gt1	⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
31	27 30	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
32	29 31	rplogcld	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℝ+ )
33	32	rpne0d	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ≠ 0 )
34	15 33	eqnetrd	⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 )
35	34	ex	⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
36		iffalse	⊢ ( ¬ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) = 0 )
37	36	necon1ai	⊢ ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
38	37 13	syl5ib	⊢ ( 𝐴 ∈ ℕ → ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
39	35 38	impbid	⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
40	4 39	syl5bb	⊢ ( 𝐴 ∈ ℕ → ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
41	3 40	bitr4d	⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ) )