Metamath Proof Explorer

Theorem prmreclem1

Description: Lemma for prmrec . Properties of the "square part" function, which extracts the m of the decomposition N = r m ^ 2 , with m maximal and r squarefree. (Contributed by Mario Carneiro, 5-Aug-2014)

Ref Expression
Hypothesis prmreclem1.1 ⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
Assertion prmreclem1 ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ∧ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 prmreclem1.1 ⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
2 ssrab2 ⊢ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℕ
3 breq2 ⊢ ( 𝑛 = 𝑁 → ( ( 𝑟 ↑ 2 ) ∥ 𝑛 ↔ ( 𝑟 ↑ 2 ) ∥ 𝑁 ) )
4 3 rabbidv ⊢ ( 𝑛 = 𝑁 → { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } = { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
5 4 supeq1d ⊢ ( 𝑛 = 𝑁 → sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
6 ltso ⊢ < Or ℝ
7 6 supex ⊢ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) ∈ V
8 5 1 7 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝑄 ‘ 𝑁 ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
9 nnssz ⊢ ℕ ⊆ ℤ
10 2 9 sstri ⊢ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℤ
11 oveq1 ⊢ ( 𝑟 = 1 → ( 𝑟 ↑ 2 ) = ( 1 ↑ 2 ) )
12 sq1 ⊢ ( 1 ↑ 2 ) = 1
13 11 12 eqtrdi ⊢ ( 𝑟 = 1 → ( 𝑟 ↑ 2 ) = 1 )
14 13 breq1d ⊢ ( 𝑟 = 1 → ( ( 𝑟 ↑ 2 ) ∥ 𝑁 ↔ 1 ∥ 𝑁 ) )
15 1nn ⊢ 1 ∈ ℕ
16 15 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ )
17 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
18 1dvds ⊢ ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 )
19 17 18 syl ⊢ ( 𝑁 ∈ ℕ → 1 ∥ 𝑁 )
20 14 16 19 elrabd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
21 20 ne0d ⊢ ( 𝑁 ∈ ℕ → { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ≠ ∅ )
22 nnz ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
23 zsqcl ⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ↑ 2 ) ∈ ℤ )
24 22 23 syl ⊢ ( 𝑧 ∈ ℕ → ( 𝑧 ↑ 2 ) ∈ ℤ )
25 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
26 dvdsle ⊢ ( ( ( 𝑧 ↑ 2 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → ( 𝑧 ↑ 2 ) ≤ 𝑁 ) )
27 24 25 26 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → ( 𝑧 ↑ 2 ) ≤ 𝑁 ) )
28 nnlesq ⊢ ( 𝑧 ∈ ℕ → 𝑧 ≤ ( 𝑧 ↑ 2 ) )
29 28 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → 𝑧 ≤ ( 𝑧 ↑ 2 ) )
30 nnre ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℝ )
31 30 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → 𝑧 ∈ ℝ )
32 31 resqcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( 𝑧 ↑ 2 ) ∈ ℝ )
33 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
34 33 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → 𝑁 ∈ ℝ )
35 letr ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 ↑ 2 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑧 ≤ ( 𝑧 ↑ 2 ) ∧ ( 𝑧 ↑ 2 ) ≤ 𝑁 ) → 𝑧 ≤ 𝑁 ) )
36 31 32 34 35 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ≤ ( 𝑧 ↑ 2 ) ∧ ( 𝑧 ↑ 2 ) ≤ 𝑁 ) → 𝑧 ≤ 𝑁 ) )
37 29 36 mpand ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ≤ 𝑁 → 𝑧 ≤ 𝑁 ) )
38 27 37 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → 𝑧 ≤ 𝑁 ) )
39 38 ralrimiva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑧 ∈ ℕ ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → 𝑧 ≤ 𝑁 ) )
40 oveq1 ⊢ ( 𝑟 = 𝑧 → ( 𝑟 ↑ 2 ) = ( 𝑧 ↑ 2 ) )
41 40 breq1d ⊢ ( 𝑟 = 𝑧 → ( ( 𝑟 ↑ 2 ) ∥ 𝑁 ↔ ( 𝑧 ↑ 2 ) ∥ 𝑁 ) )
42 41 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑁 ↔ ∀ 𝑧 ∈ ℕ ( ( 𝑧 ↑ 2 ) ∥ 𝑁 → 𝑧 ≤ 𝑁 ) )
43 39 42 sylibr ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑁 )
44 brralrspcev ⊢ ( ( 𝑁 ∈ ℤ ∧ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑁 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑥 )
45 17 43 44 syl2anc ⊢ ( 𝑁 ∈ ℕ → ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑥 )
46 suprzcl2 ⊢ ( ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℤ ∧ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑥 ) → sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
47 10 21 45 46 mp3an2i ⊢ ( 𝑁 ∈ ℕ → sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
48 8 47 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑄 ‘ 𝑁 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
49 2 48 sselid ⊢ ( 𝑁 ∈ ℕ → ( 𝑄 ‘ 𝑁 ) ∈ ℕ )
50 oveq1 ⊢ ( 𝑧 = ( 𝑄 ‘ 𝑁 ) → ( 𝑧 ↑ 2 ) = ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) )
51 50 breq1d ⊢ ( 𝑧 = ( 𝑄 ‘ 𝑁 ) → ( ( 𝑧 ↑ 2 ) ∥ 𝑁 ↔ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ) )
52 41 cbvrabv ⊢ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } = { 𝑧 ∈ ℕ ∣ ( 𝑧 ↑ 2 ) ∥ 𝑁 }
53 51 52 elrab2 ⊢ ( ( 𝑄 ‘ 𝑁 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ↔ ( ( 𝑄 ‘ 𝑁 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ) )
54 48 53 sylib ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ) )
55 54 simprd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 )
56 49 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑄 ‘ 𝑁 ) ∈ ℕ )
57 56 nncnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑄 ‘ 𝑁 ) ∈ ℂ )
58 57 mulid1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑄 ‘ 𝑁 ) · 1 ) = ( 𝑄 ‘ 𝑁 ) )
59 eluz2gt1 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐾 )
60 59 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝐾 )
61 1red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 1 ∈ ℝ )
62 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
63 62 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐾 ∈ ℕ )
64 63 nnred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐾 ∈ ℝ )
65 56 nnred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑄 ‘ 𝑁 ) ∈ ℝ )
66 56 nngt0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < ( 𝑄 ‘ 𝑁 ) )
67 ltmul2 ⊢ ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( ( 𝑄 ‘ 𝑁 ) ∈ ℝ ∧ 0 < ( 𝑄 ‘ 𝑁 ) ) ) → ( 1 < 𝐾 ↔ ( ( 𝑄 ‘ 𝑁 ) · 1 ) < ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ) )
68 61 64 65 66 67 syl112anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 1 < 𝐾 ↔ ( ( 𝑄 ‘ 𝑁 ) · 1 ) < ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ) )
69 60 68 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑄 ‘ 𝑁 ) · 1 ) < ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) )
70 58 69 eqbrtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑄 ‘ 𝑁 ) < ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) )
71 nnmulcl ⊢ ( ( ( 𝑄 ‘ 𝑁 ) ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ∈ ℕ )
72 49 62 71 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ∈ ℕ )
73 72 nnred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ∈ ℝ )
74 65 73 ltnled ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑄 ‘ 𝑁 ) < ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ↔ ¬ ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ≤ ( 𝑄 ‘ 𝑁 ) ) )
75 70 74 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ≤ ( 𝑄 ‘ 𝑁 ) )
76 45 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑥 )
77 oveq1 ⊢ ( 𝑟 = ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) → ( 𝑟 ↑ 2 ) = ( ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ↑ 2 ) )
78 77 breq1d ⊢ ( 𝑟 = ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) → ( ( 𝑟 ↑ 2 ) ∥ 𝑁 ↔ ( ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ↑ 2 ) ∥ 𝑁 ) )
79 72 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ∈ ℕ )
80 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) )
81 63 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → 𝐾 ∈ ℕ )
82 81 nnsqcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( 𝐾 ↑ 2 ) ∈ ℕ )
83 nnz ⊢ ( ( 𝐾 ↑ 2 ) ∈ ℕ → ( 𝐾 ↑ 2 ) ∈ ℤ )
84 82 83 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( 𝐾 ↑ 2 ) ∈ ℤ )
85 49 nnsqcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℕ )
86 9 85 sselid ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℤ )
87 85 nnne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ≠ 0 )
88 dvdsval2 ⊢ ( ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ↔ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ∈ ℤ ) )
89 86 87 17 88 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ↔ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ∈ ℤ ) )
90 55 89 mpbid ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ∈ ℤ )
91 90 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ∈ ℤ )
92 86 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℤ )
93 dvdscmul ⊢ ( ( ( 𝐾 ↑ 2 ) ∈ ℤ ∧ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ∈ ℤ ∧ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℤ ) → ( ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) ∥ ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) ) )
94 84 91 92 93 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) ∥ ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) ) )
95 80 94 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) ∥ ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) )
96 57 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( 𝑄 ‘ 𝑁 ) ∈ ℂ )
97 81 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → 𝐾 ∈ ℂ )
98 96 97 sqmuld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ↑ 2 ) = ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) )
99 98 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝐾 ↑ 2 ) ) = ( ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ↑ 2 ) )
100 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
101 100 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → 𝑁 ∈ ℂ )
102 85 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℕ )
103 102 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∈ ℂ )
104 87 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ≠ 0 )
105 101 103 104 divcan2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) · ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) = 𝑁 )
106 95 99 105 3brtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ↑ 2 ) ∥ 𝑁 )
107 78 79 106 elrabd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } )
108 suprzub ⊢ ( ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑧 ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } 𝑧 ≤ 𝑥 ∧ ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ∈ { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ≤ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
109 10 76 107 108 mp3an2i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ≤ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
110 8 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( 𝑄 ‘ 𝑁 ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑁 } , ℝ , < ) )
111 109 110 breqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑄 ‘ 𝑁 ) · 𝐾 ) ≤ ( 𝑄 ‘ 𝑁 ) )
112 75 111 mtand ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) )
113 112 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) )
114 49 55 113 3jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑄 ‘ 𝑁 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ∥ 𝑁 ∧ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐾 ↑ 2 ) ∥ ( 𝑁 / ( ( 𝑄 ‘ 𝑁 ) ↑ 2 ) ) ) ) )