nprmdvdsfacm1lem4

		Ref	Expression
	Assertion	nprmdvdsfacm1lem4	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N ∥ (N - 1)!$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ$
2	1	3ad2ant1	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N \in ℤ$
3		elfzoelz	$⊢ A \in (2 ..^N) \to A \in ℤ$
4		id	$⊢ A \in ℤ \to A \in ℤ$
5		2z	$⊢ 2 \in ℤ$
6	5	a1i	$⊢ A \in ℤ \to 2 \in ℤ$
7	6 4	zmulcld	$⊢ A \in ℤ \to 2 A \in ℤ$
8	4 7	zmulcld	$⊢ A \in ℤ \to A 2 A \in ℤ$
9	3 8	syl	$⊢ A \in (2 ..^N) \to A 2 A \in ℤ$
10	9	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A 2 A \in ℤ$
11		1z	$⊢ 1 \in ℤ$
12		6nn	$⊢ 6 \in ℕ$
13	12	nnzi	$⊢ 6 \in ℤ$
14		1re	$⊢ 1 \in ℝ$
15		6re	$⊢ 6 \in ℝ$
16		1lt6	$⊢ 1 < 6$
17	14 15 16	ltleii	$⊢ 1 \leq 6$
18		eluz2	$⊢ 6 \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land 6 \in ℤ \land 1 \leq 6)$
19	11 13 17 18	mpbir3an	$⊢ 6 \in ℤ_{\geq 1}$
20		uzss	$⊢ 6 \in ℤ_{\geq 1} \to ℤ_{\geq 6} \subseteq ℤ_{\geq 1}$
21	19 20	ax-mp	$⊢ ℤ_{\geq 6} \subseteq ℤ_{\geq 1}$
22	21	sseli	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ_{\geq 1}$
23		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
24	22 23	sylibr	$⊢ N \in ℤ_{\geq 6} \to N \in ℕ$
25	24	3ad2ant1	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N \in ℕ$
26		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
27	25 26	syl	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N - 1 \in ℕ_{0}$
28	27	faccld	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to (N - 1)! \in ℕ$
29	28	nnzd	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to (N - 1)! \in ℤ$
30		nprmdvdsfacm1lem1	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N ∥ A 2 A$
31		elfzo2	$⊢ A \in (2 ..^N) \leftrightarrow (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N)$
32		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
33		uzss	$⊢ 2 \in ℤ_{\geq 1} \to ℤ_{\geq 2} \subseteq ℤ_{\geq 1}$
34	32 33	ax-mp	$⊢ ℤ_{\geq 2} \subseteq ℤ_{\geq 1}$
35	34	sseli	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ_{\geq 1}$
36	35	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to A \in ℤ_{\geq 1}$
37	5	a1i	$⊢ A \in ℤ_{\geq 2} \to 2 \in ℤ$
38		eluzelz	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ$
39	37 38	zmulcld	$⊢ A \in ℤ_{\geq 2} \to 2 A \in ℤ$
40	39	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to 2 A \in ℤ$
41		1lt2	$⊢ 1 < 2$
42		eluz2	$⊢ A \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land A \in ℤ \land 2 \leq A)$
43		zre	$⊢ A \in ℤ \to A \in ℝ$
44	43	3ad2ant2	$⊢ (2 \in ℤ \land A \in ℤ \land 2 \leq A) \to A \in ℝ$
45		2re	$⊢ 2 \in ℝ$
46	45	a1i	$⊢ (2 \in ℤ \land A \in ℤ \land 2 \leq A) \to 2 \in ℝ$
47		2pos	$⊢ 0 < 2$
48		0red	$⊢ A \in ℤ \to 0 \in ℝ$
49	45	a1i	$⊢ A \in ℤ \to 2 \in ℝ$
50	48 49 43	3jca	$⊢ A \in ℤ \to (0 \in ℝ \land 2 \in ℝ \land A \in ℝ)$
51		ltletr	$⊢ (0 \in ℝ \land 2 \in ℝ \land A \in ℝ) \to ((0 < 2 \land 2 \leq A) \to 0 < A)$
52	50 51	syl	$⊢ A \in ℤ \to ((0 < 2 \land 2 \leq A) \to 0 < A)$
53	47 52	mpani	$⊢ A \in ℤ \to (2 \leq A \to 0 < A)$
54	53	imp	$⊢ (A \in ℤ \land 2 \leq A) \to 0 < A$
55	54	3adant1	$⊢ (2 \in ℤ \land A \in ℤ \land 2 \leq A) \to 0 < A$
56	44 46 55	3jca	$⊢ (2 \in ℤ \land A \in ℤ \land 2 \leq A) \to (A \in ℝ \land 2 \in ℝ \land 0 < A)$
57	42 56	sylbi	$⊢ A \in ℤ_{\geq 2} \to (A \in ℝ \land 2 \in ℝ \land 0 < A)$
58	57	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to (A \in ℝ \land 2 \in ℝ \land 0 < A)$
59		ltmulgt12	$⊢ (A \in ℝ \land 2 \in ℝ \land 0 < A) \to (1 < 2 \leftrightarrow A < 2 A)$
60	58 59	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to (1 < 2 \leftrightarrow A < 2 A)$
61	41 60	mpbii	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to A < 2 A$
62	36 40 61	3jca	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to (A \in ℤ_{\geq 1} \land 2 A \in ℤ \land A < 2 A)$
63	31 62	sylbi	$⊢ A \in (2 ..^N) \to (A \in ℤ_{\geq 1} \land 2 A \in ℤ \land A < 2 A)$
64		elfzo2	$⊢ A \in (1 ..^2 A) \leftrightarrow (A \in ℤ_{\geq 1} \land 2 A \in ℤ \land A < 2 A)$
65	63 64	sylibr	$⊢ A \in (2 ..^N) \to A \in (1 ..^2 A)$
66	65	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A \in (1 ..^2 A)$
67	11	a1i	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 1 \in ℤ$
68	5	a1i	$⊢ A \in (2 ..^N) \to 2 \in ℤ$
69	68 3	zmulcld	$⊢ A \in (2 ..^N) \to 2 A \in ℤ$
70	69	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A \in ℤ$
71	47	a1i	$⊢ A \in ℤ \to 0 < 2$
72		lemul2	$⊢ (2 \in ℝ \land A \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 \leq A \leftrightarrow 2 \cdot 2 \leq 2 A)$
73	49 43 49 71 72	syl112anc	$⊢ A \in ℤ \to (2 \leq A \leftrightarrow 2 \cdot 2 \leq 2 A)$
74		1red	$⊢ (A \in ℤ \land 2 \cdot 2 \leq 2 A) \to 1 \in ℝ$
75		2t2e4	$⊢ 2 \cdot 2 = 4$
76		4re	$⊢ 4 \in ℝ$
77	75 76	eqeltri	$⊢ 2 \cdot 2 \in ℝ$
78	77	a1i	$⊢ (A \in ℤ \land 2 \cdot 2 \leq 2 A) \to 2 \cdot 2 \in ℝ$
79	7	zred	$⊢ A \in ℤ \to 2 A \in ℝ$
80	79	adantr	$⊢ (A \in ℤ \land 2 \cdot 2 \leq 2 A) \to 2 A \in ℝ$
81		1lt4	$⊢ 1 < 4$
82	14 76 81	ltleii	$⊢ 1 \leq 4$
83	82 75	breqtrri	$⊢ 1 \leq 2 \cdot 2$
84	83	a1i	$⊢ (A \in ℤ \land 2 \cdot 2 \leq 2 A) \to 1 \leq 2 \cdot 2$
85		simpr	$⊢ (A \in ℤ \land 2 \cdot 2 \leq 2 A) \to 2 \cdot 2 \leq 2 A$
86	74 78 80 84 85	letrd	$⊢ (A \in ℤ \land 2 \cdot 2 \leq 2 A) \to 1 \leq 2 A$
87	73 86	sylbida	$⊢ (A \in ℤ \land 2 \leq A) \to 1 \leq 2 A$
88	87	3adant1	$⊢ (2 \in ℤ \land A \in ℤ \land 2 \leq A) \to 1 \leq 2 A$
89	42 88	sylbi	$⊢ A \in ℤ_{\geq 2} \to 1 \leq 2 A$
90	89	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to 1 \leq 2 A$
91	31 90	sylbi	$⊢ A \in (2 ..^N) \to 1 \leq 2 A$
92	91	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 1 \leq 2 A$
93		eluz2	$⊢ 2 A \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land 2 A \in ℤ \land 1 \leq 2 A)$
94	67 70 92 93	syl3anbrc	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A \in ℤ_{\geq 1}$
95		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
96	3 95	syl	$⊢ A \in (2 ..^N) \to A^{2} \in ℤ$
97	96	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A^{2} \in ℤ$
98		3z	$⊢ 3 \in ℤ$
99	98	a1i	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 3 \in ℤ$
100	3	3ad2ant2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A \in ℤ$
101		nprmdvdsfacm1lem2	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 3 \leq A$
102		eluz2	$⊢ A \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land A \in ℤ \land 3 \leq A)$
103	99 100 101 102	syl3anbrc	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A \in ℤ_{\geq 3}$
104		2timesltsq	$⊢ A \in ℤ_{\geq 3} \to 2 A < A^{2}$
105	103 104	syl	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A < A^{2}$
106	94 97 105	elfzod	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A \in (1 ..^A^{2})$
107		oveq2	$⊢ N = A^{2} \to (1 ..^N) = (1 ..^A^{2})$
108	107	eleq2d	$⊢ N = A^{2} \to (2 A \in (1 ..^N) \leftrightarrow 2 A \in (1 ..^A^{2}))$
109	108	3ad2ant3	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to (2 A \in (1 ..^N) \leftrightarrow 2 A \in (1 ..^A^{2}))$
110	106 109	mpbird	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to 2 A \in (1 ..^N)$
111		muldvdsfacm1	$⊢ (A \in (1 ..^2 A) \land 2 A \in (1 ..^N)) \to A 2 A ∥ (N - 1)!$
112	66 110 111	syl2anc	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to A 2 A ∥ (N - 1)!$
113	2 10 29 30 112	dvdstrd	$⊢ (N \in ℤ_{\geq 6} \land A \in (2 ..^N) \land N = A^{2}) \to N ∥ (N - 1)!$

Metamath Proof Explorer

Theorem nprmdvdsfacm1lem4

Proof