pgpfi

Description: The converse to pgpfi1 . A finite group is a P -group iff it has size some power of P . (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Hypothesis	pgpfi.1	$⊢ X = {Base}_{G}$
	Assertion	pgpfi	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}))$

Proof

Step	Hyp	Ref	Expression
1		pgpfi.1	$⊢ X = {Base}_{G}$
2		eqid	$⊢ od (G) = od (G)$
3	1 2	ispgp	$⊢ P pGrp G \leftrightarrow (P \in ℙ \land G \in Grp \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})$
4		simprl	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P \in ℙ$
5	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
6	5	ad2antrr	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to X \neq \emptyset$
7		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
8	7	ad2antlr	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
9	6 8	mpbird	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \|X\| \in ℕ$
10	4 9	pccld	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P pCnt \|X\| \in ℕ_{0}$
11	10	nn0red	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P pCnt \|X\| \in ℝ$
12	11	leidd	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P pCnt \|X\| \leq P pCnt \|X\|$
13	10	nn0zd	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P pCnt \|X\| \in ℤ$
14		pcid	$⊢ (P \in ℙ \land P pCnt \|X\| \in ℤ) \to P pCnt P^{P pCnt \|X\|} = P pCnt \|X\|$
15	4 13 14	syl2anc	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P pCnt P^{P pCnt \|X\|} = P pCnt \|X\|$
16	12 15	breqtrrd	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P pCnt \|X\| \leq P pCnt P^{P pCnt \|X\|}$
17	16	ad2antrr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p = P) \to P pCnt \|X\| \leq P pCnt P^{P pCnt \|X\|}$
18		simpr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p = P) \to p = P$
19	18	oveq1d	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p = P) \to p pCnt \|X\| = P pCnt \|X\|$
20	18	oveq1d	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p = P) \to p pCnt P^{P pCnt \|X\|} = P pCnt P^{P pCnt \|X\|}$
21	17 19 20	3brtr4d	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p = P) \to p pCnt \|X\| \leq p pCnt P^{P pCnt \|X\|}$
22		simp-4l	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \to G \in Grp$
23		simplr	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to X \in Fin$
24	23	ad2antrr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \to X \in Fin$
25		simplr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \to p \in ℙ$
26		simpr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \to p ∥ \|X\|$
27	1 2	odcau	$⊢ ((G \in Grp \land X \in Fin \land p \in ℙ) \land p ∥ \|X\|) \to \exists g \in X od (G) (g) = p$
28	22 24 25 26 27	syl31anc	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \to \exists g \in X od (G) (g) = p$
29	25	adantr	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to p \in ℙ$
30		prmz	$⊢ p \in ℙ \to p \in ℤ$
31		iddvds	$⊢ p \in ℤ \to p ∥ p$
32	29 30 31	3syl	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to p ∥ p$
33		simprr	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to od (G) (g) = p$
34	32 33	breqtrrd	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to p ∥ od (G) (g)$
35		simplrr	$⊢ (((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \to \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m}$
36		fveqeq2	$⊢ x = g \to (od (G) (x) = P^{m} \leftrightarrow od (G) (g) = P^{m})$
37	36	rexbidv	$⊢ x = g \to (\exists m \in ℕ_{0} od (G) (x) = P^{m} \leftrightarrow \exists m \in ℕ_{0} od (G) (g) = P^{m})$
38	37	rspccva	$⊢ (\forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m} \land g \in X) \to \exists m \in ℕ_{0} od (G) (g) = P^{m}$
39	35 38	sylan	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land g \in X) \to \exists m \in ℕ_{0} od (G) (g) = P^{m}$
40	39	ad2ant2r	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to \exists m \in ℕ_{0} od (G) (g) = P^{m}$
41	4	ad3antrrr	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to P \in ℙ$
42		prmnn	$⊢ p \in ℙ \to p \in ℕ$
43	29 42	syl	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to p \in ℕ$
44	33 43	eqeltrd	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to od (G) (g) \in ℕ$
45		pcprmpw	$⊢ (P \in ℙ \land od (G) (g) \in ℕ) \to (\exists m \in ℕ_{0} od (G) (g) = P^{m} \leftrightarrow od (G) (g) = P^{P pCnt od (G) (g)})$
46	41 44 45	syl2anc	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to (\exists m \in ℕ_{0} od (G) (g) = P^{m} \leftrightarrow od (G) (g) = P^{P pCnt od (G) (g)})$
47	40 46	mpbid	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to od (G) (g) = P^{P pCnt od (G) (g)}$
48	34 47	breqtrd	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to p ∥ P^{P pCnt od (G) (g)}$
49	41 44	pccld	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to P pCnt od (G) (g) \in ℕ_{0}$
50		prmdvdsexpr	$⊢ (p \in ℙ \land P \in ℙ \land P pCnt od (G) (g) \in ℕ_{0}) \to (p ∥ P^{P pCnt od (G) (g)} \to p = P)$
51	29 41 49 50	syl3anc	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to (p ∥ P^{P pCnt od (G) (g)} \to p = P)$
52	48 51	mpd	$⊢ (((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \land (g \in X \land od (G) (g) = p)) \to p = P$
53	28 52	rexlimddv	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p ∥ \|X\|) \to p = P$
54	53	ex	$⊢ (((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \to (p ∥ \|X\| \to p = P)$
55	54	necon3ad	$⊢ (((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \to (p \neq P \to \neg p ∥ \|X\|)$
56	55	imp	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to \neg p ∥ \|X\|$
57		simplr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to p \in ℙ$
58	9	ad2antrr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to \|X\| \in ℕ$
59		pceq0	$⊢ (p \in ℙ \land \|X\| \in ℕ) \to (p pCnt \|X\| = 0 \leftrightarrow \neg p ∥ \|X\|)$
60	57 58 59	syl2anc	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to (p pCnt \|X\| = 0 \leftrightarrow \neg p ∥ \|X\|)$
61	56 60	mpbird	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to p pCnt \|X\| = 0$
62		prmnn	$⊢ P \in ℙ \to P \in ℕ$
63	62	ad2antrl	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P \in ℕ$
64	63 10	nnexpcld	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P^{P pCnt \|X\|} \in ℕ$
65	64	ad2antrr	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to P^{P pCnt \|X\|} \in ℕ$
66	57 65	pccld	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to p pCnt P^{P pCnt \|X\|} \in ℕ_{0}$
67	66	nn0ge0d	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to 0 \leq p pCnt P^{P pCnt \|X\|}$
68	61 67	eqbrtrd	$⊢ ((((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \land p \neq P) \to p pCnt \|X\| \leq p pCnt P^{P pCnt \|X\|}$
69	21 68	pm2.61dane	$⊢ (((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \land p \in ℙ) \to p pCnt \|X\| \leq p pCnt P^{P pCnt \|X\|}$
70	69	ralrimiva	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \forall p \in ℙ p pCnt \|X\| \leq p pCnt P^{P pCnt \|X\|}$
71		hashcl	$⊢ X \in Fin \to \|X\| \in ℕ_{0}$
72	71	ad2antlr	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \|X\| \in ℕ_{0}$
73	72	nn0zd	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \|X\| \in ℤ$
74	64	nnzd	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to P^{P pCnt \|X\|} \in ℤ$
75		pc2dvds	$⊢ (\|X\| \in ℤ \land P^{P pCnt \|X\|} \in ℤ) \to (\|X\| ∥ P^{P pCnt \|X\|} \leftrightarrow \forall p \in ℙ p pCnt \|X\| \leq p pCnt P^{P pCnt \|X\|})$
76	73 74 75	syl2anc	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to (\|X\| ∥ P^{P pCnt \|X\|} \leftrightarrow \forall p \in ℙ p pCnt \|X\| \leq p pCnt P^{P pCnt \|X\|})$
77	70 76	mpbird	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \|X\| ∥ P^{P pCnt \|X\|}$
78		oveq2	$⊢ n = P pCnt \|X\| \to P^{n} = P^{P pCnt \|X\|}$
79	78	breq2d	$⊢ n = P pCnt \|X\| \to (\|X\| ∥ P^{n} \leftrightarrow \|X\| ∥ P^{P pCnt \|X\|})$
80	79	rspcev	$⊢ (P pCnt \|X\| \in ℕ_{0} \land \|X\| ∥ P^{P pCnt \|X\|}) \to \exists n \in ℕ_{0} \|X\| ∥ P^{n}$
81	10 77 80	syl2anc	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \exists n \in ℕ_{0} \|X\| ∥ P^{n}$
82		pcprmpw2	$⊢ (P \in ℙ \land \|X\| \in ℕ) \to (\exists n \in ℕ_{0} \|X\| ∥ P^{n} \leftrightarrow \|X\| = P^{P pCnt \|X\|})$
83		pcprmpw	$⊢ (P \in ℙ \land \|X\| \in ℕ) \to (\exists n \in ℕ_{0} \|X\| = P^{n} \leftrightarrow \|X\| = P^{P pCnt \|X\|})$
84	82 83	bitr4d	$⊢ (P \in ℙ \land \|X\| \in ℕ) \to (\exists n \in ℕ_{0} \|X\| ∥ P^{n} \leftrightarrow \exists n \in ℕ_{0} \|X\| = P^{n})$
85	4 9 84	syl2anc	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to (\exists n \in ℕ_{0} \|X\| ∥ P^{n} \leftrightarrow \exists n \in ℕ_{0} \|X\| = P^{n})$
86	81 85	mpbid	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to \exists n \in ℕ_{0} \|X\| = P^{n}$
87	4 86	jca	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n})$
88	87	3adantr2	$⊢ ((G \in Grp \land X \in Fin) \land (P \in ℙ \land G \in Grp \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m})) \to (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n})$
89	88	ex	$⊢ (G \in Grp \land X \in Fin) \to ((P \in ℙ \land G \in Grp \land \forall x \in X \exists m \in ℕ_{0} od (G) (x) = P^{m}) \to (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}))$
90	3 89	syl5bi	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \to (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}))$
91	1	pgpfi1	$⊢ (G \in Grp \land P \in ℙ \land n \in ℕ_{0}) \to (\|X\| = P^{n} \to P pGrp G)$
92	91	3expia	$⊢ (G \in Grp \land P \in ℙ) \to (n \in ℕ_{0} \to (\|X\| = P^{n} \to P pGrp G))$
93	92	rexlimdv	$⊢ (G \in Grp \land P \in ℙ) \to (\exists n \in ℕ_{0} \|X\| = P^{n} \to P pGrp G)$
94	93	expimpd	$⊢ G \in Grp \to ((P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}) \to P pGrp G)$
95	94	adantr	$⊢ (G \in Grp \land X \in Fin) \to ((P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}) \to P pGrp G)$
96	90 95	impbid	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}))$

Metamath Proof Explorer

Theorem pgpfi

Proof