Theorem aks4d1p3

Description: There exists a small enough number such that it does not divide A . (Contributed by metakunt, 27-Oct-2024)

	Ref	Expression
Hypotheses	aks4d1p3.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
	aks4d1p3.2	⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
	aks4d1p3.3	⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
Assertion	aks4d1p3	⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		aks4d1p3.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2		aks4d1p3.2	⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3		aks4d1p3.3	⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4	1 2 3	aks4d1p1	⊢ ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )
5	4	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 < ( 2 ↑ 𝐵 ) )
6		2re	⊢ 2 ∈ ℝ
7	6	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
8	3	a1i	⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
9		2pos	⊢ 0 < 2
10	9	a1i	⊢ ( 𝜑 → 0 < 2 )
11		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
12	1 11	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
13	12	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
14		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
15		3re	⊢ 3 ∈ ℝ
16	15	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
17		3pos	⊢ 0 < 3
18	17	a1i	⊢ ( 𝜑 → 0 < 3 )
19		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
20	1 19	syl	⊢ ( 𝜑 → 3 ≤ 𝑁 )
21	14 16 13 18 20	ltletrd	⊢ ( 𝜑 → 0 < 𝑁 )
22		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
23		1lt2	⊢ 1 < 2
24	23	a1i	⊢ ( 𝜑 → 1 < 2 )
25	22 24	ltned	⊢ ( 𝜑 → 1 ≠ 2 )
26	25	necomd	⊢ ( 𝜑 → 2 ≠ 1 )
27	7 10 13 21 26	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
28		5nn0	⊢ 5 ∈ ℕ0
29	28	a1i	⊢ ( 𝜑 → 5 ∈ ℕ0 )
30	27 29	reexpcld	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
31		ceilcl	⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
32	30 31	syl	⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
33	8 32	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
34	32	zred	⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
35	8 34	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
36		7re	⊢ 7 ∈ ℝ
37	36	a1i	⊢ ( 𝜑 → 7 ∈ ℝ )
38		7pos	⊢ 0 < 7
39	38	a1i	⊢ ( 𝜑 → 0 < 7 )
40	13 20	3lexlogpow5ineq3	⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
41	14 37 30 39 40	lttrd	⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
42		ceilge	⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
43	30 42	syl	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
44	14 30 34 41 43	ltletrd	⊢ ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
45	44 8	breqtrrd	⊢ ( 𝜑 → 0 < 𝐵 )
46	14 35 45	ltled	⊢ ( 𝜑 → 0 ≤ 𝐵 )
47	33 46	jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ 0 ≤ 𝐵 ) )
48		elnn0z	⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℤ ∧ 0 ≤ 𝐵 ) )
49	47 48	sylibr	⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
50	7 49	reexpcld	⊢ ( 𝜑 → ( 2 ↑ 𝐵 ) ∈ ℝ )
51	50	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 2 ↑ 𝐵 ) ∈ ℝ )
52		elfznn	⊢ ( 𝑞 ∈ ( 1 ... 𝐵 ) → 𝑞 ∈ ℕ )
53	52	adantl	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 1 ... 𝐵 ) ) → 𝑞 ∈ ℕ )
54	53	nnzd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 1 ... 𝐵 ) ) → 𝑞 ∈ ℤ )
55	54	ex	⊢ ( 𝜑 → ( 𝑞 ∈ ( 1 ... 𝐵 ) → 𝑞 ∈ ℤ ) )
56	55	ssrdv	⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℤ )
57		fzfid	⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
58		lcmfcl	⊢ ( ( ( 1 ... 𝐵 ) ⊆ ℤ ∧ ( 1 ... 𝐵 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℕ0 )
59	56 57 58	syl2anc	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℕ0 )
60	59	nn0red	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℝ )
61	60	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℝ )
62	2	a1i	⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
63		elnnz	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
64	12 21 63	sylanbrc	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
65	7 10 35 45 26	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
66	65	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
67	7 10 7 10 26	relogbcld	⊢ ( 𝜑 → ( 2 logb 2 ) ∈ ℝ )
68		0le1	⊢ 0 ≤ 1
69	68	a1i	⊢ ( 𝜑 → 0 ≤ 1 )
70	7	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
71	14 10	gtned	⊢ ( 𝜑 → 2 ≠ 0 )
72		logbid1	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
73	70 71 26 72	syl3anc	⊢ ( 𝜑 → ( 2 logb 2 ) = 1 )
74	73	eqcomd	⊢ ( 𝜑 → 1 = ( 2 logb 2 ) )
75	69 74	breqtrd	⊢ ( 𝜑 → 0 ≤ ( 2 logb 2 ) )
76		2z	⊢ 2 ∈ ℤ
77	76	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
78	7	leidd	⊢ ( 𝜑 → 2 ≤ 2 )
79		2lt7	⊢ 2 < 7
80	79	a1i	⊢ ( 𝜑 → 2 < 7 )
81	7 37 80	ltled	⊢ ( 𝜑 → 2 ≤ 7 )
82	37 30 34 40 43	ltletrd	⊢ ( 𝜑 → 7 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
83	82 8	breqtrrd	⊢ ( 𝜑 → 7 < 𝐵 )
84	37 35 83	ltled	⊢ ( 𝜑 → 7 ≤ 𝐵 )
85	7 37 35 81 84	letrd	⊢ ( 𝜑 → 2 ≤ 𝐵 )
86	77 78 7 10 35 45 85	logblebd	⊢ ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝐵 ) )
87	14 67 65 75 86	letrd	⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) )
88		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
89		flge	⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
90	65 88 89	syl2anc	⊢ ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
91	87 90	mpbid	⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
92	66 91	jca	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
93		elnn0z	⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
94	92 93	sylibr	⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
95	64 94	nnexpcld	⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℕ )
96		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
97	12	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
98		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
99	98	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
100	99	nnnn0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
101		zexpcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
102	97 100 101	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
103		1zzd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
104	102 103	zsubcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
105		1cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℂ )
106	105	addridd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 1 + 0 ) = 1 )
107	22	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℝ )
108		1nn0	⊢ 1 ∈ ℕ0
109	108	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
110	13 109	reexpcld	⊢ ( 𝜑 → ( 𝑁 ↑ 1 ) ∈ ℝ )
111	110	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 1 ) ∈ ℝ )
112	102	zred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℝ )
113		1lt3	⊢ 1 < 3
114	113	a1i	⊢ ( 𝜑 → 1 < 3 )
115	22 16 13 114 20	ltletrd	⊢ ( 𝜑 → 1 < 𝑁 )
116	13	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
117	116	exp1d	⊢ ( 𝜑 → ( 𝑁 ↑ 1 ) = 𝑁 )
118	117	eqcomd	⊢ ( 𝜑 → 𝑁 = ( 𝑁 ↑ 1 ) )
119	115 118	breqtrd	⊢ ( 𝜑 → 1 < ( 𝑁 ↑ 1 ) )
120	119	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 < ( 𝑁 ↑ 1 ) )
121	13	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℝ )
122	64	nnge1d	⊢ ( 𝜑 → 1 ≤ 𝑁 )
123	122	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ 𝑁 )
124		elfzuz	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
125	124	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
126	121 123 125	leexp2ad	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 1 ) ≤ ( 𝑁 ↑ 𝑘 ) )
127	107 111 112 120 126	ltletrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 < ( 𝑁 ↑ 𝑘 ) )
128	106 127	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 1 + 0 ) < ( 𝑁 ↑ 𝑘 ) )
129	14	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 ∈ ℝ )
130	107 129 112	ltaddsub2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 1 + 0 ) < ( 𝑁 ↑ 𝑘 ) ↔ 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
131	128 130	mpbid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
132	104 131	jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
133		elnnz	⊢ ( ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℕ ↔ ( ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
134	132 133	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℕ )
135	96 134	fprodnncl	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℕ )
136	95 135	nnmulcld	⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℕ )
137	62 136	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
138	137	nnred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
139	138	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 ∈ ℝ )
140	1 2 3	aks4d1p2	⊢ ( 𝜑 → ( 2 ↑ 𝐵 ) ≤ ( lcm ‘ ( 1 ... 𝐵 ) ) )
141	140	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 2 ↑ 𝐵 ) ≤ ( lcm ‘ ( 1 ... 𝐵 ) ) )
142	137	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
143	142	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 ∈ ℤ )
144	56	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 1 ... 𝐵 ) ⊆ ℤ )
145		fzfid	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 1 ... 𝐵 ) ∈ Fin )
146		lcmfdvdsb	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 1 ... 𝐵 ) ⊆ ℤ ∧ ( 1 ... 𝐵 ) ∈ Fin ) → ( ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ↔ ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 ) )
147	143 144 145 146	syl3anc	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ↔ ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 ) )
148	147	biimpd	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 ) )
149	148	syldbl2	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 )
150	59	nn0zd	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℤ )
151	150	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℤ )
152	137	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 ∈ ℕ )
153		dvdsle	⊢ ( ( ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 → ( lcm ‘ ( 1 ... 𝐵 ) ) ≤ 𝐴 ) )
154	151 152 153	syl2anc	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 → ( lcm ‘ ( 1 ... 𝐵 ) ) ≤ 𝐴 ) )
155	149 154	mpd	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ≤ 𝐴 )
156	51 61 139 141 155	letrd	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 2 ↑ 𝐵 ) ≤ 𝐴 )
157	51 139	lenltd	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ( 2 ↑ 𝐵 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 2 ↑ 𝐵 ) ) )
158	156 157	mpbid	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ¬ 𝐴 < ( 2 ↑ 𝐵 ) )
159	5 158	pm2.21dd	⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
160		simpr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
161	159 160	pm2.61dan	⊢ ( 𝜑 → ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
162		rexnal	⊢ ( ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 ↔ ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
163	161 162	sylibr	⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )